proposition: Lemma codeSubTermCorrect : forall (t : Term) (v : nat) (s : Term), codeSubTerm (codeTerm t) v (codeTerm s) = codeTerm (substT t v s).
proof: Proof. set (g := fun t0 recs v0 s0 : nat => cPair (switchPR (car t0) (cPair (car t0) (cdr (codeNth (t0 - S (cdr t0)) recs))) (switchPR (charFunction 2 Nat.eqb (cdr t0) v0) s0 t0)) (switchPR t0 (S (cPair (car (codeNth (t0 - S (car (pred t0))) recs)) (cdr (codeNth (t0 - S (cdr (pred t0))) recs)))) 0)). intros t v s; elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => codeSubTerms (codeTerms ts) v (codeTerm s) = codeTerms (substTs ts v s)). - intro n; simpl; replace (codeTerm (var n)) with (cPair 0 n). + unfold codeSubTerm, codeSubTermTerms, evalStrongRec; simpl. repeat rewrite cPairProjections1 || rewrite cPairProjections2. simpl; induction (eq_nat_dec v n) as [a | b]. * rewrite a, Nat.eqb_refl; simpl; reflexivity. * rewrite nat_eqb_false; simpl. -- reflexivity. -- auto. + reflexivity. - intros f t0 H; simpl; transitivity (cPair (S (cf f)) (codeTerms (substTs t0 v s))). + rewrite <- H; replace (codeTerm (apply f t0)) with (cPair (S (cf f)) (codeTerms t0)). * generalize (cf f) (codeTerms t0). clear H t0 f; intros n n0; unfold codeSubTerm, codeSubTermTerms. fold g; unfold evalStrongRec, evalComposeFunc, evalOneParamList. unfold evalList; rewrite computeEvalStrongRecHelp. -- unfold compose2, evalComposeFunc, evalOneParamList, evalList. unfold pred; repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold g at 1; repeat rewrite cPairProjections1 || rewrite cPairProjections2. assert (H: extEqual _ (evalComposeFunc 2 1 (Vector.cons _ (evalStrongRecHelp 2 g (cPair (S n) n0)) 0 (Vector.nil _)) (fun b : nat => codeNth (cPair (S n) n0 - S n0) b)) (evalStrongRec 2 g n0)) by (apply (evalStrongRecHelp2 2), cPairLt2). simpl in H; rewrite H; clear H. simpl; reflexivity. * reflexivity. + reflexivity. - simpl; unfold codeTerms, codeSubTerms, codeSubTermTerms, evalStrongRec. simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. - intros n t0 H t1 H0 ; simpl. transitivity (S (cPair (codeTerm (substT t0 v s)) (codeTerms (substTs t1 v s)))). + rewrite <- H, <- H0. replace (codeTerms (Tcons t0 t1)) with (S (cPair (codeTerm t0) (codeTerms t1))). * generalize (codeTerm t0) (codeTerms t1). clear H0 t1 H t0 n; intros n n0. unfold codeSubTerms at 1; unfold codeSubTermTerms; fold g. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList, pred. repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold g; repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold pred; repeat rewrite cPairProjections1 || rewrite cPairProjections2. assert (H: extEqual _ (evalComposeFunc 2 1 (Vector.cons _ (evalStrongRecHelp 2 g (S (cPair n n0))) 0 (Vector.nil _)) (fun b : nat => codeNth (S (cPair n n0) - S n) b)) (evalStrongRec 2 g n)). { apply (evalStrongRecHelp2 2). apply Compat815.le_lt_n_Sm. apply cPairLe1. } simpl in H; rewrite H; clear H. assert (H: extEqual _ (evalComposeFunc 2 1 (Vector.cons _ (evalStrongRecHelp 2 g (S (cPair n n0))) 0 (Vector.nil _)) (fun b : nat => codeNth (S (cPair n n0) - S n0) b)) (evalStrongRec 2 g n0)). { apply (evalStrongRecHelp2 2). apply Compat815.le_lt_n_Sm. apply cPairLe2. } simpl in H; rewrite H; clear H; simpl. reflexivity. * reflexivity. + reflexivity. Qed.
imports: hydras.Ackermann(primRec cPair folProp code extEqualNat) Coq(Arith) hydras(Compat815) NewNotations