The Coq mailing list

[David Pichardie <david.pichardie AT ens-rennes.fr>]

I like to use an example with efficient data structures, without maths and 
with good automatisation.

David
=============
(** You need Coq 8.4 and a Coq IDE like CoqIDE or the 
  Proof General emacs-mode *)

(** Our first Coq programs *)

(** In this tutorial will implements simple maps *)
Module Type MAP.
  (** the type of map keys *)
  Parameter key : Type.
  (** the type of map elements *)
  Parameter elt : Type.
  (** the type of maps *)
  Parameter t : Type.

  (** [default] is the default element in a map *)
  Parameter default: elt.

  (** [get m k] returns the elements that is binded with key [k] *)
  Parameter get: t -> key -> elt.

  (** [empty] is a map that binds every keys to [default] *)
  Parameter empty: t.

  (** [set m k e] returns a new map that contains the same
      bindings as map [m] except for key [k] that is now binded with 
      the element [e] *)
  Parameter set: t -> key -> elt -> t.
End MAP.
(** Observe that we use the same keyword for types and operators.
    What we think as types here, are term of type [Type]. *)

(** To implement this interface, we will need some basic data structures *)

(** Peano natural numbers *)
Inductive nat :=
 | O            (* zero is a nat *)
 | S (n:nat)    (* a successor of a nat is a nat *)
.

(** In Ocaml we would have written [type nat = | O | S of nat] *)

(** [nat] is a type. It is inhabited by terms 
    like O, (S O), (S (S O)), ... *)

(** The command [Check] gives the type of a term. *)

Check O.
Check (S (S (S (S O)))).

(** Coq already provides this basic data structure in its
    library. We will remove our version and load Coq's
     version instead. *)

Reset nat. 
Require Import Arith.

Check O.
Check (S (S (S (S O)))).
(** Observe that Coq now pretty-prints our terms in 
    the *response* window *)

(** We will also use other data structures like list and string.
    We load the corresponding libraries but we do not detail their
    content here *)
Require Import String.
Require Import List.
Open Scope string_scope. (* Will facilitate string input *)


(** We now begin the implementation of a MAP interface for the
  special case were keys are natural numbers and elements are string *)
Module NatStringMap <: MAP 
                 with Definition key := nat
                 with Definition elt := string.

 Definition key := nat.
 Definition elt := string.

 (** A map will be a list of string [s_0 :: ... :: s_n]  where
   a number [i] is binded with [s_i] if [i <= n] or with the 
   default element otherwise *)  
 Definition t := list string.

 (** Note: a list is either the empty list [nil]
    or a non-empty list of the form [x :: q] with 
      [x] the head of the list and
      [q] the queue of the list
 *)

 (* We arbitrarily choose the empty string as the default element *)
 Definition default := "".

 Fixpoint get (l:list string) (n:nat) : string :=
   match l, n with
     | nil, _ => default
     | x::_, O => x
     | _::q, S m => get q m
    end.

 Definition empty : t := nil.

 Fixpoint set (l:list string) (n:nat) (s:string) : list string :=
   match l, n with
     | nil, O => s :: nil
     | nil, S m => default :: set nil m s
     | _ :: q, O => s :: q
     | x :: q, S m => x :: set q m s
    end.
End NatStringMap.


Notation "m [ k ]" := (NatStringMap.get m k) (at level 20).
Notation "m +{ k ↦ e }" := (NatStringMap.set m k e) (at level 20).
Notation "{}" := (NatStringMap.empty) (at level 20).


Compute ({} +{0 ↦ "zero" } +{2 ↦ "two" } +{3 ↦ "three" } [4]).
Compute ({} +{0 ↦ "zero" } +{2 ↦ "two" } +{3 ↦ "three" } [3]).
Compute ({} +{0 ↦ "zero" } +{2 ↦ "two" } +{3 ↦ "three" } [2]).
Compute ({} +{0 ↦ "zero" } +{2 ↦ "two" } +{3 ↦ "three" } [1]).
Compute ({} +{0 ↦ "zero" } +{2 ↦ "two" } +{3 ↦ "three" } [0]).

(** That's a good start but, since we are in Coq, and not in OCaml, we can
  actually make our comments be formal statements *)

Reset MAP.
Require Import Arith.
Require Import String.
Require Import List.
Open Scope string_scope. (* Will facilitate string input *)

Module Type MAP.
  (** the type of map keys *)
  Parameter key : Type.
  (** the type of map elements *)
  Parameter elt : Type.
  (** the type of maps *)
  Parameter t : Type.

  (** [default] is the default element in a map *)
  Parameter default: elt.

  (** [get m k] returns the elements that is binded with key [k] *)
  Parameter get: t -> key -> elt.

  (** the map that binds every keys to [default] *)
  Parameter empty: t.
  Parameter empty_spec: forall k, get empty k = default.

  (** [set m k e] returns the a new map that contains the same
      bindings as map [m] except for key [k] that is now binded with 
      the element [e] *)
  Parameter set: t -> key -> elt -> t.
  Parameter get_set_new: forall k m e, 
    get (set m k e) k = e.
  Parameter get_set_old: forall k m e k', 
    k'<>k -> get (set m k e) k' = get m k'.
  (** Note that [->] means "implies" and [<>] means "different" here. *)
End MAP.

Module NatStringMap <: MAP 
                 with Definition key := nat
                 with Definition elt := string.

 Definition key := nat.
 Definition elt := string.
 Definition t := list string.
 Definition default := "".
 Fixpoint get (l:list string) (n:nat) : string :=
   match l, n with
     | nil, _ => default
     | x::_, O => x
     | _::q, S m => get q m
    end.

 Definition empty : t := nil.

 Fixpoint set (l:list string) (n:nat) (s:string) : list string :=
   match l, n with
     | nil, O => s :: nil
     | nil, S m => default :: set nil m s
     | _ :: q, O => s :: q
     | x :: q, S m => x :: set q m s
    end.

  (** This time we can't end the module so easily because we have proof
   to do ! *)

  (** The command we use to build an interactive proof are called tactics.
    The set of Coq tactics is rather large. We will only expose a limited 
number
    of them in this tutorial. When the remaining proof is easy we will use
    a custom tactic that force Coq to search alone the proof *)
  (** We call this tactic [go] and we do not explain its content *)
  Ltac go := try congruence; eauto; try econstructor (solve[go]).

  Lemma empty_spec: forall k, get empty k = default.
  Proof.
    go.
  Qed. (* [Qed] only succeeds if the system accept our proof *)


  Lemma get_set_new: forall k m e, 
    get (set m k e) k = e.
  Proof.
    intros.
    destruct k.
    - simpl.
      destruct m.
      + simpl.
        go.
      + simpl.
        go.
    - simpl.
      destruct m.
      simpl.
      (** we did not do much progress... *)
  Abort. (* we abort the current proof *)

  Lemma get_set_new: forall k m e, 
    get (set m k e) k = e.
  Proof.
    induction k; intros.
    - simpl.
      destruct m.
      + simpl.
        go.
      + simpl.
        go.
    - simpl.
      destruct m.
      + simpl.
        apply IHk. (* or [go] *)
      + simpl.
        go.
  (* ok, but since we have apply very similar on each branch of the
     proof we can put a more compact (and robust) script*)      
  Abort.

  Lemma get_set_new: forall k m e, 
    get (set m k e) k = e.
  Proof.
    induction k; destruct m; simpl; go.
  Qed.

  Lemma get_set_old: forall k m e k', 
    k'<>k -> get (set m k e) k' = get m k'.
  Proof.
    induction k; destruct m; destruct k'; simpl; go.
    (* only one remaining goal *)
    intros.
    rewrite IHk; go.
  Qed.
 
End NatStringMap.
  
(* We may have a look at the OCaml extracted version *)
Extraction NatStringMap.

(** In the previous implementation [get] and [set] have a linear 
    complexity (both in time and space) with respect to the size
    of the biggest inserted key. We now seek for an implementation 
    with a logarithmic complexity *)

(* The custom tactic [go] was not exported outside the Module when we 
   closed it. We now redefine it here. *)
Ltac go := try congruence; eauto; try econstructor (solve[go]).

                                       
(** We need first to build some data structures. The first one is a 
    functional representation of non nul binary numbers *)

Inductive positive :=
  | xH               (* 1 *)
  | xO (p:positive)  (* 2 p *)
  | xI (p:positive)  (* 2 p +1 *)
.

Check xI (xI (xO xH)).
(** represents 1 + 2 * (1 + 2 *  (2 * 1)) = 11 = Ox1011 *)

Module PosStringMap <: MAP 
                 with Definition key := positive
                 with Definition elt := string.

 Definition key := positive.
 Definition elt := string.

 (** We now want to define a tree structure. *)
 Inductive tree :=
 | Leaf
 | Node (a:string) (l r:tree).

 Definition t := tree.

 Definition default := "".

 Fixpoint get (t: tree) (p:positive) :=
   match t, p with
     | Leaf, _ => default
     | Node a l r, xH => a
     | Node a l r, xO p => get l p
     | Node a l r, xI p => get r p
   end.

 Definition empty : t := Leaf.

  Fixpoint set (t:tree) (p:positive) (s:string) :=
  match t, p with
    | Leaf, xH => Node s Leaf Leaf
    | Leaf, xO p => Node default (set Leaf p s) Leaf
    | Leaf, xI p => Node default Leaf (set Leaf p s) 
    | Node a l r, xH => Node s l r
    | Node a l r, xO p => Node a (set l p s) r
    | Node a l r, xI p => Node a l (set r p s) 
  end.

  Lemma empty_spec: forall k, get empty k = default.
  Proof.
    go.
  Qed. 

  Lemma get_set_new: forall k m e, 
    get (set m k e) k = e.
  Proof.
    induction k; destruct m; simpl; go.
  Qed.

  Lemma get_set_old: forall k m e k', 
    k'<>k -> get (set m k e) k' = get m k'.
  Proof.
    induction k; destruct m; destruct k'; simpl; go;
    intros; rewrite IHk; go.
  Qed.
 
End PosStringMap.

Notation "m [ k ]" := (PosStringMap.get m k) (at level 20).
Notation "m +{ k ↦ e }" := (PosStringMap.set m k e) (at level 20).
Notation "{}" := (PosStringMap.empty) (at level 20).

Definition p1 := xH.
Definition p2 := xO xH.
Definition p3 := xI xH.
Definition p4 := xO (xO xH).
Definition p6 := xO (xI xH).

Compute ({} +{p2 ↦ "two" } +{p3 ↦ "three" } +{p6 ↦ "six" } [p6]).
Compute ({} +{p2 ↦ "two" } +{p3 ↦ "three" } +{p6 ↦ "six" } [p4]).
Compute ({} +{p2 ↦ "two" } +{p3 ↦ "three" } +{p6 ↦ "six" } [p3]).
Compute ({} +{p2 ↦ "two" } +{p3 ↦ "three" } +{p6 ↦ "six" } [p2]).
Compute ({} +{p2 ↦ "two" } +{p3 ↦ "three" } +{p6 ↦ "six" } [p1]).



Le 30 janv. 2015 à 21:01, Eric Mullen 
<emullen AT cs.washington.edu>
 a écrit :

> If you wanted to give a 10 minute demo to show off how cool Coq was, what 
> example would you use?
> 
> Specifically, if you were talking to a bunch of undergraduates in Computer 
> Science, and you had 10 minutes to convince them that Coq was an awesome 
> research tool, what would be your go to example?
> 
> Ideas so far have been:
>  * Implementing slow and fast Fibonacci functions, and proving they 
> calculate the same thing
>  * Proving that the identity function and the Fibonacci function are both 
> monotonic
> 
> I'm leaning towards the second due to its simplicity, but I would very much 
> appreciate small examples which illustrate how cool it is to write code and 
> prove properties about it.
> 
> Thanks much,
> Eric Mullen