(** * Introduction to the Coq proof assistant

      Francesco Zappa Nardelli 
      Moscova project
      INRIA Paris-Rocquencourt

      Version of 16/1/2009
*)

(* ============================================================== *)
(** * LECTURE 1 *)

(** This file develops basic concepts of functional programming,
    logic, operational semantics, using the Coq proof assistant.  It
    is intended to be "read" in an interactive session with Coq under
    a development environment -- either CoqIDE or Proof General.

    This file is based on lectures by 

    - Benjamin C. Pierce ( http://www.cis.upenn.edu/~bcpierce/ )

    and is available from
     
      http://moscova.inria.fr/~zappa/teaching/coq/purdue/

    For questions, doubts, and comments, you can contact me by email:
    
      francesco.zappa_nardelli (@) inria.fr
*)

(** Coq can be seen as a combination of two things:

       - A simple but very expressive PROGRAMMING LANGUAGE

       - A set of tools for stating LOGICAL ASSERTIONS and
         constructing (and verifying) evidence of their
         truth.

    We will devote this first lecture to the programming language,
    while in the next lecture we will look at the logical aspects of
    the system.  

    As driving example, we will implement a "certified compiler" of a
    simple arithmetic language onto a stack machine.

    Questions are welcome!
*)

(**  

  Q: Did you really need to name it like that?

  A: Some French computer scientists have a tradition of naming their
     software as animal species: Caml, Elan, Foc or Phox are examples
     of this tacit convention.  In French, "coq" means rooster, and it
     sounds like the initials of the Calculus of Constructions ( CoC )
     on which it is based.  
*)

(** 

  Q: I have rarely felt as stupid and frustrated as I did during my 
     first weeks with Coq!

  A: I am afraid you are not the only one, but on the long term 
     the benefits outperforms the frustrations.  A very interesting
     reading:

     "Machine Obstructed Proof (or how many months can it take 
        to verify 30 assembly instructions?)" by Nick Benton

      http://www.cis.upenn.edu/~sweirich/wmm/wmm06/03-benton.pdf
*)

(* ============================================================== *)

Module Introduction.

(** In Coq's programming language, almost nothing is built in -- not
    even numbers!  Instead, it provides powerful tools for defining
    new types of data and functions that process and transform them.
*)

(* -------------------------------------------------------------- *)
(** * Days of the week *)

(** Let's start with a very simple example.  The following
    definition tells Coq that we are defining a new set of
    data values.  The set is called [day] and its members
    are [monday], [tuesday], etc.  The lines of the
    definition can be read "[monday] is a [day], [tuesday]
    is a [day], etc." *)
Inductive day : Set :=
  | monday : day
  | tuesday : day
  | wednesday : day
  | thursday : day
  | friday : day
  | saturday : day
  | sunday : day.

(** Having defined this set, we can write functions that 
    operate on its members. *)
Definition next_day (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => saturday
  | saturday => sunday
  | sunday => monday
  end.

Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.

(** There are three ways of "executing" programs written in Coq's
    programming language... *)

(* First, we can run them interactively: *)
Eval simpl in (next_weekday friday).
Eval simpl in (next_weekday (next_weekday (next_weekday saturday))).

(* Second, we can make an assertion about their results: *)
Lemma check_next_weekday1: 
  (next_weekday (next_weekday (next_weekday saturday)))
  = wednesday.
Proof. simpl. reflexivity. Qed.
(* For now, let's not worry about the details of what's going on here.
   Roughly, though, we are...  

   - making an assertion (that the third weekday after saturday is
     wednesday), 
   - giving it a name (check_next_weekday1) in case we
     want to refer to it later, and - telling Coq that it can be
     verified by "simplification".  
*)

(* Third, we can ask Coq to "extract", from a Definition, a program in
   some other, more mainstream, programming language (OCaml or
   Haskell).

   This facility is very interesting, since it gives us a way to
   construct FULLY VERIFIED programs in mainstream languages.  This is
   actually one of the main purposes for which Coq has been developed.

   For an impressive application, check out Xavier Leroy's CompCert, a
   certified optimising compiler for C:

   http://compcert.inria.fr/
*)

(* -------------------------------------------------------------- *)
(** * Numbers *)

(* The types we defined above are octen called "enumerated types"
   because their definitions explicitly enumerate a finite collection
   of elements.

   A more interesting way of defining a type is to give a collection
   of INDUCTIVE RULES describing its elements.  For example, we can
   define the natural numbers as follows: 
*)

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

(* This definition can be read: 
     - [O] is a natural number (note that this is the letter
       "O", not the numeral "0")
     - [S] is a function that takes a natural number and
       gives us another one -- that is, if [n] is a natural
       number, then [S n] is too.
*)

(* We can write simple functions that pattern match on
   natural numbers just as we did above: *)
Definition pred (m : nat) : nat :=
  match m with
    | O => O
    | S m' => m'
  end.

Definition minustwo (m : nat) : nat :=
  match m with
    | O => O
    | S O => O
    | S (S m') => m'
  end.

Eval simpl in (minustwo (S (S (S (S O))))).

(* But for other kinds of function definitions, just pattern
   matching is not enough: we need something new.  For
   example, to check that a number [n] is even, we may need
   to "recursively" check whether [n-2] is even.  To write
   such functions, we use the keyword [Fixpoint].
*)
Fixpoint even (n:nat) {struct n} : bool := 
  match n with
  | O        => true
  | S O      => false
  | S (S n') => even n'
  end.
(* One important thing to note about this definition is the
   declaration [{struct n}] on the first line.  This tells
   Coq to check that we are performing a "structural
   recursion" over the argument [n] -- i.e., that we make
   recursive calls only on strictly smaller values of [n].
   This allows Coq to check that all calls to [even] will
   eventually terminate. *)

(* What is [bool]?  Coq itself knows nothing about booleans, but
   booleans have been defined in a library.  We can use the keyword
   [Print] to display the definition of an object, the keyword
   [Locate] to find the file that defines it, and the keyword
   [SearchAbout] to display all what Coq knows about some object.  
*)

Locate bool.  
Print bool.
SearchAbout bool.

Lemma check_even1: 
  (even (S O)) = false.
Proof. simpl. reflexivity. Qed.
Lemma check_even2: 
  (even (S (S (S (S O))))) = true.
Proof. simpl. reflexivity. Qed.

(* Of course, we can also define multi-argument functions by
   recursion. *)
Fixpoint add (m : nat) (n : nat) {struct m} : nat :=
  match m with
    | O => n
    | S m' => S (add m' n)
  end.

Lemma check_add: 
    (add (S (S (S O))) (S (S (S O))) 
  = (S (S (S (S (S (S O))))))).
Proof. simpl. reflexivity. Qed.

(* Such examples are getting a little hard to read!  It is possible to
define better names for terms using the [Notation] keyword. *)

Notation zero  := O.
Notation one   := (S O).
Notation two   := (S (S O)).
Notation three := (S (S (S O))).
Notation four  := (S (S (S (S O)))).
Notation five  := (S (S (S (S (S O))))).
Notation six   := (S (S (S (S (S (S O)))))).
Notation seven := (S (S (S (S (S (S (S O))))))).

Lemma check_add_1: 
    (add four three) = seven.
Proof. simpl. reflexivity. Qed.

(* As booleans, natural numbers are defined in the standard library of
   Coq.  In what follows, we use the standard library definition of
   nat, together with its concise notations, rather than the
   definition above. 
*) 
End Introduction.

(* Let's be sure that the library definition of nat is what we expect.
*) 
Print nat.  

(* It is.  And plenty of functions and lemmas are already defined. *)
SearchAbout nat.

(* -------------------------------------------------------------- *)
(** * Lists of numbers *)

(* We can describe the type of lists of numbers like this: "A list can
   be either the empty list or else a pair of a number and another
   list." 
*) 
Inductive natlist : Set := 
  | nl_nil : natlist 
  | nl_cons : nat -> natlist -> natlist.

Definition nl123 :=
  nl_cons 1 (nl_cons 2 (nl_cons 3 nl_nil)).

(* Lists, and useful operations over them, are defined in the "List"
library.  The List library is not opened by default, and must be
explicitely imported. 
*) 
Require Import List.

Print list.

(* Observe that the above definition is parametric in the type of
objects stored in the list, so we can build:

  list bool : list of booleans
  list nat : list of natural numbers
  list (list nat) : list of lists of natural numbers
  ...

and reuse all the functions (like length of a list) which do not need
to observe the objects in a list.  This feature is known as
"polymorphism" (or generics in the object oriented world).
 *)

(* For instance, a three-element list: *)
Definition l123 := cons 1 (cons 2 (cons 3 nil)).
Print l123.

Definition ltft := cons true (cons false (cons false nil)).
Print ltft.

(* Observe that the list library also defines some concise
notations. 
*)

(* ============================================================== *)

(** * Arithmetic Expressions Over Natural Numbers *)

(* We are ready to define our driving example, a "certified compiler"
   of a simple arithmetic language onto a stack machine.  
*)

(** * The source language *)

(** An expression is either a natural number or the application of a
    binary operator, and is defined by the BNF below.  The only
    binary operators we consider are addition and multiplication.

  exp ::=
  | nat
  | plus exp exp 
  | mult exp exp 
*)

Inductive exp : Set :=
  | Const : nat -> exp
  | Plus : exp -> exp -> exp
  | Mult : exp -> exp -> exp.

(* Examples of valid expressions are

  - 42
  - plus 2 2
  - mult (plus 2 2) 3

  We can use the keyword [Check] to ask Coq to verify that a term is
  well-formed.  
*)
 
Check (Const 42).  
Check (Plus (Const 2) (Const 2)).
Check (Mult (Plus (Const 2) (Const 2)) (Const 3)).
  
(** What does an expression mean? Intuitively:

  - the expression "42" denotes the natural number 42
  - the expression "plus 2 2" denotes the natural number 4
  - the expression "mult (plus 2 2) 3" denotes the natural number 12

  We write an interpreter that can be thought of as a trivial
  denotational semantics.  If the term "denotational semantics" sounds
  unfriendly to you, no need to worry: we will stick to "common sense"
  constructions.
*)

Fixpoint meaning (e:exp) : nat :=
  match e with
  | Const n => n
  | Plus e1 e2 => (meaning e1) + (meaning e2)
  | Mult e1 e2 => (meaning e1) * (meaning e2)
end.

Eval simpl in meaning (Const 42).
Eval simpl in meaning (Plus (Const 2) (Const 2)).
Eval simpl in meaning (Mult (Plus (Const 2) (Const 2)) (Const 3)).

(** * The target machine *)

(** We will compile our source expressions onto a a simple stack
    machine (do you remember HP calculators?).  The machine is
    composed by

      - the stack: a stack of natural numbers

      - the program: a list of instructions

      where an instruction is either

      - IConst nat : put nat on top of the stack
      - IPlus : pops two values from the stack and pushes their sum
      - IMult : pops two values from the stack and pushes their sum
      
*)

Inductive instr : Set :=
  | IConst : nat -> instr
  | IPlus : instr
  | IMult : instr.

Definition prog := list instr.

Definition stack := list nat.

(* We can define a function that executes one instruction: given an
instruction and a stack, [execute_instr] returns the modified stack.
*)

Definition execute_instr (i : instr) (s : stack) : stack :=
  match i with
    | IConst n => (n :: s)
    | IPlus =>
      match s with
        | arg1 :: arg2 :: s' => (arg1 + arg2 :: s')
        | _ => nil
      end
    | IMult =>
      match s with
        | arg1 :: arg2 :: s' => (arg1 * arg2 :: s')
        | _ => nil
      end
  end.

(* With [execute_instr] defined, it is easy to define a function
   [run], which iterates application of [execute_instr] through a
   whole program.  
*)

Fixpoint run (p : prog) (s : stack) {struct p} : stack :=
  match p with
    | nil => s
    | i :: p' => run p' (execute_instr i s)
  end.

(** * Translation *)

(** Our compiler now:  

    The compiler should take an expression and generate code that puts
    the value of the expression on the top of the stack.  So:

    - a constant expression [Const n] is translated into the
      instruction that puts n on top of the stack [IConst n]

    - an expression [Plus e1 e2] should generate code that sums the
      values of the expressions e1 and e2.  So we build a program that
      when executed:

      1- evaluates e2 and pushes the value of e2 onto the stack;
         this code can be generated by recursively calling "compile"
         on e2

      2- evaluates e1 and pushes the value of e1 onto the stack;
         this code can be generated by recursively calling "compile"
         on e1

      3- call IPlus to sum the two values on the top of the stack

    - similarly for [Mult e1 e2].

   [++] is the list concatenation operator from the Coq standard
    library.  
*)

Fixpoint compile (e : exp) : prog :=
  match e with
    | Const n => IConst n :: nil
    | Plus e1 e2 => compile e2 ++ compile e1 ++ IPlus :: nil
    | Mult e1 e2 => compile e2 ++ compile e1 ++ IMult :: nil
  end.

(** Before we set about proving that this compiler is correct, we can
    try a few test runs, using our sample programs from earlier. *)

Eval simpl in compile (Const 42).
Eval simpl in compile (Plus (Const 2) (Const 2)).
Eval simpl in compile (Mult (Plus (Const 2) (Const 2)) (Const 7)).

(** We can also run our compiled programs and check that they give the
  right results. *)

Eval simpl in run (compile (Const 42)) nil.
Eval simpl in run (compile (Plus (Const 2) (Const 2))) nil.
Eval simpl in run (compile (Mult (Plus (Const 2) (Const 2)) (Const 7))) nil.

(* ============================================================== *)
(** * EXERCISES *)

(* EXERCISE: Recall that the factorial function is defined
   like this in mathematical notation:
        factorial(0) = 1
        factorial(n) = n * (factorial(n-1))    if n>0
   Translate this into Coq's notation.

Fixpoint factorial (n:nat) {struct n} : nat := 
 FILL IN HERE

Lemma check_factorial1: 
  (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
Lemma check_factorial2: 
  (factorial 5) = (10 * 12).
Proof. compute. reflexivity. Qed.
*)

(* When we say that Coq comes with nothing built-in, we
   really mean it!  Even equality testing has to be
   defined. *)
Fixpoint eqnat (m n : nat) {struct m} : bool :=
  match m with 
  | O =>
      match n with 
      | O => true
      | S n' => false
      end
  | S m' =>
      match n with
      | O => false
      | S n' => eqnat m' n'
      end
  end.

(* EXERCISE: Complete the definitions of the following
   comparison functions.
Fixpoint lenat (m n : nat) {struct m} : bool :=
FILL IN HERE

Lemma check_lenat1: 
  (lenat 2 2) = true.
Proof. simpl. reflexivity. Qed.
Lemma check_lenat2: 
  (lenat 2 4) = true.
Proof. simpl. reflexivity. Qed.
Lemma check_lenat3: 
  (lenat 4 2) = false.
Proof. simpl. reflexivity. Qed.

*)

(** * EXERCISE: bags via lists *)

(* EXERCISE: A BAG (often called a MULTISET) is a set where
   each element can appear any finite number of times.  One
   reasonable implementation of bags is to represent a bag
   of numbers as a LIST of numbers.

   Uncomment and complete the definitions.

Definition bag := list nat.  

Fixpoint count (v:nat) (s:bag) {struct s} : nat := 
FILL IN HERE

Lemma check_count1: 
  count 1 [1,2,3,1,4,1] = 3.
Proof. simpl. reflexivity. Qed.
Lemma check_count2: 
  count 6 [1,,2,3,1,4,1] = 0.
Proof. simpl. reflexivity. Qed.

Definition union := 
FILL IN HERE

Lemma check_union1: 
  count 1 (union [1,2,3] [1,4,1]) = 3.
Proof. simpl. reflexivity. Qed.

*)