# Enumerated Types

In Coq, we can build practically everything from first principles...

## Days of the Week

A datatype definition:

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
| mondaytuesday
| tuesdaywednesday
| wednesdaythursday
| thursdayfriday
| fridaymonday
| saturdaymonday
| sundaymonday
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.

## Booleans

Another familiar datatype:

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
| truefalse
| falsetrue
end.

Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| trueb2
| falsefalse
end.

Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| truetrue
| falseb2
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.)

#### 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.
This function should return true if either or both of its inputs are false.

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).

## Function Types

Every expression in Coq has a type, describing what sort of thing it computes.

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 *)

## Numbers

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
| OO
| S n'n'
end.

End Playground1.

Definition minustwo (n : nat) : nat :=
match n with
| OO
| S OO
| 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
| Otrue
| S Ofalse
| 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
| Om
| 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
| OO
| 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 _ , On
| 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
| Omatch m with
| Otrue
| S m'false
end
| S n'match m with
| Ofalse
| 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
| Otrue
| S n'
match m with
| Ofalse
| 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.

# Proof by Simplification

A general property of natural numbers:

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.

# Proof by Rewriting

A slightly more interesting theorem:

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.

# Proof by Case Analysis

Sometimes simplification and rewriting are not enough...

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) \$ *)