proposition: Remark boundSubFormulaHelp : forall (f : fol.Formula L) (v : nat) (s : fol.Term L), codeFormula (substF f v s) <= ReplaceFormulaTerm (codeFormula f) (Nat.max (codeTerm s) (pow3 (depth L f) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))).
proof: Proof. intro f; unfold ReplaceFormulaTerm; set (A := fun f0 recs s0 : nat => switchPR (car f0) (switchPR (pred (car f0)) (switchPR (pred (pred (car f0))) (switchPR (pred (pred (pred (car f0)))) (cPair (car f0) (ReplaceTermsTerm (cdr f0) s0)) (cPair 3 (cPair s0 (codeNth (f0 - S (cdr (cdr f0))) recs)))) (cPair 2 (codeNth (f0 - S (cdr f0)) recs))) (cPair 1 (cPair (codeNth (f0 - S (car (cdr f0))) recs) (codeNth (f0 - S (cdr (cdr f0))) recs)))) (cPair 0 (cPair (ReplaceTermTerm (car (cdr f0)) s0) (ReplaceTermTerm (cdr (cdr f0)) s0)))). 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; apply (evalStrongRecHelp2 1); assumption). simpl in H; elim f using Formula_depth_ind2. - intros; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. set (C := Nat.max (codeTerm s) (pow3 (depth L (equal t t0)) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula (equal t t0)))). simpl; repeat rewrite cPairProjections1. unfold A at 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl; apply cPairLe3. + apply le_n. + apply cPairLe3. * apply Nat.le_trans with (ReplaceTermTerm (codeTerm t) (fold_right Nat.max 0 (codeTerm s :: freeVarT t))). -- apply boundSubTerm. -- apply ReplaceTermTermMonotone. unfold C; simpl; apply maxLemma. ++ apply le_n. ++ apply le_S. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. apply maxLemma2. * apply Nat.le_trans with (ReplaceTermTerm (codeTerm t0) (fold_right Nat.max 0 (codeTerm s :: freeVarT t0))). -- apply boundSubTerm. -- apply ReplaceTermTermMonotone. unfold C; simpl; apply maxLemma. ++ apply le_n. ++ apply le_S. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. apply maxLemma3. - intros; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. set (C := Nat.max (codeTerm s) (pow3 (depth L (atomic r t)) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula (atomic r t)))). simpl; repeat rewrite cPairProjections1. unfold A at 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl; apply cPairLe3. + apply le_n. + apply Nat.le_trans with (ReplaceTermsTerm (codeTerms t) (fold_right Nat.max 0 (codeTerm s :: freeVarTs t))). * apply boundSubTerms. * apply ReplaceTermsTermMonotone. unfold C; simpl; apply maxLemma. -- apply le_n. -- apply le_S. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply maxLemma3. - intros f0 H0 f1 H1 v s; rewrite subFormulaImp. set (C := Nat.max (codeTerm s) (pow3 (depth L (impH f0 f1)) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula (impH f0 f1)))). unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. unfold A at 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite H with (m := codeFormula f0). + rewrite H with (m := codeFormula f1). * simpl; apply cPairLe3. -- apply le_n. -- apply cPairLe3. ++ apply Nat.le_trans with (evalStrongRec 1 A (codeFormula f0) (Nat.max (codeTerm s) (pow3 (depth L f0) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f0)))). ** auto. ** apply ReplaceFormulaTermMonotone. unfold C; apply maxLemma. apply le_n. apply Nat.add_le_mono. apply pow3Monotone. simpl; apply le_S. apply Nat.le_max_l. simpl; apply maxLemma. apply le_n. rewrite app_assoc. apply maxLemma2. ++ apply Nat.le_trans with (evalStrongRec 1 A (codeFormula f1) (Nat.max (codeTerm s) (pow3 (depth L f1) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f1)))). ** auto. ** apply ReplaceFormulaTermMonotone. unfold C; apply maxLemma. apply le_n. apply Nat.add_le_mono. apply pow3Monotone. simpl; apply le_S. apply Nat.le_max_r. simpl; apply maxLemma. apply le_n. induction (maxApp (freeVarT s) (varFormula f1)) as [a | b]. --- rewrite a; apply maxLemma2. --- rewrite b; eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. apply maxLemma3. * eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. + eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe1. - intros f0 H0 v s; rewrite subFormulaNot. set (C := Nat.max (codeTerm s) (pow3 (depth L (notH f0)) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula (notH f0)))). unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. repeat rewrite cPairProjections1. unfold A at 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite H with (m := codeFormula f0). + simpl; apply cPairLe3. * apply le_n. * apply Nat.le_trans with (evalStrongRec 1 A (codeFormula f0) (Nat.max (codeTerm s) (pow3 (depth L f0) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f0)))). -- auto. -- apply ReplaceFormulaTermMonotone. unfold C; apply maxLemma. ++ apply le_n. ++ apply Nat.add_le_mono. ** apply pow3Monotone. simpl; apply Nat.le_succ_diag_r. ** apply le_n. + apply cPairLt2. - intros v a H0 v0 s; set (C := Nat.max (codeTerm s) (pow3 (depth L (forallH v a)) + fold_right Nat.max 0 (v0 :: freeVarT s ++ varFormula (forallH v a)))). unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList; repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. unfold A at 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite H with (m := codeFormula a). + simpl; rewrite subFormulaForall. induction (eq_nat_dec v v0) as [a0 |b]. * simpl; apply cPairLe3. apply le_n. -- apply cPairLe3. ++ unfold C; rewrite a0. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. simpl; apply Nat.le_max_l. ++ apply Nat.le_trans with (codeFormula (substF a 0 (var 0))). ** rewrite (subFormulaId L). apply le_n. ** apply Nat.le_trans with (evalStrongRec 1 A (codeFormula a) (Nat.max (codeTerm (var 0)) (pow3 (depth L a) + fold_right Nat.max 0 (0 :: freeVarT (L:=L)(var 0) ++ varFormula a)))). apply H0. apply depthForall. apply ReplaceFormulaTermMonotone. unfold C; apply maxLemma. apply Nat.le_0_l. apply Nat.add_le_mono. apply pow3Monotone. simpl; apply Nat.le_succ_diag_r. simpl; eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. simpl; apply Nat.le_max_r. * induction (In_dec eq_nat_dec v (freeVarT s)) as [a0 | b0]. -- simpl; apply cPairLe3. apply le_n. set (nv := newVar (v0 :: freeVarT s ++ freeVarF a)). apply cPairLe3. ++ unfold C; eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. simpl; apply Nat.le_trans with (1 + Nat.max v0 (fold_right Nat.max 0 (freeVarT s ++ v :: varFormula a))). ** simpl; unfold nv, newVar. eapply Nat.le_trans. apply mapListLemma. apply le_n_S. simpl; apply maxLemma. apply le_n. induction (maxApp (freeVarT s) (freeVarF a)) as [a1 | b1]. --- rewrite a1. apply maxLemma2. --- rewrite b1; eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. simpl; eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply maxVarFreeVar. ** apply Nat.add_le_mono. eapply Nat.le_trans; [ idtac | apply Nat.le_add_r ]. apply pow3Min. apply le_n. ++ set (B := substF a v (var nv)). apply Nat.le_trans with (evalStrongRec 1 A (codeFormula B) (Nat.max (codeTerm s) (pow3 (depth L B) + fold_right Nat.max 0 (v0 :: freeVarT s ++ varFormula B)))). ** apply H0. unfold B; eapply eqDepth. symmetry; apply subFormulaDepth. apply depthForall. ** unfold B at 1; rewrite ReplaceFormulaTermSub. apply ReplaceFormulaTermMonotone. simpl; unfold B at 1 2; rewrite subFormulaDepth. unfold C; simpl; apply maxLemma. apply le_n. rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply (Nat.max_case v0 (fold_right Nat.max 0 (freeVarT s ++ varFormula (substF a v (var nv))))). eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply Nat.le_max_l. induction (maxApp (freeVarT s) (varFormula (substF a v (var nv)))) as [a1 | b1]. --- rewrite a1. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply maxLemma2. --- rewrite b1; clear b1. clear H0 C B. unfold nv; clear nv. eapply Nat.le_trans. apply boundSubFormulaHelp1. apply Nat.add_le_mono. apply le_n. repeat apply maxLemma. apply le_n. apply Nat.max_case. apply maxLemma2. eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. simpl; apply maxLemma. apply le_n. apply Nat.max_case; apply le_n. -- simpl; apply cPairLe3. ++ apply le_n. ++ apply cPairLe3. unfold C; simpl. ** eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. simpl; apply Nat.le_max_l. ** eapply Nat.le_trans. apply H0. apply depthForall. apply ReplaceFormulaTermMonotone. unfold C; apply maxLemma. apply le_n. apply Nat.add_le_mono. simpl; apply Nat.le_add_r. simpl; apply maxLemma. apply le_n. induction (maxApp (freeVarT s) (varFormula a)) as [a0 | b1]. --- rewrite a0; apply maxLemma2. --- rewrite b1; eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. simpl; apply Nat.le_max_r. + eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)