proposition: Lemma makeTraceCorrect : forall (f : fol.Formula L) (v : nat) (s : fol.Term L), checkSubFormulaTrace (makeTrace f (v, s)) = 1.
proof: Proof. intro f; unfold checkSubFormulaTrace; set (A := fun trace recs : nat => switchPR (car (cTriplePi3 (cTriplePi1 trace))) (switchPR (pred (car (cTriplePi3 (cTriplePi1 trace)))) (switchPR (pred (pred (car (cTriplePi3 (cTriplePi1 trace))))) (switchPR (pred (pred (pred (car (cTriplePi3 (cTriplePi1 trace)))))) (charFunction 2 Nat.eqb (cTriplePi2 trace) (cPair (car (cTriplePi3 (cTriplePi1 trace))) (codeSubTerms (cdr (cTriplePi3 (cTriplePi1 trace))) (cTriplePi1 (cTriplePi1 trace)) (cTriplePi2 (cTriplePi1 trace))))) (switchPR (charFunction 2 Nat.eqb (cTriplePi1 (cTriplePi1 trace)) (car (cdr (cTriplePi3 (cTriplePi1 trace))))) (charFunction 2 Nat.eqb (cTriplePi3 (cTriplePi1 trace)) (cTriplePi2 trace)) (switchPR (codeIn (car (cdr (cTriplePi3 (cTriplePi1 trace)))) (codeFreeVarTerm (cTriplePi2 (cTriplePi1 trace)))) (charFunction 0 (Nat.eqb (cTriplePi2 trace) (cPair 3 (cPair (codeNewVar (S (cPair (cTriplePi1 (cTriplePi1 trace)) (codeApp (codeFreeVarTerm (cTriplePi2 (cTriplePi1 trace))) (codeFreeVarFormula (cdr (cdr (cTriplePi3 (cTriplePi1 trace))))))))) (cTriplePi2 (cdr (cTriplePi3 trace))))) && (Nat.eqb (cTriple (cTriplePi1 (cTriplePi1 trace)) (cTriplePi2 (cTriplePi1 trace)) (cTriplePi2 (car (cTriplePi3 trace)))) (cTriplePi1 (cdr (cTriplePi3 trace))) && Nat.eqb (cTriple (car (cdr (cTriplePi3 (cTriplePi1 trace)))) (cPair 0 (codeNewVar (S (cPair (cTriplePi1 (cTriplePi1 trace)) (codeApp (codeFreeVarTerm (cTriplePi2 (cTriplePi1 trace))) (codeFreeVarFormula (cdr (cdr (cTriplePi3 (cTriplePi1 trace)))))))))) (cdr (cdr (cTriplePi3 (cTriplePi1 trace))))) (cTriplePi1 (car (cTriplePi3 trace))))) * (codeNth (trace - S (car (cTriplePi3 trace))) recs * codeNth (trace - S (cdr (cTriplePi3 trace))) recs)) (charFunction 0 (Nat.eqb (cTriplePi2 trace) (cPair 3 (cPair (car (cdr (cTriplePi3 (cTriplePi1 trace)))) (cTriplePi2 (cTriplePi3 trace)))) && Nat.eqb (cTriple (cTriplePi1 (cTriplePi1 trace)) (cTriplePi2 (cTriplePi1 trace)) (cdr (cdr (cTriplePi3 (cTriplePi1 trace))))) (cTriplePi1 (cTriplePi3 trace))) * codeNth (trace - S (cTriplePi3 trace)) recs)))) (charFunction 0 (Nat.eqb (cTriplePi2 trace) (cPair 2 (cTriplePi2 (cTriplePi3 trace))) && Nat.eqb (cTriple (cTriplePi1 (cTriplePi1 trace)) (cTriplePi2 (cTriplePi1 trace)) (cdr (cTriplePi3 (cTriplePi1 trace)))) (cTriplePi1 (cTriplePi3 trace))) * codeNth (trace - S (cTriplePi3 trace)) recs)) (charFunction 0 (Nat.eqb (cTriplePi2 trace) (cPair 1 (cPair (cTriplePi2 (car (cTriplePi3 trace))) (cTriplePi2 (cdr (cTriplePi3 trace))))) && (Nat.eqb (cTriple (cTriplePi1 (cTriplePi1 trace)) (cTriplePi2 (cTriplePi1 trace)) (car (cdr (cTriplePi3 (cTriplePi1 trace))))) (cTriplePi1 (car (cTriplePi3 trace))) && Nat.eqb (cTriple (cTriplePi1 (cTriplePi1 trace)) (cTriplePi2 (cTriplePi1 trace)) (cdr (cdr (cTriplePi3 (cTriplePi1 trace))))) (cTriplePi1 (cdr (cTriplePi3 trace))))) * (codeNth (trace - S (car (cTriplePi3 trace))) recs * codeNth (trace - S (cdr (cTriplePi3 trace))) recs))) (charFunction 2 Nat.eqb (cTriplePi2 trace) (cPair 0 (cPair (codeSubTerm (car (cdr (cTriplePi3 (cTriplePi1 trace)))) (cTriplePi1 (cTriplePi1 trace)) (cTriplePi2 (cTriplePi1 trace))) (codeSubTerm (cdr (cdr (cTriplePi3 (cTriplePi1 trace)))) (cTriplePi1 (cTriplePi1 trace)) (cTriplePi2 (cTriplePi1 trace))))))). elim f using Formula_depth_ind2. - intros t t0 v s; unfold makeTrace, Formula_depth_rec2, Formula_depth_rec; simpl. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. rewrite cPairProjections1. unfold A at 1 in |- *; repeat first [ rewrite cTripleProj1 | rewrite cTripleProj2 | rewrite cTripleProj3 | rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl; unfold codeTerm; repeat rewrite codeSubTermCorrect. now rewrite Nat.eqb_refl. - intros r t v s; unfold makeTrace, Formula_depth_rec2, Formula_depth_rec; simpl. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList in |- *. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; rewrite cPairProjections1. unfold A at 1 in |- *; repeat first [ rewrite cTripleProj1 | rewrite cTripleProj2 | rewrite cTripleProj3 | rewrite cPairProjections1 | rewrite cPairProjections2 ]. unfold codeTerm; rewrite codeSubTermsCorrect; simpl. now rewrite Nat.eqb_refl. - intros f0 H f1 H0 v s. 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 evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. rewrite cPairProjections1. unfold A at 1 in |- *; repeat first [ rewrite cTripleProj1 | rewrite cTripleProj2 | rewrite cTripleProj3 | rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite evalStrongRecHelp1 with (m := makeTrace f0 (v, s)). * rewrite evalStrongRecHelp1 with (m := makeTrace f1 (v, s)). -- simpl; repeat rewrite makeTrace1; repeat rewrite makeTrace2. rewrite subFormulaImp, H, H0. simpl; repeat rewrite Nat.eqb_refl; reflexivity. -- apply Nat.le_lt_trans with (cPair (makeTrace f0 (v, s)) (makeTrace f1 (v, s))). ++ apply cPairLe2. ++ unfold cTriple; apply Nat.le_lt_trans with (cPair (codeFormula (substF (impH f0 f1) v s)) (cPair (makeTrace f0 (v, s)) (makeTrace f1 (v, s)))). apply cPairLe2. apply Nat.lt_le_trans with (cPair 1 (cPair (codeFormula (substF (impH f0 f1) v s)) (cPair (makeTrace f0 (v, s)) (makeTrace f1 (v, s))))). ** apply cPairLt2. ** apply cPairLe3. apply Nat.le_trans with (cPair 1 (cPair (codeFormula f0) (codeFormula f1))). apply cPairLe1. apply Nat.le_trans with (cPair (codeTerm s) (cPair 1 (cPair (codeFormula f0) (codeFormula f1)))). apply cPairLe2. apply cPairLe2. apply le_n. * apply Nat.le_lt_trans with (cPair (makeTrace f0 (v, s)) (makeTrace f1 (v, s))). -- apply cPairLe1. -- unfold cTriple; apply Nat.le_lt_trans with (cPair (codeFormula (substF (impH f0 f1) v s)) (cPair (makeTrace f0 (v, s)) (makeTrace f1 (v, s)))). ++ apply cPairLe2. ++ apply Nat.lt_le_trans with (cPair 1 (cPair (codeFormula (substF (impH f0 f1) v s)) (cPair (makeTrace f0 (v, s)) (makeTrace f1 (v, s))))). ** apply cPairLt2. ** apply cPairLe3. apply Nat.le_trans with (cPair 1 (cPair (codeFormula f0) (codeFormula f1))). apply cPairLe1. apply Nat.le_trans with (cPair (codeTerm s) (cPair 1 (cPair (codeFormula f0) (codeFormula f1)))). apply cPairLe2. apply cPairLe2. apply le_n. + symmetry; 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 H v s; 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 evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; rewrite cPairProjections1. unfold A at 1 in |- *; repeat first [ rewrite cTripleProj1 | rewrite cTripleProj2 | rewrite cTripleProj3 | rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite evalStrongRecHelp1 with (m := makeTrace f0 (v, s)). * simpl; repeat rewrite makeTrace1; repeat rewrite makeTrace2. rewrite subFormulaNot, H; simpl; repeat rewrite Nat.eqb_refl; reflexivity. * apply Nat.le_lt_trans with (cPair (codeFormula (substF (notH f0) v s)) (makeTrace f0 (v, s))). -- apply cPairLe2. -- apply Nat.lt_le_trans with (cPair 2 (cPair (codeFormula (substF (notH f0) v s)) (makeTrace f0 (v, s)))). ++ apply cPairLt2. ++ unfold cTriple in |- *. apply cPairLe3. apply Nat.le_trans with (cPair 2 (codeFormula f0)). ** apply cPairLe1. ** apply Nat.le_trans with (cPair (codeTerm s) (cPair 2 (codeFormula f0))); apply cPairLe2. ** apply le_n. + symmetry; 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 in |- *; reflexivity. * apply makeTraceImpNice. * apply makeTraceNotNice. * apply makeTraceForallNice. - intros v a H v0 s; replace (makeTrace (forallH v a) (v0, s)) with (makeTraceForall v a (fun (b : fol.Formula L) _ => makeTrace b) (v0, s)). + unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. rewrite cPairProjections1; unfold makeTraceForall; simpl. rewrite (subFormulaForall L). destruct (eq_nat_dec v v0) as [a0 | b]. * simpl; unfold A at 1; repeat first [ rewrite cTripleProj1 | rewrite cTripleProj2 | rewrite cTripleProj3 | rewrite cPairProjections1 | rewrite cPairProjections2 ]. replace (charFunction 2 Nat.eqb v0 v) with 1. -- simpl; rewrite Nat.eqb_refl; reflexivity. -- simpl; now rewrite a0, Nat.eqb_refl. * induction (In_dec eq_nat_dec v (freeVarT s)) as [a0 | b0]. -- simpl; unfold A at 1; repeat first [ rewrite cTripleProj1 | rewrite cTripleProj2 | rewrite cTripleProj3 | rewrite cPairProjections1 | rewrite cPairProjections2 ]. replace (charFunction 2 Nat.eqb v0 v) with 0. replace (codeIn v (codeFreeVarTerm (codeTerm s))) with 1. ++ rewrite evalStrongRecHelp1 with (m := makeTrace a (v, var (newVar (v0 :: freeVarT s ++ freeVarF a)))). ** rewrite evalStrongRecHelp1 with (m := makeTrace (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a)))) (v0, s)). replace (codeNewVar (S (cPair v0 (codeApp (codeFreeVarTerm (codeTerm s)) (codeFreeVarFormula (codeFormula a)))))) with (newVar (v0 :: freeVarT s ++ freeVarF a)). simpl; repeat rewrite makeTrace1. repeat rewrite makeTrace2. repeat rewrite Nat.eqb_refl. repeat rewrite H. reflexivity. eapply eqDepth. symmetry in |- *. apply subFormulaDepth. apply depthForall. apply depthForall. unfold codeTerm; rewrite codeFreeVarTermCorrect. unfold codeFormula in |- *. rewrite codeFreeVarFormulaCorrect. rewrite codeAppCorrect. rewrite <- codeNewVarCorrect. reflexivity. generalize (makeTrace (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a)))) (v0, s)) (makeTrace a (v, var (newVar (v0 :: freeVarT s ++ freeVarF a)))) (cPair (newVar (v0 :: freeVarT s ++ freeVarF a)) (codeFormula (substF (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a)))) v0 s))) (cTriple v0 (codeTerm s) (cPair 3 (cPair v (codeFormula a)))). intros n n0 n1 n2. apply Nat.le_lt_trans with (cPair n0 n). apply cPairLe2. unfold cTriple in |- *. apply Nat.lt_le_trans with (cPair 3 (cPair n0 n)). apply cPairLt2. apply Nat.le_trans with (cPair (cPair 3 n1) (cPair n0 n)). apply cPairLe3. apply cPairLe1. apply le_n. apply cPairLe2. ** generalize (makeTrace (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a)))) (v0, s)) (makeTrace a (v, var (newVar (v0 :: freeVarT s ++ freeVarF a)))) (cPair (newVar (v0 :: freeVarT s ++ freeVarF a)) (codeFormula (substF (substF a v (var (newVar (v0 :: freeVarT s ++ freeVarF a)))) v0 s))) (cTriple v0 (codeTerm s) (cPair 3 (cPair v (codeFormula a)))). intros n n0 n1 n2. apply Nat.le_lt_trans with (cPair n0 n). apply cPairLe1. unfold cTriple in |- *. apply Nat.lt_le_trans with (cPair 3 (cPair n0 n)). apply cPairLt2. apply Nat.le_trans with (cPair (cPair 3 n1) (cPair n0 n)). apply cPairLe3. apply cPairLe1. apply le_n. apply cPairLe2. ++ unfold codeTerm; rewrite codeFreeVarTermCorrect. rewrite codeInCorrect. induction (In_dec eq_nat_dec v (freeVarT s)) as [a1 | b0]. ** reflexivity. ** elim b0; assumption. ++ simpl; rewrite nat_eqb_false. ** reflexivity. ** congruence. -- simpl; unfold A at 1; repeat first [ rewrite cTripleProj1 | rewrite cTripleProj2 | rewrite cTripleProj3 | rewrite cPairProjections1 | rewrite cPairProjections2 ]. replace (charFunction 2 Nat.eqb v0 v) with 0. ++ replace (codeIn v (codeFreeVarTerm (codeTerm s))) with 0. ** rewrite evalStrongRecHelp1 with (m := makeTrace a (v0, s)). simpl; repeat rewrite makeTrace1. repeat rewrite makeTrace2. repeat rewrite Nat.eqb_refl. repeat rewrite H. reflexivity. apply depthForall. generalize (makeTrace a (v0, s)) (cPair v (codeFormula (substF a v0 s))) (cTriple v0 (codeTerm s) (cPair 3 (cPair v (codeFormula a)))). intros n n0 n1. unfold cTriple; apply Nat.lt_le_trans with (cPair 3 n). apply cPairLt2. apply Nat.le_trans with (cPair (cPair 3 n0) n). apply cPairLe3. apply cPairLe1. apply le_n. apply cPairLe2. ** unfold codeTerm in |- *. rewrite codeFreeVarTermCorrect. rewrite codeInCorrect. destruct (In_dec eq_nat_dec v (freeVarT s)) as [a0 | b1]. elim b0; assumption. reflexivity. ++ simpl; rewrite nat_eqb_false. ** reflexivity. ** congruence. + unfold makeTrace; 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; reflexivity. * apply makeTraceImpNice. * apply makeTraceNotNice. * apply makeTraceForallNice. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)