proposition: Lemma checkPrfCorrect1 (l : list Formula) (f : Formula) (p : Prf l f): checkPrf (codeFormula f) (codePrf l f p) = S (codeList (map codeFormula l)).
proof: Proof. unfold checkPrf; rewrite (wellFormedFormulaCorrect1 L cL codeArityF codeArityFIsCorrect1 codeArityR codeArityRIsCorrect1). simpl; lazy beta delta [checkPrfHelp] in |- *. set (A := fun p0 recs : nat => let type := car (cdr p0) in switchPR type (switchPR (pred type) (switchPR (pred (pred type)) (switchPR (pred (pred (pred type))) (switchPR (pred (pred (pred (pred type)))) (switchPR (pred (pred (pred (pred (pred type))))) (switchPR (pred (pred (pred (pred (pred (pred type)))))) (switchPR (pred (pred (pred (pred (pred (pred (pred type))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred type)))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred type))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred type)))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred type))))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred type)))))))))))) (switchPR (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred (pred type))))))))))))) 0 (checkPrfEQ5 p0 recs)) (checkPrfEQ4 p0 recs)) (checkPrfEQ3 p0 recs)) (checkPrfEQ2 p0 recs)) (checkPrfEQ1 p0 recs)) (checkPrfFA3 p0 recs)) (checkPrfFA2 p0 recs)) (checkPrfFA1 p0 recs)) (checkPrfCP p0 recs)) (checkPrfIMP2 p0 recs)) (checkPrfIMP1 p0 recs)) (checkPrfGEN p0 recs)) (checkPrfMP p0 recs)) (checkPrfAXM p0 recs)) in *. induction p as [A0| Axm1 Axm2 A0 B p1 Hrecp1 p0 Hrecp0| Axm A0 v n p Hrecp| A0 B| A0 B C| A0 B| A0 v t| A0 v n| A0 B v| | | | R| f]; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList in |- *; rewrite computeEvalStrongRecHelp; unfold compose2, evalComposeFunc, evalOneParamList, evalList in |- *; simpl in |- *; rewrite cPairProjections1. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]; simpl in |- *. unfold checkPrfAXM; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]; simpl. rewrite Nat.eqb_refl. reflexivity. - set (C := cPair (cPair (cPair 1 (cPair (codeFormula A0) (codeFormula B))) (codePrf Axm1 (impH A0 B) p1)) (cPair (codeFormula A0) (codePrf Axm2 A0 p0))) in *. unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl; unfold C at 1 in |- *. unfold checkPrfMP in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. + repeat rewrite evalStrongRecHelp1. * rewrite Nat.eqb_refl. rewrite Hrecp0. replace (cPair 1 (cPair (codeFormula A0) (codeFormula B))) with (codeFormula (impH A0 B)); [ idtac | reflexivity ]. rewrite Hrecp1. rewrite (wellFormedFormulaCorrect1 L cL codeArityF codeArityFIsCorrect1 codeArityR codeArityRIsCorrect1). simpl in |- *. replace (map (codeFormula) (Axm1 ++ Axm2)) with (map (codeFormula ) Axm1 ++ map (codeFormula ) Axm2). { rewrite codeAppCorrect; reflexivity. } generalize (codeFormula ); intro n. clear p1 A Hrecp1 Hrecp0 C. induction Axm1 as [| a Axm1 HrecAxm1]. -- reflexivity. -- simpl; rewrite HrecAxm1; reflexivity. * eapply Nat.lt_le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. unfold C in |- *; apply cPairLe2. * eapply Nat.lt_le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. unfold C in |- *. apply cPairLe1. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. unfold checkPrfGEN in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. repeat rewrite evalStrongRecHelp1. + rewrite Hrecp. unfold pred in |- *. rewrite codeFreeVarListFormulaCorrect. rewrite codeInCorrect. induction (In_dec eq_nat_dec v (freeVarListFormula L Axm)). * elim n; assumption. * replace (charFunction 2 Nat.eqb (cPair 3 (cPair v (codeFormula A0))) (cPair 3 (cPair v (codeFormula A0)))) with 1. { simpl; reflexivity. } simpl in |- *. rewrite Nat.eqb_refl. reflexivity. + eapply Nat.lt_le_trans; [ idtac | apply cPairLe2 ]. eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. unfold checkPrfIMP1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. unfold charFunction in |- *. rewrite Nat.eqb_refl. reflexivity. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. unfold checkPrfIMP2 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. unfold charFunction in |- *. rewrite Nat.eqb_refl. reflexivity. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. unfold checkPrfCP in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. unfold charFunction in |- *. rewrite Nat.eqb_refl. reflexivity. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. unfold checkPrfFA1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite codeSubFormulaCorrect. unfold charFunction in |- *. rewrite Nat.eqb_refl. rewrite (wellFormedTermCorrect1 L cL codeArityF codeArityFIsCorrect1). reflexivity. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. unfold checkPrfFA2 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite codeFreeVarFormulaCorrect. rewrite codeInCorrect. induction (In_dec eq_nat_dec v (freeVarF A0)). + elim n; assumption. + unfold charFunction in |- *; rewrite Nat.eqb_refl. reflexivity. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl; unfold checkPrfFA3 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. unfold charFunction in |- *. now rewrite Nat.eqb_refl. - set (C := cPair 0 (cPair (codeTerm (var 0)) (codeTerm (var 0)))) in *. unfold A at 1 in |- *. cut (car (cdr (cPair C (cPair 9 0))) = 9); [ intro H; rewrite H; clear H | idtac ]. + simpl in |- *; unfold checkPrfEQ1 in |- *. rewrite (cPairProjections2 C (cPair 9 0)). rewrite (cPairProjections1 C (cPair 9 0)). rewrite (cPairProjections2 9 0). unfold C in |- *; unfold charFunction in |- *; rewrite Nat.eqb_refl. simpl in |- *. reflexivity. + rewrite (cPairProjections2 C (cPair 9 0)). rewrite (cPairProjections1 9 0). reflexivity. - set (C := cPair 1 (cPair (cPair 0 (cPair (codeTerm (var 0)) (codeTerm (var 1)))) (cPair 0 (cPair (codeTerm (var 1)) (codeTerm (var 0)))))) in *. unfold A at 1 in |- *. cut (car (cdr (cPair C (cPair 10 0))) = 10). + generalize (car (cdr (cPair C (cPair 10 0)))). intros n H; rewrite H. simpl in |- *. unfold checkPrfEQ2 in |- *. replace (codeFormula (cl:= cL) (impH (equal (var 0) (var 1)) (equal (var 1) (var 0)))) with C ; [ idtac | reflexivity ]. generalize C; intros C0. rewrite (cPairProjections2 C0 (cPair 10 0)). rewrite (cPairProjections2 10 0). rewrite (cPairProjections1 C0 (cPair 10 0)). unfold charFunction in |- *. repeat rewrite Nat.eqb_refl. reflexivity. + rewrite (cPairProjections2 C (cPair 10 0)). now rewrite (cPairProjections1 10 0). - set (C := cPair 1 (cPair (cPair 0 (cPair (codeTerm (var 0)) (codeTerm (var 1)))) (cPair 1 (cPair (cPair 0 (cPair (codeTerm (var 1)) (codeTerm (var 2)))) (cPair 0 (cPair (codeTerm (var 0)) (codeTerm (var 2)))))))) in *. unfold A at 1 in |- *. cut (car (cdr (cPair C (cPair 11 0))) = 11). + generalize (car (cdr (cPair C (cPair 11 0)))). intros n H; rewrite H; simpl. unfold checkPrfEQ3 in |- *. replace (codeFormula (cl:=cL) (impH (equal (var 0) (var 1)) (impH (equal (var 1) (var 2)) (equal (var 0) (var 2))))) with C; [ idtac | reflexivity ]. generalize C; intros. rewrite (cPairProjections2 C0 (cPair 11 0)). rewrite (cPairProjections1 C0 (cPair 11 0)). rewrite (cPairProjections2 11 0). unfold charFunction in |- *. repeat rewrite Nat.eqb_refl. reflexivity. + rewrite (cPairProjections2 C (cPair 11 0)). rewrite (cPairProjections1 11 0). reflexivity. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. unfold checkPrfEQ4 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. unfold codeR. rewrite codeArityRIsCorrect1. replace (codeAxmEqHelp (pred (S (arityR L R))) (codeIff (cPair (S (S (S (S (cr R))))) (codeNVars1 (pred (S (arityR L R))))) (cPair (S (S (S (S (cr R))))) (codeNVars2 (pred (S (arityR L R))))))) with (codeFormula (AxmEq4 L R)). unfold charFunction in |- *. repeat rewrite Nat.eqb_refl. reflexivity. unfold AxmEq4 in |- *. clear A. simpl in |- *. induction (codeNVarsCorrect (arityR L R)). rewrite H. rewrite H0. clear H H0. induction (nVars L (arityR L R)). simpl in |- *. replace (codeIff (cPair (S (S (S (S (cr R))))) (codeTerms a)) (cPair (S (S (S (S (cr R))))) (codeTerms b))) with (codeFormula (iffH (atomic R a) (atomic R b))). + generalize (arityR L R). intros n; induction n as [| n Hrecn]. * reflexivity. * simpl; now rewrite Hrecn. + rewrite <- codeIffCorrect; reflexivity. - unfold A at 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. unfold checkPrfEQ5 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. unfold codeF. rewrite codeArityFIsCorrect1. replace (codeAxmEqHelp (pred (S (arityF L f))) (cPair 0 (cPair (cPair (S (cf f)) (codeNVars1 (pred (S (arityF L f))))) (cPair (S (cf f)) (codeNVars2 (pred (S (arityF L f)))))))) with (codeFormula (AxmEq5 L f)). + unfold charFunction, codeF in |- *; repeat rewrite Nat.eqb_refl. reflexivity. + unfold AxmEq5 in |- *; clear A; simpl. induction (codeNVarsCorrect (arityF L f)). rewrite H, H0. clear H H0. induction (nVars L (arityF L f)). simpl; replace (cPair 0 (cPair (cPair (S (cf f)) (codeTerms a)) (cPair (S (cf f)) (codeTerms b)))) with (codeFormula (equal (apply f a) (apply f b))). * generalize (arityF L f). intros n;induction n as [| n Hrecn]. -- reflexivity. -- simpl; rewrite Hrecn. reflexivity. * reflexivity. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)