Corrections to chapter 11 (primitive recursive functions)

doc/chapter-primrec.tex

@@ -563,20 +563,30 @@ \subsubsection{The minimum of two natural numbers}
 \end{exercise}
 
 \index{ackermann}{Exercises}
-\begin{exercise}
+\begin{exercise}[The integer square root]
+
+\mbox{}
+\vspace{4pt}
+
+\noindent
+ \textbf{1)} 
+Please consider the following specification of the function \texttt{boundedSearch} defined in 
+\href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec}.
+
+\inputsnippets{isqrt/boundedSearchSpec}
 
-Prove the following lemmas (which may help to solve the next  exercise).
+Prove the following lemmas.
 
 \inputsnippets{isqrt/boundedSearch3, isqrt/boundedSearch4}
 
-\textbf{Note:}  The function \texttt{boundedSearch} is defined
-in Library \href{../theories/html/hydras.Ackermann.primRec.html}{Ackermann.primRec}. 
-\end{exercise}
+\noindent
+\textbf{2)} 
+Let us consider the following definition of the relation `` $r$ is the integer square root of $n$ ''.
 
-\index{ackermann}{Exercises}
+\inputsnippets{isqrt/isqrtSpec}
 
-\begin{exercise}
-Prove that the function which returns the  integer square root of any natural number  is primitive recursive.
+Prove that the function which returns the  integer square root of any natural number  is primitive recursive (you may use 
+the function \texttt{boundedSearch} for this purpose).
 
 \emph{You may start this exercise with the file
     \href{https://github.com/coq-community/hydra-battles/blob/master/exercises/primrec/isqrt.v}{exercises/primrec/isqrt.v}.}
@@ -591,6 +601,11 @@ \section{Proving that a given function is \emph{not} primitive recursive}
 the treatment of primitive recursive functions by R. O'Connor,
 and to play with dependent types.
 
+With respect to proof methods, we will see a first \emph{proof by induction on the set of all primitive recursive functions}.
+First, we will prove a property shared by all primitive function, 
+then show that the Ackermann function doesn't satisfy this property.
+
+
 \subsection{Ackermann function}
 
 Ackermann function is traditionally defined as a function from 

exercises/primrec/isqrt.v

@@ -7,6 +7,11 @@
 From hydras Require Import  primRec extEqualNat.
 From Coq Require Import Min ArithRing Lia Compare_dec Arith Lia.
 
+(* begin snippet boundedSearchSpec *)
+Check boundedSearch.
+Search boundedSearch.
+(* end snippet boundedSearchSpec *)
+
 
 
 (** Please consider the following specification of the integer square root *)
@@ -19,7 +24,7 @@ Definition isqrt_spec n r := r * r <= n < S r * S r.
 Section sqrtIsPR.
 
 Let P (n r: nat) :=  Nat.ltb n (S r * S r).
-Definition isqrt  := boundedSearch P . 
+Definition isqrt  := boundedSearch P. 
 
 Lemma sqrt_correct (n: nat) : isqrt_spec n (isqrt n).
 Admitted.

theories/ordinals/MoreAck/PrimRecExamples.v

@@ -1,17 +1,13 @@
-Require Import Arith ArithRing List.
-Require Import Vector.
-Require Import Utf8.
+From Coq Require Import Arith ArithRing List Vector Utf8.
 Import VectorNotations.
 
-Require Import primRec cPair.
-Import extEqualNat.
-Import PRNotations.
+From hydras Require Import primRec cPair.
+Import extEqualNat PRNotations.
+
 (* begin snippet naryFunc3 *)
 Compute naryFunc 3.
 (* end snippet naryFunc3 *)
 
-
-
 (* begin snippet naryRel2 *)
 Check leBool : naryRel 2.
 
@@ -42,7 +38,6 @@ 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 *)
 Proof. 
   intros x y; cbn.
@@ -65,7 +60,7 @@ Qed.
 Example Ex1 : PReval zeroFunc = 0.
 Proof. reflexivity. Qed.
 
-Example Ex2 a : PReval succFunc a = S a.
+Example Ex2 a : PReval succFunc a = a.+1.
 Proof. reflexivity. Qed.
 
 Example Ex3 a b c d e f: forall (H: 2 < 6),
@@ -110,11 +105,13 @@ End Primitive_recursion.
 (* end snippet evalPrimRecEx  *)  
 
 Section compose2Examples.
-Variables (f: naryFunc 1) (g: naryFunc 2).
+Variables (f: naryFunc 1) (g: naryFunc 2) (h: naryFunc 3)
+  (f': naryFunc 4) (g': naryFunc 5). 
+
 Eval simpl in compose2 1 f g.
-Variable (h: naryFunc 3). 
+
 Eval simpl in compose2 2 g h. 
-Variables (f': naryFunc 4) (g': naryFunc 5).
+
 Eval simpl in compose2 _ f' g'.
 End compose2Examples.
 
@@ -235,10 +232,6 @@ Goal forall f g x, evalPrimRec 1 (PRcompose1 g f) x =
 reflexivity. 
 Qed.
 
-(** Note : see lemma compose1_1IsPR  *)
-
-
-
 Remark compose2_0 (a:nat) (g: nat -> nat)  : compose2 0 a g = g a.
 Proof.   reflexivity. Qed.
 
@@ -464,7 +457,7 @@ Qed.
 
 (* Move to MoreAck *)
 
-Section Exs. (* Todo: exercise *)
+Section Exs. 
 Let f: naryFunc 2 := fun x y => x + pred (cPairPi1 y).
 
   (* To prove !!! *)

theories/ordinals/solutions_exercises/isqrt.v

@@ -1,12 +1,18 @@
 (* @todo  add as an exercise *)
 
-(** Returns smallest value of x less or equal than b such that (P b x). 
-    Otherwise returns b  *)
 
 
-From hydras Require Import  primRec extEqualNat.
+
+From hydras Require Import  primRec extEqualNat ssrnat_extracts.
 From Coq Require Import Min ArithRing Lia Compare_dec Arith Lia.
 
+(** Returns smallest value of x less or equal than b such that (P b x). 
+    Otherwise returns b  *)
+(* begin snippet boundedSearchSpec *)
+Check boundedSearch.
+Search boundedSearch.
+(* end snippet boundedSearchSpec *)
+
 
 (* begin snippet boundedSearch3:: no-out *)
 Lemma boundedSearch3 :
@@ -34,8 +40,9 @@ Proof.
   now rewrite H0.
 Qed.
 
-
-Definition isqrt_spec n r := r * r <= n < S r * S r.
+(* begin snippet isqrtSpec *)
+Definition isqrt_spec n r := r * r <= n < r.+1 * r.+1.
+(* end snippet isqrtSpec *)
 
 Section sqrtIsPR.
 
@@ -48,10 +55,10 @@ Section sqrtIsPR.
     Remark R00 : P n (isqrt n) = true.
     Proof.
       apply boundedSearch4.
-      unfold P; cbn;  apply leb_correct; lia.
+      unfold P; cbn; apply leb_correct; lia.
     Qed.
 
-    Lemma R01 : n < S (isqrt n) * S (isqrt n).
+    Lemma R01 :  n < (isqrt n).+1 * (isqrt n).+1.
     Proof.
       generalize R00; intro H; apply leb_complete in H; auto.
     Qed.
@@ -108,10 +115,12 @@ Qed.
 
 End sqrtIsPR.
 
-(** slow! *)
-
 Compute isqrt 22.
 
+Compute isqrt 26.
+
+
+
 (** Extra work :
    Define a faster implementation of [sqrt_spec], and prove your function is 
    extensionnaly equal to [isqrt] (hence PR!)