BasicsFunctional Programming in Coq
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 compute in (next_weekday friday).
(* ==> monday : day *)
Eval compute 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. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. reflexivity. Qed.
(Note that we've dropped the simpl in the proofs. It's not
actually needed because reflexivity will automatically perform
simplification.)
This function should return true if either or both of
its inputs are false.
Exercise: 1 star (nandb)
Complete the definition of the following function, then make sure that the Example assertions below can each be verified by Coq.Definition nandb (b1:bool) (b2:bool) : bool :=
(* FILL IN HERE *) admit.
Remove "Admitted." and fill in each proof with
"Proof. 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 in input
as a shorthand for sequences of applications of S to O,
and Coq uses the same shorthand on output:
Check (S (S (S (S O)))).
Eval compute 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.
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. reflexivity. Qed.
Example test_oddb2: (oddb (S (S (S (S O))))) = false.
Proof. 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 compute 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.
Example test_mult1: (mult 3 3) = 9.
Proof. reflexivity. Qed.
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.
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. reflexivity. Qed.
Example test_ble_nat2: (ble_nat 2 4) = true.
Proof. reflexivity. Qed.
Example test_ble_nat3: (ble_nat 4 2) = false.
Proof. reflexivity. Qed.
Theorem plus_O_n : ∀n : nat, 0 + n = n.
Proof.
intros n. reflexivity. Qed.
It is worth stepping through this proof to observe how
the context and the goal change.
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."
As before, we need to be able to reason by assuming the existence
of some numbers n and m. We also need to assume the hypothesis
n = m. The intros tactic will serve to move all three of these
from the goal into assumptions in the current context.
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! *)
Abort.
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.
(* $Date: 2013-08-29 10:15:14 -0400 (Thu, 29 Aug 2013) $ *)