(* =========== Basic tactics :
-> intro - introduction rule for Pi;
-> apply - elimination rule for Pi;
-> assumption, exact - match conclusion with an hypothesis. 
*)

(* =========== Tactics for EQUALITY and REWRITING :
-> rewrite - rewrites an equality;
-> rewrite <- - reverse rewrite of an equality;
-> reflexivity - reflexivity property for equality;
-> symmetry - symmetry property for equality;
-> transitivity - transitivity property for equality.
*)

(* =========== Tactics for EVALUATION and CONVERTIBILITY :
-> simpl, red, cbv, lazy - performs evaluation;
-> pattern - performs a beta-expansion on the goal;
-> change - replaces the goal by a convertible one.
*)

(* =========== Tactics for INDUCTION :
-> elim - to apply the corresponding induction principle;
-> induction - performs induction on an identifier;
-> destruct - case analysis;
-> discriminate - discriminates objects built from different constructors;
-> injection - constructors of inductive types are injections; 
-> inversion - given an inductive type instance, find all the necessary condition 
               that must hold on the arguments of its constructors.
*)

(* =========== LIBRARIES 
A large base of definitions and facts found in the Coq Standard Library.
Often used libraries: 
-> Arith - unary integers;
-> ZArith - binary integers;
-> List - polymorphic lists;

Useful commands for finding theorems acting on a given identifier:
-> Search
-> SearchAbout
-> SearchPattern
*)

(* =========== AUTOMATISATION
For some specific domains, Coq is able to support some degree of automatisation:
-> auto - automatically applies theorems from a database;
-> tauto, intuition - decision procedures for specific classes of goals (e.g. propositional logic);
-> omega, ring - specialized tactics for numerical properties.
*)

(* =========== USEFUL tactics and commands...
Tactics:
-> clear - removes an hypothesis from the environment;
-> generalize - re-introduce an hypothesis into the goal;
-> cut, assert - proves the goal through an intermediate result;
-> pattern - performs eta-expansion on the goal.

Commands:
-> Admitted - aborts the current proof (property is assumed);
-> Set Implicit Arguments - makes possible to omit some arguments (when inferable by the system);
-> Open Scope - opens a syntax notation scope (constants, operators, etc.)

See the Reference Manual...
*)



(* ================================================================== *)
(* =============== Reasoning about naturals and lists =============== *)
(* ================================================================== *)

Require Import List.

Set Implicit Arguments.

Print list.
Print app.



Theorem app_l_nil : forall (A:Set) (l:list A), app l nil = l.
intros A l. 
pattern l. (* pattern performs a beta-expansion *)
Check list_ind.
apply list_ind.
reflexivity.
intros a l0 IH. simpl. rewrite IH. reflexivity.
Qed.

Theorem app_l_nil' : forall (A:Set) (l:list A), app l nil = l.
intros A l.
elim l.
reflexivity.
intros a l0 IH; simpl; rewrite IH; reflexivity.
Qed.

Theorem app_l_nil'' : forall (A:Set) (l:list A), app l nil = l.
Proof.
induction l.
reflexivity. simpl. rewrite IHl. reflexivity.
Qed.


Print nat.
Print length.


(* 
 Exercise: prove that the length of the append of two lists is equal 
           to the addition of the length of each list 
*)





(* A predicate defined inductively *)

Fixpoint In (A:Set) (a:A) (l:list A) {struct l} : Prop :=
    match l with
      | nil => False
      | cons x xs => x = a \/ In a xs
    end.


Lemma in_app : forall (A:Set) (l1 l2:list A) (a:A), 
                           In a (app l1 l2) -> In a l1 \/ In a l2.
Proof.
intros.
generalize H. 
clear H. 
induction l1.
simpl. intro H. tauto.
intros.
simpl in H.
destruct H as [H|H].
rewrite H. left. simpl.
left. reflexivity.
destruct (IHl1 H) as [H0|H0].
left. simpl.
right; assumption.
right; assumption.
Qed.



Print rev.

Lemma rev_rev_l : forall (A:Set) (l:list A), rev (rev l) = l.
Proof.
induction l.
simpl; reflexivity.
simpl.

(*
Lemma rev_aux : forall (A:Set) (l: list A) (a:A), rev (app l (cons a nil)) = cons a (rev l).
*)
Lemma rev_aux : forall (A:Set) (l: list A) (a:A), rev (l ++ (a :: nil)) = a :: (rev l).
induction l.
simpl. reflexivity.
intro. simpl.
rewrite IHl.
simpl. reflexivity.
Qed.

rewrite rev_aux.
rewrite IHl.
reflexivity.
Qed.


Print nat.

(* A property (predicate) on natural numbers *)
Inductive Even : nat -> Prop :=
| Even_base : Even 0
| Even_step : forall n, Even n -> Even (S (S n)).

Print plus.


Lemma not_1_even : ~(Even 3).
red.
intros.
inversion_clear H.
inversion H0.
Qed.


Proposition sum_even : forall n m:nat, Even n -> Even m -> Even (n+m).
intros n m H.
elim H.
  intro; simpl; assumption.
  intros.
  simpl.
  apply Even_step.
  apply H1; assumption.
Qed.


Lemma double_even : forall n:nat, Even (2*n).
intros.
simpl.
elim n.
simpl.
apply Even_base.

intros.
simpl.

cut (forall x y:nat, x+(S y) = S (x+y)).

intros.
rewrite H0.
apply Even_step. assumption.

clear H.
intros.
induction x.
  simpl.
  reflexivity.

  simpl.
  rewrite IHx.
  reflexivity.
Qed.

(*
 Exercise: rewrite the prove of the previous lemma without using the cut tactic.
 Hint: use the command SearchAbout to find out a useful lemma in the database.

 Lemma double_even' : forall n:nat, Even (2*n).
*)





SearchAbout le.
SearchAbout lt.
Print lt.
SearchPattern ( _ <= _ ).


(*
 Exercise: define the "Odd" predicate and prove that for every n, (Even n)->(Odd (S n)).
*)





(* An inductive relation "x is the last element of list l" *)
Inductive last (A:Type) (x:A) : list A -> Prop :=
| last_base : last x (cons x nil)
| last_step : forall l y, last x l -> last x (cons y l).


Lemma last_nil : forall (A:Type) (x:A), ~(last x nil).
intros.
intro.
inversion H.
Qed.


(* The prove of  ~(last x nil)  without using the inversion tactic. *)

Lemma last_nil_aux : forall (A:Type) l (x:A), last x l -> l=nil -> False.
intros A l x H. elim H.
  intro H0. discriminate H0.
  intros. discriminate H2.
Qed.

Theorem last_nil' : forall (A:Type) (x:A), ~(last x nil).
intros. red. intros.
apply last_nil_aux with A nil x.
assumption.
reflexivity.
Qed.




(* An example of mutually defined inductive types *)
Inductive EVEN : nat -> Prop :=
| EVEN_base : EVEN 0
| EVEN_step : forall n, ODD n -> EVEN (S n)
with ODD : nat -> Prop :=
| ODD_step : forall n, EVEN n -> ODD (S n).