proposition: Lemma evalStrongRecHelpParam : forall (a n c : nat) (f : naryFunc a.+3), extEqual a (evalStrongRecHelp (S a) f n c) (evalStrongRecHelp a (fun x y : nat => f x y c) n).
proof: Proof. intros a n c f; unfold evalStrongRecHelp in |- *. eapply extEqualTrans. - apply extEqualSym. apply evalPrimRecParam. - assert (H: extEqual a.+1 (evalPrimRecFunc a (evalComposeFunc a.+1 0 (Vector.nil (naryFunc a.+1)) (codeList nil) c) (fun x y : nat => evalComposeFunc a.+3 2 (Vector.cons (naryFunc a.+3) f 1 (Vector.cons _ (evalProjFunc _ a.+1 (Nat.lt_lt_succ_r a.+1 a.+2 (Nat.lt_succ_diag_r a.+1))) 0 (Vector.nil (naryFunc a.+3)))) (fun a0 b : nat => S (cPair a0 b)) x y c)) (evalPrimRecFunc a (evalComposeFunc a 0 (Vector.nil (naryFunc a)) (codeList nil)) (evalComposeFunc a.+2 2 (Vector.cons (naryFunc a.+2) (fun x y : nat => f x y c) 1 (Vector.cons (naryFunc a.+2) (evalProjFunc _ a (Nat.lt_lt_succ_r a a.+1 (Nat.lt_succ_diag_r a))) 0 (Vector.nil (naryFunc a.+2)))) (fun a0 b : nat => S (cPair a0 b))))). { apply (extEqualPrimRec a (evalComposeFunc a.+1 0 (Vector.nil (naryFunc a.+1)) (codeList nil) c)). simpl in |- *; apply extEqualRefl. - simpl in |- *; fold (naryFunc a) in |- *. induction (sumbool_rec (fun _ : {a = a.+1} + {a <> a.+1} => {a.+1 = a.+2} + {a.+1 <> a.+2}) (fun a0 : a = a.+1 => left (a.+1 <> a.+2) (f_equal S a0 )) (fun b : a <> S a => right (a.+1 = a.+2) (not_eq_S a a.+1 b)) (eq_nat_dec a a.+1)). + elim (Compat815.lt_not_le a.+1 a.+2). * apply Nat.lt_succ_diag_r. * rewrite <- a0; auto. + induction (sumbool_rec (fun _ : {a = a} + {a <> a} => {a.+1 = a.+1} + {a.+1 <> a.+1}) (fun a0 : a = a => left (a.+1 <> a.+1) (f_equal S a0)) (fun b0 : a <> a => right (a.+1 = a.+1) (not_eq_S a a b0)) (eq_nat_dec a a)). induction (eq_nat_dec a a.+1). * elim (Compat815.lt_not_le a a.+1). -- apply Nat.lt_succ_diag_r. -- rewrite <- a1; auto. * induction (eq_nat_dec a a). -- intros; apply extEqualRefl. -- elim b1; auto. * elim b0; auto. } apply (H n). Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction