Tutorial, Equations: Basics

Tutorial_Equations_basics.v

@@ -7,7 +7,7 @@ Arguments to_fill {_}.
 
 (** * Tutorial Equations : Basic Definitions and Reasoning with Equations
 
-  *** Summary:
+  *** Summary
   [Equations] is a plugin for Coq that offers a powerful support
   for writing functions by dependent pattern matching, possibly using
   well-founded recursion and obligations.
@@ -26,17 +26,17 @@ Arguments to_fill {_}.
   pattern matching.
 
 
-  *** Table of content:
+  *** Table of content
 
   - 1. Basic definitions and reasoning
     - 1.1 Defining functions by dependent pattern matching
     - 1.2 Reasoning with [Equations]
   - 2. [With] clauses
   - 3. [Where] clauses
 
-  *** Prerequisites:
+  *** Prerequisites
 
-  Needed :
+  Needed:
   - We assume known basic knowledge of Coq, of and defining functions by recursion
 
   Installation:
@@ -70,15 +70,15 @@ Arguments nil {_}.
 Arguments cons {_} _ _.
 
 (** To write a function [f : list A -> B] on lists or another a basic
-      inductive type, it suffices to write :
+      inductive type, it suffices to write:
     - Equation at the beginning of you function rather than Fixpoint
     - For each constructor [cst x1 ... xn] like [cons a l], specify how [f]
       computes on it by writing [f (cst x1 ... xn) := t] where [t] may
       contain [f] recursively.
     - Separate the different cases by semi-colon "[;]"
     - As usual finish you definition by a dot "[.]"
 
-  For instance, we can define the function [tail], [length] and [map] by :
+  For instance, we can define the function [tail], [length] and [app] by:
 *)
 
 Equations tail {A} (l : list A) : list A :=
@@ -97,16 +97,16 @@ Infix "++" := app (right associativity, at level 60).
 
 
 (** [Equations] is compatible with usual facilities provided by Coq to write
-    terms :
+    terms:
     - It is compatible with implicit arguments that as usual do not need to
       be written provided it can be inferred, for instance, above, we wrote
-      [map f nil] rather than [map f (nil A)] as [A] was declared as an
+      [app nil l'] rather than [map (nil A) l'] as [A] was declared as an
       implicit argument of [nil].
     - We can use the underscores "_" for terms that we do not use, terms
       that Coq can infer on its own, but also to describe what to do in all
       remaining cases of our pattern matching.
       As [list] only two has constructors to it is not really useful here,
-      but we can still see it works by defining a constant function :
+      but we can still see it works by defining a constant function:
 *)
 
 Equations cst_b {A B} (b : B) (l : list A) : B :=
@@ -116,7 +116,7 @@ cst_b b (_) := b.
       side of :=) or in the bodies of the function (on the right-hand side
       of :=). This provides an easy and very visual way to define functions.
       For instance, with the usual notations for lists, we can redefine
-      [length] and [map] as :
+      [length] and [app] as:
 *)
 
 Notation "[]" := nil.
@@ -165,7 +165,7 @@ Proof.
   autorewrite with nth_option'.
 Abort.
 
-(** As exercices, you can try to define :
+(** As exercices, you can try to define:
     - A function [map f l] that applies [f] pointwise, on [ [a, ... ,a] ] it
       returns [ [f a1, ... , f an] ]
     - A function [head_option] that returns the head of a list and [None] otherwise
@@ -174,14 +174,23 @@ Abort.
 *)
 
 Equations map {A B} (f : A -> B) (l : list A) : list B :=
-map f _ := to_fill.
+map f nil := nil ;
+map f (a::l) := (f a)::(map f l).
 
 Equations head_option {A} (l : list A) : option A :=
 head_option _ := to_fill.
 
 Equations fold_right {A B} (f : A -> B -> B) (b : B) (l : list A) : B :=
 fold_right f b _ := to_fill.
 
+(* You can uncomment the following tests to try your functions *)
+(*
+Succeed Example testing : map (Nat.add 1) (1::2::3::4::[]) = (2::3::4::5::[])
+  := eq_refl.
+Succeed Example testing : @head_option nat [] = None := eq_refl.
+Succeed Example testing : head_option (1::2::3::[]) = Some 1 := eq_refl.
+Succeed Example testing : fold_right Nat.mul 1 (1::2::3::4::[]) = 24 := eq_refl.
+*)
 
 
 (** ** 1.2 Reasoning with Equations  *)
@@ -292,7 +301,7 @@ Abort.
 
     As an example, let's prove [app_nil], [app_assoc], and [nth_eq] for
     which we can already see the advantages over trying to reproduce the
-    pattern matching by hand :
+    pattern matching by hand:
 *)
 
 Lemma app_nil {A} (l : list A) : l ++ [] = l.
@@ -319,7 +328,7 @@ Proof.
   - apply H.
 Abort.
 
-(** By default, the tactic [autorewrite with f] only simplify a term by the
+(** By default, the tactic [autorewrite with f] only simplifies a term by the
     equations defining [f], like [[] ++ l = l] for [app].
     Yet, in practice, it often happens that there are more equations
     that we have proven that we would like to automatically simplify by
@@ -328,7 +337,7 @@ Abort.
     by [app_nil : l + [] = l] or [app_assoc : (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)].
     It is possible to extend [autorewrite] to make it automatic by adding
     lemma to the database associated to [f].
-    This can be done by the syntax :
+    This can be done by the syntax:
 
       [ #[local] Hint Rewrite @name_lemma : name_function. ]
 
@@ -337,7 +346,7 @@ Abort.
     to become non terminating if one adds the right lemma.
 
     To see how it can be useful, let's define a tail-recursive version of
-    list reversal and prove it equal the usual one :
+    list reversal and prove it equal the usual one:
 *)
 
 Equations rev {A} (l : list A) : list A :=
@@ -387,8 +396,8 @@ Abort.
 
     Linking [simpl] with [funelim] like [funelim sth ; simp f1 ... fn] then
     enables us to simplify all the goals and at the same to automatically
-    prove uninterresting ones.
-    As examples, let's reprove [nth_eq] and [rev_rev_acc] :
+    prove uninteresting ones.
+    As examples, let's prove again [nth_eq] and [rev_rev_acc]:
 *)
 
 Definition nth_eq {A} (l : list A) (n : nat) : nth_option n l = nth_option' l n.
@@ -416,7 +425,10 @@ Lemma nth_overflow {A} (n : nat) (l : list A) : length l <= n -> nth_option n l
 Proof.
 Admitted.
 
-(* You will need to use the lemma [Arith_prebase.lt_S_n] *)
+(* You will need to use the lemma [Arith_prebase.lt_S_n]
+  HINT : [funelim] must be applied to the parameters you are doing the induction on.
+         Here, it is [n] and [l], and not [n] and [l++l'].
+*)
 Lemma app_nth1 {A} (n : nat) (l l' : list A) :
       n < length l -> nth_option n (l++l') = nth_option n l.
 Proof.
@@ -440,8 +452,8 @@ Admitted.
 
 (** ** 1.2 With clauses
 
-    The structure of real programs is richer than a simple case tree on the
-    original arguments in general.
+    The structure of real programs is generally richer than a simple case tree on the
+    original arguments.
     In the course of a computation, we might want to compute or scrutinize
     intermediate results (e.g. coming from function calls) to produce an answer.
     In terms of dependent pattern matching, this literally means adding a new
@@ -451,7 +463,7 @@ Admitted.
 
     [With] clause are available in [Equations] with the following syntax
     where [b] is the term we wish to inspect, and [p1 ... pk] the patterns we
-    match [b] to :
+    match [b] to:
 
     [[
       f (cxt x1 ... xn) with b => {
@@ -465,7 +477,7 @@ Admitted.
     predicate [p].
     In the case [cons a l], the [with] clause enables us to compute
     the intermediate value [p a] and to check whether it is [true] or [false],
-    and hence if [a] verify the predicate [p] and should be kept or not :
+    and hence if [a] verify the predicate [p] and should be kept or not:
 *)
 
 Equations filter {A} (l : list A) (p : A -> bool) : list A :=
@@ -485,7 +497,7 @@ filter (cons a l) p with p a => {
     introduced by the [with] clause.
 
     This enables to rewrite the [with] clause of the function filter
-    much more concisely :
+    much more concisely:
 *)
 
 Equations filter' {A} (l : list A) (p : A -> bool) : list A :=
@@ -514,10 +526,10 @@ In x [] => False ;
 In x (a::l) => (x = a) \/ In x l.
 
 (** For function defined using [with] clauses, [funelim] does the usual
-    disjunction of cases for us, and additionally destruct the pattern
+    disjunction of cases for us, and additionally destructs the pattern
     associated to the |with] clause and remembers it.
     In the case of [filter], it means additionally destructing [p a] and
-    remembering  whether [p a = true] or [p a = false].
+    remembering whether [p a = true] or [p a = false].
 
     For regular patterns, simplifying [filter] behaves as usual.
     For the [with] clause, simplifying [filter] makes a subclause
@@ -539,7 +551,7 @@ Proof.
 Qed.
 
 (** [With] clauses can also be useful to inspect a recursive call.
-    For instance, with clause enables us to define a particularly concise
+    For instance, [with] clause enables us to write a particularly concise
     definition of the [unzip] function:
 *)
 
@@ -551,7 +563,7 @@ unzip ((a,b)::l) with unzip l => {
 
 (** They can also be useful to discard impossible branches.
     For instance, rather than returning an option type, we can define a
-    [head] function by requiring that its input is different than the
+    [head] function by requiring for the input to be different than the
     empty list.
     In the [nil] case, we can then destruct [pf eq_refl : False] which
     as no constructors to define our function.
@@ -561,21 +573,14 @@ Equations head {A} (l : list A) (pf : l <> nil) : A :=
 head [] pf with (pf eq_refl) := { };
 head (a::l) _ := a.
 
-(** As exercices, you can try to :
+(** As exercices, you can try to:
+    - Prove that both head functions are equal up to [Some]
+    - Prove that a filtered list has a smaller length than the original one
     - Define a function [find_dictionary] that given a key and an
-      equality test, return the first element associated to the key and
+      equality test, returns the first element associated to the key and
       [None] otherwise
-    - Prove that both head functions are equal up to [Some]
-    - Prove that a filtered list is small than the original one
 *)
 
-Equations find_dictionary {A B} (eq : A -> A -> bool) (key : A)
-          (l : list (A * B)) : option B :=
-find_dictionary eq key [] := to_fill;
-find_dictionary eq key _ with to_fill => {
-  | _ := to_fill
-}.
-
 Definition head_head {A} (l : list A) (pf : l <> nil)
            : Some (head l pf) = head_option l.
 Proof.
@@ -587,6 +592,20 @@ Definition filter_length {A} (l : list A) (p : A -> bool)
 Proof.
 Admitted.
 
+Equations find_dictionary {A B} (eq : A -> A -> bool) (key : A)
+          (l : list (A * B)) : option B :=
+find_dictionary eq key [] := to_fill;
+find_dictionary eq key _ with to_fill => {
+  | _ := to_fill
+}.
+
+(* You can uncomment the following tests to try your function *)
+(* Definition example_dictionnary :=
+  (3,true::true::[]) :: (0,[]) :: (2,true::false::[]) :: (1,true::[]) :: [].
+Succeed Example testing :
+  find_dictionary Nat.eqb 2 example_dictionnary = Some (true::false::[]) := eq_refl.
+Succeed Example testing :
+  find_dictionary Nat.eqb 4 example_dictionnary = None := eq_refl. *)
 
 
 
@@ -645,7 +664,7 @@ Abort.
     - We can automatically deal with [app_nil] and [app_assoc] by adding
       them to simplification done by [autorewrite] as done in 1.1.2
     - We can combine that with a proof search using [simp]
-    This enables to rewrite the proof to :
+    This enables to rewrite the proof to:
 *)
 
 Lemma rev_acc_rev {A} (l : list A) : rev_acc' l = rev l.