proposition: Lemma ReplaceFormulaTermMonotone : forall a s1 s2 : nat, s1 <= s2 -> ReplaceFormulaTerm a s1 <= ReplaceFormulaTerm a s2.
proof: Proof. assert (H: forall a s1 s2 n : nat, n < a -> s1 <= s2 -> ReplaceFormulaTerm n s1 <= ReplaceFormulaTerm n s2). { unfold ReplaceFormulaTerm in |- *. set (A := fun f recs s : nat => switchPR (car f) (switchPR (pred (car f)) (switchPR (pred (pred (car f))) (switchPR (pred (pred (pred (car f)))) (cPair (car f) (ReplaceTermsTerm (cdr f) s)) (cPair 3 (cPair s (codeNth (f - S (cdr (cdr f))) recs)))) (cPair 2 (codeNth (f - S (cdr f)) recs))) (cPair 1 (cPair (codeNth (f - S (car (cdr f))) recs) (codeNth (f - S (cdr (cdr f))) recs)))) (cPair 0 (cPair (ReplaceTermTerm (car (cdr f)) s) (ReplaceTermTerm (cdr (cdr f)) s)))). 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)). { intros n m H; now apply (evalStrongRecHelp2 1). } simpl in H; simple induction a. - intros s1 s2 n H0 H1; elim (Nat.nlt_0_r _ H0). - intros n H0 s1 s2 n0 H1 H2. assert (H1': n0 <= n) by lia. rewrite Nat.lt_eq_cases in H1'; destruct H1' as [H3 | H3 ]. + apply H0. * apply H3. * apply H2. + unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. unfold A at 3 1 in |- *; destruct n0. * simpl; apply cPairLe3. apply le_n. apply cPairLe3; apply ReplaceTermTermMonotone; assumption. * assert (H4: cPair (car (S n0)) (cdr (S n0)) = S n0) by apply cPairProjections. destruct (car (S n0)). -- simpl; apply cPairLe3. ++ apply le_n. ++ apply cPairLe3; apply ReplaceTermTermMonotone; assumption. -- assert (H5: cdr (S n0) < S n0). { apply Nat.lt_le_trans with (cPair (S n1) (cdr (S n0))). - apply cPairLt2. - rewrite H4; apply le_n. } assert (H6: car (cdr (S n0)) < S n0). { apply Nat.le_lt_trans with (cdr (S n0)). - apply Nat.le_trans with (cPair (car (cdr (S n0))) (cdr (cdr (S n0)))). + apply cPairLe1. + rewrite cPairProjections; apply le_n. - assumption. } assert (H7: cdr (cdr (S n0)) < S n0). { apply Nat.le_lt_trans with (cdr (S n0)). - apply Nat.le_trans with (cPair (car (cdr (S n0))) (cdr (cdr (S n0)))). + apply cPairLe2. + rewrite cPairProjections; apply le_n. - assumption. } destruct n1. ++ repeat rewrite H with (m := car (cdr (S n0))); try assumption. repeat rewrite H with (m := cdr (cdr (S n0))); try assumption. simpl; apply cPairLe3. ** apply le_n. ** apply cPairLe3. apply H0. rewrite <- H3. assumption. assumption. apply H0. rewrite <- H3. assumption. assumption. ++ destruct n1. ** repeat rewrite H with (m := cdr (S n0)); try assumption. simpl; apply cPairLe3. apply le_n. apply H0. rewrite <- H3. assumption. assumption. ** destruct n1. repeat rewrite H with (m := cdr (cdr (S n0))); try assumption. simpl; apply cPairLe3. apply le_n. apply cPairLe3. assumption. apply H0. rewrite <- H3. assumption. assumption. simpl; apply cPairLe3. apply le_n. apply ReplaceTermsTermMonotone. assumption. } intros a s1 s2 H0; apply (H (S a)); auto. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)