small corrections

Author: Casteran

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}

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}

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 :=

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,15 +193,15 @@ 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. 
  - intro p; rewrite mult_eqn1, (IHn p) , plus_correct. cbn. ring.
 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 *)