BasicsFunctional 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 Admitteds 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 equality, yielding a boolean. Note the use of nested matches (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 : ∀ 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' : ∀ n : nat, 0 + n = n.
Proof.
  intros n. reflexivity. Qed.
Any other (fresh) identifier could be used instead of n:

Theorem plus_O_n'' : ∀ n : nat, 0 + n = n.
Proof.
  intros m. reflexivity. Qed.

Other similar theorems can be proved with the same pattern.

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.

Proof by Rewriting

A (slightly) more interesting theorem:

Theorem plus_id_example : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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' : ∀ 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' : ∀ 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'' :
  ∀ 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.