proposition: Lemma codeInductionSchemaCorrect2 (f : Formula): codeInductionSchema (codeFormula f) = true -> InductionSchema f.
proof: Proof. intros H; lazy beta delta [codeInductionSchema] in H; rewrite codeOpenCorrect in H. set (n := car (cdr (cddddr (codeFormula (open f))))) in *. set (g := cdr (cdr (cddddr (codeFormula (open f))))) in *. cbv zeta in H. induction (eq_nat_dec (codeImp (codeSubFormula g n (codeTerm Zero)) (codeImp (codeForall n (codeImp g (codeSubFormula g n (codeTerm (Succ (var n)))))) (codeForall n g))) (codeFormula (open f))) as [a | b]. - rewrite a in H; unfold codeFormula in H; rewrite codeCloseCorrect in H; fold codeFormula in H. destruct (formula_eqdec LNT LNT_eqdec (close LNT (open f)) f) as [a0 | b]. + unfold codeImp at 1 in a. destruct (open f) as [t t0| r t| f0 f1| f0| n0 f0]; simpl in a; try match goal with | h:(cPair ?X1 ?X2 = cPair ?X3 ?X4) |- _ => assert False by (cut (X1 = X3); [ discriminate | eapply cPairInj1; apply h]) ; contradiction end. assert (H0: codeSubFormula g n (codeTerm Zero) = codeFormula f0). { eapply cPairInj1, cPairInj2; apply a. } assert (H1: codeImp (codeForall n (codeImp g (codeSubFormula g n (codeTerm (Succ (var n)))))) (codeForall n g) = codeFormula f1). { eapply cPairInj2; eapply cPairInj2; apply a. } clear a. Opaque cPairPi1. Opaque cPairPi2. unfold codeImp at 1 in H1. destruct f1 as [t t0| r t| f1 f2| f1| n0 f1]; simpl in H1; try match goal with | h:(cPair ?X1 ?X2 = cPair ?X3 ?X4) |- _ => assert False by (cut (X1 = X3); [ discriminate | eapply cPairInj1; apply h ]); contradiction end. assert (H2: codeForall n (codeImp g (codeSubFormula g n (codeTerm (Succ (var n))))) = codeFormula f1). { eapply cPairInj1; eapply cPairInj2; apply H1. } assert (H3: codeForall n g = codeFormula f2). { eapply cPairInj2; eapply cPairInj2; apply H1. } clear H1. unfold codeForall at 1 in H3; destruct f2 as [t t0| r t| f2 f3| f2| n0 f2]; simpl in H3; try match goal with | h:(cPair ?X1 ?X2 = cPair ?X3 ?X4) |- _ => assert False by (cut (X1 = X3); [ discriminate | eapply cPairInj1; apply h ]); contradiction end. simpl in (value of n). simpl in (value of g). unfold InductionSchema in |- *. exists f2, n0. unfold PA7; replace (substF f2 n0 Zero) with f0. * replace (forallH n0 (impH f2 (substF f2 n0 (Succ (var n0))))) with f1. -- symmetry; apply a0. -- apply codeFormulaInj; simpl; rewrite <- codeSubFormulaCorrect. symmetry; unfold n, g in H2. repeat rewrite cPairProjections1 in H2 || rewrite cPairProjections2 in H2; apply H2. * apply codeFormulaInj; rewrite <- codeSubFormulaCorrect. symmetry; unfold n, g in H0. repeat rewrite cPairProjections1 in H0 || rewrite cPairProjections2 in H0; apply H0. + rewrite nat_eqb_false in H. * discriminate H. * unfold not in |- *; intros; apply b. apply codeFormulaInj, H0. - rewrite nat_eqb_false in H. discriminate H. unfold not in |- *; intros; apply b. rewrite <- codeOpenCorrect, <- H0. unfold codeImp; generalize (cPair (codeSubFormula g n (codeTerm Zero)) (cPair 1 (cPair (codeForall n (cPair 1 (cPair g (codeSubFormula g n (codeTerm (Succ (var n))))))) (codeForall n g)))). intros n0; unfold codeClose; assert (H1: forall m : nat, m <= codeNoDup (codeFreeVarFormula (cPair 1 n0)) -> cPair 1 n0 = codeOpen (codeCloseList m (cPair 1 n0))). { induction (codeNoDup (codeFreeVarFormula (cPair 1 n0))). intros m H1; replace m with 0 by lia. - unfold codeCloseList, evalStrongRec. unfold evalComposeFunc, evalOneParamList, evalList; simpl. rewrite cPairProjections1. unfold codeOpen, evalStrongRec. unfold evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. repeat rewrite cPairProjections1. simpl; repeat rewrite cPairProjections1; reflexivity. - intros m H1; destruct (Compat815.le_lt_or_eq _ _ H1) as [H2 | H2]. + apply IHn1. apply Compat815.lt_n_Sm_le. assumption. + rewrite H2. unfold codeCloseList in |- *. set (g0 := fun l recs f0 : nat => switchPR l (cPair 3 (cPair (car (pred l)) (codeNth (l - S (cdr (pred l))) recs))) f0). unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. assert (H3: forall n m : nat, m < n -> extEqual 1 (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 g0 n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - S m) b)) (evalStrongRec 1 g0 m)). { intros n2 m0; apply (evalStrongRecHelp2 1). } simpl in H3. unfold g0 at 1; rewrite H3; simpl. * repeat rewrite cPairProjections1. unfold codeCloseList in IHn1. move g0 after IHn1; fold g0 in IHn1. set (A := evalStrongRec 1 g0 (cdr n1) (cPair 1 n0)) in *. unfold codeOpen. set (g1 := fun f0 recs : nat => switchPR (car f0) (switchPR (pred (car f0)) (switchPR (pred (pred (car f0))) (switchPR (pred (pred (pred (car f0)))) f0 (codeNth (f0 - S (cdr (cdr f0))) recs)) f0) f0) f0). unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp; unfold compose2. unfold evalComposeFunc, evalOneParamList, evalList; unfold g1 at 1 in |- *. unfold pred at 1 in |- *. repeat rewrite cPairProjections1. repeat rewrite evalStrongRecHelp1. simpl; repeat rewrite cPairProjections2. unfold A; unfold codeOpen in IHn1. move g1 after IHn1; fold g1 in IHn1; apply IHn1. apply cPairLe2A. repeat rewrite cPairProjections2. eapply Nat.le_lt_trans; [ idtac | apply cPairLt2 ]. apply cPairLe2; simpl; apply Compat815.le_lt_n_Sm. * specialize (cPairLe2A n1); lia. } apply H1, le_n. Qed.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815) hydras.Ackermann(PA codeSubFormula)