proposition: Remark ReplaceTermTermsTermMonotone : forall a s1 s2 : nat, s1 <= s2 -> ReplaceTermTerm a s1 <= ReplaceTermTerm a s2 /\ ReplaceTermsTerm a s1 <= ReplaceTermsTerm a s2.
proof: Proof. assert (H: forall a s1 s2 n : nat, n < a -> s1 <= s2 -> ReplaceTermTerm n s1 <= ReplaceTermTerm n s2 /\ ReplaceTermsTerm n s1 <= ReplaceTermsTerm n s2). { intro a; unfold ReplaceTermTerm, ReplaceTermsTerm, ReplaceTermTermsTerm. set (A := fun t recs s : nat => cPair (switchPR (car t) (cPair (car t) (cdr (codeNth (t - S (cdr t)) recs))) (cPair 0 s)) (switchPR t (S (cPair (car (codeNth (t - S (car (pred t))) recs)) (cdr (codeNth (t - S (cdr (pred t))) recs)))) 0)). induction a as [| a Hreca]; simpl in |- *. - intros s1 s2 n H; elim (Nat.nlt_0_r _ H). - intros s1 s2 n H H0; assert (H1: 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 n0 m H1; now apply (evalStrongRecHelp2 1). } simpl in H1; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. repeat rewrite cPairProjections1; split. + unfold A at 3 1; repeat rewrite cPairProjections1. assert (H2: cPair (car n) (cdr n) = n) by apply cPairProjections. destruct (car n). * simpl in |- *. apply cPairLe3. apply le_n. assumption. * simpl; assert (H3: cdr n < n). { apply Nat.lt_le_trans with (cPair (S n0) (cdr n)). - apply cPairLt2. - rewrite H2; apply le_n. } repeat rewrite H1. -- apply cPairLe3. apply le_n. eapply proj2. apply Hreca. ++ apply Nat.lt_le_trans with n. ** apply H3. ** apply Compat815.lt_n_Sm_le. assumption. ++ assumption. -- assumption. -- assumption. + unfold A at 3 1 in |- *. repeat rewrite cPairProjections2. destruct n. * simpl; apply le_n. * assert (H2: cdr n < S n). { apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (car n) (cdr n)). - apply cPairLe2. - rewrite cPairProjections; apply le_n. } assert (H3: car n < S n). { apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (car n) (cdr n)). - apply cPairLe1. - rewrite cPairProjections; apply le_n. } repeat rewrite H1. -- simpl; apply le_n_S. apply cPairLe3. eapply proj1. apply Hreca. apply Nat.le_lt_trans with n. ++ lia. ++ apply Nat.succ_lt_mono. assumption. ++ assumption. ++ eapply proj2. apply Hreca. apply Nat.le_lt_trans with n. ** lia. ** apply Nat.lt_succ_r. assumption. ** assumption. -- assumption. -- assumption. -- assumption. -- assumption. } intros a s1 s2 H0; apply H with (S a). - apply Nat.lt_succ_diag_r. - assumption. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)