BasicsFunctional Programming
(* $Date: 2012-12-26 11:12:50 -1000 (Wed, 26 Dec 2012) $ *)
Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
A function on days:
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
Simplification
Eval simpl in (next_weekday friday).
(* ==> monday : day *)
Eval simpl in (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)
A "unit test" for our function — i.e., a mathematical
claim about its behavior:
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
A proof script giving evidence for the claim:
Proof. simpl. reflexivity. Qed.
Inductive bool : Type :=
| true : bool
| false : bool.
Booleans are also provided in Coq's standard library, but
in this course we'll define everything from scratch, just to see
how it's done.
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => b2
| false => false
end.
Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => true
| false => b2
end.
Note the syntax for defining multi-argument
functions (andb and orb). Here's the corresponding
multi-argument application syntax...
Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.
Definition admit {T: Type} : T. Admitted.
Exercise: 1 star (nandb)
Complete the definition of the following function, then make sure that the Example assertions below each can be verified by Coq.Definition nandb (b1:bool) (b2:bool) : bool :=
(* FILL IN HERE *) admit.
Remove "Admitted." and fill in each proof with
"Proof. simpl. reflexivity. Qed."
Example test_nandb1: (nandb true false) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb2: (nandb false false) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb3: (nandb false true) = true.
(* FILL IN HERE *) Admitted.
Example test_nandb4: (nandb true true) = false.
(* FILL IN HERE *) Admitted.
☐
All but a few of the exercises are omitted from the "terse"
version of the notes that we'll be looking at in lectures. The
"full" version has many exercises, including some optional ones
for extra practice (and a lot of additional explanatory text).
Check true.
(* ===> true : bool *)
Check (negb true).
(* ===> negb true : bool *)
Functions like negb itself are also data values, just like
true and false. Their types are called function types, and
they are written with arrows.
Check negb.
(* ===> negb : bool -> bool *)
Module Playground1.
A proper inductive type — natural numbers (in unary
notation):
Inductive nat : Type :=
| O : nat
| S : nat → nat.
Inductive declarations create inductively defined sets,
which consist of all possible combinations of the constructors.
Definition pred (n : nat) : nat :=
match n with
| O => O
| S n' => n'
end.
End Playground1.
Definition minustwo (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
Standard arabic numerals can be used as a shorthand for
elements of nat, and it expands arabic numerals in its input
into appropriate sequences of applications of S to O:
Check (S (S (S (S O)))).
Eval simpl in (minustwo 4).
Recursive functions are defined using Fixpoint.
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
Coq notes that evenb is "decreasing on 1st argument."
We can define oddb by a similar Fixpoint declaration, but here
is a simpler definition that will be a bit easier to work with:
Definition oddb (n:nat) : bool := negb (evenb n).
Example test_oddb1: (oddb (S O)) = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: (oddb (S (S (S (S O))))) = false.
Proof. simpl. reflexivity. Qed.
A multi-argument recursive function.
Module Playground2.
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Eval simpl in (plus (S (S (S O))) (S (S O))).
(* plus (S (S (S O))) (S (S O))
==> S (plus (S (S O)) (S (S O))) by the second clause of the match
==> S (S (plus (S O) (S (S O)))) by the second clause of the match
==> S (S (S (plus O (S (S O))))) by the second clause of the match
==> S (S (S (S (S O)))) by the first clause of the match
*)
Fixpoint mult (n m : nat) : nat :=
match n with
| O => O
| S n' => plus m (mult n' m)
end.
Pattern-matching two values at the same time:
Fixpoint minus (n m:nat) : nat :=
match n, m with
| O , _ => O
| S _ , O => n
| S n', S m' => minus n' m'
end.
The _ in the first line is a wildcard pattern. Writing _ in a
pattern is the same as writing some variable that doesn't get used
on the right-hand side. This avoids the need to invent a bogus
variable name.
End Playground2.
Fixpoint exp (base power : nat) : nat :=
match power with
| O => S O
| S p => mult base (exp base p)
end.
Example test_mult1: (mult 3 3) = 9.
Proof. simpl. reflexivity. Qed.
We can make numerical expressions a little easier to read and
write by introducing "notations" for addition, multiplication, and
subtraction.
Notation "x + y" := (plus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x - y" := (minus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x * y" := (mult x y)
(at level 40, left associativity)
: nat_scope.
Check ((0 + 1) + 1).
The beq_nat function tests natural numbers for equality,
yielding a boolean. Note the use of nested matches (we could
also have used a simultaneous match, as we did in minus.)
Fixpoint beq_nat (n m : nat) : bool :=
match n with
| O => match m with
| O => true
| S m' => false
end
| S n' => match m with
| O => false
| S m' => beq_nat n' m'
end
end.
Similarly, the ble_nat function tests natural numbers for
less-or-equal, yielding a boolean.
Fixpoint ble_nat (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => ble_nat n' m'
end
end.
Example test_ble_nat1: (ble_nat 2 2) = true.
Proof. simpl. reflexivity. Qed.
Example test_ble_nat2: (ble_nat 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_ble_nat3: (ble_nat 4 2) = false.
Proof. simpl. reflexivity. Qed.
Theorem plus_O_n : ∀n:nat, 0 + n = n.
Proof.
simpl. reflexivity. Qed.
The reflexivity command implicitly simplifies both sides of the
equality before testing to see if they are the same, so we can
shorten the proof a little.
Theorem plus_O_n' : ∀n:nat, 0 + n = n.
Proof.
reflexivity. Qed.
Theorem plus_O_n'' : ∀n:nat, 0 + n = n.
Proof.
intros n. reflexivity. Qed.
Theorem plus_1_l : ∀n:nat, 1 + n = S n.
Proof.
intros n. reflexivity. Qed.
Theorem mult_0_l : ∀n:nat, 0 * n = 0.
Proof.
intros n. reflexivity. Qed.
Theorem plus_id_example : ∀n m:nat,
n = m →
n + n = m + m.
Instead of making a completely universal claim about all numbers
n and m, this theorem talks about a more specialized property
that only holds when n = m. The arrow symbol is pronounced
"implies."
Since n and m are arbitrary numbers, we can't just use
simplification to prove this theorem. Instead, we prove it by
observing that, if we are assuming n = m, then we can replace
n with m in the goal statement and obtain an equality with the
same expression on both sides. The tactic that tells Coq to
perform this replacement is called rewrite.
Proof.
intros n m. (* move both quantifiers into the context *)
intros H. (* move the hypothesis into the context *)
rewrite → H. (* Rewrite the goal using the hypothesis *)
reflexivity. Qed.
We can also use the rewrite tactic with a previously proved
theorem instead of a hypothesis from the context.
Theorem mult_0_plus : ∀n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m.
rewrite → plus_O_n.
reflexivity. Qed.
Theorem plus_1_neq_0_firsttry : ∀n : nat,
beq_nat (n + 1) 0 = false.
Proof.
intros n. simpl. (* does nothing! *)
Admitted.
We can use destruct to perform case analysis:
Theorem plus_1_neq_0 : ∀n : nat,
beq_nat (n + 1) 0 = false.
Proof.
intros n. destruct n as [| n'].
reflexivity.
reflexivity. Qed.
Another example (using booleans)
Theorem negb_involutive : ∀b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b.
reflexivity.
reflexivity. Qed.
Require String. Open Scope string_scope.
Ltac move_to_top x :=
match reverse goal with
| H : _ ⊢ _ => try move x after H
end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move_to_top x
| assert_eq x name; move_to_top x
| fail 1 "because we are working on a different case" ].
Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.
... to here.
Here's how to use it:
Theorem andb_true_elim1 : ∀b c : bool,
andb b c = true → b = true.
Proof.
intros b c H.
destruct b.
Case "b = true".
reflexivity.
Case "b = false".
rewrite ← H. reflexivity. Qed.
Induction
Theorem plus_0_r_firsttry : ∀n:nat,
n + 0 = n.
Proof.
intros n.
simpl. (* Does nothing! *)
Admitted.
Case analysis gets us a little further, but not all the way:
Theorem plus_0_r_secondtry : ∀n:nat,
n + 0 = n.
Proof.
intros n. destruct n as [| n'].
Case "n = 0".
reflexivity. (* so far so good... *)
Case "n = S n'".
simpl. (* ...but here we are stuck again *)
Admitted.
We need a bigger hammer: the principle of induction over
natural numbers:
In Coq, the style of reasoning is "backwards" (or
"goal-directed"): 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'). For example...
- If P(n) is some proposition involving a natural number n,
and we want to show that P holds for all numbers, 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.
Theorem plus_0_r : ∀n:nat, n + 0 = n.
Proof.
intros n. induction n as [| n'].
Case "n = 0". reflexivity.
Case "n = S n'". simpl. rewrite → IHn'. reflexivity. Qed.
Let's try this one together:
Theorem minus_diag : ∀n,
minus n n = 0.
Proof.
(* WORK IN CLASS *) Admitted.
Formal vs. Informal Proof
Theorem plus_assoc' : ∀n m p : nat,
n + (m + p) = (n + m) + p.
Proof. intros n m p. induction n as [| n']. reflexivity.
simpl. rewrite → IHn'. reflexivity. Qed.
A careful informal proof of the same theorem:
Here is a formal proof with the same structure:
- Theorem: For any n, m and p,
n + (m + p) = (n + m) + p.Proof: By induction on n.
- First, suppose n = 0. We must show
0 + (m + p) = (0 + m) + p.This follows directly from the definition of +.
- Next, suppose n = S n', where
n' + (m + p) = (n' + m) + p.We must show(S n') + (m + p) = ((S n') + m) + p.By the definition of +, this follows fromS (n' + (m + p)) = S ((n' + m) + p),which is immediate from the induction hypothesis. ☐
- First, suppose n = 0. We must show
Theorem plus_assoc : ∀n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p. induction n as [| n'].
Case "n = 0".
reflexivity.
Case "n = S n'".
simpl. rewrite → IHn'. reflexivity. Qed.