proposition: Lemma codeSubFormulaCorrect (f : Formula) (v : nat) (s : Term): codeSubFormula (codeFormula f) v (codeTerm s) = codeFormula (substF f v s).
proof: Proof. unfold codeSubFormula; set (P := fun p x : nat => ltBool 0 (checkSubFormulaTrace (cPair (car p) x))). set (b := boundComputation (codeFormula f) (cTriple (cPair 0 (pow3 (codeFormula f) + (v + (codeTerm s + codeFormula f)))) (cPair 0 (pow3 (codeFormula f) + (v + (codeTerm s + codeFormula f)))) (ReplaceFormulaTerm (codeFormula f) (cPair 0 (pow3 (codeFormula f) + (v + (codeTerm s + codeFormula f)))))) (ReplaceFormulaTerm (codeFormula f) (cPair 0 (pow3 (codeFormula f) + (v + (codeTerm s + codeFormula f)))))). induction (boundedSearch2 P (cPair (cTriple v (codeTerm s) (codeFormula f)) (S b))) as [H | ?]. - assert (H0: P (cPair (cTriple v (codeTerm s) (codeFormula f)) (S b)) (cdr (makeTrace f (v, s))) = true). { unfold P; rewrite cPairProjections1. replace (cPair (cTriple v (codeTerm s) (codeFormula f)) (cdr (makeTrace f (v, s)))) with (makeTrace f (v, s)). - rewrite makeTraceCorrect. unfold ltBool in |- *. induction (le_lt_dec 1 0) as [a | b0]. + now lia. + reflexivity. - transitivity (cPair (car (makeTrace f (v, s))) (cdr (makeTrace f (v, s)))). + symmetry in |- *. apply cPairProjections. + rewrite makeTrace1. reflexivity. } assert (H1: P (cPair (cTriple v (codeTerm s) (codeFormula f)) (S b)) (cdr (makeTrace f (v, s))) = false). { apply boundedSearch1. rewrite H. eapply Nat.lt_le_trans; [ idtac | apply cPairLe2 ]. apply Nat.lt_succ_r. eapply Nat.le_trans with (cPair (car (makeTrace f (v, s))) (cdr (makeTrace f (v, s)))). + apply cPairLe2. + rewrite cPairProjections. eapply Nat.le_trans. * apply boundMakeTrace. * unfold b in |- *. assert (H1: depth L f <= codeFormula f). { clear H0 H b P s v. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl in |- *. - apply Nat.le_0_l. - apply Nat.le_0_l. - apply Compat815.lt_n_Sm_le. rewrite <- Nat.succ_lt_mono. eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply Nat.max_case. eapply Nat.le_trans. + apply Hrecf1. + apply cPairLe1. + eapply Nat.le_trans. * apply Hrecf0. * apply cPairLe2. - apply Compat815.lt_n_Sm_le. rewrite <- Nat.succ_lt_mono. eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. assumption. - apply Compat815.lt_n_Sm_le. rewrite <- Nat.succ_lt_mono. eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. eapply Nat.le_trans. + apply Hrecf. + apply cPairLe2. } assert (H2: Nat.max (codeTerm s) (cPair 0 (pow3 (depth L f) + fold_right Nat.max 0 (v :: freeVarT s ++ varFormula f))) <= cPair 0 (pow3 (codeFormula f) + (v + (codeTerm s + codeFormula f)))). { apply Nat.max_case. - eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. apply Nat.le_add_r. - apply cPairLe3. + apply le_n. + apply Nat.add_le_mono. * apply pow3Monotone. assumption. * simpl in |- *. apply Nat.max_case. -- apply Nat.le_add_r. -- eapply Nat.le_trans; [ idtac | apply Compat815.le_plus_r ]. induction (maxApp (freeVarT s) (varFormula f)) as [a | b0]. ++ rewrite a; eapply Nat.le_trans. ** apply codeTermFreeVar. ** apply Nat.le_add_r. ++ rewrite b0. eapply Nat.le_trans with (codeFormula f). ** clear b0 H1 H0 H b P s v. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl in |- *. --- eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. induction (maxApp (freeVarT t) (freeVarT t0)) as [a | b]. +++ rewrite a. eapply Nat.le_trans. *** apply codeTermFreeVar. *** apply cPairLe1. +++ rewrite b; eapply Nat.le_trans. *** apply codeTermFreeVar. *** apply cPairLe2. --- eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. induction t as [| n t t0 Hrect]. +++ simpl in |- *. apply Nat.le_0_l. +++ replace (freeVarTs (Tcons t t0)) with (freeVarT t ++ freeVarTs t0); [ idtac | reflexivity ]. replace (codeTerms (Tcons t t0)) with (S (cPair (codeTerm t) (codeTerms t0))); [ idtac | reflexivity ]. apply le_S. induction (maxApp (freeVarT t) (freeVarTs t0)) as [a | b]. *** rewrite a; eapply Nat.le_trans. apply codeTermFreeVar. apply cPairLe1. *** rewrite b; eapply Nat.le_trans. apply Hrect. apply cPairLe2. --- eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. induction (maxApp (varFormula f1) (varFormula f0)) as [a | b]. +++ rewrite a; eapply Nat.le_trans. *** apply Hrecf1. *** apply cPairLe1. +++ rewrite b. eapply Nat.le_trans. *** apply Hrecf0. *** apply cPairLe2. --- eapply Nat.le_trans. +++ apply Hrecf. +++ apply cPairLe2. --- eapply Nat.le_trans; [ idtac | apply cPairLe2 ]. apply Nat.max_case. +++ apply cPairLe1. +++ eapply Nat.le_trans. *** apply Hrecf. *** apply cPairLe2. ** rewrite Nat.add_comm. apply Nat.le_add_r. } apply boundComputationMonotone. -- assumption. -- unfold cTriple in |- *. repeat apply cPairLe3. assumption. assumption. apply ReplaceFormulaTermMonotone. assumption. -- apply ReplaceFormulaTermMonotone. assumption. } rewrite H0 in H1. discriminate H1. - unfold P at 1 in H. rewrite cPairProjections1 in H. symmetry; apply checkTraceCorrect with (m := cdr (boundedSearch P (cPair (cTriple v (codeTerm s) (codeFormula f)) (S b)))). intros H0; unfold cTriple at 1 in H0. rewrite cPairProjections in H0. rewrite H0 in H; cbn in H; discriminate. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)