proposition: Lemma codeSysPrfCorrect1 : forall (f : fol.Formula L) (A : list (fol.Formula L)) (p : Prf L A f), (forall g : fol.Formula L, In g A -> mem _ U g) -> SysPrf T (substF (substF codeSysPrf 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A f p))).
proof: Proof. intros f A p H; unfold codeSysPrf; set (nvl := 2 :: 1 :: 0 :: v0 :: nil). set (nv := newVar nvl); assert (H0: nv <> 0). { unfold nv, not in |- *; intros; elim (newVar1 nvl). rewrite H0; unfold nvl in |- *. simpl in |- *; auto. } assert (H1: nv <> 1). { unfold nv, not in |- *; intros; elim (newVar1 nvl). rewrite H1; unfold nvl; simpl; auto. } assert (H2: nv <> 2). { unfold nv, not in |- *; intros; elim (newVar1 nvl). rewrite H2; unfold nvl; simpl; auto. } assert (H3: nv <> v0). { unfold nv, not in |- *; intros; elim (newVar1 nvl). rewrite H3; unfold nvl; simpl; auto. } rewrite (subFormulaExist LNN). induction (eq_nat_dec nv 0) as [a | b]. - elim H0; assumption. - induction (In_dec eq_nat_dec nv (freeVarT (natToTerm (codeFormula f)))) as [a | b0]. + elim (closedNatToTerm _ _ a). + clear b b0; rewrite (subFormulaExist LNN). induction (eq_nat_dec nv 1) as [a | b]. * elim H1; assumption. * induction (In_dec eq_nat_dec nv (freeVarT (natToTerm (codePrf A f p)))) as [a | b0]. -- elim (closedNatToTerm _ _ a). -- clear b b0. apply existI with (natToTerm (codeList (map (codeFormula) A))). repeat rewrite (subFormulaAnd LNN). apply andI. ++ apply sysExtend with NN. ** apply TextendsNN. ** set (B := primRecFormula 2 (proj1_sig (checkPrfIsPR L cL codeArityF codeArityR codeArityFIsPR codeArityRIsPR))). apply impE with (substF (substF (substF (substF B 0 (Succ (var nv))) 2 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A f p))) nv (natToTerm (codeList (map (codeFormula) A)))). --- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). intros H4; assert (H5: In 0 (freeVarF (substF B 0 (Succ (var nv))))) by eapply in_remove, H4. induction (freeVarSubFormula3 _ _ _ _ _ H5). +++ elim (in_remove_neq _ _ _ _ _ H6); reflexivity. +++ simpl in H6; decompose sum H6; auto. --- apply impE with (substF (substF (substF (substF B 2 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A f p))) 0 (Succ (var nv))) nv (natToTerm (codeList (map (codeFormula) A)))). +++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply iffTrans with (substF (substF (substF B 2 (natToTerm (codeFormula f))) 0 (Succ (var nv))) 1 (natToTerm (codePrf A f p))). *** repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). discriminate. simpl in |- *. unfold not in |- *; intros. decompose sum H4. apply H2; assumption. apply closedNatToTerm. *** apply (subFormulaExch LNN). discriminate. simpl in |- *. unfold not in |- *; intros. decompose sum H4. apply H1; assumption. apply closedNatToTerm. +++ unfold B in |- *. clear B. assert (H4: Representable NN 2 (checkPrf L cL codeArityF codeArityR) (primRecFormula 2 (proj1_sig (checkPrfIsPR L cL codeArityF codeArityR codeArityFIsPR codeArityRIsPR)))) by apply primRecRepresentable. induction H4 as (H4, H5). set (F := primRecFormula 2 (proj1_sig (checkPrfIsPR L cL codeArityF codeArityR codeArityFIsPR codeArityRIsPR))) in *. simpl in H5. apply impE with (substF (substF (equal (var 0) (natToTerm (checkPrf L cL codeArityF codeArityR (codeFormula f) (codePrf A f p)))) 0 (Succ (var nv))) nv (natToTerm (codeList (map (codeFormula) A)))). *** apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply H5. *** rewrite (subFormulaEqual LNN). rewrite (subTermVar1 LNN). rewrite (subTermNil LNN). rewrite (subFormulaEqual LNN). replace (substT (Succ (var nv)) nv (natToTerm (codeList (map (codeFormula) A)))) with (natToTerm (S (codeList (map (codeFormula) A)))). ---- rewrite (subTermNil LNN). rewrite checkPrfCorrect1. apply eqRefl. apply codeArityFIsCorrect1. apply codeArityRIsCorrect1. apply closedNatToTerm. ---- generalize nv ; intro nv0. simpl in |- *. induction (eq_nat_dec nv0 nv0). reflexivity. elim b. reflexivity. ---- apply closedNatToTerm. ++ assert (H4: S nv <> 1). ** unfold not in |- *; intros. lia. ** assert (S nv <> 2). --- unfold not in |- *; intros. lia. --- assert (H6: S nv <> nv) by lia. rewrite (subFormulaForall LNN). induction (eq_nat_dec (S nv) 0). +++ discriminate a. +++ induction (In_dec eq_nat_dec (S nv) (freeVarT (natToTerm (codeFormula f)))). *** elim (closedNatToTerm _ _ a). *** clear b b0. rewrite (subFormulaForall LNN). induction (eq_nat_dec (S nv) 1). elim H4; assumption. induction (In_dec eq_nat_dec (S nv) (freeVarT (natToTerm (codePrf A f p)))). ---- elim (closedNatToTerm _ _ a). ---- clear b b0. rewrite (subFormulaForall LNN). induction (eq_nat_dec (S nv) nv). ++++ elim H6; assumption. ++++ induction (In_dec eq_nat_dec (S nv) (freeVarT (natToTerm (codeList (map (codeFormula) A))))). **** elim (closedNatToTerm _ _ a). **** clear b b0. repeat rewrite (subFormulaImp LNN). replace (substF (substF (substF (LT (var (S nv)) (var nv)) 0 (natToTerm (codeFormula f))) 1 (natToTerm (codePrf A f p))) nv (natToTerm (codeList (map (codeFormula) A)))) with (LT (var (S nv)) (natToTerm (codeList (map (codeFormula) A)))). set (G := list_rec (fun _ => Formula) (equal Zero Zero) (fun (a : fol.Formula L) _ (rec : Formula) => andH (substF fU v0 (natToTerm (codeFormula a))) rec) A) in *. assert (H7: forall v : nat, ~ In v (freeVarF G)). { unfold G in |- *. intros. generalize A. intro. induction A0 as [| a A0 HrecA0]. simpl in |- *. auto. simpl in |- *. unfold not in |- *; intros. induction (in_app_or _ _ _ H7). induction (freeVarSubFormula3 _ _ _ _ _ H8). absurd (v = v0). eapply in_remove_neq. apply H9. apply freeVarfU. eapply in_remove. apply H9. elim (closedNatToTerm _ _ H9). auto. } apply impE with G. apply sysExtend with NN. assumption. apply impI. assert (H8: forall v : nat, ~ In_freeVarSys LNN v (Ensembles.Add (fol.Formula LNN) NN G)). { unfold not in |- *; intros. induction H8 as (x, H8). induction H8 as (H8, H9). induction H9 as [x H9| x H9]. elim (closedNN v). exists x. auto. induction H9. apply (H7 v). assumption. } apply forallI. apply H8. apply impI. apply impE with G. apply impE with (LT (var (S nv)) (natToTerm (codeList (map (codeFormula) A)))). repeat simple apply sysWeaken. apply boundedLT. intros n H9. rewrite (subFormulaImp LNN). apply impTrans with G. apply iffE1. apply (subFormulaNil LNN). apply H7. apply impI. repeat rewrite (subFormulaOr LNN). induction (In_dec eq_nat_dec n (map (codeFormula ) A)). apply orI2. apply impE with (substF fU v0 (natToTerm n)). apply iffE2. apply sysWeaken. assert (H10: forall v : nat, ~ In v (List.remove eq_nat_dec v0 (freeVarF fU))). { intros v H10; absurd (v = v0). - eapply in_remove_neq, H10. - apply freeVarfU; eapply in_remove, H10. } apply iffTrans with (substF (substF (substF (substF fU v0 (var (S nv))) 1 (natToTerm (codePrf A f p))) nv (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H11). apply (H10 0). assumption. simpl in H12. decompose sum H12. discriminate H13. apply iffTrans with (substF (substF (substF fU v0 (var (S nv))) nv (natToTerm (codeList (map codeFormula A)))) (S nv) (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H11). apply (H10 1). assumption. simpl in H12. decompose sum H12. apply H4; assumption. apply iffTrans with (substF (substF fU v0 (var (S nv))) (S nv) (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H11). apply (H10 nv). assumption. simpl in H12. decompose sum H12. apply H6; assumption. apply (subFormulaTrans LNN). unfold not in |- *; intros. absurd (S nv = v0). unfold not in |- *; intros. { elim (Compat815.le_not_lt (S nv) v0). rewrite H12. apply le_n. apply Nat.lt_lt_succ_r. unfold nv in |- *. apply newVar2. unfold nvl in |- *; simpl in |- *; auto. } apply freeVarfU. eapply in_remove. apply H11. clear H9 H8 H7 H p. induction A as [| a0 A HrecA]. elim a. simpl in (value of G). simpl in a. induction a as [H| H]. unfold G in |- *. rewrite H. eapply andE1. apply Axm; right; constructor. apply impE with (list_rec (fun _ => Formula) (equal Zero Zero) (fun (a : fol.Formula L) (_ : list (fol.Formula L)) (rec : Formula) => andH (substF fU v0 (natToTerm (codeFormula a))) rec) A). apply sysWeaken. apply impI. apply HrecA. assumption. eapply andE2. unfold G in |- *. apply Axm; right; constructor. apply orI1. assert (H10: Representable NN 2 codeIn (primRecFormula 2 (proj1_sig codeInIsPR))) by apply primRecRepresentable. induction H10 as (H10, H11). set (J := primRecFormula 2 (proj1_sig codeInIsPR)) in *. simpl in H11. apply sysWeaken. apply impE with (substF (substF (substF J 2 (natToTerm n)) 1 (natToTerm (codeList (map (codeFormula) A)))) 0 Zero). apply iffE2. apply iffTrans with (substF (substF (substF (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) 0 Zero) 1 (natToTerm (codePrf A f p))) nv (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H12). elim (in_remove_neq _ _ _ _ _ H13). reflexivity. apply H13. apply iffTrans with (substF (substF (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) 0 Zero) nv (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaNil LNN). unfold not in |- *; intros. induction (freeVarSubFormula3 _ _ _ _ _ H12). assert (H14: In 1 (freeVarF (substF (substF J 2 (var (S nv))) 1 (var nv)))) by eapply in_remove, H13. induction (freeVarSubFormula3 _ _ _ _ _ H14). elim (in_remove_neq _ _ _ _ _ H15). reflexivity. simpl in H15. decompose sum H15. apply H1; assumption. apply H13. apply iffTrans with (substF (substF (substF (substF (substF J 2 (var (S nv))) 1 (var nv)) nv (natToTerm (codeList (map (codeFormula) A)))) 0 Zero) (S nv) (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). unfold not in |- *; intros; apply H0; symmetry in |- *; assumption. auto. apply closedNatToTerm. apply iffTrans with (substF (substF (substF (substF J 2 (var (S nv))) 1 (natToTerm (codeList (map (codeFormula) A)))) 0 Zero) (S nv) (natToTerm n)). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). intros H12; assert (H13: In nv (freeVarF (substF J 2 (var (S nv))))) by eapply in_remove, H12. induction (freeVarSubFormula3 _ _ _ _ _ H13). apply (Compat815.le_not_lt nv 2). apply H10. eapply in_remove. apply H14. destruct nv as [| n0]. elim H0; reflexivity. destruct n0. elim H1; reflexivity. destruct n0. elim H2; reflexivity. repeat apply Compat815.lt_n_S. apply Nat.lt_0_succ. simpl in H14. decompose sum H14. apply H6; assumption. apply iffTrans with (substF (substF (substF (substF J 2 (var (S nv))) 1 (natToTerm (codeList (map (codeFormula) A)))) (S nv) (natToTerm n)) 0 Zero). apply (subFormulaExch LNN). discriminate. auto. apply closedNatToTerm. apply iffTrans with (substF (substF (substF (substF J 2 (var (S nv))) (S nv) (natToTerm n)) 1 (natToTerm (codeList (map (codeFormula) A)))) 0 Zero). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). unfold not in |- *; intros; apply H4; symmetry in |- *; assumption. apply closedNatToTerm. apply closedNatToTerm. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaTrans LNN). unfold not in |- *; intros. apply (Compat815.le_not_lt (S nv) 2). apply H10. eapply in_remove. apply H12. apply Compat815.le_lt_n_Sm. destruct nv as [| n0]. elim H0; reflexivity. destruct n0. elim H1; reflexivity. repeat apply le_n_S. apply Nat.le_0_l. apply impE with (substF (equal (var 0) (natToTerm (codeIn n (codeList (map (codeFormula) A))))) 0 Zero). apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply H11. rewrite codeInCorrect. induction (In_dec eq_nat_dec n (map (codeFormula) A)). elim b; assumption. rewrite (subFormulaEqual LNN). rewrite (subTermVar1 LNN). rewrite (subTermNil LNN). apply eqRefl. apply closedNatToTerm. apply Axm; right; constructor. apply Axm; left; right; constructor. clear p H7. induction A as [| a A HrecA]; simpl in (value of G). unfold G in |- *. apply eqRefl. simpl in H. unfold G in |- *. apply andI. apply expressU1. apply H. auto. apply HrecA. intros. apply H. auto. assert (H7: forall (t1 t2 s : Term) (v : nat), substF (LT t1 t2) v s = LT (substT t1 v s) (substT t2 v s)) by reflexivity. repeat rewrite H7. repeat rewrite (subTermVar1 LNN) || rewrite (subTermVar2 LNN); try unfold not in |- *; intros. reflexivity. apply H1; auto. apply H0; auto. apply H6; auto. apply H4; auto. discriminate H8. Qed.
imports: Coq(Ensembles) Coq(List) hydras.Ackermann(checkPrf) hydras.Ackermann(code) hydras.Ackermann(Languages) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folLogic3) hydras.Ackermann(folReplace) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(primRec) Coq(Arith Lia) hydras.Ackermann(PA) hydras.Ackermann(NNtheory) hydras.Ackermann(codeList) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) hydras.Ackermann(cPair) hydras.Ackermann(wellFormed) hydras.Ackermann(prLogic) hydras(Compat815)