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