From 11b82b14d98573e72c6f14ee4c110e21920b9ceb Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Fri, 26 Jan 2024 11:36:04 +0100 Subject: [PATCH 1/7] minor change --- theories/ordinals/Epsilon0/Canon.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v index 67f933d0..68cbb8ae 100644 --- a/theories/ordinals/Epsilon0/Canon.v +++ b/theories/ordinals/Epsilon0/Canon.v @@ -1046,9 +1046,9 @@ Lemma CanonSSn (i:nat) : CanonS (Cons alpha (S n) E0zero) i = Cons alpha n (CanonS (E0_phi0 alpha) i). Proof. - intros; apply E0_eq_intro; - unfold CanonS;repeat (rewrite cnf_rw || rewrite cnf_Cons); auto. - - unfold canonS; rewrite canon_SSn_zero; auto with E0. + intros; apply E0_eq_intro. + unfold Canon; repeat (rewrite cnf_rw || rewrite cnf_Cons); auto. + - rewrite canon_SSn_zero; auto with E0. - unfold lt, E0_phi0; repeat rewrite cnf_rw. apply canonS_LT ; trivial. apply nf_phi0;auto with E0. From 37876eea5ed1432c968b7a4676a3eff7bd8a254c Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Mon, 29 Jan 2024 14:48:33 +0100 Subject: [PATCH 2/7] small changes in doc --- doc/Gamma0-chapter.tex | 2 +- doc/epsilon0-chapter.tex | 33 +++++++++++++++++---------------- doc/gaia-chapter.tex | 18 ++++++++---------- doc/hydras.tex | 14 +++++++------- doc/schutte-chapter.tex | 2 ++ theories/ordinals/Epsilon0/T1.v | 2 +- 6 files changed, 36 insertions(+), 35 deletions(-) diff --git a/doc/Gamma0-chapter.tex b/doc/Gamma0-chapter.tex index 24871163..a9ecdb50 100644 --- a/doc/Gamma0-chapter.tex +++ b/doc/Gamma0-chapter.tex @@ -1,5 +1,5 @@ \chapter{The Ordinal \texorpdfstring{$\Gamma_0$}{Gamma0} (first draft)} - +\label{chap:gamma0} \emph{This chapter and the files it presents are still very incomplete, considering the impressive properties of $\Gamma_0$~\cite{Gallier91}. We hope to add new material soon, and accept contributions!} diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex index a7fd3cdf..6b246ebb 100644 --- a/doc/epsilon0-chapter.tex +++ b/doc/epsilon0-chapter.tex @@ -5,8 +5,8 @@ \label{cnf-math-def} \label{chap:T1} -In this chapter, we adapt to \coq{} the well-known~\cite{KP82} proof that Hercules eventually wins every battle, whichever the strategy of each player. -In other words, we present a formal and self contained proof of termination of all [free] hydra battles. +In this chapter, we adapt to \coq{} the well-known proof~\cite{KP82} that Hercules eventually wins every battle, whichever the strategy of each player. +In other words, we present a formal and self-contained proof of termination of all [free] hydra battles. First, we take from Manolios and Vroon~\cite{Manolios2005} a representation of the ordinal $\epsilon_0$ as terms in Cantor normal form. Then, we define a variant for hydra battles as a measure that maps any hydra to some ordinal strictly less than $\epsilon_0$. @@ -16,7 +16,7 @@ \section{The ordinal \texorpdfstring{\(\epsilon_0\)}{epsilon0}} The ordinal \(\epsilon_0\) is the least ordinal number that satisfies the equation \(\alpha = \omega^\alpha\), where \(\omega\) is -the least infinite ordinal. +the least infinite ordinal\footnote{For a precise ---\,\emph{i.e.} mathematical\,--- definition of $\omega^\alpha$, please see Sect.~\vref{sect:AP-and-phi0}.} . Thus, we can intuitively consider \(\epsilon_0\) as an \emph{infinite} \(\omega\)-tower. @@ -28,10 +28,10 @@ \subsection{Cantor normal form} Any ordinal strictly less that \(\epsilon_0\) can be finitely represented by a unique \emph{Cantor normal form}, -that is, an expression which is either the ordinal \(0\) or +that is, an expression which is a sum \(\omega^{\alpha_1} \times n_1 + \omega^{\alpha_2} \times n_2 + - \dots + \omega^{\alpha_p} \times n_p\) where all the \(\alpha_i\) -are ordinals in Cantor normal form, \(\alpha_1 > \alpha_2 > \alpha_p\), + \dots + \omega^{\alpha_p} \times n_p\) where $p\in\mathbb{N}$, all the \(\alpha_i\) +are ordinals in Cantor normal form, \(\alpha_1 > \alpha_2 > \alpha_p\) and all the \(n_i\) are positive integers. An example of Cantor normal form is displayed in Fig \ref{fig:cnf-example}: @@ -55,8 +55,7 @@ \subsection{Cantor normal form} to this type, and finally prove that our representation fits well with the expected mathematical properties: the order we define is a well order, and the decomposition into Cantor normal form is consistent -with the implementation of the arithmetic operations of exponentiation of base \(\omega\) -and addition. +with usual definition of ordinals, for instance in \gaia~\cite{Gaia}, Schütte's book~\cite{schutte}, or larger ordinal notations~\vref{chap:gamma0}. \paragraph*{Remark} \label{sec:orgheadline65} @@ -131,7 +130,7 @@ \subsubsection{Example} \paragraph{Remark} For simplicity's sake, we chose to forbid expressions of the form $\omega^\alpha\times 0 + \beta$. Thus, the construction (\texttt{cons $\alpha$ $n$ $\beta$}) is intended to represent the ordinal $\omega^\alpha\times(n+1)+\beta$ and not $\omega^\alpha\times n+\beta$. -In a future version, we should replace the type \texttt{nat} with \texttt{positive} in \texttt{T1}'s +In a future version, we would like to replace the type \texttt{nat} with standard library's type \texttt{positive} in \texttt{T1}'s definition. But this replacement would take a lot of time \dots{} @@ -210,11 +209,11 @@ \subsubsection{The ordinal \(\omega\)} \input{movies/snippets/T1/omegaDef} -Note that \texttt{omega} is not an identifier in \HydrasLib, thus any tactic like \texttt{unfold omega} would fail. +Note that \texttt{T1omega} is not an identifier in \HydrasLib, thus any tactic like \texttt{unfold T1omega} would fail. \index{gaiabridge}{The ordinal $\omega$} \paragraph*{\gaiasign} -In \texttt{gaia.ssete9}, the ordinal $\omega$ is bound to the \emph{constant} \texttt{T1omega}. +In \texttt{gaia.ssete9}, the ordinal $\omega$ is bound to the \emph{constant} \texttt{T1omega} (not a notation). @@ -292,7 +291,7 @@ \subsection{Pretty-printing ordinals in Cantor normal form} \index{hydras}{Projects} \begin{project} -Design (in \ocaml?) a set of tools for systematically pretty printing ordinal terms in Cantor normal form. +Design tools for systematically pretty printing ordinal terms in Cantor normal form. \end{project} @@ -315,6 +314,8 @@ \subsection{Comparison between ordinal terms} \input{movies/snippets/T1/compareDef} +\input{movies/snippets/T1/Instances} + \label{Predicates:lt-T1} Please note that this definition of \texttt{lt} makes it easy to write proofs by computation, as shown by the following examples. @@ -325,11 +326,11 @@ \subsection{Comparison between ordinal terms} \input{movies/snippets/T1/ltExamples} -Links between the function \texttt{compare} and the relations -\texttt{lt} and \texttt{eq} are established through the following lemmas (~\vref{sect:comparable-def}). -\vspace{4pt} +% Links between the function \texttt{compare} and the relations +% \texttt{lt} and \texttt{eq} are established through the following lemmas (~\vref{sect:comparable-def}). +% \vspace{4pt} + -\input{movies/snippets/T1/Instances} \paragraph*{\gaiasign} \index{gaiabridge}{Strict order on ordinals below $\epsilon_0$} diff --git a/doc/gaia-chapter.tex b/doc/gaia-chapter.tex index 05574beb..2cd4aa28 100644 --- a/doc/gaia-chapter.tex +++ b/doc/gaia-chapter.tex @@ -121,21 +121,19 @@ \subsubsection{Refinements: Definitions} Functions \texttt{h2g} and \texttt{g2h} allow us to define -a notion of ``data-refinement'' for constants, functions, predicates and relations. The following definitions express that some +a notion of ``data-refinement'' for constants, functions, predicates and relations. The following definitions express that a given constant, function, relation defined in \HydrasLib ``implements'' the same concept of \gaia. - - - - - - +From~\href{../theories/html/gaia_hydras/T1Bridge.html}% +{\texttt{gaia\_hydras.T1Bridge}}. \inputsnippets{T1Bridge/refineDefs} Refinement lemmas can be easily ``reversed''. -\inputsnippets{T1Bridge/refines1R, T1Bridge/refines2R} +\inputsnippets{T1Bridge/refines1R} + +\inputsnippets{T1Bridge/refines2R} \subsection{Examples of refinement} Both of our libraries define constants like $0$, $1$, $\omega$, and arithmetic functions: successor, addition, multiplication, and exponential of base $\omega$ (function $\phi_0$). We prove that these definitions are mutually consistent. Finally, we prove that the boolean predicates `` to be in normal form'' are equivalent. @@ -202,10 +200,10 @@ \subsection{Looking for a lemma} $\alpha \times \beta=\beta$. The following command lists us `gaia's lemmas (thanks to -\gaia's \texttt{cantor\_scope}. +\gaia's \texttt{cantor\_scope}). \inputsnippets{T1Bridge/SearchDemoa} -With \texttt{t1\_scope}: +Within \texttt{t1\_scope}: \inputsnippets{T1Bridge/SearchDemob} \section{Importing Definitions and theorems from \HydrasLib} diff --git a/doc/hydras.tex b/doc/hydras.tex index 4c2ccc8a..375c3980 100644 --- a/doc/hydras.tex +++ b/doc/hydras.tex @@ -556,15 +556,15 @@ \part{Hydras and ordinals} \include{Gamma0-chapter} -\part{Ackermann, G\"{o}del, Peano\,\dots} +%\part{Ackermann, G\"{o}del, Peano\,\dots} -\include{chap-intro-goedel} +%\include{chap-intro-goedel} \include{chapter-primrec} -\include{chapter-fol} -\include{chapter-natural-deduction} -\include{chapter-lnn-lnt} -\include{chapter-encoding} -\include{chapter-expressible} +% \include{chapter-fol} +% \include{chapter-natural-deduction} +% \include{chapter-lnn-lnt} +% \include{chapter-encoding} +% \include{chapter-expressible} \part{A few certified algorithms} diff --git a/doc/schutte-chapter.tex b/doc/schutte-chapter.tex index c083c7ce..a0cddf3b 100644 --- a/doc/schutte-chapter.tex +++ b/doc/schutte-chapter.tex @@ -419,6 +419,7 @@ \subsubsection{Multiplication by a natural number} \input{movies/snippets/Addition/multFin} \section{The exponential of basis \texorpdfstring{$\omega$}{omega}} +\label{sect:AP-and-phi0} In this section, we define the function which maps any $\alpha\in\mathbb{O}$ to the ordinal $\omega^\alpha$, also written @@ -446,6 +447,7 @@ \subsection{Additive principal ordinals} \subsection{The function \texttt{phi0}} + Let us call $\phi_0$ the ordering function of \texttt{AP}. In the mathematical text, we shall use indifferently the notations $\omega^\alpha$ and $\phi_0(\alpha)$. diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v index c9872957..7ac6252c 100644 --- a/theories/ordinals/Epsilon0/T1.v +++ b/theories/ordinals/Epsilon0/T1.v @@ -543,7 +543,7 @@ Fixpoint nf_b (alpha : T1) : bool := (nf_b a && nf_b b && (bool_decide (lt a' a)))%bool end. -Definition nf alpha :Prop := nf_b alpha. +Definition nf alpha :Prop := nf_b alpha. (* end snippet nfDef *) (* begin snippet badTerm *) From ac1e16da2b5122240783c8c7304830cff1f3a677 Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Tue, 30 Jan 2024 11:18:59 +0100 Subject: [PATCH 3/7] simplify the proposition 'alpha < phi0 beta' --- theories/ordinals/Epsilon0/T1.v | 38 ++++++++++++++++----------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v index 7ac6252c..66dc262b 100644 --- a/theories/ordinals/Epsilon0/T1.v +++ b/theories/ordinals/Epsilon0/T1.v @@ -826,7 +826,7 @@ Ltac nf_decomp H := end. (** lt alpha (phi0 beta) *) -(** Should be deprecated *) + Inductive nf_helper : T1 -> T1 -> Prop := @@ -838,6 +838,8 @@ Inductive nf_helper : T1 -> T1 -> Prop := #[global] Hint Constructors nf_helper : T1. +Reserved Notation "x '<_phi0' y" (at level 70, no associativity). +Infix "<_phi0" := nf_helper. (* A tactic for decomposing a non zero ordinal *) (* use : H : lt zero ?c ; a n b : names to give to the constituents of @@ -1147,16 +1149,12 @@ Proof. Qed. Lemma nf_helper_inv1 : - forall a n b a', - nf_helper (cons a n b) a' -> lt a a'. + forall a n b a', cons a n b <_phi0 a'-> lt a a'. Proof. now inversion 1. Qed. Lemma nf_intro : - forall a n b, - nf a -> - nf b -> - nf_helper b a -> - nf (cons a n b). + forall a n b, nf a -> nf b -> b <_phi0 a -> + nf (cons a n b). Proof. destruct 3; eauto with T1. Qed. Lemma nf_intro' : @@ -1174,7 +1172,7 @@ Qed. Lemma nf_helper_intro : - forall a n b, nf (cons a n b) -> nf_helper b a. + forall a n b, nf (cons a n b) -> b <_phi0 a. Proof. intros a n b H; unfold nf in H; cbn in H. destruct b. @@ -1196,7 +1194,7 @@ Proof. Qed. Lemma nf_helper_phi0 : - forall a b, nf_helper b a -> lt b ( phi0 a). + forall a b, b <_phi0 a -> lt b ( phi0 a). Proof. induction 1; auto with T1. Qed. @@ -1211,7 +1209,7 @@ Qed. Lemma nf_helper_iff : forall a b, nf a -> nf b -> - (nf_helper b a <-> forall n, nf (cons a n b)). + (b <_phi0 a <-> forall n, nf (cons a n b)). Proof. split. - intros; now apply nf_intro. @@ -1229,7 +1227,7 @@ Definition nf_rect : forall P : T1 -> Type, (forall n: nat, P (cons zero n zero)) -> (forall a n b n' b', nf (cons a n b) -> P (cons a n b)-> - nf_helper b' (cons a n b) -> + b' <_phi0 (cons a n b) -> nf b' -> P b' -> P (cons (cons a n b) n' b')) -> @@ -1640,7 +1638,7 @@ Module Direct_proof. Lemma Acc_strong_stronger : forall alpha, nf alpha -> Acc_strong alpha -> Acc LT alpha. Proof. - intros alpha H H0. apply acc_impl with (phi0 alpha). + intros alpha H H0; apply acc_impl with (phi0 alpha). - repeat split; trivial. + now apply lt_a_phi0_a. - apply H0; now apply single_nf. @@ -1654,11 +1652,12 @@ Module Direct_proof. Lemma Acc_implies_Acc_strong : forall alpha, Acc LT alpha -> Acc_strong alpha. (* .no-out *) Proof. (* .no-out *) - (* main induction (on a's accessibility) *) + (* main induction (on alpha's accessibility) *) + unfold Acc_strong; intros alpha Aalpha. (*| .. coq:: -.h#Acc_strong |*) - unfold Acc_strong; intros alpha Aalpha; pattern alpha; + pattern alpha; eapply Acc_ind with (R:= LT);[| assumption]; clear alpha Aalpha; intros alpha Aalpha IHalpha. (*||*) @@ -1671,10 +1670,11 @@ Module Direct_proof. *) assert(beta_Acc: - forall beta, nf_helper beta alpha -> nf alpha -> nf beta -> Acc LT beta). + forall beta, beta <_phi0 alpha -> nf alpha -> nf beta + -> Acc LT beta). (* Proof of beta_Acc: Since beta is less than omega ^ alpha, - beta is of the form omega^alpha'*(p+1)+beta' where + beta is of the form omega ^ alpha'*(p+1)+beta' where LT alpha' alpha, so the inductive hypothesis IHalpha can be used *) { intros b H H' H''; assert (H0 : LT b (phi0 alpha)). @@ -1833,7 +1833,7 @@ Ltac transfinite_induction alpha := (* begin hide *) Lemma succ_nf_helper : - forall c a n b, nf_helper c (cons a n b) -> nf_helper (succ c) (cons a n b). + forall c a n b, c <_phi0 (cons a n b) -> succ c <_phi0 (cons a n b). Proof. induction c. - simpl; repeat constructor. @@ -2830,7 +2830,7 @@ Proof. split. intros H. repeat split; eauto with T1. - apply nf_helper_phi0. + apply nf_helper_phi0. eapply nf_helper_intro; eauto. intro H; decompose [and] H. apply nf_intro; eauto. From ef62b06d098ed8a42531c0673aefff847eac9008 Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Tue, 30 Jan 2024 11:40:01 +0100 Subject: [PATCH 4/7] simplify the proposition 'alpha < phi0 beta' --- theories/ordinals/Epsilon0/Canon.v | 44 +++++------ theories/ordinals/Epsilon0/E0.v | 2 +- theories/ordinals/Epsilon0/Epsilon0rpo.v | 4 +- theories/ordinals/Epsilon0/Hessenberg.v | 84 ++++++++++----------- theories/ordinals/Epsilon0/Paths.v | 10 +-- theories/ordinals/Epsilon0/T1.v | 85 +++++++++++----------- theories/ordinals/Schutte/Correctness_E0.v | 8 +- 7 files changed, 118 insertions(+), 119 deletions(-) diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v index 122206da..caa33f17 100644 --- a/theories/ordinals/Epsilon0/Canon.v +++ b/theories/ordinals/Epsilon0/Canon.v @@ -402,15 +402,15 @@ Proof. - destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial. now apply head_lt. discriminate. - - apply nf_helper_phi0R. + - apply lt_a_phi0_b_phi0R. apply T1.lt_trans with (cons alpha2_1 n1 alpha2_2). + destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial. apply head_lt; auto. * discriminate. * tauto. + - apply nf_helper_phi0. - apply nf_helper_intro with n;auto. + apply lt_a_phi0_b_phi0. + apply lt_a_phi0_b_intro with n;auto. } split. @@ -524,15 +524,15 @@ Proof. - destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial. now apply head_lt. discriminate. - - apply nf_helper_phi0R. + - apply lt_a_phi0_b_phi0R. apply T1.lt_trans with (cons alpha2_1 n1 alpha2_2). + destruct (Hrec (cons alpha2_1 n1 alpha2_2)) ; trivial. apply head_lt; auto. * discriminate. * tauto. + - apply nf_helper_phi0. - apply nf_helper_intro with n;auto. + apply lt_a_phi0_b_phi0. + apply lt_a_phi0_b_intro with n;auto. } split. @@ -694,7 +694,7 @@ Proof. ++ apply LT2; trivial. apply nf_intro; trivial. now apply nf_canon. - apply nf_helper_phi0R. + apply lt_a_phi0_b_phi0R. apply canon_lt. eapply nf_coeff_irrelevance;eauto. discriminate. @@ -709,7 +709,7 @@ Proof. { apply nf_intro; trivial. apply nf_canon; trivial. - apply nf_helper_phi0R. + apply lt_a_phi0_b_phi0R. apply canon_lt. eapply nf_coeff_irrelevance;eauto. discriminate. @@ -728,8 +728,8 @@ Proof. -- split. ++ eapply nf_inv2, Hbeta. ++ split. - ** apply nf_helper_phi0. - apply nf_helper_intro with n0;auto with T1. + ** apply lt_a_phi0_b_phi0. + apply lt_a_phi0_b_intro with n0;auto with T1. ** eapply nf_coeff_irrelevance;eauto. } subst; @@ -746,8 +746,8 @@ Proof. - split. + eapply nf_inv2, Hbeta. + split. - * apply nf_helper_phi0. - apply nf_helper_intro with n;auto with T1. + * apply lt_a_phi0_b_phi0. + apply lt_a_phi0_b_intro with n;auto with T1. * eapply nf_coeff_irrelevance;eauto. } destruct H4; exists x; rewrite canon_SSn_zero. @@ -755,7 +755,7 @@ Proof. { apply nf_intro; auto with T1. eauto with T1. - apply nf_helper_phi0R. + apply lt_a_phi0_b_phi0R. apply canon_lt. now apply nf_phi0. intro; subst; discriminate. @@ -775,11 +775,11 @@ Proof. { apply nf_intro; trivial. eauto with T1. apply nf_canon; trivial; eauto with T1. - apply nf_helper_phi0R. + apply lt_a_phi0_b_phi0R. apply T1.lt_trans with lambda2. apply canon_lt; eauto with T1. - apply nf_helper_phi0. - apply nf_helper_intro with n; eauto with T1. + apply lt_a_phi0_b_phi0. + apply lt_a_phi0_b_intro with n; eauto with T1. } auto. auto. @@ -788,11 +788,11 @@ Proof. { apply nf_intro. - eauto with T1. - apply nf_canon; eauto with T1. - - apply nf_helper_phi0R. + - apply lt_a_phi0_b_phi0R. apply T1.lt_trans with lambda2. apply canon_lt; eauto with T1. - apply nf_helper_phi0. - apply nf_helper_intro with n; eauto with T1. + apply lt_a_phi0_b_phi0. + apply lt_a_phi0_b_intro with n; eauto with T1. } all: auto. -- subst; assert ({i: nat | beta2 t1< (canon lambda2 (S i))})%t1. @@ -807,11 +807,11 @@ Proof. apply nf_intro. eauto with T1. apply nf_canon; eauto with T1. - apply nf_helper_phi0R. + apply lt_a_phi0_b_phi0R. apply T1.lt_trans with lambda2. apply canon_lt; eauto with T1. - apply nf_helper_phi0. - apply nf_helper_intro with n; eauto with T1. + apply lt_a_phi0_b_phi0. + apply lt_a_phi0_b_intro with n; eauto with T1. } all: auto. - destruct s as [t [Ht Ht']]; subst lambda. diff --git a/theories/ordinals/Epsilon0/E0.v b/theories/ordinals/Epsilon0/E0.v index 1f6af1ac..eb62e80b 100644 --- a/theories/ordinals/Epsilon0/E0.v +++ b/theories/ordinals/Epsilon0/E0.v @@ -651,7 +651,7 @@ Proof. destruct H1. rewrite cnf_phi0 in H1. apply nf_intro; auto. - now apply nf_helper_phi0R. + now apply lt_a_phi0_b_phi0R. red. apply succ_lt_limit. rewrite cnf_phi0. diff --git a/theories/ordinals/Epsilon0/Epsilon0rpo.v b/theories/ordinals/Epsilon0/Epsilon0rpo.v index fcd626a0..1ef663a4 100644 --- a/theories/ordinals/Epsilon0/Epsilon0rpo.v +++ b/theories/ordinals/Epsilon0/Epsilon0rpo.v @@ -299,8 +299,8 @@ Proof. auto with arith rpo. auto with rpo. apply lt_le_trans with (cons o'1 0 zero). - apply nf_helper_phi0. - eapply nf_helper_intro. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro. eauto. auto with T1 rpo. auto with T1 rpo. diff --git a/theories/ordinals/Epsilon0/Hessenberg.v b/theories/ordinals/Epsilon0/Hessenberg.v index 5bb7b9c9..1f9e64c6 100644 --- a/theories/ordinals/Epsilon0/Hessenberg.v +++ b/theories/ordinals/Epsilon0/Hessenberg.v @@ -180,10 +180,10 @@ Proof. Qed. -Lemma nf_helper_oplus : forall gamma alpha beta, - nf_helper alpha gamma -> - nf_helper beta gamma -> - nf_helper (alpha o+ beta) gamma. +Lemma lt_a_phi0_b_oplus : forall gamma alpha beta, + alpha <_phi0 gamma -> + beta <_phi0 gamma -> + alpha o+ beta <_phi0 gamma. Proof with auto. induction gamma; destruct alpha, beta. - simpl; constructor. @@ -195,8 +195,8 @@ Proof with auto. - simpl; auto. - rewrite oplus_eqn; case_eq (compare alpha1 beta1). + constructor; now inversion H0. - + right; eapply nf_helper_inv1;eauto. - + right; eapply nf_helper_inv1;eauto. + + right; eapply lt_a_phi0_b_inv1;eauto. + + right; eapply lt_a_phi0_b_inv1;eauto. Qed. @@ -207,11 +207,11 @@ Lemma oplus_bounded_phi0 alpha beta gamma : lt (alpha o+ beta) (phi0 gamma). Proof. intros H H0 H1 H2 H3. - apply nf_helper_phi0; auto. - apply nf_helper_oplus; auto. - eapply nf_helper_intro with 0; auto. + apply lt_a_phi0_b_phi0; auto. + apply lt_a_phi0_b_oplus; auto. + eapply lt_a_phi0_b_intro with 0; auto. eapply nf_intro;auto. - 1,2 :now apply nf_helper_phi0R. + 1,2 :now apply lt_a_phi0_b_phi0R. Qed. Section Proof_of_plus_nf. @@ -233,28 +233,28 @@ Section Proof_of_plus_nf. repeat split; auto with T1. -- apply le_lt_trans with (cons alpha1 n alpha2); auto. now apply le_phi0. - -- apply nf_helper_phi0, nf_helper_intro with n, Hnf_1. - -- apply nf_helper_phi0, nf_helper_intro with n, Hnf_2. - * apply nf_helper_oplus; eapply nf_helper_intro; eauto. + -- apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n, Hnf_1. + -- apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n, Hnf_2. + * apply lt_a_phi0_b_oplus; eapply lt_a_phi0_b_intro; eauto. + apply nf_intro; auto. * eapply IHgamma with (phi0 beta1); auto with T1. -- repeat split; auto with T1. apply le_lt_trans with (cons beta1 n0 beta2); auto. apply le_phi0. - -- now apply nf_helper_phi0, nf_helper_intro with n. - * apply nf_helper_oplus; auto. - -- now apply nf_helper_phi0R, head_lt. - -- now apply nf_helper_intro with n. + -- now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n. + * apply lt_a_phi0_b_oplus; auto. + -- now apply lt_a_phi0_b_phi0R, head_lt. + -- now apply lt_a_phi0_b_intro with n. + apply nf_intro; trivial. * eapply IHgamma with (phi0 alpha1); trivial. -- repeat split; auto with T1. apply le_lt_trans with (cons alpha1 n alpha2); auto. apply le_phi0; eauto with T1. - -- apply nf_helper_phi0. - eapply nf_helper_intro; eauto. + -- apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro; eauto. -- now apply head_lt. - * apply nf_helper_oplus; auto. - eapply nf_helper_intro; eauto. + * apply lt_a_phi0_b_oplus; auto. + eapply lt_a_phi0_b_intro; eauto. now constructor 2. Qed. @@ -304,7 +304,7 @@ Section Proof_of_oplus_comm. - apply compare_eq_iff in Hcomp as <-. repeat rewrite (Nat.add_comm n n0); f_equal. + apply H0 with (phi0 alpha1); trivial. - 2-3: apply nf_helper_phi0, nf_helper_intro with n; eauto. + 2-3: apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n; eauto. apply LE_LT_trans with (cons alpha1 n0 beta2). * now apply LE_phi0. * now repeat split. @@ -316,14 +316,14 @@ Section Proof_of_oplus_comm. apply LE_phi0; auto. repeat split; trivial. + now apply head_lt, compare_lt_iff. - + now apply nf_helper_phi0, nf_helper_intro with n. + + now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n. - rewrite <- oplus_compare_Gt; auto. rewrite oplus_compare_Gt; auto. f_equal; apply H0 with (phi0 alpha1); trivial. apply LE_LT_trans with (cons alpha1 n alpha2); trivial. + now apply LE_phi0. - + repeat split; eauto with T1; apply nf_helper_phi0. - + apply nf_helper_phi0, nf_helper_intro with n; eauto. + + repeat split; eauto with T1; apply lt_a_phi0_b_phi0. + + apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n; eauto. + now apply head_lt, compare_gt_iff. Qed. @@ -348,14 +348,14 @@ Section Proof_of_oplus_comm. End Proof_of_oplus_comm. Lemma oplus_lt_rw2 : forall a n b x, nf (cons a n b) -> nf x -> - nf_helper x a -> + x <_phi0 a -> cons a n b o+ x = cons a n (b o+ x). Proof. destruct x. - now (intros; repeat rewrite oplus_0_r). - intros; rewrite (oplus_eqn (cons a n b) (cons x1 n0 x2)). - apply nf_helper_phi0 in H1. + apply lt_a_phi0_b_phi0 in H1. destruct (lt_inv H1). + unfold T1.lt in H2. rewrite compare_rev, H2. @@ -404,17 +404,17 @@ Section Proof_of_oplus_assoc. + f_equal; abstract lia. + apply tail_lt_cons; auto. + apply lt_le_trans with (phi0 a1). - * now apply nf_helper_phi0, nf_helper_intro with n0. + * now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n0. * now apply le_phi0. + apply lt_le_trans with (phi0 a1). - * now apply nf_helper_phi0, nf_helper_intro with n0. + * now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n0. * now apply le_phi0. - apply compare_eq_iff in Hbc as <-. ass_rw Hrec (cons b1 n0 b2) (cons a1 n a2) b2 c2; trivial. + now apply head_lt. + now apply tail_lt_cons. + apply lt_le_trans with (phi0 b1). - * now apply nf_helper_phi0, nf_helper_intro with n1. + * now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n1. * now apply le_phi0. - apply compare_eq_iff in Hbc as <-. f_equal. @@ -445,7 +445,7 @@ Section Proof_of_oplus_assoc. * now apply head_lt, compare_gt_iff. * apply lt_le_trans with (phi0 a1). -- apply compare_eq_iff in Hac as ->. - now apply nf_helper_phi0, nf_helper_intro with n1. + now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n1. -- now apply le_phi0. + ass_rw Hrec (cons c1 n1 c2) (cons a1 n a2) (cons b1 n0 b2) c2 ; trivial. @@ -463,7 +463,7 @@ Section Proof_of_oplus_assoc. + now apply tail_lt_cons. + apply lt_le_trans with (phi0 a1). * apply compare_eq_iff in Hab as ->. - now apply nf_helper_phi0, nf_helper_intro with n0. + now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n0. * now apply le_phi0. + now apply head_lt, compare_gt_iff. - ass_rw_rev Hrec (cons b1 n0 b2) (cons a1 n a2) b2 @@ -601,10 +601,10 @@ Proof with eauto with T1. apply le_lt_trans with (cons a1 n a2) ; trivial. apply le_phi0. auto with T1. - apply nf_helper_phi0. - eapply nf_helper_intro; auto with T1. - apply nf_helper_phi0. - eapply nf_helper_intro ; auto with T1. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro; auto with T1. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro ; auto with T1. } { intro Ha1b1; rewrite compare_lt_iff in Ha1b1. @@ -666,8 +666,8 @@ Proof with eauto with T1. apply le_phi0. eapply nf_inv2, nf2. eapply nf_inv2, nf4. - apply nf_helper_phi0. eapply nf_helper_intro; eauto with T1. - apply nf_helper_phi0. eapply nf_helper_intro; eauto with T1. + apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro; eauto with T1. + apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro; eauto with T1. } { apply compare_eq_iff in H6 as <-. @@ -719,8 +719,8 @@ Proof with eauto with T1. apply le_lt_trans with (cons a1 n a2). apply le_phi0; info_eauto with T1. auto with T1. - apply nf_helper_phi0. - eapply nf_helper_intro, Ha. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro, Ha. apply head_lt; now rewrite compare_gt_iff in H4. } } @@ -750,8 +750,8 @@ Proof with eauto with T1. apply Hrec with (phi0 a1) ; trivial. apply le_lt_trans with (cons a1 n a2) ; trivial. apply le_phi0 ; info_eauto with T1. - apply nf_helper_phi0. - eapply nf_helper_intro;eauto with T1. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro;eauto with T1. auto with T1. } Unshelve. diff --git a/theories/ordinals/Epsilon0/Paths.v b/theories/ordinals/Epsilon0/Paths.v index b91d1b1f..20c348bb 100644 --- a/theories/ordinals/Epsilon0/Paths.v +++ b/theories/ordinals/Epsilon0/Paths.v @@ -553,7 +553,7 @@ Proof. apply nf_intro; [auto | | ]. * destruct H1; subst. apply nf_canon; now apply nf_phi0. - * apply nf_helper_phi0R. + * apply lt_a_phi0_b_phi0R. destruct H1; subst. generalize (@canonS_LT i0 (T1.phi0 alpha) (nf_phi0 H)). destruct 1. @@ -732,11 +732,11 @@ Proof. destruct (IHs alpha n (canon beta (S a))); auto. * apply nf_intro; auto. apply nf_canon;auto. - apply nf_helper_phi0R. + apply lt_a_phi0_b_phi0R. apply T1.lt_trans with beta. apply canon_lt;auto. - apply nf_helper_phi0. - eapply nf_helper_intro; eauto. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro; eauto. * destruct H3 as [s2 [H4 [H5 H6]]]; exists (a::x), s2. subst s; split;auto. Qed. @@ -1798,7 +1798,7 @@ Proof. apply nf_intro. eauto with T1. apply nf_canon; eauto with T1. - apply nf_helper_phi0R. + apply lt_a_phi0_b_phi0R. destruct (@canonS_LT p (T1.cons alpha1 0 zero)). eauto with T1. discriminate. diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v index 66dc262b..4952e69e 100644 --- a/theories/ordinals/Epsilon0/T1.v +++ b/theories/ordinals/Epsilon0/T1.v @@ -825,21 +825,20 @@ Ltac nf_decomp H := | nf (cons ?t1 ?n ?t2) => assert (nf0 := nf_inv1 H); assert(nf1 := nf_inv2 H) end. -(** lt alpha (phi0 beta) *) - +(** lt alpha (phi0 beta) *) -Inductive nf_helper : T1 -> T1 -> Prop := -| nf_helper_z : forall alpha, nf_helper zero alpha -| nf_helper_c : forall alpha alpha' n' beta', +Inductive lt_a_phi0_b : T1 -> T1 -> Prop := +| lt_a_phi0_b_z : forall alpha, lt_a_phi0_b zero alpha +| lt_a_phi0_b_c : forall alpha alpha' n' beta', lt alpha' alpha -> - nf_helper (cons alpha' n' beta') alpha. + lt_a_phi0_b (cons alpha' n' beta') alpha. -#[global] Hint Constructors nf_helper : T1. +#[global] Hint Constructors lt_a_phi0_b : T1. Reserved Notation "x '<_phi0' y" (at level 70, no associativity). -Infix "<_phi0" := nf_helper. +Infix "<_phi0" := lt_a_phi0_b. (* A tactic for decomposing a non zero ordinal *) (* use : H : lt zero ?c ; a n b : names to give to the constituents of @@ -1007,7 +1006,7 @@ Qed. Arguments le_inv [a n b a' n' b'] _. -Lemma nf_helper_inv : +Lemma lt_a_phi0_b_inv : forall a n b a', lt (cons a n b) (phi0 a') -> lt a a'. Proof. intros a n b a' H; destruct (lt_inv H); auto. @@ -1148,7 +1147,7 @@ Proof. - intros n0 a H; apply head_lt; eapply nf_inv3; eauto. Qed. -Lemma nf_helper_inv1 : +Lemma lt_a_phi0_b_inv1 : forall a n b a', cons a n b <_phi0 a'-> lt a a'. Proof. now inversion 1. Qed. @@ -1167,11 +1166,11 @@ Proof. destruct b. - eauto with T1. - intros H H0 H1; apply cons_nf; auto. - now apply nf_helper_inv in H1. + now apply lt_a_phi0_b_inv in H1. Qed. -Lemma nf_helper_intro : +Lemma lt_a_phi0_b_intro : forall a n b, nf (cons a n b) -> b <_phi0 a. Proof. intros a n b H; unfold nf in H; cbn in H. @@ -1190,30 +1189,30 @@ Proof. intros; apply nf_intro. - eapply nf_inv1; eauto. - eapply nf_inv2; eauto. - - eapply nf_helper_intro; eauto. + - eapply lt_a_phi0_b_intro; eauto. Qed. -Lemma nf_helper_phi0 : +Lemma lt_a_phi0_b_phi0 : forall a b, b <_phi0 a -> lt b ( phi0 a). Proof. induction 1; auto with T1. Qed. -Lemma nf_helper_phi0R : - forall a b, lt b (phi0 a) -> nf_helper b a. +Lemma lt_a_phi0_b_phi0R : + forall a b, lt b (phi0 a) -> lt_a_phi0_b b a. Proof. induction b. - constructor. - - intro H; apply nf_helper_inv in H; constructor; auto. + - intro H; apply lt_a_phi0_b_inv in H; constructor; auto. Qed. -Lemma nf_helper_iff : +Lemma lt_a_phi0_b_iff : forall a b, nf a -> nf b -> (b <_phi0 a <-> forall n, nf (cons a n b)). Proof. split. - intros; now apply nf_intro. - - intro; now apply nf_helper_intro with 0. + - intro; now apply lt_a_phi0_b_intro with 0. Qed. Lemma nf_omega_tower : forall n, nf (omega_tower n). @@ -1240,7 +1239,7 @@ Proof. + intros c n0 c0 IHc0 H2; apply Hcons. * eapply nf_inv1;eauto. * apply IHc0; eapply nf_inv1; eauto. - * eapply nf_helper_intro; eauto. + * eapply lt_a_phi0_b_intro; eauto. * eapply nf_inv2;eauto. * apply IHa2; eapply nf_inv2;eauto. Defined. @@ -1678,7 +1677,7 @@ Module Direct_proof. LT alpha' alpha, so the inductive hypothesis IHalpha can be used *) { intros b H H' H''; assert (H0 : LT b (phi0 alpha)). - { repeat split;auto; apply nf_helper_phi0; auto. } + { repeat split;auto; apply lt_a_phi0_b_phi0; auto. } generalize H0; pattern b; case b. - intro;apply Acc_zero. - intros t n t0 H1; case H1; destruct 2; @@ -1707,7 +1706,7 @@ Module Direct_proof. - (* n=0 : let's use b's accessibility for doing an induction on b *) intros b Hb; assert (H : Acc LT b). { apply beta_Acc. - - eapply nf_helper_intro; eauto. + - eapply lt_a_phi0_b_intro; eauto. - eapply nf_inv1;eauto. - eapply nf_inv2;eauto. } @@ -1751,7 +1750,7 @@ Module Direct_proof. * subst n0 c;apply H1; auto. case H3;auto. - apply beta_Acc. - + eapply nf_helper_intro;eauto. + + eapply lt_a_phi0_b_intro;eauto. + eapply nf_inv1;eauto. + eapply nf_inv2;eauto. } @@ -1832,7 +1831,7 @@ Ltac transfinite_induction alpha := (** ** Properties of successor *) (* begin hide *) -Lemma succ_nf_helper : +Lemma succ_lt_a_phi0_b : forall c a n b, c <_phi0 (cons a n b) -> succ c <_phi0 (cons a n b). Proof. induction c. @@ -1852,7 +1851,7 @@ Proof. + intros c n0 c0 H H0; apply nf_intro. * eapply nf_inv1; eauto. * apply IHalpha2; eapply nf_inv2 ; eauto. - * apply succ_nf_helper; eapply nf_helper_intro; eauto. + * apply succ_lt_a_phi0_b; eapply lt_a_phi0_b_intro; eauto. Qed. (** ** properties of addition *) @@ -1961,10 +1960,10 @@ Proof. * destruct 1. { rewrite (plus_cons_cons_rw1 n t n0 c1_2 l); auto. } subst c1_1; rewrite (plus_cons_cons_rw2 H1 H5). - apply nf_helper_inv in H6. + apply lt_a_phi0_b_inv in H6. auto with T1. * intro H7; rewrite plus_cons_cons_rw3;auto. - apply nf_helper_inv in H3; auto with T1. + apply lt_a_phi0_b_inv in H3; auto with T1. Qed. Lemma ap_plusR : @@ -2033,17 +2032,17 @@ Proof. * eapply nf_inv1;eauto with T1. * nf_decomp H1; nf_decomp H2. eapply Cx with b1; trivial. - apply nf_helper_inv in H;auto with T1. - apply nf_helper_phi0. - eapply nf_helper_intro with n; trivial. - apply nf_helper_phi0. - eapply nf_helper_intro with n0; trivial. + apply lt_a_phi0_b_inv in H;auto with T1. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro with n; trivial. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro with n0; trivial. apply cons_nf; auto. * nf_decomp H1; nf_decomp H2. - apply nf_helper_phi0R; apply ap_plus; trivial. + apply lt_a_phi0_b_phi0R; apply ap_plus; trivial. constructor. - apply nf_helper_phi0. - eapply nf_helper_intro; trivial. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro; trivial. auto with T1. Unshelve. exact 0. @@ -2830,11 +2829,11 @@ Proof. split. intros H. repeat split; eauto with T1. - apply nf_helper_phi0. - eapply nf_helper_intro; eauto. + apply lt_a_phi0_b_phi0. + eapply lt_a_phi0_b_intro; eauto. intro H; decompose [and] H. apply nf_intro; eauto. - apply nf_helper_phi0R. destruct H3; tauto. + apply lt_a_phi0_b_phi0R. destruct H3; tauto. Qed. Lemma lt_plus_l: @@ -3202,7 +3201,7 @@ Section Proof_of_mult_nf. generalize (@IHbeta d); intro H1; destruct H1; auto with T1. apply tail_LT_cons; eauto with T1. eauto with T1. - apply nf_helper_phi0R. + apply lt_a_phi0_b_phi0R. apply lt_le_trans with (cons a n b * phi0 c). { generalize (@IHbeta (phi0 c)); intro H1; unfold P in H1. @@ -3496,9 +3495,9 @@ Proof with eauto with T1. { apply nf_intro; auto. inversion H; auto. apply nf_inv1 in H. auto. - apply nf_helper_phi0R; apply lt_trans with (succ beta0);auto. + apply lt_a_phi0_b_phi0R; apply lt_trans with (succ beta0);auto. apply lt_succ. - apply nf_helper_phi0; eapply nf_helper_intro; eauto. + apply lt_a_phi0_b_phi0; eapply lt_a_phi0_b_intro; eauto. } reflexivity. Defined. @@ -3655,11 +3654,11 @@ Lemma lt_cons_phi0_inv alpha n beta gamma : Proof. split. - destruct 1 as [H [H0 H1]]; repeat split; eauto with T1. - apply nf_helper_inv in H0; auto. + apply lt_a_phi0_b_inv in H0; auto. rewrite nf_LT_iff in H. destruct H; eauto with T1. destruct H2; eauto with T1. - now apply nf_helper_inv in H0. + now apply lt_a_phi0_b_inv in H0. - destruct 1. apply LT2; auto. rewrite nf_LT_iff; eauto with T1. diff --git a/theories/ordinals/Schutte/Correctness_E0.v b/theories/ordinals/Schutte/Correctness_E0.v index a983e62c..6f8639f1 100644 --- a/theories/ordinals/Schutte/Correctness_E0.v +++ b/theories/ordinals/Schutte/Correctness_E0.v @@ -199,8 +199,8 @@ Proof with eauto with T1. * apply T1.lt_trans with (T1.cons gamma1 n0 gamma2) ... + apply lt_trans with (inject (T1.phi0 beta1)). * eapply IHbeta2 ... - apply T1.nf_helper_phi0. - apply T1.nf_helper_intro with n; auto. + apply T1.lt_a_phi0_b_phi0. + apply T1.lt_a_phi0_b_intro with n; auto. apply Comparable.le_lt_trans with (T1.cons beta1 n beta2); auto with T1. apply T1.le_phi0 ; eauto with T1. eapply T1.lt_trans ... @@ -213,8 +213,8 @@ Proof with eauto with T1. subst; apply coeff_lt. + replace (AP._phi0 (inject gamma1)) with (inject (T1.phi0 gamma1)). * apply IHbeta2. - apply T1.nf_helper_phi0. - eapply T1.nf_helper_intro; eauto. + apply T1.lt_a_phi0_b_phi0. + eapply T1.lt_a_phi0_b_intro; eauto. apply Comparable.le_lt_trans with (T1.cons gamma1 n0 gamma2); auto. destruct n0. apply T1.le_tail ... From 281535802b0fa1fb5688f9202bd0005835e64c84 Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Tue, 30 Jan 2024 17:43:37 +0100 Subject: [PATCH 5/7] improve Alectryon output --- doc/epsilon0-chapter.tex | 18 +++-- theories/ordinals/Epsilon0/T1.v | 125 +++++++++++++++++--------------- 2 files changed, 76 insertions(+), 67 deletions(-) diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex index 6b246ebb..c886d15c 100644 --- a/doc/epsilon0-chapter.tex +++ b/doc/epsilon0-chapter.tex @@ -701,19 +701,23 @@ \subsubsection{Using a stronger inductive predicate.} \label{sec:orgheadline79} First, we prove that, for any \texttt{LT}-accessible term $\alpha$, $\alpha$ is -strongly accessible too (\emph{i.e.} any well formed -term (\texttt{cons $\alpha$ $n$ $\beta$}) is accessible). - -The proof is structured as an induction on $\alpha'$s accessibility. Let us consider +strongly accessible too. +The following proof is structured as an induction on $\alpha'$s accessibility. Let us consider any accessible term $\alpha$. \input{movies/snippets/T1/AccImpAccStrong} +First, we prove that, for any $n$ and $\beta$, if (\texttt{cons $\alpha$ $n$ $\beta$}) is in normal form, then + $\beta$ is accessible. + +\inputsnippets{T1/betaAcc} + +The lemma \texttt{betaAcc} allows us to prove by well-founded induction on $\beta$, +and natural induction on $n$ that (\texttt{cons $\alpha$ $n$ $\beta$}) is accessible. + +\inputsnippets{T1/useBetaAcc} -Let \texttt{n:nat} and \texttt{beta:T1} such that (\texttt{cons alpha n beta}) is in normal form. -We prove first that \texttt{beta} is accessible, which allows us to prove by well-founded induction on \texttt{beta}, -and natural induction on \texttt{n}, that (\texttt{cons alpha n beta}) is accessible. The proof, quite long, can be consulted in \href{../theories/html/hydras.Epsilon0.T1.html}{Epsilon0.T1}. \paragraph{Accessibility of any well-formed ordinal term} diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v index 4952e69e..f682b085 100644 --- a/theories/ordinals/Epsilon0/T1.v +++ b/theories/ordinals/Epsilon0/T1.v @@ -425,11 +425,9 @@ Proof. now apply Nat.compare_lt_iff in H as ->. Qed. - - Lemma tail_lt : forall alpha n beta beta', - lt beta beta' -> + lt beta beta' -> lt (cons alpha n beta) (cons alpha n beta'). Proof. unfold lt. @@ -702,7 +700,7 @@ Proof. reflexivity. Qed. Lemma single_nf : forall a n, nf a -> nf (cons a n zero). -Proof. unfold nf; now cbn. Qed. +Proof. unfold nf; now cbn. Qed. Lemma cons_nf : forall a n a' n' b, @@ -754,8 +752,6 @@ Proof. decompose [and] H; apply (bool_decide_eq_true _); auto. Qed. - - Lemma nf_cons_inv a n b : nf (cons a n b) -> nf a /\ nf b /\ lt b (phi0 a). Proof. unfold nf; cbn; destruct b. @@ -827,14 +823,12 @@ Ltac nf_decomp H := (** lt alpha (phi0 beta) *) - Inductive lt_a_phi0_b : T1 -> T1 -> Prop := | lt_a_phi0_b_z : forall alpha, lt_a_phi0_b zero alpha | lt_a_phi0_b_c : forall alpha alpha' n' beta', lt alpha' alpha -> lt_a_phi0_b (cons alpha' n' beta') alpha. - #[global] Hint Constructors lt_a_phi0_b : T1. Reserved Notation "x '<_phi0' y" (at level 70, no associativity). @@ -893,8 +887,7 @@ Qed. (** ** Second part on [lt] and [le] *) Lemma finite_lt : - forall n p : nat, - (n < p)%nat -> lt (FS n) (FS p). + forall n p : nat, (n < p)%nat -> lt (FS n) (FS p). Proof. intros; auto with T1. Qed. @@ -1199,13 +1192,23 @@ Proof. Qed. Lemma lt_a_phi0_b_phi0R : - forall a b, lt b (phi0 a) -> lt_a_phi0_b b a. + forall a b, lt b (phi0 a) -> b <_phi0 a. Proof. induction b. - constructor. - intro H; apply lt_a_phi0_b_inv in H; constructor; auto. Qed. + + +Lemma lt_a_phi0_b_def : + forall a b, b <_phi0 a <-> lt b (phi0 a). +Proof. + split. + - intros; now apply lt_a_phi0_b_phi0. + - intros; now apply lt_a_phi0_b_phi0R. +Qed. + Lemma lt_a_phi0_b_iff : forall a b, nf a -> nf b -> (b <_phi0 a <-> forall n, nf (cons a n b)). @@ -1226,7 +1229,7 @@ Definition nf_rect : forall P : T1 -> Type, (forall n: nat, P (cons zero n zero)) -> (forall a n b n' b', nf (cons a n b) -> P (cons a n b)-> - b' <_phi0 (cons a n b) -> + lt b' (phi0 (cons a n b)) -> nf b' -> P b' -> P (cons (cons a n b) n' b')) -> @@ -1239,7 +1242,8 @@ Proof. + intros c n0 c0 IHc0 H2; apply Hcons. * eapply nf_inv1;eauto. * apply IHc0; eapply nf_inv1; eauto. - * eapply lt_a_phi0_b_intro; eauto. + * rewrite <- lt_a_phi0_b_def; + eapply lt_a_phi0_b_intro; eauto. * eapply nf_inv2;eauto. * apply IHa2; eapply nf_inv2;eauto. Defined. @@ -1652,66 +1656,69 @@ Module Direct_proof. Acc LT alpha -> Acc_strong alpha. (* .no-out *) Proof. (* .no-out *) (* main induction (on alpha's accessibility) *) - unfold Acc_strong; intros alpha Aalpha. (*| .. coq:: -.h#Acc_strong |*) + unfold Acc_strong; intros alpha Aalpha. pattern alpha; - eapply Acc_ind with (R:= LT);[| assumption]; + eapply Acc_ind with (R:= LT);[| assumption]; clear alpha Aalpha; intros alpha Aalpha IHalpha. - (*||*) - (*| -.. coq:: none -|*) - - (* for any n and b, such that (cons a n b) is well formed, +(* end snippet AccImpAccStrong *) + (* for any n and b, such that (cons a n b) is well formed, b is accessible *) - +(* begin snippet betaAcc:: -.h#Acc_strong -.g#* .g#2*) assert(beta_Acc: - forall beta, beta <_phi0 alpha -> nf alpha -> nf beta - -> Acc LT beta). - (* Proof of beta_Acc: + forall beta, lt beta (phi0 alpha) -> nf alpha -> nf beta + -> Acc LT beta). + (* ... *) (* .no-out *) + (* end snippet betaAcc *) + (* Proof of beta_Acc: Since beta is less than omega ^ alpha, beta is of the form omega ^ alpha'*(p+1)+beta' where LT alpha' alpha, so the inductive hypothesis IHalpha can be used - *) - { intros b H H' H''; assert (H0 : LT b (phi0 alpha)). - { repeat split;auto; apply lt_a_phi0_b_phi0; auto. } - generalize H0; pattern b; case b. - - intro;apply Acc_zero. - - intros t n t0 H1; case H1; destruct 2; - case (lt_inv H3). - + intro H5;generalize H2;case n. - { inversion 1. - - intros; apply IHalpha. - + split. - * apply nf_inv1 in H2. auto. - * split;auto. - + auto. - } - intros;apply IHalpha. - split;auto. - eapply nf_inv1;eauto. - auto. - + destruct 1. - case H5;intros H6 H7; abstract lia. - case H5;intros _ (_,H6);destruct (not_lt_zero H6). - } - - (* end of proof of beta_Acc *) - (* we can now use a nested induction on n (Peano induction) - then on b (well_founded induction using b_Acc) *) - induction n. + *) + { + intros beta H H' H''; assert (H0 : LT beta (phi0 alpha)). + { repeat split;auto; apply lt_a_phi0_b_phi0; auto. } + generalize H0; pattern beta; case beta. + - intro;apply Acc_zero. + - intros t n t0 H1; case H1; destruct 2; + case (lt_inv H3). + + intro H5;generalize H2;case n. + { inversion 1. + - intros; apply IHalpha. + + split. + * apply nf_inv1 in H2. auto. + * split;auto. + + auto. + } + intros;apply IHalpha. + split;auto. + eapply nf_inv1;eauto. + auto. + + destruct 1. + case H5;intros H6 H7; abstract lia. + case H5;intros _ (_,H6);destruct (not_lt_zero H6). + (* begin snippet useBetaAcc:: no-in unfold -.h#Acc_strong *) + } + (* end snippet useBetaAcc *) + + + (* end of proof of beta_Acc *) + + (* we can now use a nested induction on n (Peano induction) + then on b (well_founded induction using b_Acc) *) + induction n. - (* n=0 : let's use b's accessibility for doing an induction on b *) intros b Hb; assert (H : Acc LT b). { apply beta_Acc. - - eapply lt_a_phi0_b_intro; eauto. + - rewrite <- lt_a_phi0_b_def; eapply lt_a_phi0_b_intro; eauto. - eapply nf_inv1;eauto. - eapply nf_inv2;eauto. } (* let's prove that every predecessor of (cons a 0 b) - is accessible *) + is accessible *) { pattern b;eapply Acc_ind;[|eexact H]. intros; split; intro y; case y. @@ -1750,14 +1757,12 @@ Module Direct_proof. * subst n0 c;apply H1; auto. case H3;auto. - apply beta_Acc. - + eapply lt_a_phi0_b_intro;eauto. + + rewrite <- lt_a_phi0_b_def. eapply lt_a_phi0_b_intro;eauto. + eapply nf_inv1;eauto. + eapply nf_inv2;eauto. } Qed. - (*||*) - - (* end snippet AccImpAccStrong *) + (** *** A (last) structural induction *) @@ -1768,7 +1773,7 @@ Module Direct_proof. induction alpha. (* .no-out *) - (* .no-out *) intro; apply Acc_zero. (* .no-out *) - (* .no-out *) intros; eapply Acc_implies_Acc_strong;auto. (* .no-out *) - apply IHalpha1; eauto. + apply IHalpha1; eauto. (* -.h#Acc_strong *) apply nf_inv1 in H; auto. Qed. From 8e7ea1ec6443d014e257b05478a64c05dd6adcb9 Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Fri, 2 Feb 2024 08:13:56 +0100 Subject: [PATCH 6/7] minor changes in pdf doc --- doc/epsilon0-chapter.tex | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex index c886d15c..bb03c049 100644 --- a/doc/epsilon0-chapter.tex +++ b/doc/epsilon0-chapter.tex @@ -659,7 +659,7 @@ \subsubsection{A first attempt} $\alpha=\texttt{cons $\beta\;n\;\gamma$}$, and assume that \(\beta\) and \(\gamma\) are \texttt{LT}-accessible. In order to prove the accessibility of $\alpha$, we have to consider any well formed term \(\delta\) such that \(\delta<\alpha\). -But nothing guarantees that \(\delta\) is strictly less than \(\beta\) nor \(\gamma\), and we cannot use the induction hypotheses on \(\beta\) nor \(\gamma\). +% But nothing guarantees that \(\delta\) is strictly less than \(\beta\) nor \(\gamma\), and we cannot use the induction hypotheses on \(\beta\) nor \(\gamma\). \input{movies/snippets/T1/wfLTBada} @@ -713,7 +713,7 @@ \subsubsection{Using a stronger inductive predicate.} \inputsnippets{T1/betaAcc} -The lemma \texttt{betaAcc} allows us to prove by well-founded induction on $\beta$, +The new hypothesis \texttt{beta\_Acc} allows us to prove by well-founded induction on $\beta$, and natural induction on $n$ that (\texttt{cons $\alpha$ $n$ $\beta$}) is accessible. \inputsnippets{T1/useBetaAcc} @@ -730,6 +730,7 @@ \subsubsection{Using a stronger inductive predicate.} \input{movies/snippets/T1/T1Wf} +\subsection{Transfinite induction} \index{maths}{Transfinite induction} From c702ca29b33264966d7c61b45ff0263977854c21 Mon Sep 17 00:00:00 2001 From: Pierre Casteran Date: Wed, 7 Feb 2024 16:26:49 +0100 Subject: [PATCH 7/7] minor changes in pdf doc --- doc/chapter-primrec.tex | 31 +++++++++------- doc/epsilon0-chapter.tex | 5 +-- doc/ordinal-chapter.tex | 12 +++---- theories/ordinals/Ackermann/primRec.v | 1 + theories/ordinals/MoreAck/PrimRecExamples.v | 39 ++++++++++----------- 5 files changed, 45 insertions(+), 43 deletions(-) diff --git a/doc/chapter-primrec.tex b/doc/chapter-primrec.tex index f4012e42..8590b4ab 100644 --- a/doc/chapter-primrec.tex +++ b/doc/chapter-primrec.tex @@ -50,19 +50,25 @@ \subsubsection{Projections} For instance, the projection $\pi_{2,3}$ satisfies the equation $\pi_{2,3}(x,y,z)=y$ for any natural numbers $x$, $y$ and $z$. -\subsubsection{The constant function of value 0} +\subsubsection{Constant functions} \label{sect:k0} -The \emph{unary} function which always returns $0$ may be defined through the \emph{composition} construction (with $n=1$, $m=0$, and $h=\texttt{zero}$). +The \emph{nullary} constant function which returns $0$ is +simply the \texttt{zero} construction. -% If we consider any value of $n$, the same construction -% builds the constant function of type $\mathbb{N}^n \arrow \mathbb{N}$ which returns $0$. +If we want to consider the \emph{unary} function which +maps any natural number $i$ to $0$, we may built it +through the \emph{composition} construction, instanciated +with $n=1$, $m=0$, and $h=\texttt{zero}$. -\subsubsection{Constant functions} +\index{hydras}{Exercises} + +\begin{exercise} +Let $m$ and $k$ be two natural numbers; please build the primitive recursive function which maps any +tuple $t\in \mathbb{N}^m$ to $k$. +\end{exercise} -Let $k$ be some natural number; the unary constant function which always returns $k$ is built through $k$ nested compositions of the -successor function with the unary constant function which returns $0$. \subsubsection{Addition on natural natural numbers} @@ -179,10 +185,11 @@ \subsection{Extensional equality} \index{ackermann}{Predicates!extEqual} \inputsnippets{extEqualNat/extEqualDef} -Module \href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec} defines and export the notation ``\texttt{$f$ =x= $g$}'' for ``\texttt{extEqual $n$ $f$ $g$}'' \footnote{in parsing mode, provided $f$ has explicitely the type (\texttt{naryFunc $n$}).} - - +Module \href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec} defines and export the notation ``\texttt{$f$ =x= $g$}'' for ``\texttt{extEqual $n$ $f$ $g$}'' \footnote{in parsing mode, the provided $f$ should be explicitely typed as (\texttt{naryFunc $n$}).} +\vspace{6pt} +\noindent +\emph{From \href{../theories/html/hydras.MoreAck.PrimRecExamples.html}{MoreAck.PrimRecExamples}} \input{movies/snippets/PrimRecExamples/extEqual2a} @@ -266,11 +273,11 @@ \subsubsection{Examples} \subsection{A little bit of semantics} \label{primrec-semantics} -Inhabitants of type (\texttt{PrimRec $n$}) are not \coq{} functions like \texttt{Nat.mul}, or \texttt{Arith.Factorial.fact}, etc. but terms of an abstract syntax for the language of primitive recursive functions. The bridge between this language and the word of usual functions +Inhabitants of type (\texttt{PrimRec $n$}) are not \coq{} functions like \texttt{Nat.mul}, \linebreak \texttt{Arith.Factorial.fact}, etc. but terms of an abstract syntax for the language of primitive recursive functions. The bridge between this language and the word of usual functions is an interpretation function (\texttt{evalprimRec $n$}) of type $\texttt{PrimRec}\,n \rightarrow \texttt{naryFunc}\,n$. This function is defined by mutual recursion, together with the function -(\texttt{evalprimRecS $n$ $m$}) of type +(\texttt{evalprimRecS $n$ $m$}) of type \linebreak ($\texttt{PrimRecs}\,n\,m \rightarrow \texttt{Vector.t}\,(\texttt{naryFunc}\,n)\,m$). \index{ackermann}{Functions!evalPrimRec} diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex index bb03c049..a517382a 100644 --- a/doc/epsilon0-chapter.tex +++ b/doc/epsilon0-chapter.tex @@ -1,6 +1,6 @@ %------------------------------------------------------------------------ -\chapter[A proof of termination, using epsilon0]{A proof of termination, using ordinals below \texorpdfstring{$\epsilon_0$}{Epsilon0}} +\chapter[The ordinal epsilon0]{The Ordinal \texorpdfstring{$\epsilon_0$}{Epsilon0}} \label{cnf-math-def} \label{chap:T1} @@ -817,7 +817,8 @@ \subsection{An ordinal notation for \gaia's ordinals} \section{An ordinal notation for \texorpdfstring{$\omega^\omega$}{omega\^omega}} - + \label{sect:omegaomega} + In Module \href{https://github.com/coq-community/hydra-battles/blob/master/theories/ ordinals/OrdinalNotations/OmegaOmega.v}{theories/ordinals/OrdinalNotations/OmegaOmega.v}, we represent ordinals below $\omega^\omega$ by lists of pairs of natural numbers (with the same coefficient shift as in \texttt{T1}). diff --git a/doc/ordinal-chapter.tex b/doc/ordinal-chapter.tex index 0d4f9cf7..ad285a11 100644 --- a/doc/ordinal-chapter.tex +++ b/doc/ordinal-chapter.tex @@ -933,14 +933,6 @@ \subsubsection{See also \dots} \inputsnippets{ON_gfinite/Examples, ON_gfinite/Examplesb} - - - - - - - - %%% \section{Comparing two ordinal notations} @@ -1194,5 +1186,9 @@ \section{Other ordinal notations} The set of ordinal terms in Cantor normal form (see Chap.~\ref{chap:T1}) and in Veblen normal form (see \href{../theories/html/hydras.Gamma0.Gamma0.html}{Gamma0.Gamma0}) are shown to be ordinal notation systems, but there is a lot of work to be done in order to unify ad-hoc definitions and proofs which were written before the definition of the \texttt{ON} type class. + + +In Section~\vref{sect:omegaomega}, we present a notation system for the ordinal $\omega^\omega$ as a \emph{refinement} +of the ordinal notation for $\epsilon_0$. \end{remark} diff --git a/theories/ordinals/Ackermann/primRec.v b/theories/ordinals/Ackermann/primRec.v index b8d1b526..df1ce23b 100644 --- a/theories/ordinals/Ackermann/primRec.v +++ b/theories/ordinals/Ackermann/primRec.v @@ -31,6 +31,7 @@ with PrimRecs : nat -> nat -> Set := (* end snippet PrimRecDef *) + Notation "f '=x=' g" := (extEqual _ f g) (at level 70, no associativity). diff --git a/theories/ordinals/MoreAck/PrimRecExamples.v b/theories/ordinals/MoreAck/PrimRecExamples.v index 2498a04f..7bfdb1cc 100644 --- a/theories/ordinals/MoreAck/PrimRecExamples.v +++ b/theories/ordinals/MoreAck/PrimRecExamples.v @@ -38,7 +38,7 @@ Check (fun n p q : nat => n * p + q): naryFunc 3. (* begin snippet extEqual2a *) Compute extEqual 2. -Example extEqual_ex1: extEqual 2 Nat.mul (fun x y => y * x + x - x). (* .no-out *) +Example extEqual_ex1: (Nat.mul: naryFunc 2) =x= fun x y => y * x + x - x. (* .no-out *) Proof. intros x y; cbn. (* end snippet extEqual2a *) @@ -119,10 +119,10 @@ End compose2Examples. (* begin snippet FirstExamples *) Module MoreExamples. -(** The constant function which returns 0 *) +(** The unary constant function which returns 0 *) Definition cst0 : PrimRec 1 := (PRcomp zeroFunc (PRnil _))%pr. -(** The constant function which returns i *) +(** The unary constant function which returns i *) Fixpoint cst (i: nat) : PrimRec 1 := match i with 0 => cst0 @@ -170,23 +170,21 @@ Compute PReval fact 5. (* end snippet tests *) (* begin snippet correctness:: no-out *) -Lemma cst0_correct (i:nat) : - forall p:nat, PReval cst0 p = 0. -Proof. intro p; reflexivity. Qed. +Lemma cst0_correct : (PReval cst0) =x= (fun _ => 0). +Proof. intros ?; reflexivity. Qed. -Lemma cst_correct (i:nat) : - forall p:nat, PReval (cst i) p = i. +Lemma cst_correct (k:nat) : PReval (cst k) =x= (fun _ => k). Proof. - induction i as [| i IHi]; simpl; intros p . + induction k as [| k IHk]; simpl; intros p. - reflexivity. - - now rewrite IHi. + - now rewrite IHk. Qed. Lemma plus_correct: - forall n p, PReval plus n p = n + p. + PReval plus =x= Nat.add. Proof. - induction n as [ | n IHn]. - - reflexivity. + intros n; induction n as [ | n IHn]. + - intro; reflexivity. - intro p; cbn in IHn |- *; now rewrite IHn. Qed. @@ -195,19 +193,19 @@ Remark mult_eqn1 n p: PReval plus (PReval mult n p) p. Proof. reflexivity. Qed. -Lemma mult_correct n p: PReval mult n p = n * p. +Lemma mult_correct: PReval mult =x= Nat.mul. Proof. - revert p; induction n as [ | n IHn]. + intro n; induction n as [ | n IHn]. - intro p; reflexivity. - - intro p; rewrite mult_eqn1, IHn, plus_correct; ring. + - intro p; rewrite mult_eqn1, (IHn p) , plus_correct. cbn. ring. Qed. -Lemma fact_correct n : PReval fact n = Coq.Arith.Factorial.fact n. +Lemma fact_correct : PReval fact =x= Coq.Arith.Factorial.fact. (* ... *) (* end snippet correctness *) Proof. - assert (fact_eqn1: forall n, PReval fact (S n) = + intro n; assert (fact_eqn1: forall n, PReval fact (S n) = PReval mult (PReval fact n) (S n)) by reflexivity. @@ -228,9 +226,8 @@ Definition PRcompose1 (g f : PrimRec 1) : PrimRec 1 := PRcomp g [f]%pr. Goal forall f g x, evalPrimRec 1 (PRcompose1 g f) x = - evalPrimRec 1 g (evalPrimRec 1 f x). -reflexivity. -Qed. + evalPrimRec 1 g (evalPrimRec 1 f x). +Proof. reflexivity. Qed. Remark compose2_0 (a:nat) (g: nat -> nat) : compose2 0 a g = g a. Proof. reflexivity. Qed.