proposition: Remark boundSubFormulaHelp1 : forall (b a : fol.Formula L) (v0 v : nat) (s : fol.Term L), fold_right Nat.max 0 (varFormula (substF b v (var (newVar (v0 :: freeVarT s ++ freeVarF a))))) <= pow3 (depth L b) + pow3 (depth L b) + Nat.max v0 (Nat.max (fold_right Nat.max 0 (freeVarT s)) (Nat.max v (Nat.max (fold_right Nat.max 0 (varFormula b)) (fold_right Nat.max 0 (varFormula a))))).
proof: Proof. intro b; elim b using Formula_depth_ind2. - intros t t0 a v0 v s; set (nv := newVar (v0 :: freeVarT s ++ freeVarF a)). simpl; apply le_S. induction (maxApp (freeVarT (substT t v (var nv))) (freeVarT (substT t0 v (var nv)))) as [a0 | b0]. + rewrite a0; eapply Nat.le_trans. * apply maxSubTerm. * simpl; apply (Nat.max_case nv (fold_right Nat.max 0 (freeVarT t))). -- eapply Nat.le_trans. ++ apply (boundSubFormulaHelp2 a v0 s). ++ apply le_n_S. simpl; repeat apply maxLemma; try apply le_n. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply Nat.le_max_r. -- apply le_S. do 3 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). eapply Nat.le_trans; [ idtac | apply Nat.le_max_l ]. apply maxLemma2. + rewrite b0; eapply Nat.le_trans. * apply maxSubTerm. * simpl; apply (Nat.max_case nv (fold_right Nat.max 0 (freeVarT t0))). -- eapply Nat.le_trans. ++ apply (boundSubFormulaHelp2 a v0 s). ++ apply le_n_S. simpl; repeat apply maxLemma; try apply le_n. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply Nat.le_max_r. -- apply le_S. do 3 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). eapply Nat.le_trans; [ idtac | apply Nat.le_max_l ]. apply maxLemma3. - intros r t a v0 v s; set (nv := newVar (v0 :: freeVarT s ++ freeVarF a)); eapply Nat.le_trans. + simpl; apply maxSubTerms. + simpl; apply le_S. apply (Nat.max_case nv (fold_right max 0 (freeVarTs t))). * eapply Nat.le_trans. -- apply (boundSubFormulaHelp2 a v0 s). -- apply le_n_S. simpl; repeat apply maxLemma; try apply le_n. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply Nat.le_max_r. * apply le_S. do 3 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). eapply Nat.le_trans; [ idtac | apply Nat.le_max_l ]. apply le_n. - intros f H f0 H0 a v0 v s; set (nv := newVar (v0 :: freeVarT s ++ freeVarF a)). rewrite subFormulaImp; simpl. induction (maxApp (varFormula (substF f v (var nv))) (varFormula (substF f0 v (var nv)))) as [a0 | b0]. + rewrite a0; eapply Nat.le_trans. * apply (H a v0 v s). * apply Nat.add_le_mono. -- eapply Nat.le_trans; [ idtac | apply Nat.le_add_r ]. assert (H1: pow3 (depth L f) <= pow3 (Nat.max (depth L f) (depth L f0))) by (apply pow3Monotone; apply Nat.le_max_l). apply Nat.add_le_mono. ++ assumption. ++ eapply Nat.le_trans; [ idtac | apply Nat.le_add_r ]. assumption. -- repeat apply maxLemma; try apply le_n. apply maxLemma2. + rewrite b0; eapply Nat.le_trans. * apply (H0 a v0 v s). * apply Nat.add_le_mono. -- eapply Nat.le_trans; [ idtac | apply Nat.le_add_r ]. assert (H1: pow3 (depth L f0) <= pow3 (Nat.max (depth L f) (depth L f0))) by (apply pow3Monotone; apply Nat.le_max_r). apply Nat.add_le_mono. ++ assumption. ++ eapply Nat.le_trans; [ idtac | apply Nat.le_add_r ]. assumption. -- repeat apply maxLemma; try apply le_n. apply maxLemma3. - intros f H a v0 v s; set (nv := newVar (v0 :: freeVarT s ++ freeVarF a)). rewrite subFormulaNot; eapply Nat.le_trans. + apply (H a v0 v s). + apply Nat.add_le_mono. * simpl; eapply Nat.le_trans; [ idtac | apply Nat.le_add_r ]. apply Compat815.le_plus_r. * apply le_n. - intros v a H a0 v0 v1 s; set (nv := newVar (v0 :: freeVarT s ++ freeVarF a)); clear nv. rewrite subFormulaForall; induction (eq_nat_dec v v1) as [a1 | b0]. + eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. do 3 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). apply Nat.le_max_l. + induction (In_dec eq_nat_dec v (freeVarT (var (newVar (v0 :: freeVarT s ++ freeVarF a0))))) as [a1 | b1]. * simpl; apply (Nat.max_case (newVar (v1 :: newVar (v0 :: freeVarT s ++ freeVarF a0) :: freeVarF a)) (fold_right Nat.max 0 (varFormula (substF (substF a v (var (newVar (v1 :: newVar (v0 :: freeVarT s ++ freeVarF a0) :: freeVarF a)))) v1 (var (newVar (v0 :: freeVarT s ++ freeVarF a0))))))). -- unfold newVar at 1; eapply Nat.le_trans. ++ apply mapListLemma. ++ apply Nat.le_trans with (1 + 1 + Nat.max v0 (Nat.max (fold_right Nat.max 0 (freeVarT s)) (Nat.max v1 (Nat.max (Nat.max v (fold_right Nat.max 0 (varFormula a))) (fold_right Nat.max 0 (varFormula a0)))))). ** simpl; apply le_n_S. apply (Nat.max_case v1 (Nat.max (newVar (v0 :: freeVarT s ++ freeVarF a0)) (fold_right Nat.max 0 (freeVarF a)))). apply le_S. do 2 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). apply Nat.le_max_l. apply (Nat.max_case (newVar (v0 :: freeVarT s ++ freeVarF a0)) (fold_right max 0 (freeVarF a))). eapply Nat.le_trans. apply boundSubFormulaHelp2. apply le_n_S. simpl; repeat apply maxLemma; try apply le_n. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply Nat.le_max_r. apply le_S. do 3 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). eapply Nat.le_trans; [ idtac | apply Nat.le_max_l ]. eapply Nat.le_trans. apply maxVarFreeVar. apply Nat.le_max_r. ** apply Nat.add_le_mono. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply Nat.add_le_mono. apply pow3Min. simpl; eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply pow3Min. apply le_n. -- eapply Nat.le_trans. ++ apply H. eapply eqDepth. ** symmetry in |- *. apply subFormulaDepth. ** apply depthForall. ++ rewrite subFormulaDepth. rewrite (Nat.add_assoc (pow3 (depth L a)) (pow3 (depth L a)) (pow3 (depth L a))). repeat rewrite <- (Nat.add_assoc (pow3 (depth L a) + pow3 (depth L a))). apply Nat.add_le_mono. ** apply le_n. ** apply (Nat.max_case v0 (Nat.max (fold_right Nat.max 0 (freeVarT s)) (Nat.max v1 (Nat.max (fold_right Nat.max 0 (varFormula (substF a v (var (newVar (v1 :: newVar (v0 :: freeVarT s ++ freeVarF a0) :: freeVarF a)))))) (fold_right Nat.max 0 (varFormula a0)))))). eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply Nat.le_max_l. apply (Nat.max_case (fold_right Nat.max 0 (freeVarT s)) (Nat.max v1 (Nat.max (fold_right Nat.max 0 (varFormula (substF a v (var (newVar (v1 :: newVar (v0 :: freeVarT s ++ freeVarF a0) :: freeVarF a)))))) (fold_right Nat.max 0 (varFormula a0))))). eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]. apply Nat.le_max_l. apply (Nat.max_case v1 (Nat.max (fold_right Nat.max 0 (varFormula (substF a v (var (newVar (v1 :: newVar (v0 :: freeVarT s ++ freeVarF a0) :: freeVarF a)))))) (fold_right Nat.max 0 (varFormula a0)))). eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. do 2 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). apply Nat.le_max_l. apply (Nat.max_case (fold_right Nat.max 0 (varFormula (substF a v (var (newVar (v1 :: newVar (v0 :: freeVarT s ++ freeVarF a0) :: freeVarF a)))))) (fold_right Nat.max 0 (varFormula a0))). eapply Nat.le_trans. apply H with (b := a) (v := v) (v0 := v1) (a := a) (s := var (newVar (v0 :: freeVarT s ++ freeVarF a0))). apply depthForall. rewrite (Nat.add_comm (pow3 (depth L a)) (pow3 (depth L a) + pow3 (depth L a) + pow3 (depth L a))). repeat rewrite <- (Nat.add_assoc (pow3 (depth L a) + pow3 (depth L a))). apply Nat.add_le_mono. apply le_n. apply (Nat.max_case v1 (Nat.max (fold_right Nat.max 0 (freeVarT (var (newVar (v0 :: freeVarT s ++ freeVarF a0))))) (Nat.max v (Nat.max (fold_right Nat.max 0 (varFormula a)) (fold_right Nat.max 0 (varFormula a)))))). eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. do 2 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). apply Nat.le_max_l. apply (Nat.max_case (fold_right Nat.max 0 (freeVarT (var (newVar (v0 :: freeVarT s ++ freeVarF a0))))) (Nat.max v (Nat.max (fold_right Nat.max 0 (varFormula a)) (fold_right Nat.max 0 (varFormula a))))). simpl; apply (Nat.max_case (newVar (v0 :: freeVarT s ++ freeVarF a0)) 0). eapply Nat.le_trans. apply boundSubFormulaHelp2. apply Nat.le_trans with (1 + Nat.max v0 (Nat.max (fold_right Nat.max 0 (freeVarT s)) (Nat.max v1 (Nat.max (Nat.max v (fold_right Nat.max 0 (varFormula a))) (fold_right Nat.max 0 (varFormula a0)))))). simpl; apply le_n_S. repeat apply maxLemma; try apply le_n. repeat (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). apply le_n. apply Nat.add_le_mono. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply pow3Min. apply le_n. apply Nat.le_0_l. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. do 3 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). apply (Nat.max_case v (Nat.max (fold_right Nat.max 0 (varFormula a)) (fold_right Nat.max 0 (varFormula a)))). eapply Nat.le_trans; [ idtac | apply Nat.le_max_l ]. apply Nat.le_max_l. apply (Nat.max_case (fold_right Nat.max 0 (varFormula a)) (fold_right Nat.max 0 (varFormula a))); (eapply Nat.le_trans; [ idtac | apply Nat.le_max_l ]; apply Nat.le_max_r). eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. repeat (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). apply le_n. * simpl; apply (Nat.max_case v (fold_right Nat.max 0 (varFormula (substF a v1 (var (newVar (v0 :: freeVarT s ++ freeVarF a0))))))). -- eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. do 3 (eapply Nat.le_trans; [ idtac | apply Nat.le_max_r ]). eapply Nat.le_trans; [ idtac | apply Nat.le_max_l ]. apply Nat.le_max_l. -- eapply Nat.le_trans. ++ apply H. apply depthForall. ++ apply Nat.add_le_mono. ** eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply Nat.add_le_mono. apply le_n. apply Nat.le_add_r. ** repeat apply maxLemma; try apply le_n. apply Nat.le_max_r. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)