proposition: Remark wellFormedTermTermsCorrect2 : forall n : nat, (wellFormedTerm n <> 0 -> exists t : Term, codeTerm t = n) /\ (wellFormedTerms n <> 0 -> exists m : nat, (exists ts : Terms m, codeTerms ts = n)).
proof: Proof. assert (H: forall m n : nat, n < m -> (wellFormedTerm n <> 0 -> exists t : Term, codeTerm t = n) /\ (wellFormedTerms n <> 0 -> exists m : nat, (exists ts : Terms m, codeTerms ts = n))). { intro m; induction m as [| m Hrecm]. - intros n H; inversion H. - intros n H; assert (H': n <= m) by lia. rewrite Nat.lt_eq_cases in H'; destruct H' as [H0 | H0]. + apply Hrecm; auto. + unfold wellFormedTerm, wellFormedTerms, wellFormedTermTerms. set (A := fun t recs : nat => cPair (switchPR (cPairPi1 t) (charFunction 2 Nat.eqb (codeArityF (pred (cPairPi1 t))) (S (codeLength (cPairPi2 t))) * cPairPi2 (codeNth (t - S (cPairPi2 t)) recs)) 1) (switchPR t (cPairPi1 (codeNth (t - S (cPairPi1 (pred t))) recs) * cPairPi2 (codeNth (t - S (cPairPi2 (pred t))) recs)) 1)). unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList; rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList; simpl; rewrite cPairProjections1. split. * unfold A at 1; rewrite cPairProjections1. assert (H1: cPair (cPairPi1 n) (cPairPi2 n) = n) by apply cPairProjections. destruct (cPairPi1 n); simpl. -- exists (var (cPairPi2 n)). transitivity (cPair 0 (cPairPi2 n)). ++ reflexivity. ++ assumption. -- rewrite evalStrongRecHelp1. ++ simpl; intros H2. induction (eq_nat_dec (codeArityF n0) (S (codeLength (cPairPi2 n)))) as [a | b]. ** assert (H3: wellFormedTerms (cPairPi2 n) <> 0) by eapply multLemma2, H2. assert (H4: cPairPi2 n < m). { apply Nat.lt_le_trans with (cPair (S n0) (cPairPi2 n)). - apply cPairLt2. - rewrite H1, H0; apply le_n. } induction (Hrecm _ H4) as [_ H6]. induction (H6 H3) as [x [x0 H5]]. assert (H7: codeArityF n0 <> 0). { intro H7; rewrite H7 in a; discriminate a. } induction (codeArityFIsCorrect2 _ H7) as [x1 H8]. rewrite <- H8 in a. rewrite codeArityFIsCorrect1 in a. injection a; clear a. intro H9; rewrite <- H5 in H9. rewrite lengthTerms in H9. cut (codeTerms x0 = cPairPi2 n). --- clear H5; generalize x0; clear x0. rewrite <- H9. intros x0 H5. exists (apply x1 x0). transitivity (cPair (S n0) (cPairPi2 n)). +++ rewrite <- H8. now rewrite <- H5. +++ assumption. --- assumption. ** rewrite nat_eqb_false in H2. --- elim H2; reflexivity. --- assumption. ++ apply Nat.lt_le_trans with (cPair (S n0) (cPairPi2 n)). ** apply cPairLt2. ** rewrite H1; apply le_n. * unfold A at 1; rewrite cPairProjections2; destruct n. -- simpl; intros H1; exists 0. exists (Tnil); easy. -- repeat rewrite evalStrongRecHelp1. ++ simpl; intros H1; assert (H2: cPairPi1 n < m). { rewrite <- H0; apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (cPairPi1 n) (cPairPi2 n)). - apply cPairLe1. - rewrite cPairProjections. apply le_n. } assert (H3: cPairPi2 n < m). { rewrite <- H0. apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (cPairPi1 n) (cPairPi2 n)). - apply cPairLe2. - rewrite cPairProjections; apply le_n. } induction (Hrecm _ H2) as [H4 H5]. induction (Hrecm _ H3) as [_ H6]. assert (H7: wellFormedTerm (cPairPi1 n) <> 0) by eapply multLemma1, H1. assert (H8: wellFormedTerms (cPairPi2 n) <> 0) by eapply multLemma2, H1. induction (H4 H7) as [x H9]. induction (H6 H8) as [x0 H10]. induction H10 as (x1, H10). exists (S x0), (Tcons x x1). rewrite <- (cPairProjections n). now rewrite <- H9, <- H10. ++ simpl; apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (cPairPi1 n) (cPairPi2 n)). ** apply cPairLe2. ** rewrite cPairProjections; apply le_n. ++ apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (cPairPi1 n) (cPairPi2 n)). ** apply cPairLe1. ** rewrite cPairProjections; apply le_n. } intros n; eapply H; apply Nat.lt_succ_diag_r . Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)