(** * Basics: Functional Programming in Coq *)
(* ################################################################# *)
(** * Data and Functions *)
(* ================================================================= *)
(** ** Enumerated Types *)
(** In Coq, we can build practically everything from first
principles... *)
(* ================================================================= *)
(** ** Days of the Week *)
(** A datatype definition: *)
Inductive day : Type :=
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
| sunday.
(** 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: *)
Compute (next_weekday friday).
(* ==> monday : day *)
Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)
(** Second, we can record what we _expect_ the result to be in the
form of a Coq example: *)
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
(** A proof script giving evidence for the claim: *)
Proof. simpl. reflexivity. Qed.
(** The [Require Export] statement on the next line tells Coq to use
the [String] module from the standard library. We'll use strings
ourselves in later chapters, but we need to [Require] it here so
that the grading scripts can use it for internal purposes. *)
From Coq Require Export String.
(* ================================================================= *)
(** ** Booleans *)
(** Another familiar enumerated type: *)
Inductive bool : Type :=
| true
| false.
(** Booleans are also available from 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]). *)
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.
(** We can define new symbolic notations for existing definitions. *)
Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.
(** **** Exercise: 1 star, standard (nandb)
The command [Admitted] can be used as a placeholder for an
incomplete proof. We use it in exercises to indicate the parts
that we're leaving for you -- i.e., your job is to replace
[Admitted]s with real proofs.
Remove "[Admitted.]" and complete the definition of the following
function; then make sure that the [Example] assertions below can
each be verified by Coq. (I.e., fill in each proof, following the
model of the [orb] tests above, and make sure Coq accepts it.) The
function should return [true] if either or both of its inputs are
[false]. *)
Definition nandb (b1:bool) (b2:bool) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
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.
(** [] *)
(** Most exercises are omitted from the "terse" version of the
notes used in lecture.
The "full" version contains both the assigned reading and all the
exercises for your homework assignment. *)
(* ================================================================= *)
(** ** Types *)
(** Every expression in Coq has a type, describing what sort of
thing it computes. The [Check] command asks Coq to print the type
of an expression. *)
Check true.
(* ===> true : bool *)
(** If the expression after [Check] is followed by a colon and a type,
Coq will verify that the type of the expression matches the given
type and halt with an error if not. *)
Check true
: bool.
Check (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
: bool -> bool.
(* ================================================================= *)
(** ** New Types from Old *)
(** A more interesting type definition: *)
Inductive rgb : Type :=
| red
| green
| blue.
Inductive color : Type :=
| black
| white
| primary (p : rgb).
(** Atomic identifiers like [red], [green], [blue], [black], [white],
and [primary] (and [true], [false], [monday], etc.) are
_constructors_.
From these, we build _constructor expressions_, each of which is
either a simple constructor or a constructor applied to one or
more arguments (each of which is in turn a constructor
expression). *)
(** Let's look at this in a little more detail. Every inductively
defined type ([day], [bool], [rgb], [color], etc.) describes a set
of _constructor expressions_ built from _constructors_
- We start with an infinite set of _constructors_. E.g., [red],
[primary], [true], [false], [monday], etc. are constructors.
- _Constructor expressions_ are formed by applying constructors to
zero or more constructor expressions. E.g.,
[red],
[true],
[primary],
[primary red],
[red primary],
[red true],
[primary (primary primary)],
etc.
- Each [Inductive] definition carves out a subset of these constructor
expressions and gives it a name, like [bool], [rgb], or [color].
*)
(** In particular, the definitions of [rgb] and [color] say how
constructor expressions belonging to the sets [rgb] and [color]
can be built:
- the constructor expression [red] belongs to the set [rgb], as do
the constructor expressions [green] and [blue];
- the constructor expressions [black] and [white] belong to the
set [color];
- if [p] is a constructor expression belonging to the set [rgb],
then [primary p] (pronounced "the constructor [primary] applied
to the argument [p]") is a constructor expression belonging to
the set [color]; and
- constructor expressions formed in these ways are the _only_ ones
belonging to the sets [rgb] and [color]. *)
(** We can define functions on colors using pattern matching just as
we did for [day] and [bool]. *)
Definition monochrome (c : color) : bool :=
match c with
| black => true
| white => true
| primary p => false
end.
(** Since the [primary] constructor takes an argument, a pattern
matching [primary] should include either a variable (as above --
note that we can choose its name freely) or a constant of
appropriate type (as below). *)
Definition isred (c : color) : bool :=
match c with
| black => false
| white => false
| primary red => true
| primary _ => false
end.
(** The pattern "[primary _]" here is shorthand for "the constructor
[primary] applied to any [rgb] constructor except [red]." (The
wildcard pattern [_] has the same effect as the dummy pattern
variable [p] in the definition of [monochrome].) *)
(* ================================================================= *)
(** ** Modules *)
(** [Module] declarations create separate namespaces. *)
Module Playground.
Definition b : rgb := blue.
End Playground.
Definition b : bool := true.
Check Playground.b : rgb.
Check b : bool.
(* ================================================================= *)
(** ** Tuples *)
Module TuplePlayground.
(** A nybble is half a byte -- that is, four bits. *)
Inductive bit : Type :=
| B0
| B1.
Inductive nybble : Type :=
| bits (b0 b1 b2 b3 : bit).
Check (bits B1 B0 B1 B0)
: nybble.
(** We deconstruct a nybble by pattern-matching. *)
Definition all_zero (nb : nybble) : bool :=
match nb with
| (bits B0 B0 B0 B0) => true
| (bits _ _ _ _) => false
end.
Compute (all_zero (bits B1 B0 B1 B0)).
(* ===> false : bool *)
Compute (all_zero (bits B0 B0 B0 B0)).
(* ===> true : bool *)
End TuplePlayground.
(* ================================================================= *)
(** ** Numbers *)
Module NatPlayground.
(** There are many representations possible of natural numbers.
You may be familiar with decimal, hexadecimal, octal, and binary.
For simplicity in proofs, we choose unary: [O] represents zero,
and [S] represents adding an additional unary digit. That is, [S]
is the "successor" operation, which, when applied to the
representation of n, gives the representation of n+1. *)
Inductive nat : Type :=
| O
| S (n : nat).
(** With this definition, 0 is represented by [O], 1 by [S O],
2 by [S (S O)], and so on. *)
(** Again, let's look at this in a little more detail. The definition
of [nat] says how expressions in the set [nat] can be built:
- the constructor expression [O] belongs to the set [nat];
- if [n] is a constructor expression belonging to the set [nat],
then [S n] is also a constructor expression belonging to the set
[nat]; and
- constructor expressions formed in these two ways are the only
ones belonging to the set [nat]. *)
(** Critical point: this just defines a _representation_ of
numbers -- a unary notation for writing them down.
The names [O] and [S] are arbitrary. They are just two different
"marks", with no intrinsic meaning.
We could just as well represent numbers with different marks: *)
Inductive nat' : Type :=
| stop
| tick (foo : nat').
(** The _interpretation_ of these marks comes from how we use them to
compute. *)
Definition pred (n : nat) : nat :=
match n with
| O => O
| S n' => n'
end.
End NatPlayground.
(** As a convenience, standard decimal numerals can be used as
a shorthand for sequences of applications of [S] to [O]; Coq uses
the same shorthand when printing things: *)
Check (S (S (S (S O)))).
(* ===> 4 : nat *)
Definition minustwo (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
Compute (minustwo 4).
(* ===> 2 : nat *)
(** Recursive functions are defined using the [Fixpoint] keyword. *)
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
(** We could define [oddb] by a similar [Fixpoint] declaration, but
here is a simpler way: *)
Definition oddb (n:nat) : bool :=
negb (evenb n).
Example test_oddb1: oddb 1 = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity. Qed.
(** A multi-argument recursive function. *)
Module NatPlayground2.
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Compute (plus 3 2).
(* ===> 5 : nat *)
(* [plus 3 2]
i.e. [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]
i.e. [5] *)
(** Another: *)
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. simpl. 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.
End NatPlayground2.
(** Again, we can make numerical expressions 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) : nat.
(** When we say that Coq comes with almost nothing built-in, we really
mean it: even equality testing is a user-defined operation!
Here is a function [eqb], which tests natural numbers for
[eq]uality, yielding a [b]oolean. Note the use of nested
[match]es (we could also have used a simultaneous match, as we did
in [minus].) *)
Fixpoint eqb (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' => eqb n' m'
end
end.
(** Similarly, the [leb] function tests whether its first argument is
less than or equal to its second argument, yielding a boolean. *)
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb n' m'
end
end.
Example test_leb1: leb 2 2 = true.
Proof. simpl. reflexivity. Qed.
Example test_leb2: leb 2 4 = true.
Proof. simpl. reflexivity. Qed.
Example test_leb3: leb 4 2 = false.
Proof. simpl. reflexivity. Qed.
(** We'll be using these (especially [eqb]) a lot, so let's give
them infix notations. *)
Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.
Example test_leb3': (4 <=? 2) = false.
Proof. simpl. reflexivity. Qed.
(** We have two notions of equality:
- [=] is already defined in Coq and that we attempt to _prove_.
- [=?] is something we coded up and that Coq _computes_. *)
(* ################################################################# *)
(** * Proof by Simplification *)
(** A general property of natural numbers: *)
Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
intros n. simpl. reflexivity. Qed.
(** The [simpl] tactic is actually redundant, as [reflexivity]
already does some simplification for us: *)
Theorem plus_O_n' : forall n : nat, 0 + n = n.
Proof.
intros n. reflexivity. Qed.
(** Any other (fresh) identifier could be used instead of [n]: *)
Theorem plus_O_n'' : forall n : nat, 0 + n = n.
Proof.
intros m. reflexivity. Qed.
(** Other similar theorems can be proved with the same pattern. *)
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
intros n. reflexivity. Qed.
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
intros n. reflexivity. Qed.
(* ################################################################# *)
(** * Proof by Rewriting *)
(** A (slightly) more interesting theorem: *)
Theorem plus_id_example : forall n m:nat,
n = m ->
n + n = m + m.
Proof.
(* move both quantifiers into the context: *)
intros n m.
(* move the hypothesis into the context: *)
intros H.
(* rewrite the goal using the hypothesis: *)
rewrite -> H.
reflexivity. Qed.
(** The uses of [intros] name the hypotheses as they are moved
to the context. The [rewrite] needs to know which equality is being
used and in which direction to do the replacement. *)
(** The [Check] command can also be used to examine the statements of
previously declared lemmas and theorems. The two examples below
are lemmas about multiplication that are proved in the standard
library. (We will see how to prove them ourselves in the next
chapter.) *)
Check mult_n_O.
(* ===> forall n : nat, 0 = n * 0 *)
Check mult_n_Sm.
(* ===> forall n m : nat, n * m + n = n * S m *)
(** We can use the [rewrite] tactic with a previously proved theorem
instead of a hypothesis from the context. If the statement of the
previously proved theorem involves quantified variables, as in the
example below, Coq tries to instantiate them by matching with the
current goal. *)
Theorem mult_n_0_m_0 : forall p q : nat,
(p * 0) + (q * 0) = 0.
Proof.
intros p q.
rewrite <- mult_n_O.
rewrite <- mult_n_O.
reflexivity. Qed.
(* ################################################################# *)
(** * Proof by Case Analysis *)
(** Sometimes simple calculating and rewriting are not
enough... *)
Theorem plus_1_neq_0_firsttry : forall n : 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 : forall n : nat,
(n + 1) =? 0 = false.
Proof.
intros n. destruct n as [| n'] eqn:E.
- reflexivity.
- reflexivity. Qed.
(** Note the "bullets" marking the proofs of the two subgoals. *)
(** Another example (using booleans): *)
Theorem negb_involutive : forall b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b eqn:E.
- reflexivity.
- reflexivity. Qed.
(** We can have nested subgoals (and we use different "bullets"
to mark the inner ones): *)
Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b eqn:Eb.
- destruct c eqn:Ec.
+ reflexivity.
+ reflexivity.
- destruct c eqn:Ec.
+ reflexivity.
+ reflexivity.
Qed.
(** Besides [-] and [+], we can use [*] (asterisk) or any repetition
of a bullet symbol (e.g. [--] or [***]) as a bullet. We can also
enclose sub-proofs in curly braces: *)
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b eqn:Eb.
{ destruct c eqn:Ec.
{ reflexivity. }
{ reflexivity. } }
{ destruct c eqn:Ec.
{ reflexivity. }
{ reflexivity. } }
Qed.
(** One final convenience: Instead of
intros x y. destruct y as [|y] eqn:E.
we can write
intros x [|y].
*)
Theorem plus_1_neq_0' : forall n : nat,
(n + 1) =? 0 = false.
Proof.
intros [|n].
- reflexivity.
- reflexivity. Qed.
(** If there are no constructor arguments that need names, we can just
write [[]] to get the case analysis. *)
Theorem andb_commutative'' :
forall b c, andb b c = andb c b.
Proof.
intros [] [].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
(* ################################################################# *)
(** * Testing Your Solutions *)
(** Run [make BasicsTest.vo] to check your solution for common errors:
- Deleting or renaming exercises.
- Changing what you were supposed to prove.
- Leaving the exercise unfinished.
*)