proposition: Lemma boundMakeTrace : forall (f : fol.Formula L) (v : nat) (s : fol.Term L), let C := Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))) in makeTrace f (v, s) <= boundComputation (depth L f) (cTriple C C (ReplaceFormulaTerm (codeFormula f) C)) (ReplaceFormulaTerm (codeFormula f) C).
proof: Proof. set (A := fun f2 recs s0 : nat => switchPR (car f2) (switchPR (pred (car f2)) (switchPR (pred (pred (car f2))) (switchPR (pred (pred (pred (car f2)))) (cPair (car f2) (ReplaceTermsTerm (cdr f2) s0)) (cPair 3 (cPair s0 (codeNth (f2 - S (cdr (cdr f2))) recs)))) (cPair 2 (codeNth (f2 - S (cdr f2)) recs))) (cPair 1 (cPair (codeNth (f2 - S (car (cdr f2))) recs) (codeNth (f2 - S (cdr (cdr f2))) recs)))) (cPair 0 (cPair (ReplaceTermTerm (car (cdr f2)) s0) (ReplaceTermTerm (cdr (cdr f2)) s0)))). assert (E : forall (f : fol.Formula L) (v : nat) (s : fol.Term L), codeFormula (substF f v s) <= ReplaceFormulaTerm (codeFormula f) (Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))))). { intros f v s; eapply Nat.le_trans. - apply boundSubFormulaHelp. - apply ReplaceFormulaTermMonotone, maxLemma. + apply le_n. + apply cPairLe2. } assert (D : 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; apply (evalStrongRecHelp2 1); assumption). simpl in D; intro f. assert (H: forall w v n s : nat, v <= Nat.max s (cPair 0 (w + Nat.max v n))). { intros w v n s; eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply Nat.le_max_l. } assert (H0 :forall (f : fol.Formula L) (v : nat) (s : fol.Term L), codeFormula f <= ReplaceFormulaTerm (codeFormula f) (Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))))). { intros f0 v s; apply Nat.le_trans with (codeFormula (substF f0 0 (var 0))). - rewrite (subFormulaId L); apply le_n. - eapply Nat.le_trans. + apply E. + apply ReplaceFormulaTermMonotone. apply maxLemma. apply Nat.le_0_l. apply cPairLe3. apply le_n. apply Nat.add_le_mono. apply le_n. simpl; eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply maxLemma3. } elim f using Formula_depth_ind2. - intros t t0 v s C; simpl. unfold Formula_depth_rec2, Formula_depth_rec; simpl. unfold cTriple, C; simpl; repeat apply cPairLe3. + apply (H 1 v (fold_right Nat.max 0 (freeVarT s ++ freeVarT t ++ freeVarT t0)) (codeTerm s)). + apply Nat.le_max_l. + apply (H0 (equal t t0) v s). + apply (E (equal t t0) v s). + apply le_n. - intros r t v s C; simpl; unfold makeTrace in |- *. unfold Formula_depth_rec2, Formula_depth_rec; simpl. unfold cTriple, C; simpl. repeat apply cPairLe3. + apply (H 1 v (fold_right Nat.max 0 (freeVarT s ++ freeVarTs t)) (codeTerm s)). + apply Nat.le_max_l. + apply (H0 (atomic r t) v s). + apply (E (atomic r t) v s). + apply le_n. - intros f0 H1 f1 H2 v s C; simpl; replace (makeTrace (impH f0 f1) (v, s)) with (cTriple (cTriple v (codeTerm s) (codeFormula (impH f0 f1))) (codeFormula (substF (impH f0 f1) v s)) (cPair (makeTrace f0 (v, s)) (makeTrace f1 (v, s)))). + unfold cTriple; repeat apply cPairLe3. * unfold C; simpl. apply (H (pow3 (Nat.max (depth L f0) (depth L f1)) + (pow3 (Nat.max (depth L f0) (depth L f1)) + pow3 (Nat.max (depth L f0) (depth L f1)))) v (fold_right Nat.max 0 (freeVarT s ++ varFormula f0 ++ varFormula f1)) (codeTerm s)). * unfold C; simpl; apply Nat.le_max_l. * apply (H0 (impH f0 f1) v s). * apply (E (impH f0 f1) v s). * eapply Nat.le_trans. -- apply H1. -- assert (H3 : Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f0) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f0))) <= C). { unfold C; apply maxLemma. - apply le_n. - apply cPairLe3. + apply le_n. + apply Nat.add_le_mono. * apply pow3Monotone. simpl; apply le_S. apply Nat.le_max_l. * simpl; apply Nat.max_case. -- apply Nat.le_max_l. -- eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. induction (maxApp (freeVarT s) (varFormula f0)) as [a | b]. ++ rewrite a; apply maxLemma2. ++ rewrite b; eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. apply maxLemma2. } assert (H4: ReplaceFormulaTerm (codeFormula f0) (Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f0) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f0)))) <= ReplaceFormulaTerm (cPair 1 (cPair (codeFormula f0) (codeFormula f1))) C). { unfold ReplaceFormulaTerm at 2; fold A; unfold evalStrongRec. unfold evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; unfold A at 1. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite D with (m := codeFormula f0). - simpl; eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_trans; [ idtac | apply cPairLe1 ]. apply ReplaceFormulaTermMonotone. apply H3. - eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe1. } apply boundComputationMonotone. ++ apply Nat.le_max_l. ++ unfold cTriple; repeat apply cPairLe3. ** apply H3. ** apply H3. ** apply H4. ++ apply H4. * eapply Nat.le_trans. -- apply H2. -- assert (H3: Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f1) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f1))) <= C). { unfold C; apply maxLemma. - apply le_n. - apply cPairLe3. + apply le_n. + apply Nat.add_le_mono. * apply pow3Monotone. simpl; apply le_S. apply Nat.le_max_r. * simpl; apply Nat.max_case. -- apply Nat.le_max_l. -- eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. induction (maxApp (freeVarT s) (varFormula f1)) as [a | b]. ++ rewrite a. apply maxLemma2. ++ rewrite b; eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. apply maxLemma3. } assert (H4: ReplaceFormulaTerm (codeFormula f1) (Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f1) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f1)))) <= ReplaceFormulaTerm (cPair 1 (cPair (codeFormula f0) (codeFormula f1))) C). { unfold ReplaceFormulaTerm at 2; fold A; unfold evalStrongRec. unfold evalComposeFunc, evalOneParamList, evalList; repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl; unfold A at 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite D with (m := codeFormula f1). - simpl; eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. apply ReplaceFormulaTermMonotone. apply H3. - eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. } apply boundComputationMonotone. ++ apply Nat.le_max_r. ++ unfold cTriple in |- *. ** repeat apply cPairLe3. apply H3. apply H3. apply H4. ++ apply H4. + unfold makeTrace; rewrite (Formula_depth_rec2_imp L) with (Q := fun _ : fol.Formula L => (nat * fol.Term L)%type) (P := fun _ : fol.Formula L => nat). * unfold makeTraceImp at 1; reflexivity. * apply makeTraceImpNice. * apply makeTraceNotNice. * apply makeTraceForallNice. - intros f0 H1 v s C; simpl; replace (makeTrace (notH f0) (v, s)) with (cTriple (cTriple v (codeTerm s) (codeFormula (notH f0))) (codeFormula (substF (notH f0) v s)) (makeTrace f0 (v, s))). + unfold cTriple in |- *. repeat apply cPairLe3. * unfold C ; simpl. apply (H (pow3 (depth L f0) + (pow3 (depth L f0) + pow3 (depth L f0))) v (fold_right Nat.max 0 (freeVarT s ++ varFormula f0)) (codeTerm s)). * unfold C; simpl; apply Nat.le_max_l. * apply (H0 (notH f0) v s). * apply (E (notH f0) v s). * eapply Nat.le_trans. -- apply H1. -- assert (H2: Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f0) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f0))) <= C). unfold C; simpl; apply maxLemma. ++ apply le_n. ++ apply cPairLe3. apply le_n. apply Nat.add_le_mono. apply Nat.le_add_r. apply le_n. ++ assert (H3: ReplaceFormulaTerm (codeFormula f0) (Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f0) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f0)))) <= ReplaceFormulaTerm (cPair 2 (codeFormula f0)) C). { unfold ReplaceFormulaTerm at 2; fold A; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. unfold A at 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite D with (m := codeFormula f0). - simpl; eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. apply ReplaceFormulaTermMonotone. apply H2. - apply cPairLt2. } eapply Nat.le_trans; [ idtac | apply cPairLe1 ]. apply boundComputationMonotone. ** apply le_n. ** unfold cTriple; repeat apply cPairLe3. apply H2. apply H2. apply H3. ** apply H3. + unfold makeTrace. rewrite (Formula_depth_rec2_not L) with (Q := fun _ : fol.Formula L => (nat * fol.Term L)%type) (P := fun _ : fol.Formula L => nat). * unfold makeTraceNot at 1; reflexivity. * apply makeTraceImpNice. * apply makeTraceNotNice. * apply makeTraceForallNice. - intros v a H1 v0 s C; replace (makeTrace (forallH v a) (v0, s)) with (makeTraceForall v a (fun (b : fol.Formula L) _ => makeTrace b) (v0, s)). unfold makeTraceForall; simpl. induction (eq_nat_dec v v0) as [a0 | b0]; simpl in |- *. + unfold cTriple; repeat apply cPairLe3. * unfold C; simpl; apply (H (pow3 (depth L a) + (pow3 (depth L a) + pow3 (depth L a))) v0 (fold_right Nat.max 0 (freeVarT s ++ v :: varFormula a)) (codeTerm s)). * unfold C; simpl; apply Nat.le_max_l. * apply (H0 (forallH v a) v0 s). * apply (E (forallH v a) v0 s). * apply Nat.le_0_l. + induction (In_dec eq_nat_dec v (freeVarT s)) as [a0 | b1]; simpl in |- *. * unfold cTriple; repeat apply cPairLe3. -- unfold C; simpl. apply (H (pow3 (depth L a) + (pow3 (depth L a) + pow3 (depth L a))) v0 (fold_right Nat.max 0 (freeVarT s ++ v :: varFormula a)) (codeTerm s)). -- unfold C; simpl; apply Nat.le_max_l. -- apply (H0 (forallH v a) v0 s). -- apply (E (forallH v a) v0 s). -- eapply Nat.le_trans. ++ apply H1. apply depthForall. ++ assert (H2: Nat.max (codeTerm (var (newVar (v0 :: freeVarT (L:=L) s ++ freeVarF a)))) (cPair 0 (pow3 (depth L a) + fold_right Nat.max 0 (v :: freeVarT (L:=L) (var (newVar (v0 :: freeVarT (L:=L) s ++ freeVarF a))) ++ varFormula a))) <= C). { assert (H2: newVar (v0 :: freeVarT s ++ freeVarF a) <= pow3 (depth L a) + fold_right Nat.max 0 (v0 :: freeVarT s ++ varFormula (forallH v a))). { apply Nat.le_trans with (1 + fold_right Nat.max 0 (v0 :: fold_right Nat.max 0 (freeVarT s) :: varFormula a)). - apply boundSubFormulaHelp2 with (a := a) (v0 := v0) (s := s). - apply Nat.add_le_mono. + apply pow3Min. + simpl; apply Nat.max_case. * apply Nat.le_max_l. * eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply Nat.max_case. -- apply maxLemma2. -- eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. simpl; apply Nat.le_max_r. } apply Nat.max_case. - replace (codeTerm (var (newVar (v0 :: freeVarT s ++ freeVarF a)))) with (cPair 0 (newVar (v0 :: freeVarT s ++ freeVarF a))); [ idtac | reflexivity ]. unfold C; eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply cPairLe3. + apply le_n. + eapply Nat.le_trans. apply H2. apply Nat.add_le_mono_r. simpl; apply Nat.le_add_r. - unfold C; eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply cPairLe3. + apply le_n. + simpl; rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.max_case. * 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. * apply Nat.max_case. -- rewrite <- Nat.add_assoc. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply H2. -- eapply Nat.le_trans; [ idtac | apply Compat815.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_r. } assert (H3: ReplaceFormulaTerm (codeFormula a) (Nat.max (codeTerm (var (newVar (v0 :: freeVarT (L:=L) s ++ freeVarF a)))) (cPair 0 (pow3 (depth L a) + fold_right Nat.max 0 (v :: freeVarT (L:=L) (var (newVar (v0 :: freeVarT s ++ freeVarF a))) ++ varFormula a)))) <= ReplaceFormulaTerm (cPair 3 (cPair v (codeFormula a))) C). { unfold ReplaceFormulaTerm at 2; fold A; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl; unfold A at 1. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite D with (m := codeFormula a). -- simpl; eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. apply ReplaceFormulaTermMonotone. simpl in H2. apply H2. -- eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. } apply boundComputationMonotone. ** apply le_n. ** unfold cTriple in |- *. repeat apply cPairLe3. apply H2. apply H2. apply H3. ** apply H3. -- eapply Nat.le_trans. ++ apply H1. eapply eqDepth. symmetry; apply subFormulaDepth. apply depthForall. ++ rewrite subFormulaDepth. assert (H2: Nat.max (codeTerm s) (cPair 0 (pow3 (depth L a) + fold_right Nat.max 0 (v0 :: freeVarT s ++ varFormula (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a))))))) <= C). { unfold C; apply maxLemma. - apply le_n. - apply cPairLe3. + apply le_n. + simpl; rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.max_case. * eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply Nat.le_max_l. * induction (maxApp (freeVarT s) (varFormula (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a)))))) 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 b0. eapply Nat.le_trans. ++ apply boundSubFormulaHelp1. ++ apply Nat.add_le_mono_l. 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. } assert (H3: ReplaceFormulaTerm (codeFormula (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a))))) (Nat.max (codeTerm s) (cPair 0 (pow3 (depth L a) + fold_right Nat.max 0 (v0 :: freeVarT s ++ varFormula (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a)))))))) <= ReplaceFormulaTerm (cPair 3 (cPair v (codeFormula a))) C). { unfold ReplaceFormulaTerm at 2; fold A. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; unfold A at 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite D with (m := codeFormula a). - simpl; eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. rewrite ReplaceFormulaTermSub. apply ReplaceFormulaTermMonotone. apply H2. - eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. } apply boundComputationMonotone. ** apply le_n. ** unfold cTriple in |- *. repeat apply cPairLe3. apply H2. apply H2. apply H3. ** apply H3. * unfold cTriple in |- *. repeat apply cPairLe3. -- unfold C; simpl. apply (H (pow3 (depth L a) + (pow3 (depth L a) + pow3 (depth L a))) v0 (fold_right Nat.max 0 (freeVarT s ++ v :: varFormula a)) (codeTerm s)). -- unfold C in |- *; simpl in |- *. apply Nat.le_max_l. -- apply (H0 (forallH v a) v0 s). -- apply (E (forallH v a) v0 s). -- eapply Nat.le_trans. ++ apply H1. apply depthForall. ++ assert (H2: Nat.max (codeTerm s) (cPair 0 (pow3 (depth L a) + fold_right Nat.max 0 (v0 :: freeVarT s ++ varFormula a))) <= C). { unfold C in |- *. apply maxLemma. - apply le_n. - apply cPairLe3. + apply le_n. + apply Nat.add_le_mono. * simpl in |- *. apply Nat.le_add_r. * simpl; apply maxLemma. -- apply le_n. -- induction (maxApp (freeVarT s) (varFormula a)) as [a0 | b2]. ++ rewrite a0. apply maxLemma2. ++ rewrite b2. eapply Nat.le_trans; [ idtac | apply maxLemma3 ]. simpl; apply Nat.le_max_r. } assert (H4: ReplaceFormulaTerm (codeFormula a) (Nat.max (codeTerm s) (cPair 0 (pow3 (depth L a) + fold_right Nat.max 0 (v0 :: freeVarT s ++ varFormula a)))) <= ReplaceFormulaTerm (cPair 3 (cPair v (codeFormula a))) C). { unfold ReplaceFormulaTerm at 2; fold A; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; unfold A at 1. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite D with (m := codeFormula a). - simpl; eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. apply ReplaceFormulaTermMonotone. apply H2. - eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. } eapply Nat.le_trans; [ idtac | apply cPairLe1 ]. apply boundComputationMonotone. ** apply le_n. ** unfold cTriple in |- *. repeat apply cPairLe3. apply H2. apply H2. apply H4. ** apply H4. + unfold makeTrace in |- *. rewrite (Formula_depth_rec2_forall L) with (Q := fun _ : fol.Formula L => (nat * fol.Term L)%type) (P := fun _ : fol.Formula L => nat). * unfold makeTraceForall at 1 in |- *. reflexivity. * apply makeTraceImpNice. * apply makeTraceNotNice. * apply makeTraceForallNice. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)