diff --git a/doc/chapter-primrec.tex b/doc/chapter-primrec.tex index 8590b4ab..f9218b06 100644 --- a/doc/chapter-primrec.tex +++ b/doc/chapter-primrec.tex @@ -413,18 +413,10 @@ \subsubsection{Using function composition} Let us look at the proof that any constant $n$ of type \texttt{nat} has type (\texttt{PR 0}) (lemma \texttt{const0\_NIsPR} of \texttt{primRec}). We carry out a proof by induction on $n$, the base case of which is already proven. -Now, let us assume $n$ is \texttt{PR $0$}, with $x:\texttt{PrimRec}\,0$ as a ``realizer''. +Now, let us assume $n$ is \texttt{PR $0$}, and call $(x:\texttt{PrimRec}\,0)$ its ``realizer''. Thus we would like to compose this constant function with the unary successor function. -This is exactly the role of the instance \texttt{composeFunc 0 1} of the dependently typed -function \texttt{composeFunc}, as shown by the following lemma. - -\vspace{4pt} -\input{movies/snippets/PrimRecExamples/compose01} - - -\vspace{4pt} -Here is a quite simple proof of \texttt{const0\_NIsPR}. +This is exactly the role of the function \texttt{(composeFunc 0 1)}. Here is a quite simple proof of \texttt{const0\_NIsPR}. \vspace{4pt} @@ -435,13 +427,13 @@ \subsubsection{Using function composition} \subsubsection{Another proof that \texttt{Nat.add} is primitive recursive} -We have already proven that \texttt{Nat.add} is primitive recursive. The following alternative proof, --- more detalled ---, +We have already proven that \texttt{Nat.add} is primitive recursive. The following alternative proof, --- more detailed ---, shows how to search and apply lemmas from the \texttt{Ackermann} library. -Let us look for some lemma which could help to prove some +Let us look for some lemma which could help to prove a given recursive arithmetic binary function is primitive recursive. \inputsnippets{PrimRecExamples/PRnatRecSearch} diff --git a/doc/hydras.tex b/doc/hydras.tex index 375c3980..4c2ccc8a 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/theories/ordinals/Ackermann/primRec.v b/theories/ordinals/Ackermann/primRec.v index df1ce23b..00935373 100644 --- a/theories/ordinals/Ackermann/primRec.v +++ b/theories/ordinals/Ackermann/primRec.v @@ -231,6 +231,11 @@ Fixpoint evalPrimRec (n : nat) (f : PrimRec n) {struct f} : Notation PReval f := (evalPrimRec _ f). Notation PRevalN fs := (evalPrimRecs _ _ fs). +(** [p] is a correct implementation of [f] in [PrimRec n] *) + +Definition PRcorrect {n:nat}(p:PrimRec n)(f: naryFunc n) := + PReval p =x= f. + (* end snippet evalPrimRecDef *) Definition extEqualVectorGeneral (n m : nat) (l : Vector.t (naryFunc n) m) : @@ -331,7 +336,7 @@ Qed. Class isPR (n : nat) (f : naryFunc n) : Set := is_pr : {p : PrimRec n | extEqual n (PReval p) f}. -Definition fun2PR {n:nat}(f: naryFunc n) +Definition fun2PR {n:nat}(f: naryFunc n) {p: isPR _ f}: PrimRec n := proj1_sig p. Class isPRrel (n : nat) (R : naryRel n) : Set := diff --git a/theories/ordinals/MoreAck/PrimRecExamples.v b/theories/ordinals/MoreAck/PrimRecExamples.v index 7bfdb1cc..70068840 100644 --- a/theories/ordinals/MoreAck/PrimRecExamples.v +++ b/theories/ordinals/MoreAck/PrimRecExamples.v @@ -170,18 +170,18 @@ Compute PReval fact 5. (* end snippet tests *) (* begin snippet correctness:: no-out *) -Lemma cst0_correct : (PReval cst0) =x= (fun _ => 0). + +Lemma cst0_correct : PRcorrect cst0 (fun _ => 0). Proof. intros ?; reflexivity. Qed. -Lemma cst_correct (k:nat) : PReval (cst k) =x= (fun _ => k). +Lemma cst_correct (k:nat) : PRcorrect (cst k) (fun _ => k). Proof. induction k as [| k IHk]; simpl; intros p. - reflexivity. - - now rewrite IHk. + - cbn; now rewrite IHk. Qed. -Lemma plus_correct: - PReval plus =x= Nat.add. +Lemma plus_correct: PRcorrect plus Nat.add. Proof. intros n; induction n as [ | n IHn]. - intro; reflexivity. @@ -193,7 +193,7 @@ Remark mult_eqn1 n p: PReval plus (PReval mult n p) p. Proof. reflexivity. Qed. -Lemma mult_correct: PReval mult =x= Nat.mul. +Lemma mult_correct: PRcorrect mult Nat.mul. Proof. intro n; induction n as [ | n IHn]. - intro p; reflexivity. @@ -201,7 +201,7 @@ Proof. Qed. -Lemma fact_correct : PReval fact =x= Coq.Arith.Factorial.fact. +Lemma fact_correct : PRcorrect fact Coq.Arith.Factorial.fact. (* ... *) (* end snippet correctness *) Proof. @@ -222,14 +222,13 @@ Qed. These lemmas are trivial and theoretically useless, but they may help to make the construction more concrete *) -Definition PRcompose1 (g f : PrimRec 1) : PrimRec 1 := - PRcomp g [f]%pr. +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). Proof. reflexivity. Qed. -Remark compose2_0 (a:nat) (g: nat -> nat) : compose2 0 a g = g a. +Remark compose2_0 (a:nat) (g: nat -> nat) : compose2 0 a g = g a. Proof. reflexivity. Qed. Remark compose2_1 (f: nat -> nat) (g : nat -> nat -> nat) x @@ -349,16 +348,13 @@ Proof. reflexivity. Qed. #[export] Instance const0_NIsPR n : isPR 0 n. (* .no-out *) Proof. (* .no-out *) - induction n. (* .no-out *) - - apply zeroIsPR. (* .no-out *) - - destruct IHn as [x Hx]. - exists (PRcomp succFunc [x])%pr; cbn in *; intros; - now rewrite Hx. + induction n as [ | n [x Hx]]. + - (* .no-out *) apply zeroIsPR. + - (* .no-out *) exists (composeFunc _ _ [x] succFunc)%pr; cbn in *; intros; + now rewrite Hx. (* .no-out *) Qed. (* end snippet const0NIsPR *) - - (* begin snippet PRnatRecSearch *) Search (isPR 2 (fun _ _ => nat_rec _ _ _ _)). (* end snippet PRnatRecSearch *)