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 6b246ebb..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} @@ -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} @@ -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 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} -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} @@ -726,6 +730,7 @@ \subsubsection{Using a stronger inductive predicate.} \input{movies/snippets/T1/T1Wf} +\subsection{Transfinite induction} \index{maths}{Transfinite induction} @@ -812,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/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 7ac6252c..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. @@ -825,19 +821,18 @@ Ltac nf_decomp H := | nf (cons ?t1 ?n ?t2) => assert (nf0 := nf_inv1 H); assert(nf1 := nf_inv2 H) end. -(** lt alpha (phi0 beta) *) -(** Should be deprecated *) - -Inductive nf_helper : T1 -> T1 -> Prop := -| nf_helper_z : forall alpha, nf_helper zero alpha -| nf_helper_c : forall alpha alpha' n' beta', +(** 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 -> - 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" := 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 @@ -892,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. @@ -1005,7 +999,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. @@ -1146,17 +1140,13 @@ Proof. - intros n0 a H; apply head_lt; eapply nf_inv3; eauto. Qed. -Lemma nf_helper_inv1 : - forall a n b a', - nf_helper (cons a n b) a' -> lt a a'. +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. 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' : @@ -1169,12 +1159,12 @@ 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 : - forall a n b, nf (cons a n b) -> nf_helper b a. +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. destruct b. @@ -1192,30 +1182,40 @@ 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 : - forall a b, nf_helper b a -> lt b ( phi0 a). +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) -> b <_phi0 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_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 -> - (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. - - 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). @@ -1229,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)-> - nf_helper b' (cons a n b) -> + lt b' (phi0 (cons a n b)) -> nf b' -> P b' -> P (cons (cons a n b) n' b')) -> @@ -1242,7 +1242,8 @@ Proof. + intros c n0 c0 IHc0 H2; apply Hcons. * eapply nf_inv1;eauto. * apply IHc0; eapply nf_inv1; eauto. - * eapply nf_helper_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. @@ -1640,7 +1641,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,65 +1655,70 @@ 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) *) (*| .. coq:: -.h#Acc_strong |*) - unfold Acc_strong; intros alpha Aalpha; pattern alpha; - eapply Acc_ind with (R:= LT);[| assumption]; + unfold Acc_strong; intros alpha Aalpha. + pattern alpha; + 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, nf_helper beta 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 + 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 nf_helper_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 nf_helper_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. @@ -1751,14 +1757,12 @@ Module Direct_proof. * subst n0 c;apply H1; auto. case H3;auto. - apply beta_Acc. - + eapply nf_helper_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 *) @@ -1769,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. @@ -1832,8 +1836,8 @@ Ltac transfinite_induction alpha := (** ** Properties of successor *) (* 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). +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. - simpl; repeat constructor. @@ -1852,7 +1856,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 +1965,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 +2037,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 +2834,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 +3206,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 +3500,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 +3659,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/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. 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 ...