(** Beging ignore, just for presentation *)
Axiom todo : forall {A}, A.
Ltac todo := apply todo.
Ltac exercise := apply todo.
Set Asymmetric Patterns.
(** End ignore *)
(** If you're using CollaCoq https://x80.org/collacoq
you can freely edit the document. To get Coq's answer:
- Alt-Enter (Cmd should work in Macs too) goes to the
current point;
- Alt-N/P or Alt-Down/Up will move through the proof;
- Goals appear on the right-hand-side panel;
- Errors and answers appear on the lower-right panel.
https://www.irif.fr/~sozeau//EJCP17_demo.v
*)
(** Lambda calculus *)
Module Lambda.
(** We suppose a type [T] and a value [t : T] *)
Parameter T : Type.
Parameter t : T.
(** Calling the type inference algorithm *)
Check t.
Fail Check x.
Check (fun x : T => x).
(** Definining new constants: identity on T *)
Definition idT := fun x : T => x.
Print idT.
(** Definitions can take arguments *)
Definition applyT (f : T -> T) (x : T) := f x.
(** Arguments of the function are just
lambda/fun-abstractions *)
Print applyT.
(** Compute the normal form *)
Eval compute in idT t.
(** applyT idT t -> (fun x : T => x) t -> x[x:=t] = t *)
(** Pairs / cartesian products *)
Print pair.
(* Inductive prod (A B : Type) : Type := *)
(* pair : A -> B -> A * B *)
Check pair t t.
Check (t, t).
Check prod T T.
Definition proj1 (x : T * T) : T :=
match x with
| pair l r => l
end.
(** Quantification: *)
Check (forall x : T, x = x).
Check (fun x : T => eq_refl x).
(** Ascribing a type to a definition *)
Definition reflT : forall x : T, x = x :=
fun x : T => eq_refl x.
(** Application in the dependent case:
the argument t is substituted in the _type_ of reflT. *)
Definition eqTterm : t = t :=
reflT t.
(** Our first lemma! *)
Lemma eqT : t = t.
Proof.
apply reflT.
Show Proof.
Qed.
End Lambda.
(** Simple data types *)
Module Unit.
(** Set is just an alias for Type(0) *)
Inductive unit : Set := tt.
Print unit.
Check (fun x : unit => x).
Check (fun x : unit => (x, tt)).
Check (fun x : unit => x = tt).
Parameter x : unit.
Check (match tt with tt => x end).
(** Reduction of case expressions. *)
Eval compute in match tt with tt => x end.
End Unit.
Module Booleans.
(** Booleans and equational reasoning *)
(** Simplest enumeration *)
Inductive bool : Set := true | false.
(** Boolean negation *)
Definition negb (b : bool) : bool :=
match b with
| true => false
| false => true
end.
Eval compute in negb true.
Eval compute in negb false.
(** Booleam conjunction *)
Definition andb (b b' : bool) : bool :=
match b with
| true => b'
| false => false
end.
Eval compute in andb true false.
Eval compute in andb true true.
(** Boolean disjunction *)
Definition orb (b b' : bool) : bool :=
match b with
| true => true
| false => b'
end.
Eval compute in orb true false.
Eval compute in orb false false.
(** Interactive proof: basic tactics.
[intros x1 .. xn] for introduction of variables in
the context
[destruct H] for case analysis on a named hypothesis [H]:
replaces it by each possible _constructor_
of the inductive type
[unfold d] for unfolding a definition [d] to its body
[apply f] for application of lemma [f : ... -> B] to
a goal [B]
[;] for sequencing of tactics
*)
Lemma negb_involutive : forall b : bool, negb (negb b) = b.
Proof.
intros b.
destruct b.
unfold negb.
apply eq_refl.
unfold negb; apply eq_refl.
Qed.
(** Constructors have particular properties.
[discriminate H] solves the goal if [H] is an equality
between different constructors. *)
Lemma discriminable : true = false -> False.
Proof.
intros H.
discriminate H.
Qed.
(** Higher-level tactics *)
Lemma reflexivity_test (x : bool) : x = x.
Proof.
(** No need to remember the name of the
reflexivity proof/program *)
reflexivity.
Show Proof.
Qed.
(** Proof by computation:
[simpl] to simplify the goal by unfolding
definitions and computation/reduction rules. *)
Lemma andb_true_l b' : andb true b' = b'.
Proof.
Print andb.
simpl.
reflexivity.
Show Proof.
Qed.
(** Another proof by case analysis, left to the reader *)
Lemma andb_true_r b : andb b true = b.
Proof.
destruct b; simpl; reflexivity.
Qed.
(** De-Morgan law: by case analysis and computation.
Goal selectors: [all:tac] applies tac to all goals. *)
Lemma negb_andb b b' :
negb (andb b b') = orb (negb b) (negb b').
Proof.
destruct b; destruct b'.
all:simpl.
all:reflexivity.
Qed.
(** Exercise: state and prove another de Morgan law *)
End Booleans.
Module Logic.
(** Logical connectives:
They are all inductively defined, so [destruct] can be
used to replace a variable of type True, False, a
conjuction or disjunction by its possible constructors
if any.
*)
Print True.
Print False.
Print and.
Check and True False.
Check or True False.
Print or.
(** Implication is the same in Prop as in Type,
it is just the function type. *)
Check (True -> False).
Check (fun x : True => x).
(** To build proof terms apply the _constructor_
of the inductive type, or use [constructor] *)
Goal True /\ True.
apply conj.
all:apply I.
Undo 2.
constructor.
all:constructor.
Show Proof.
Qed.
Goal False \/ True.
constructor.
Show Proof.
Print or.
Undo.
constructor 2.
constructor.
Qed.
(** Reasoning with implication. *)
Lemma AimpA (A : Prop) : A -> A.
Proof.
intros a.
apply a.
Show Proof.
Qed.
Lemma AimpA' : forall (A : Prop), A -> A.
Proof.
intros A a.
apply a.
Qed.
Lemma curry (P Q : Prop) : (P -> Q) /\ P -> Q.
Proof.
intros H.
destruct H as [Hpq Hp].
apply (Hpq Hp).
Qed.
Print curry.
Lemma absurd : forall A : Type, False -> A.
Proof.
intros A Hf.
destruct Hf.
Qed.
Print conj.
(* Inductive conj (A B : Prop) : Prop := *)
(* | pair (a : A) (b : B) : conj A B. *)
Definition fst (A B : Prop) (p : A /\ B) : A.
Proof.
destruct p as [a b]. apply a.
Defined.
Definition snd (A B : Prop) (p : A /\ B) : B :=
match p with
| conj a b => b
end.
Print not.
Lemma notand (A B : Prop) : not A \/ not B -> not (A /\ B).
Proof.
intros Hf.
unfold not.
intros Hab.
destruct Hab as [Ha Hb].
destruct Hf.
unfold not in H.
apply (H Ha).
apply (H Hb).
Qed.
Lemma notand_inv (A B : Prop) :
not (A /\ B) -> not A \/ not B.
Proof.
intros Hnab.
unfold not in Hnab.
Abort.
(** Exercises *)
Lemma imp_trans (A B C : Prop) : (A->B)->(B->C)->A->C.
Proof.
intros Hab. intros Hbc. intro a.
apply Hbc. apply Hab. apply a.
(* apply Hab in a. apply Hbc in a. apply a. *)
Qed.
Lemma and_comm (A B : Prop) : A /\ B -> B /\ A.
Proof.
intros Hab. destruct Hab as [Ha Hb].
apply conj; assumption.
Qed.
Lemma AimpnnA (A : Prop) : A -> ~ ~ A.
Proof.
intros a. unfold not. intros Haf.
apply (Haf a).
Qed.
(** Existential quantification: written [exists x : T, P]
for an existential on T with property P. *)
Lemma ex0 : exists x : nat, x = 0.
Proof.
exists 0. reflexivity.
Show Proof.
Qed.
(** [destruct H] can be used to destruct an existential
hypothesis H, just like a pair or a conjunction.
[rewrite H in H'] rewrite with the equational lemma
H in H' *)
Lemma ex_elim : (exists x : bool, x = true /\ x = false) ->
False.
Proof.
intros H.
destruct H as [x H].
destruct H as [xt xf].
rewrite xt in xf.
discriminate xf.
Qed.
Lemma ex_exercise : exists x : bool, andb x x = true.
Proof.
exists true. reflexivity.
Qed.
End Logic.
Module Naturals.
(** {6 Recursive datatypes} *)
(**
Inductive nat :=
| O : nat
| S : nat -> nat.
*)
(** Two constructors, O for 0 and [S] for successor,
which is recursive, it takes a natural number as
argument to produce its successor *)
Check (S O).
Unset Printing Notations.
Check 0.
Check 1.
Check 3.
Set Printing Notations.
(** A recursive definition (i.e. [let rec] in OCaml) *)
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
(** A recursive definition (i.e. [let rec] in OCaml) *)
Fail Fixpoint bad_plus (n m : nat) { struct n } : nat :=
match n with
| O => m
| S n' =>
(** Structurally recursive call:
n is not smaller than n, hence recursion
fails to terminate (checked by Coq) *)
S (bad_plus n m)
end.
Infix "+" := plus : nat_scope.
(** Constructors have particular properties.
[discriminate H] solves the goal if [H] is an equality
between _different_ constructors. *)
Lemma discriminable : forall n, 0 = S n -> False.
Proof. intros ; discriminate. Qed.
(** They are injective too,
[injection H] on an hypothesis [C x = C y],
an equality between
the _same_ constructors, gives a proof of [x = y].
*)
Lemma injective : forall n m, S n = S m -> n = m.
Proof. intros n m H. injection H. intros H'. apply H'. Qed.
(** Induction on natural numbers, rewriting tactic.
[induction n as [x1 xn|...|y1..yn]]
Perform induction/recurrence on [n], naming hypotheses
x1 .. xn ... y1 .. yn in the corresponding branches.
[rewrite e] when [e] is a lemma of conclusion [t = u],
and [t] appears in the goal, substitute it by [u].
*)
Lemma plus_n_O n : n + O = n.
Proof.
induction n as [ | n'].
reflexivity.
simpl.
rewrite IHn'.
reflexivity.
Qed.
Lemma plus_n_Sm n m : n + S m = S (n + m).
Proof.
induction n as [|n'].
- reflexivity.
- simpl. now rewrite IHn'.
Qed.
(** Induction is implemented by recursion! *)
Eval compute in nat_ind.
(* = fun (P : nat -> Prop)
(f : P 0) (f0 : forall n : nat, P n -> P (S n)) =>
fix F (n : nat) : P n :=
match n as n0 return (P n0) with
| 0 => f
| S n0 => f0 n0 (F n0)
end
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n
*)
(** Compare with iteration *)
Fixpoint nat_iter (init : nat) (f : nat -> nat) (x : nat) :
nat :=
match x with
| 0 => init
| S n => f (nat_iter init f n)
end.
Lemma plus_sym n m : n + m = m + n.
Admitted.
(** plus_sym is added as an _axiom_, we
did not provide a proof *)
(** Equivalently: *)
Axiom plus_assoc : forall n m p, n + m + p = n + (m + p).
(** Multiplication *)
Fixpoint mult (n m : nat) : nat :=
match n with
| O => 0
| S n' => m + mult n' m
end.
Infix "*" := mult : nat_scope.
(** Simplification is part of every tactic *)
Lemma mult_n_O n : n * 0 = 0.
Proof.
induction n as [|n'].
- reflexivity.
- simpl. now rewrite IHn'.
Qed.
(** Simplification is part of every tactic *)
Lemma mult_n_1 n : n * 1 = n.
Proof.
induction n as [|n'].
- reflexivity.
- simpl. now rewrite IHn'.
Qed.
(** Axioms needed for the following definitions and proof,
can be proved as well *)
Axiom mult_n_Sm : forall n m, n * S m = n + n * m.
Axiom mult_sym : forall n m, n * m = m * n.
Axiom plus_mult_distr : forall n m p,
(n + m) * p = n * p + m * p.
Axiom mult_assoc : forall n m p, n * m * p = n * (m * p).
Fixpoint power (n m : nat) : nat :=
match m with
| 0 => 1
| S m' => n * power n m'
end.
Infix "^" := power.
(** Test your function first *)
Check (eq_refl : power 3 0 = 1).
Check (eq_refl : power 3 1 = 3).
Check (eq_refl : power 3 3 = 27).
Check (eq_refl : power 0 3 = 0).
(** Now lets prove an easy lemma. *)
Lemma power_1 n : power n 1 = n.
Proof.
simpl. apply mult_n_1.
Qed.
(** The relation between exponentiation and addition.
This lemma is a bit harder:
Choose induction wisely, on which variable is it
likely to be true by induction ?
Use rewriting with the previous lemmas *)
Lemma power_n_plus_m k n m : k ^ (n + m) = k ^ n * k ^ m.
Proof.
induction n as [|n']; simpl.
- now rewrite plus_n_O.
- rewrite IHn'.
now rewrite mult_assoc.
Qed.
(** Exercise: express and prove decidability of
equality on natural numbers (two numbers are either
equal or not). It requires injectivity and
discrimination on natural numbers.
Look at the proof and obverse it's computational
behavior, what does it do ? *)
Lemma eq_nat_dec : forall n m : nat, (n = m) + (~ n = m).
Proof.
induction n; destruct m.
- left; reflexivity.
- right. intro ; discriminate.
- right. intro ; discriminate.
- destruct (IHn m) as [e|ne]. left. now rewrite e.
right. intros Heq. apply ne. injection Heq. intros Hnm; apply Hnm.
Qed.
Print eq_nat_dec.
(** Extraction to ML *)
Extraction eq_nat_dec.
(** It basically implements the boolean equality test *)
End Naturals.
Module Drinker. (* Challenge *)
(** Consider the following statement: “Consider a room with
at least one person. There exists a person such that if
he drinks, then everybody drinks”. Write the assumptions
and the statement of the problem, including a type
representing the persons, and a predicate of persons
that drink (those are axioms/parameters). The
proof of this proposition requires the excluded-middle,
which can be equivalently stated as
[forall P:Prop, P \/ ~P] or [forall P:Prop, ~ ~ P -> P].
Prove that the 2 formulations are indeed equivalent, and
that the drinker’s paradox can be proved using
excluded-middle. *)
Axiom em : forall P : Prop, P \/ ~ P.
(** Double negation elimination *)
Axiom nnelim : forall P : Prop, ~ ~ P -> P.
Lemma em_nnelim : (forall P : Prop, P \/ ~ P) <->
(forall P : Prop, ~ ~ P -> P).
Proof.
split.
exercise.
exercise.
Qed.
(** Now model the Drinker's paradox *)
End Drinker.