proposition: Lemma boundSubTerm : forall (t : fol.Term L) (v : nat) (s : fol.Term L), codeTerm (substT t v s) <= ReplaceTermTerm (codeTerm t) (fold_right Nat.max 0 (codeTerm s :: freeVarT t)).
proof: Proof. intro t; unfold ReplaceTermTerm, ReplaceTermsTerm, ReplaceTermTermsTerm. set (A := fun t0 recs s0 : nat => cPair (switchPR (car t0) (cPair (car t0) (cdr (codeNth (t0 - S (cdr t0)) recs))) (cPair 0 s0)) (switchPR t0 (S (cPair (car (codeNth (t0 - S (car (pred t0))) recs)) (cdr (codeNth (t0 - S (cdr (pred t0))) recs)))) 0)). assert (H: forall n m : nat, m < n -> extEqual 1 (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 A n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - S m) b)) (evalStrongRec 1 A m)) by (intros n m H; now apply (evalStrongRecHelp2 1)). simpl in H. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => forall (v : nat) (s : fol.Term L), codeTerms (substTs ts v s) <= ReplaceTermsTerm (codeTerms ts) (fold_right Nat.max 0 (codeTerm s :: freeVarTs ts))); simpl in |- *; intros; unfold evalStrongRec in |- *; unfold evalComposeFunc, evalOneParamList, evalList in |- *; repeat rewrite computeEvalStrongRecHelp; unfold compose2 in |- *; unfold evalComposeFunc, evalOneParamList, evalList in |- *; simpl in |- *; repeat rewrite cPairProjections1. - unfold A; simpl; repeat rewrite cPairProjections1. replace (codeTerm (var n)) with (cPair 0 n); [ idtac | reflexivity ]. repeat rewrite cPairProjections1. simpl in |- *. destruct (eq_nat_dec v n) as [a | b]. + eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. apply Nat.le_max_l. + replace (codeTerm (var n)) with (cPair 0 n); [ idtac | reflexivity ]. apply cPairLe3. * apply le_n. * eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply Nat.le_max_l. - unfold A; repeat rewrite cPairProjections1. replace (codeTerm (apply f t0)) with (cPair (S (cf f)) (codeTerms t0)); [ idtac | reflexivity ]. repeat rewrite cPairProjections1. rewrite H with (m := cdr (cPair (S (cf f)) (codeTerms t0))). + simpl; replace (codeTerm (apply f (substTs t0 v s))) with (cPair (S (cf f)) (codeTerms (substTs t0 v s))); [ idtac | reflexivity ]. apply cPairLe3. apply le_n. unfold ReplaceTermsTerm, ReplaceTermTermsTerm in H0. fold A in H0. repeat rewrite cPairProjections2. apply (H0 v s). + repeat rewrite cPairProjections2; apply cPairLt2. - apply Nat.le_0_l. - replace (codeTerms (Tcons (substT t0 v s) (substTs t1 v s))) with (S (cPair (codeTerm (substT t0 v s)) (codeTerms (substTs t1 v s)))); [ idtac | reflexivity ]. unfold ReplaceTermsTerm in |- *. unfold ReplaceTermsTerm in H1. unfold ReplaceTermTermsTerm in |- *. unfold ReplaceTermTermsTerm in H1. fold A in H1 |- *. unfold evalStrongRec in |- *. unfold evalComposeFunc, evalOneParamList, evalList in |- *. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. unfold A at 1 in |- *. repeat rewrite cPairProjections2. repeat rewrite H. * replace (codeTerms (Tcons t0 t1)) with (S (cPair (codeTerm t0) (codeTerms t1))); [ idtac | reflexivity ]. -- simpl; repeat rewrite cPairProjections1. apply le_n_S. apply cPairLe3. ++ eapply Nat.le_trans. ** apply H0. ** apply (ReplaceTermTermMonotone (codeTerm t0) (Nat.max (codeTerm s) (fold_right Nat.max 0 (freeVarT t0))) (Nat.max (codeTerm s) (fold_right Nat.max 0 (freeVarTs (Tcons t0 t1))))). apply maxLemma. apply le_n. replace (freeVarTs (Tcons t0 t1)) with (freeVarT t0 ++ freeVarTs t1); [ idtac | reflexivity ]. apply maxLemma2. ++ eapply Nat.le_trans. ** apply H1. ** repeat rewrite cPairProjections2. apply (ReplaceTermsTermMonotone (codeTerms t1) (Nat.max (codeTerm s) (fold_right Nat.max 0 (freeVarTs t1))) (Nat.max (codeTerm s) (fold_right Nat.max 0 (freeVarTs (Tcons t0 t1))))). apply maxLemma. apply le_n. replace (freeVarTs (Tcons t0 t1)) with (freeVarT t0 ++ freeVarTs t1); [ idtac | reflexivity ]. apply maxLemma3. * replace (codeTerms (Tcons t0 t1)) with (S (cPair (codeTerm t0) (codeTerms t1))); [ idtac | reflexivity ]. simpl; repeat rewrite cPairProjections2. apply Nat.lt_succ_r. apply cPairLe2. * replace (codeTerms (Tcons t0 t1)) with (S (cPair (codeTerm t0) (codeTerms t1))); [ idtac | reflexivity ]. simpl; repeat rewrite cPairProjections1. apply Nat.lt_succ_r, cPairLe1. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)