diff --git a/doc/chapter-primrec.tex b/doc/chapter-primrec.tex index d7edab24..a075a64b 100644 --- a/doc/chapter-primrec.tex +++ b/doc/chapter-primrec.tex @@ -879,15 +879,18 @@ \subsection{Looking for a contradiction} Thus, our impossibility proof is just a sequence of easy small steps. \begin{remark} -In the following snippet, \emph{Alectryon}'s \texttt{Latex} generator prints the \emph{local definition} of $x$ (as the maximum of $2$ and $m$) as a simple \emph{declaration} \texttt{x: nat}. +In the following snippet, some versions \emph{Alectryon}'s \texttt{Latex} generator print the \emph{local definition} of $x$ (as the maximum of $2$ and $m$) as a simple \emph{declaration} \texttt{x: nat}. Thus the proof script is correct, but the three last sub-goals are not correctly displayed, since they do not show how the inequalities $2\leq x$ and $m \leq x$ could be inferred by \texttt{lia}. + +A correct goal display can be obtained with +\href{https://github.com/Casteran/alectryonFix}{this fork}. \end{remark} \input{movies/snippets/AckNotPR/AckNotPR} \begin{remark} -It is easy to prove that any unary function which dominates \texttt{fun n => Ack n n} fails to be primitive recursive. To this end, we use an instance of \texttt{majorAnyPR} dealing with unary functions. +It is easy to prove that any unary function which dominates (\texttt{fun n => Ack n n}) fails to be primitive recursive. To this end, we use an instance of \texttt{majorAnyPR} dealing with unary functions. \vspace{4pt} \noindent diff --git a/theories/ordinals/Schutte/CNF.v b/theories/ordinals/Schutte/CNF.v index c8ec79a9..272dadc7 100644 --- a/theories/ordinals/Schutte/CNF.v +++ b/theories/ordinals/Schutte/CNF.v @@ -10,7 +10,6 @@ From hydras Require Export Schutte_basics Ordering_Functions PartialFun Countable Schutte.Addition AP. From Coq Require Export Classical. - Set Implicit Arguments. (** A Cantor normal form for a countable ordinal [alpha] is just a sorted @@ -22,33 +21,29 @@ are less _or equal_ than [alpha]. For instance, the Cantor Normal Form of [epsilon0] is just [epsilon0 :: nil]. -*) + *) (* begin snippet Defs *) - Definition cnf_t := list Ord. Fixpoint eval (l : cnf_t) : Ord := - match l with nil => zero - | beta :: l' => phi0 beta + eval l' + match l with + | nil => zero + | beta :: l' => phi0 beta + eval l' end. Definition sorted (l: cnf_t) := LocallySorted (fun alpha beta => beta <= alpha) l. - Definition is_cnf_of (alpha : Ord)(l : cnf_t) : Prop := sorted l /\ alpha = eval l. - (* end snippet Defs *) - Definition exponents_lt (alpha: Ord) := - Forall (fun beta => beta < alpha). + Forall (fun beta => beta < alpha). Definition exponents_le (alpha : Ord) := - Forall (fun beta => beta <= alpha). - + Forall (fun beta => beta <= alpha). (* begin hide *) @@ -57,58 +52,55 @@ Definition exponents_le (alpha : Ord) := (* end hide *) -Lemma exponents_lt_eval alpha l: exponents_lt alpha l -> - eval l < phi0 alpha. +Lemma exponents_lt_eval alpha l: exponents_lt alpha l -> + eval l < phi0 alpha. Proof. - induction 1; cbn. - - apply phi0_positive. - - apply AP_plus_closed; trivial. - + apply AP_phi0; auto. - + apply phi0_mono;auto. + induction 1; cbn. + - apply phi0_positive. + - apply AP_plus_closed; trivial. + + apply AP_phi0; auto. + + apply phi0_mono;auto. Qed. -Lemma sorted_tail alpha l: - sorted (cons alpha l) -> sorted l. +Lemma sorted_tail alpha l: sorted (cons alpha l) -> sorted l. Proof. inversion 1; auto with schutte. Qed. -Lemma nf_bounded : forall beta l alpha, - alpha <= phi0 beta -> - is_cnf_of alpha l -> exponents_le beta l. +Lemma nf_bounded beta l alpha : + alpha <= phi0 beta -> is_cnf_of alpha l -> + exponents_le beta l. Proof. - intros beta l ; elim l. - - constructor. - - intros a l0 H alpha H0 H1; right. - + case H1;intros H3; simpl in H3. - intro ; subst alpha; apply phi0_mono_R_weak. - apply le_trans with (phi0 a + eval l0);auto. - apply le_plus_l. - + apply H with (eval l0). - * case H1; intros H2 H3; simpl in H3. - apply le_trans with alpha. - -- subst alpha; apply le_plus_r. - -- auto with schutte. - * split; [ | trivial]. - case H1; inversion 1; auto with schutte. + revert alpha; elim l. + - constructor. + - intros a l0 H alpha H0 H1; right. + + case H1;intros H3; simpl in H3. + intro ; subst alpha; apply phi0_mono_R_weak. + apply le_trans with (phi0 a + eval l0);auto. + apply le_plus_l. + + apply H with (eval l0). + * case H1; intros H2 H3; simpl in H3. + apply le_trans with alpha. + -- subst alpha; apply le_plus_r. + -- auto with schutte. + * split; [ | trivial]. + case H1; inversion 1; auto with schutte. Qed. - - Lemma cnf_of_ap (alpha : Ord) : - In AP alpha -> exists l, is_cnf_of alpha l. + In AP alpha -> exists l, is_cnf_of alpha l. Proof. - intros H; case phi0_ordering. - intros H0 H1 H2 H3; destruct (H2 alpha H) as [x [Hx Ex]]. - subst alpha; exists (cons x nil); split. - - constructor. - - simpl; now rewrite alpha_plus_zero. + intros H; case phi0_ordering. + intros H0 H1 H2 H3; destruct (H2 alpha H) as [x [Hx Ex]]. + subst alpha; exists (cons x nil); split. + - constructor. + - simpl; now rewrite alpha_plus_zero. Qed. Lemma sorted_lt_lt (beta: Ord) : forall l alpha, - sorted (cons alpha l) -> alpha < beta -> - eval (cons alpha l) < phi0 beta. - Proof. + sorted (cons alpha l) -> alpha < beta -> + eval (cons alpha l) < phi0 beta. +Proof. induction l. - simpl; inversion_clear 1. intro H;apply AP_plus_closed. @@ -125,30 +117,30 @@ Lemma sorted_lt_lt (beta: Ord) : forall l alpha, Qed. - Lemma sorted_lt_lt_2 l alpha : - sorted (cons alpha l) -> - eval (cons alpha l) < phi0 (succ alpha). +Lemma sorted_lt_lt_2 l alpha : + sorted (cons alpha l) -> + eval (cons alpha l) < phi0 (succ alpha). Proof. - intros;apply (sorted_lt_lt H). - inversion H;intros;eauto with schutte. + intros;apply (sorted_lt_lt H). + inversion H;intros;eauto with schutte. Qed. Lemma cnf_head_eq alpha beta ol ol': - sorted (cons alpha ol) -> - sorted (cons beta ol') -> - eval (cons alpha ol) = eval (cons beta ol') -> - alpha = beta. + sorted (cons alpha ol) -> + sorted (cons beta ol') -> + eval (cons alpha ol) = eval (cons beta ol') -> + alpha = beta. Proof. - intros H H0 H1; tricho alpha beta H2; [ | trivial | ]. - - generalize (sorted_lt_lt H H2) ; intro H3. - case (@lt_irrefl (eval (cons alpha ol))). - apply lt_le_trans with (phi0 beta); [trivial | ]. - + rewrite H1; simpl ; apply le_plus_l. - - generalize (sorted_lt_lt H0 H2); intro H3. - case (@lt_irrefl (eval (cons beta ol'))). - apply lt_le_trans with (phi0 alpha); [trivial | ]. - + rewrite <- H1; simpl; apply le_plus_l. + intros H H0 H1; tricho alpha beta H2; [ | trivial | ]. + - generalize (sorted_lt_lt H H2) ; intro H3. + case (@lt_irrefl (eval (cons alpha ol))). + apply lt_le_trans with (phi0 beta); [trivial | ]. + + rewrite H1; simpl ; apply le_plus_l. + - generalize (sorted_lt_lt H0 H2); intro H3. + case (@lt_irrefl (eval (cons beta ol'))). + apply lt_le_trans with (phi0 alpha); [trivial | ]. + + rewrite <- H1; simpl; apply le_plus_l. Qed. Lemma cnf_eq alpha beta ol ol': @@ -157,67 +149,67 @@ Lemma cnf_eq alpha beta ol ol': eval (cons alpha ol) = eval (cons beta ol') -> alpha = beta /\ eval ol = eval ol'. Proof. - intros H H0 H1; generalize (cnf_head_eq H H0 H1). - intro; subst beta; split;[trivial | ]. - simpl in H1; now eapply plus_reg_r with (phi0 alpha). + intros H H0 H1; generalize (cnf_head_eq H H0 H1). + intro; subst beta; split;[trivial | ]. + simpl in H1; now eapply plus_reg_r with (phi0 alpha). Qed. Lemma cnf_plus1 (ol : cnf_t) : - sorted ol -> forall alpha, + sorted ol -> forall alpha, exists ol', is_cnf_of (phi0 alpha + eval ol) ol'. Proof. - induction ol. - - inversion_clear 1 . - intros alpha; simpl; exists (cons alpha nil). - split. - + constructor. - + split ; simpl. - - intros H alpha; simpl; tricho alpha a H1. - + exists (cons a ol); split. - * auto. - * rewrite plus_assoc, phi0_alpha_phi0_beta; [simpl|]; auto. - + subst a; exists (cons alpha (cons alpha ol)); split. - * constructor; eauto with schutte. - * simpl; auto. - + exists (cons alpha (cons a ol)); split. - * constructor;auto with schutte. - * now simpl. + induction ol. + - inversion_clear 1 . + intros alpha; simpl; exists (cons alpha nil). + split. + + constructor. + + split ; simpl. + - intros H alpha; simpl; tricho alpha a H1. + + exists (cons a ol); split. + * auto. + * rewrite plus_assoc, phi0_alpha_phi0_beta; [simpl|]; auto. + + subst a; exists (cons alpha (cons alpha ol)); split. + * constructor; eauto with schutte. + * simpl; auto. + + exists (cons alpha (cons a ol)); split. + * constructor;auto with schutte. + * now simpl. Qed. Lemma cnf_plus2 : forall ol, sorted ol -> - forall ol', sorted ol' -> - exists ol'', is_cnf_of (eval ol + eval ol') ol''. + forall ol', sorted ol' -> + exists ol'', is_cnf_of (eval ol + eval ol') ol''. Proof. - induction ol. - - simpl; intros; rewrite zero_plus_alpha;auto. - exists ol';split;auto. - - intros; simpl; assert (sorted ol). - { inversion H;auto with schutte. } - destruct (IHol H1 _ H0) as [x [H3 H4]]. - destruct (@cnf_plus1 _ H3 a) as [x0 H5]. - exists x0; rewrite <- H4 in H5; now rewrite <- plus_assoc. + induction ol. + - simpl; intros; rewrite zero_plus_alpha;auto. + exists ol';split;auto. + - intros; simpl; assert (sorted ol). + { inversion H;auto with schutte. } + destruct (IHol H1 _ H0) as [x [H3 H4]]. + destruct (@cnf_plus1 _ H3 a) as [x0 H5]. + exists x0; rewrite <- H4 in H5; now rewrite <- plus_assoc. Qed. Lemma cnf_plus : forall ol alpha, - is_cnf_of alpha ol -> forall ol' beta, is_cnf_of beta ol' -> - exists ol'', is_cnf_of (alpha + beta) ol''. + is_cnf_of alpha ol -> forall ol' beta, is_cnf_of beta ol' -> + exists ol'', is_cnf_of (alpha + beta) ol''. Proof. - destruct 1 as [H H0]. - destruct 1 as [H1 H2]. - rewrite H0;rewrite H2; apply cnf_plus2;auto. + destruct 1 as [H H0]. + destruct 1 as [H1 H2]. + rewrite H0;rewrite H2; apply cnf_plus2;auto. Qed. (* begin hide *) Lemma not_AP_inv_0 : forall alpha, - zero < alpha -> - ~ (AP alpha) -> - exists beta,zero < beta /\ - beta < alpha /\ - alpha < beta + alpha . + zero < alpha -> + ~ (AP alpha) -> + exists beta,zero < beta /\ + beta < alpha /\ + alpha < beta + alpha . Proof with eauto with schutte. intros alpha H H0; apply Classical_Prop.NNPP. intro H1;apply H0; split ... @@ -233,9 +225,9 @@ Proof with eauto with schutte. Qed. Lemma not_AP_inv2 : forall alpha, zero < alpha -> ~AP alpha -> - exists beta, exists gamma, - zero < beta /\ zero < gamma /\ - beta < alpha /\ gamma < alpha /\ + exists beta, exists gamma, + zero < beta /\ zero < gamma /\ + beta < alpha /\ gamma < alpha /\ alpha = beta + gamma. Proof with eauto with schutte. intros alpha H H0; case (not_AP_inv_0 H H0). @@ -274,32 +266,32 @@ Theorem cnf_exists (alpha : Ord) : exists l: cnf_t, is_cnf_of alpha l. (* .no-out *) (*| .. coq:: none |*) Proof. - case (le_eq_or_lt (zero_le alpha)). - - exists nil; split. - + constructor. - + simpl;auto. - - pattern alpha; apply transfinite_induction;auto. - intros a H0 H1; case (classic (AP a)). - + intros H2; apply cnf_of_ap; auto. - + intros H2; case (not_AP_inv2 H1 H2). - intros x H3; destruct H3 as [z [H4' [H5' H6]]]. - case (H0 x). - * case H6;auto. - * auto. - * intros x0 H; case (H0 z). - -- tauto. - -- auto. - -- intros x1 H4; decompose [and] H6; subst a. - destruct (cnf_plus H H4) as [x2 Hx2]; exists x2; auto. + case (le_eq_or_lt (zero_le alpha)). + - exists nil; split. + + constructor. + + simpl;auto. + - pattern alpha; apply transfinite_induction;auto. + intros a H0 H1; case (classic (AP a)). + + intros H2; apply cnf_of_ap; auto. + + intros H2; case (not_AP_inv2 H1 H2). + intros x H3; destruct H3 as [z [H4' [H5' H6]]]. + case (H0 x). + * case H6;auto. + * auto. + * intros x0 H; case (H0 z). + -- tauto. + -- auto. + -- intros x1 H4; decompose [and] H6; subst a. + destruct (cnf_plus H H4) as [x2 Hx2]; exists x2; auto. Qed. (*||*) (* end snippet cnfExists *) -Lemma sorted_lt : forall l alpha, sorted (cons alpha l) -> - eval l < phi0 alpha + eval l. +Lemma sorted_lt l alpha: sorted (alpha::l) -> + eval l < phi0 alpha + eval l. Proof. - induction l. - - inversion 1; simpl; rewrite alpha_plus_zero; apply phi0_positive;auto. + revert alpha; induction l. + - inversion 1; simpl; rewrite alpha_plus_zero; apply phi0_positive;auto. - inversion 1; simpl; rewrite plus_assoc. generalize (IHl _ H2); intro H5. apply le_lt_trans with (phi0 alpha + eval l). @@ -314,28 +306,28 @@ Qed. (Proof by induction on lists) -*) + *) (* begin snippet cnfUnicity *) -Lemma cnf_unicity : forall l alpha, - is_cnf_of alpha l -> - forall l', is_cnf_of alpha l' -> - l=l'. (* .no-out *) +Lemma cnf_unicity l alpha: + is_cnf_of alpha l -> + forall l', is_cnf_of alpha l' -> + l = l'. (* .no-out *) (*| .. coq:: none |*) Proof. - induction l. - - destruct 1 as [H H0]. - simpl in H0; subst alpha; destruct l'. - + auto. - + destruct 1 as [H0 H1]; simpl in H1; case (@lt_irrefl zero). - pattern zero at 2;rewrite H1. - apply lt_le_trans with (phi0 o);auto with schutte. - apply phi0_positive. - apply le_plus_l;auto. - - destruct l' as [ | o l']. - + intro; case H;case H0;intros H1 H2 H3 H4. - simpl in H2, H4 ; rewrite H2 in H4. + revert alpha; induction l. + - destruct 1 as [H H0]. + simpl in H0; subst alpha; destruct l'. + + auto. + + destruct 1 as [H0 H1]; simpl in H1; case (@lt_irrefl zero). + pattern zero at 2;rewrite H1. + apply lt_le_trans with (phi0 o);auto with schutte. + apply phi0_positive. + apply le_plus_l;auto. + - destruct l' as [ | o l']. + + intro; case H;case H0;intros H1 H2 H3 H4. + simpl in H2, H4 ; rewrite H2 in H4. assert (ordinal a) by split. case (@lt_irrefl zero). pattern zero at 2; rewrite H4. @@ -363,8 +355,8 @@ Qed. Theorem cnf_exists_unique (alpha:Ord) : exists! l: cnf_t, is_cnf_of alpha l. Proof. - destruct (cnf_exists alpha) as [l Hl]; exists l; split; auto. - now apply cnf_unicity. + destruct (cnf_exists alpha) as [l Hl]; exists l; split; auto. + now apply cnf_unicity. Qed. (*||*) (* end snippet cnfExUnique *) @@ -388,7 +380,7 @@ Proof. assert (Hlt : a < phi0 a). { apply lt_phi0; simpl in e; subst alpha; - apply le_lt_trans with (phi0 a); auto with schutte. + apply le_lt_trans with (phi0 a); auto with schutte. - apply le_phi0. - apply le_lt_trans with (2 := H0); apply le_plus_l. } @@ -397,12 +389,12 @@ Proof. + apply le_plus_l. + specialize (IHl (eval l)); unfold is_cnf_of in IHl. apply Forall_impl with (fun o => o < eval l). - * intros a0 H1; apply lt_le_trans with (1 := H1). - subst alpha; apply le_plus_r. - * apply IHl . - { split; auto ; eapply sorted_tail; eauto. } - apply le_lt_trans with (2 := H0). - subst alpha; apply (le_plus_r). + * intros a0 H1; apply lt_le_trans with (1 := H1). + subst alpha; apply le_plus_r. + * apply IHl . + { split; auto ; eapply sorted_tail; eauto. } + apply le_lt_trans with (2 := H0). + subst alpha; apply (le_plus_r). Qed. (*||*) diff --git a/theories/ordinals/Schutte/Critical.v b/theories/ordinals/Schutte/Critical.v index ba1000a5..3a81da8c 100644 --- a/theories/ordinals/Schutte/Critical.v +++ b/theories/ordinals/Schutte/Critical.v @@ -28,9 +28,8 @@ Definition Cr_fun : forall alpha : Ord, (forall beta : Ord, beta < alpha -> Ensemble Ord) -> Ensemble Ord := - fun (alpha :Ord) - (Cr : forall beta, - beta < alpha -> Ensemble Ord) + fun (alpha: Ord) + (Cr : forall beta, beta < alpha -> Ensemble Ord) (x : Ord) => ( (alpha = zero /\ AP x) \/ (zero < alpha /\ @@ -61,11 +60,9 @@ Definition Gamma0 := the_least strongly_critical. (* begin snippet phiDef *) -Definition phi (alpha : Ord) : Ord -> Ord - := ord (Cr alpha). +Definition phi (alpha : Ord) : Ord -> Ord := ord (Cr alpha). -Definition A_ (alpha : Ord) : Ensemble Ord := - the_ordering_segment (Cr alpha). +Definition A_ (alpha : Ord) : Ensemble Ord := the_ordering_segment (Cr alpha). (* end snippet phiDef *) @@ -212,7 +209,7 @@ Proof. intro alpha;unfold phi, finite; now rewrite Cr_zero_AP. Qed. -Lemma Cr_1_equiv (alpha : Ord): +Lemma Cr_1_iff (alpha : Ord): Cr 1 alpha <-> AP alpha /\ phi0 alpha = alpha. Proof. generalize (Cr_pos_inv (alpha := F 1)). @@ -256,7 +253,7 @@ Qed. Lemma epsilon0_Cr1 : In (Cr 1) epsilon0. (* .no-out *) (*| .. coq:: none |*) Proof. - red;rewrite Cr_1_equiv; split. + red;rewrite Cr_1_iff; split. - apply epsilon0_AP. - apply epsilon0_fxp. Qed.