proposition: Lemma wellFormedFormulaCorrect2 : forall n : nat, wellFormedFormula n <> 0 -> exists f : Formula, codeFormula f = n.
proof: Proof. assert (H: forall m n : nat, n < m -> wellFormedFormula n <> 0 -> exists f : Formula, codeFormula f = n). { intro m; induction m as [| m Hrecm]. - intros n H; lia. - intros n H; assert (H': n <= m) by lia. rewrite Nat.lt_eq_cases in H'; destruct H'. + apply Hrecm; auto. + unfold wellFormedFormula; set (A := fun f recs : nat => switchPR (cPairPi1 f) (switchPR (pred (cPairPi1 f)) (switchPR (pred (pred (cPairPi1 f))) (switchPR (pred (pred (pred (cPairPi1 f)))) (charFunction 2 Nat.eqb (codeArityR (pred (pred (pred (pred (cPairPi1 f)))))) (S (codeLength (cPairPi2 f))) * wellFormedTerms (cPairPi2 f)) (codeNth (f - S (cPairPi2 (cPairPi2 f))) recs)) (codeNth (f - S (cPairPi2 f)) recs)) (codeNth (f - S (cPairPi1 (cPairPi2 f))) recs * codeNth (f - S (cPairPi2 (cPairPi2 f))) recs)) (wellFormedTerm (cPairPi1 (cPairPi2 f)) * wellFormedTerm (cPairPi2 (cPairPi2 f)))). unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList; rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl. rewrite cPairProjections1; unfold A at 1. assert (H1: cPair (cPairPi1 n) (cPairPi2 n) = n) by apply cPairProjections. destruct (cPairPi1 n); simpl in |- *. intros H2; assert (H3: wellFormedTerm (cPairPi1 (cPairPi2 n)) <> 0). { eapply multLemma1; apply H2. } assert (H4: wellFormedTerm (cPairPi2 (cPairPi2 n)) <> 0) by eapply multLemma2, H2. induction (wellFormedTermCorrect2 _ H3) as [x H5]. induction (wellFormedTermCorrect2 _ H4) as [x0 H6]. exists (equal x x0). simpl; rewrite H5, H6, cPairProjections. assumption. destruct n0. * simpl; assert (H2: cPairPi2 n < m). { apply Nat.lt_le_trans with (cPair 1 (cPairPi2 n)). - apply cPairLt2. - rewrite H1, H0; apply le_n. } assert (H3: cPairPi1 (cPairPi2 n) < m). { apply Nat.le_lt_trans with (cPair (cPairPi1 (cPairPi2 n)) (cPairPi2 (cPairPi2 n))). - apply cPairLe1. - now rewrite cPairProjections. } assert (H4: cPairPi2 (cPairPi2 n) < m). { apply Nat.le_lt_trans with (cPair (cPairPi1 (cPairPi2 n)) (cPairPi2 (cPairPi2 n))). - apply cPairLe2. - now rewrite cPairProjections. } -- repeat rewrite evalStrongRecHelp1. ++ intros H5; assert (H6: evalStrongRec 0 A (cPairPi1 (cPairPi2 n)) <> 0). { eapply multLemma1. apply H5. } assert (H7: evalStrongRec 0 A (cPairPi2 (cPairPi2 n)) <> 0) by eapply multLemma2, H5. induction (Hrecm _ H3 H6) as [x H8]. induction (Hrecm _ H4 H7) as [x0 H9]. exists (impH x x0); simpl; rewrite H8, H9. now rewrite cPairProjections. ++ eapply Nat.lt_le_trans. ** apply H4. ** rewrite H0. apply le_n. ++ eapply Nat.lt_le_trans. ** apply H3. ** rewrite H0. apply le_n. * destruct n0. -- simpl; assert (H2: cPairPi2 n < m). { apply Nat.lt_le_trans with (cPair 2 (cPairPi2 n)). apply cPairLt2. rewrite H1. rewrite H0. apply le_n. } repeat rewrite evalStrongRecHelp1. ++ intros H3; induction (Hrecm _ H2 H3). exists (notH x); simpl; now rewrite H4. ++ eapply Nat.lt_le_trans. ** apply H2. ** rewrite H0; apply le_n. -- destruct n0. ++ simpl; assert (H2: cPairPi2 n < m). { apply Nat.lt_le_trans with (cPair 3 (cPairPi2 n)). - apply cPairLt2. - rewrite H1, H0; apply le_n. } assert (H3: cPairPi2 (cPairPi2 n) < m). { apply Nat.le_lt_trans with (cPair (cPairPi1 (cPairPi2 n)) (cPairPi2 (cPairPi2 n))). - apply cPairLe2. - now rewrite cPairProjections. } repeat rewrite evalStrongRecHelp1. ** intros H4; induction (Hrecm _ H3 H4) as [x H5]. exists (forallH (cPairPi1 (cPairPi2 n)) x). simpl; now rewrite H5, cPairProjections. ** eapply Nat.lt_le_trans. --- apply H3. --- rewrite H0; apply le_n. ++ simpl; induction (eq_nat_dec (codeArityR n0) (S (codeLength (cPairPi2 n)))) as [a | ?]. ** assert (H2: codeArityR n0 <> 0). { intro H2; rewrite H2 in a; discriminate a. } induction (codeArityRIsCorrect2 _ H2) as [x H3]. intros H4; assert (H5: wellFormedTerms (cPairPi2 n) <> 0) by eapply multLemma2, H4. rewrite <- H3 in a. rewrite codeArityRIsCorrect1 in a. injection a. clear a. intros H6; induction (wellFormedTermsCorrect2 _ H5) as [x0 [x1 H7]]. rewrite <- H7 in H6. rewrite lengthTerms in H6. cut (codeTerms x1 = cPairPi2 n). --- generalize x1; clear H7 x1. rewrite <- H6. intros x1 H7; exists (atomic x x1). simpl;rewrite H7; unfold codeR; rewrite H3; assumption. --- assumption. ** rewrite nat_eqb_false. intros H2; simpl in H2; elim H2. reflexivity. assumption. } intros n H0; eapply H. apply Nat.lt_succ_diag_r. assumption. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)