(** * Introduction to the Coq proof assistant

      Francesco Zappa Nardelli 
      Moscova project
      INRIA Paris-Rocquencourt

      Version of 26/1/2009
*)

(* ============================================================== *)
(** * LECTURE 2 *)

(* In this lecture we will look at how we can REASON in Coq about the
   programs we've written. 
*)

(* ---------------------------------------------------------------------- *)
(* Before moving on, we define an useful function to test if two
   natural numbers are the same (part of last lecture exercises).  
*)
Print nat.

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.

(* Some examples *)
Eval simpl in (eqnat 3 4).
Eval simpl in (eqnat 3 3).

(* ---------------------------------------------------------------------- *)
(** * Reasoning by "partial evaluation" *)

(* Some facts about functions can be proved simply by unfolding their
   recursive definitions. *)

(* For example, the fact that zero is a neutral element for plus on
   the left can be proved just by observing that [plus zero n] reduces
   to [n] no matter what [n] is, since the definition of [plus] is
   recursive in its first argument. *)

Print plus.

Lemma zero_plus : forall n:nat, 
  0 + n = n.
Proof.
  simpl. 
  reflexivity. 
Qed.

(* Here is another fact that can be proved by the same "partial
   evaluation" technique. *)
Lemma one_plus : forall n:nat, 
  1 + n = S n.
Proof.
  simpl. 
  reflexivity. 
Qed.

(* ---------------------------------------------------------------------- *)
(** ** The [intros] and [rewrite] tactics *)

(* It will often happen that the goal we're trying to prove
   begins with some kind of quantifier (e.g., "for all
   numbers n, ...") or hypothesis ("assuming m=n, ...").  

   In such situations, it is convenient to be able to move
   the "left-hand part" out of the way and concentrate on
   the "right-hand part."  The [intros] tactic permits us to
   do this, by moving a quantifier or hypothesis from the
   goal to a "context" of current assumptions.

   For example, here is a slightly different -- perhaps
   slightly clearer -- proof of one of the facts we proved a
   minute ago.
*)
Lemma zero_plus' : forall n:nat, 
  0 + n = n.
Proof.
  intros n.
  simpl.
  reflexivity. 
Qed.

(* Here is a more interesting proof that involves moving a
   hypothesis into the context and then APPLYING this
   hypothesis to rewrite the rest of the goal. *)
Lemma plus_id_common : forall m n:nat, 
  m = n -> m + n = n + m.    (* -> is pronounced "implies" *)
Proof.
  intros m n.     (* move both quantifiers into the context at once *)
  intros eq.      (* move the hypothesis into the context *)
  rewrite <- eq.  (* Rewrite the goal according to the hypothesis *)
  reflexivity. 
Qed.

(* The [->] annotation in [rewrite ->] tells Coq to apply the rewrite
   from left to right.  To rewrite from right to left, you can use
   [rewrite <-].  Try this in the above proof and see what changes.

   Note that this has nothing to do with the use of the symbol [->] to
   denote implication in the statement of the lemma. *)

(* We can also use the [rewrite] tactic with a previously proved lemma
   instead of a hypothesis from the context. *)
Lemma times_zero_plus : forall m n : nat, 
  (0 + n) * m = n * m.
Proof.
  intros m n.
  Check zero_plus'.
  rewrite -> zero_plus'. 
  reflexivity.
Qed.
(* Note, too, that we applied a rewrite here justified by a previously
   proved lemma ([zero_plus']) rather than an assumption in the
   immediate context. *)

(* ---------------------------------------------------------------------- *)
(** ** Case analysis *)

(* Of course, not everything can be proved by simple calculation: In
   general, unknown, hypothetical values (arbitrary numbers, booleano
   values, lists, etc.) can show up in the "head position" of
   functions that we want to reason about, blocking simplification.
   For example, if we try to prove the following fact using the
   [simpl] tactic as above, we get stuck.
 *)
Lemma plus_one_neq_zero_firsttry : forall n,
  eqnat (n + 1) 0 = false.
Proof.
  intros n. 
  simpl.  (* does nothing! *)
Admitted.
(* The [Admitted] command tells Coq that we want to give up trying to
   prove this lemma and just accept it as a given.  This can be useful
   for developing longer proofs, since we can state subsidiary facts
   that we believe will be useful for making some larger argument, use
   [Admitted] to accept them on faith for the moment, and continue
   thinking about the larger argument until we are sure it is working;
   then we can go back and fill in the proofs we skipped.  Be careful,
   though: Every time you say [Admitted] you are leaving a door open
   for total nonsense to enter your nice rigorous formally checked
   world! *)

(* What we need is to be able to consider the possible forms of [n]
   separately: if it is [O], then we can calculate the final result of
   [eqnat (plus n one) zero] and check that it is, indeed, [no].  And
   if [n = S(n')] for some [n'], then, although we don't know exactly
   what number [plus n one] yields, we can calculate that, at least,
   it begins with one [S], and this is enough to calculate that,
   again, [eqnat (plus n one) zero] will yield [no]. 

   The tactic that tells Coq to consider the cases where [n = O] and
   where [n = S n'] separately is called [destruct].  It generates TWO
   subgoals, which we must then prove, separately, in order to get Coq
   to accept the Lemma as proved.  (There is no special command for
   moving from one subgoal to the other.  When the first subgoal has
   been proved, it just disappears and we are left with the other "in
   focus.") *)
Lemma plus_one_neq_zero : forall n,
  eqnat (n + 1) 0 = false.
Proof.
  intros n. 
  destruct n.
    simpl. reflexivity.
    simpl. reflexivity.
Qed.

(* We can do case analysis on arbitrary datatypes. *)
Definition swap (b:bool) : bool :=
  match b with
  | true => false
  | false => true
end.

Lemma swap_swap : forall b : bool,
  swap (swap b) = b.
Proof.
  intros b.
  destruct b.
    simpl. reflexivity.
    simpl. reflexivity.
Qed.

(* ---------------------------------------------------------------------- *)
(** ** Induction on numbers *)

(* We proved above that zero is a neutral element for plus on the left
   using a simple partial evaluation argument.  The fact that it is
   also a neutral element on the RIGHT cannot be proved in the same
   simple way... *)
Lemma plus_zero_firsttry : forall n:nat, 
  n + 0 = n.
Proof.
  intros n.
  simpl. (* Does nothing! *) 
Admitted.

(* Case analysis gets us a little further, but not all the way. *)
Lemma plus_zero_secondtry : forall n:nat, 
  n + 0 = n.
Proof.
  intros n. 
  destruct n.
    simpl. reflexivity. (* so far so good... *)
    simpl.              (* ...but here we are stuck again *)
Admitted.

(* To prove such facts -- indeed, to prove most interesting facts
   about numbers, lists, and other inductively defined sets -- we need
   a more powerful reasoning principle: INDUCTION.

   Recall (from high school) the principle of induction over
   natural numbers:

     If [P(n)] is some proposition involving a natural number n, and
     we want to show that P holds for ALL numbers n, we can reason
     like this:

        - show that [P(O)] holds
        - show that, if [P(n)] holds, then so does [P(S n)]
        - conclude that [P(n)] holds for all n.

   In Coq, the style of reasoning is "backwards": we begin with the
   goal of proving [P(n)] for all n and break it down (by applying the
   [induction] tactic) into two separate subgoals: first showing P(O)
   and then showing [P(n) -> P(S n)]. *)
Lemma plus_zero : forall n:nat, 
  n + 0 = n.
Proof.
  intros n. 
  induction n.      
    (* First subgoal: *)
    simpl. reflexivity.
    (* Second subgoal: *)
    simpl. rewrite -> IHn. reflexivity.
Qed.

Lemma plus_assoc : forall m n p : nat, 
  m + (n + p) = (m + n) + p.   
Proof.
  intros m n p. 
  induction m.
    simpl. reflexivity.
    simpl. rewrite -> IHm. reflexivity.
Qed.

(* ---------------------------------------------------------------------- *)
(** * Induction on lists *)

Require Import List.

Print list.
(* We can do induction not just on numbers, but on any inductively
   defined type: Coq generates an appropriate induction principle when
   it processes the [Inductive] declaration.

   Here is the induction principle for (polymorphic) lists:

     If X is a type and [P l] is some proposition involving a list l
     of type [list X], and we want to show that P holds for all l, we
     can reason like this:

        - show that P (nil) holds
        - show that, for any element x:X and any list l : list X, if
          [P l] holds, then so does [P (x::l)]
        - conclude that [P l] holds for all lists l.
*)
Lemma append_nil : forall X:Set, forall l : list X,
  l = l ++ nil.
Proof.
  intros X l.
  induction l. 
    simpl. reflexivity.
    simpl. rewrite <- IHl. reflexivity.
Qed.

Lemma append_assoc : forall X:Set, forall l1 l2 l3 : list X, 
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).   
Proof.
  intros X l1 l2 l3. 
  induction l1.
    simpl. reflexivity.
    simpl. rewrite -> IHl1. reflexivity.
Qed.

(* Now let's try something a little more intricate: proving that
   reversing a list does not change its length.  The reverse 
   function [rev] recursively copies the head element of a list 
   to its end. *)

Print length.
Print rev.

(* Our first attempt gets stuck in the successor case... *)
Lemma length_reverse_firsttry : 
  forall X : Set, forall l : list X,
  length l = length (rev l).
Proof.
  intros X l. 
  induction l.
    simpl. reflexivity.
    simpl. rewrite IHl.
    (* hum, it would be nice to have the following lemma:

         forall l', S (length l') = length (l' ++ (a::nil)) 

       because we might instatiate [l'] to be [rev l] and concluding 
       would be easy.  So... *)
Admitted.

Lemma length_app_one :
  forall X : Set, forall l : list X, forall a : X,
  S (length l) = length (l ++ (a::nil)).
Proof.
  intros X l a. 
  induction l. 
    simpl. reflexivity. 
    simpl. rewrite -> IHl. reflexivity. 
Qed.

Lemma length_reverse : 
  forall X : Set, forall l : list X,
  length l = length (rev l).
Proof.
  intros X l. 
  induction l.
    simpl. reflexivity.
    simpl. rewrite IHl. rewrite <- length_app_one. reflexivity.
    (* observe that we did rewriting using the name of the lemma just
       proved *)
Qed.    

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

(** * Arithmetic Expressions Over Natural Numbers *)

(* We are now ready to prove the correctness of our compiler 
   of a simple arithmetic language onto a stack machine.  
   Let's recall the definitions.
*)

(** * The source language *)

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

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.

(* Examples *)

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

(** * The target machine *)

(** 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.

(* Given an instruction and a stack, the [execute_instr] executes the
   instruction and 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.

(* The function [run] 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 *)

(** The compiler takes 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].
*)

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 7)) (Const 3)).
Eval simpl in compile (Mult (Const 3) (Plus (Const 2) (Const 7))).

(* Observe that compiling (2+7)*3 and 3*(2+7) resulted in quite
   different programs. Do we really trust our compiler? *)

(** Let's attempt to prove the following theorem. *)

Theorem compile_correct_firsttry: 
  forall e, run (compile e) nil = meaning e :: nil.
Proof.
  intros e.
  induction e.
    simpl. reflexivity.
    simpl.
  (* It is very unclear how to go on from here.  The problem is that
  the induction hypothesis IHe1 and IHe2 suppose that:

  - the programs obtained by compiling e1 and e2 are executed starting
    from an empty stack;

  - the programs only contain the instructions of the compilation of
    e1 or e2.

  These induction hypothesis are too weak to help us.  

  Maybe we can prove a stronger theorem...
*)
Admitted.

Lemma compile_correct': 
  forall e p s, run (compile e ++ p) s = run p (meaning e :: s).
Proof.
  intros e.
  (* we do not [intros p s] because we want [p] and [s] to be 
     universally quantified in the induction hypothesis *) 
  induction e.
  (* Case e = Const n *)
  intros p s. simpl. reflexivity.
  (* Case e = Plus e1 e2 *)
  intros p s. 
  simpl.
  (* We cannot apply directly IHe1 because the program we are
     executing is of the form [ (compile e2 ++ p1) ++ p2 ] and not of
     the form [ compile e2 ++ (p1 ++ p2) ].  However we proved above
     that list concatenation is associative in the [append_assoc]
     lemma.  We can then rewrite the first in the latter.  
  *)
  rewrite append_assoc.
  (* Now we can apply the induction hypothesis IHe2. *)
  rewrite IHe2.
  (* Similarly, we can apply the induction hypothesis IHe1. *)
  rewrite append_assoc.
  rewrite IHe1. 
  (* And we can conclude by simplification. *)
  simpl.
  reflexivity.
  (* Case e = Mult e1 e2
     This case is similar to the Plus e1 e2 case. *)
  intros. 
  simpl.
  rewrite append_assoc.
  rewrite IHe2.
  rewrite append_assoc.
  rewrite IHe1. 
  simpl.
  reflexivity.
Qed.

(* We can finally prove the compiler correctness theorem! 
*)

Theorem compile_correct: 
  forall e, run (compile e) nil = meaning e :: nil.
Proof.
  intros.
  (* The lemma we proved above requires the program being executed to
     be of the form [compile e ++ p] for an arbitrary program [p],
     while the program in our goal is just [compile e].  But we proved
     above that [l = l ++ nil] for any list [l].

     However we cannot just [rewrite append_nil] because the goal
     contains too many lists and Coq cannot determine which one we
     want to rewrite.  So we specialize the [append_nil] lemma to
     [compile e = compile e ++ nil] before rewriting.  The underscore
     stands for the type [instr], which is inferred by Coq.  
  *)
  Check append_nil.
  Check (append_nil _ (compile e)).
  rewrite (append_nil _ (compile e)).  
  rewrite compile_correct'.  
  simpl.  
  reflexivity.  
Qed.

(** * We can now extract OCaml code that implements our stack machine *)
Recursive Extraction run.
(* and we can extract our certified compiler. *)
Recursive Extraction compile.

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

(* Giving a two hour introduction to Coq was great because I could
  show some nice features of the proof assistant, avoiding all the
  dark corners.

  Do not believe that using Coq is that easy!

  If you want to learn more about Coq and mechanised proofs, then I
  believe that the best tutorial is given by Benjamin Pierce lectures:

  http://www.seas.upenn.edu/~cis500/cis500-f07/schedule.html

  The book by Bertot and Casteran 

    "Interactive Theorem Proving and Program Development" 

  is a valuable source of in-depth informations.
  
  Thank you.
  *)

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

(* Complete these proofs *)

Lemma plus_id_exercise : forall m n o : nat, 
  m = n -> n = o -> m + n = n + o.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.

Lemma times_zero_exercise : forall n : nat, 
  n * 0 = 0.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.

Lemma one_times : forall n:nat, 
  1 * n = n.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.

Lemma length_append : forall X : Set,
                      forall l1 l2 : list X,
  length (l1 ++ l2) = (length l1) + (length l2).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.

(* A more difficult exercise: show that [map] and [rev] "commute". *)

Print map.

Lemma map_reverse : forall X Y : Set, 
                    forall f : X->Y,
                    forall s : list X,
  map f (rev s) = rev (map f s).
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.

(* There is a short solution to the next exercise.  If you find
   yourself getting tangled up, step back and try to look for a
   simpler way... *)
Lemma append_assoc4 : forall X : Set,
                      forall l1 l2 l3 l4 : list X,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
(* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Can you extend the source language of our compiler to include 
   subtraction (denoted [-] in Coq)?

   - Redefine the source grammar [exp] and the [meaning] function.

   - Extend the stack machine with the new [Isub] instruction.

   - Extend appropriately the compiler.  Be careful: subtraction
     is not commutative, and the order in which you place the
     operands on the stack is important!

   - Prove the correctness of the extended compiler.
*)