(** * 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.
(* ================================================================= *)
(** ** 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 notation for an existing definition. *)
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)
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.) 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 *)
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 *)
(* ================================================================= *)
(** ** New Types from Old *)
(** A more interesting type definition: *)
Inductive rgb : Type :=
| red
| green
| blue.
Inductive color : Type :=
| black
| white
| primary (p : rgb).
(** In general, [Inductive] declarations introduce "inductively
defined sets," which consist of all legal combinations of the
constructors.
Let's look at this in a little more detail.
Every inductively defined type ([day], [bool], [rgb], [color],
etc.) contains a set of _constructor expressions_ built from
_constructors_ like [red], [primary], [true], [false], [monday],
etc.
The definitions of [rgb] and [color] say how expressions in the
sets [rgb] and [color] can be built:
- [red], [green], and [blue] are the constructors of [rgb];
- [black], [white], and [primary] are the constructors of [color];
- the expression [red] belongs to the set [rgb], as do the
expressions [green] and [blue];
- the expressions [black] and [white] belong to the set [color];
- if [p] is an expression belonging to the set [rgb], then
[primary p] (pronounced "the constructor [primary] applied to
the argument [p]") is an expression belonging to the set
[color]; and
- 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 have done for [day] and [bool]. *)
Definition monochrome (c : color) : bool :=
match c with
| black => true
| white => true
| primary q => 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 "[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].) *)
(* ================================================================= *)
(** ** Tuples *)
(** 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).
(* ==> 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 *)
(* ================================================================= *)
(** ** Modules *)
(** This [Module] declaration puts the following definitions in
their own namespace (so that they don't conflict with things from
the standard library). *)
Module NatPlayground.
(* ================================================================= *)
(** ** Numbers *)
(** 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
the act of adding an additional unary digit, that 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:
- [O] and [S] are constructors;
- the expression [O] belongs to the set [nat];
- if [n] is an expression belonging to the set [nat], then [S n]
is also an expression belonging to the set [nat]; and
- 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.
(** Standard decimal numerals can be used in input expressions,
as a shorthand for sequences of applications of [S] to [O],
and Coq uses the same shorthand in things it prints: *)
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 can define [oddb] by a similar [Fixpoint] declaration, but here
is a simpler definition: *)
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).
(* [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]
*)
(** 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).
(** 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.
(** Since we'll be using these (especially [eqb]) a lot, 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.
(* ################################################################# *)
(** * 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.
(** 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. *)
(** We can also 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_0_plus : forall n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m.
rewrite -> plus_O_n.
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) as a third kind of
bullet. We can also enclose sub-proofs in curly braces, which is
useful in case we ever encounter a proof that generates more than
three levels of subgoals: *)
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 arguments to name, we can just write [[]]. *)
Theorem andb_commutative'' :
forall b c, andb b c = andb c b.
Proof.
intros [] [].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.