Episode 02: Hello PeaCoq

Comments go between left-paren star and star right-paren. 
(* (* they can even be nested *) *)
This binding associates the name x to the expression 0:

Definition x := 0.

Coq code is primarily a sequence of bindings. In PeaCoq, we can step through the bindings one at a time by pressing: 
  Control-Alt-Down
When we ask Coq to process a binding like: 
  Definition foo := bar.
it does the following:
  • Type check the expression bar.
    • This ensures that, if asked, Coq will be able to evaluate bar down to a value.
  • Extend the environment to associate the name foo to the expression bar.
Coq also has commands which let us poke around and ask Coq questions. For example, the Print command displays the value associated with a name:

Print x.

It only works on names though; this will crash: 
Print 1.
The Check command displays the type of an expression:

Check x.

The Eval cbv in command evaluates an expression down to a value:

Eval cbv in (1 + 1).

Here is a simple inductive definition:

Inductive boolean :=
| btrue : boolean
| bfalse : boolean.

It says that boolean is a type and that there are exactly two values that have type boolean, btrue and bfalse.
Coq actually doesn't have any built-in types! However, the standard prelude provides a several familiar types. For example, the type bool from the standard prelude is just like our type boolean:

Print bool.

We can also bind names to functions by including arguments to our Definitions:

Definition bid (x: bool) := x.

This binds a function bid to a function which takes a sinlge argument, x of type bool and when called simply returns x.
We call functions via juxtaposition which is a fancy way of saying we just write the function name and the argument next to it:

Eval cbv in (bid true).
Eval cbv in (bid false).

In Coq we can also prove that our functions work as expected. Here is a simple proof showing that bid has the behavior we expect: it always just returns its argument:

Lemma bid_ok :
  forall b, bid b = b.
Proof.
  intro.

The tactic intro above transforms the proof goal from: 
  
  ============================
   forall b : bool, bid b = b
to: 
  b : bool
  ============================
   bid b = b
You can think of it as proving a universally quantified claim about booleans by considering an arbitrary boolean.

  unfold bid.

The tactic unfold bid above transforms the proof goal to: 
  b : bool
  ============================
   b = b
This simply replaces the identifier bid with whatever it is bound to in the current environment.

  reflexivity.

Finally, the reflexivity tactic solves this subgoal. Since we don't have any outstanding subgoals, the proof is done and we end with a nice Qed.

Qed.

We can also define functions that do case analysis, or pattern matching, on their arguments:

Definition bneg (b: bool) : bool :=
  match b with
    | true => false
    | false => true
  end.

Eval cbv in (bneg true).
Eval cbv in (bneg false).

To define functions of multiple arguments, just add another argument!

Definition band (l: bool) (r: bool) : bool :=
  match l with
    | true =>
      match r with
        | true => true
        | false => false
       end
    | false => false
  end.

Eval cbv in (band true true).
Eval cbv in (band true false).
Eval cbv in (band false true).
Eval cbv in (band false false).

We can also lump arguments of the same type together.

Definition bor (l r: bool) : bool :=
  match l with
    | true => true
    | false =>
      match r with
        | true => true
        | false => false
       end
  end.

Eval cbv in (bor true true).
Eval cbv in (bor true false).
Eval cbv in (bor false true).
Eval cbv in (bor false false).

What types do our functions have?

Check bid.
bid
     : bool -> bool

Check bneg.
bid
     : bool -> bool

Check band.
band
     : bool -> bool -> bool

Check bor.
bor
     : bool -> bool -> bool
A function with type A -> B takes an argument of type A and returns a result of type B. The arrow -> associates to the right, so A -> B -> C means the same as A -> (B -> C). Here we see currying where we can encode functions of multiple arguments as functions of single arguments which take an argument and return a function that takes the next argument and return a function that takes the next argument and return ... until all the arguments have been taken and then the function can simply return the result.

Lemma demorgan_band:
  forall l r,
  band l r = bneg (bor (bneg l) (bneg r)).
Proof.
  intros.

intros works like intro, but it slurps up all the universally quantified variables at the front of a goal.

  intros.

destruct does case analysis.
  destruct l.

In the case that l = true, we want to also do case analysis on r:
  destruct r.

We can solve both the subcases with reflexivity.
  reflexivity.
  reflexivity.

In the case that l = false, reflexivity does the trick.
  { reflexivity. }
Qed.

Another of DeMorgan's laws can be proved similarly:

Lemma demorgan_bor:
  forall l r,
  bor l r = bneg (band (bneg l) (bneg r)).
Proof.
  intros. destruct l.
  { reflexivity. }
  { destruct r.
    { reflexivity. }
    { reflexivity. }
  }
Qed.

The curly baces ``{'' and ``}'' help us note which subgoals we're in and make the structure of the proof a little bit clearer. While they're technically optional, PeaCoq will always generate them to help make the resulting proof term easier to understand.
Side Note : We can write our functions to just bind a name to an expression and use fun to build an anonymous function:

Definition bneg' : bool -> bool :=
  fun (b: bool) =>
    match b with
      | true => false
      | false => true
    end.

Also we can often omit certain type annotations, and Coq will figure them out automatically!

Definition bneg'' :=
  fun (b: bool) =>
    match b with
      | true => false
      | false => true
    end.

Check bneg''.

Definition bneg''' : bool -> bool :=
  fun b =>
    match b with
      | true => false
      | false => true
    end.

Check bneg'''.

The same goes for functions with multiple arguments:

Definition band' : bool -> bool -> bool :=
  fun (l: bool) =>
    fun (r: bool) =>
      match l with
        | true =>
          match r with
            | true => true
            | false => false
          end
        | false => false
      end.

Lemma band_equiv_band':
  forall b, band b = band' b.
Proof.
  reflexivity.
Qed.

OK, enough booleans. Let's look at numbers.

Definition nid (x: nat) := x.

Eval cbv in (nid 0).
Eval cbv in (nid 1).
Eval cbv in (nid 2).

Check (nid 2).

Lemma nid_ok :
  forall n, nid n = n.
Proof.
  reflexivity.
Qed.

nat is defined a bit differently from bool:

Print nat.
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.
The S constructor takes a nat as an argument. This allows nat to contain infinitely many terms: O represents 0 and S n represents 1 + n.

Eval cbv in O.
Eval cbv in (S O).
Eval cbv in (S (S O)).
Eval cbv in (S (S (S O))).
Eval cbv in (S (S (S (S O)))).

This also means that if we want to write functions over nat, we need recursive definitions, which we introduce with Fixpoint:

Fixpoint nadd (n1 n2: nat) : nat :=
  match n1 with
    | O => n2
    | S n => S (nadd n n2)
  end.

Fixpoint nmult (n1 n2: nat) : nat :=
  match n1 with
    | O => O
    | 1 => n2
    | S n => nadd n2 (nmult n n2)
  end.

Fixpoint factorial n :=
  match n with
  | O => 1
  | S m => n * factorial m
  end.

We can prove things about functions over nat similar to our proofs about functions over bool:

Lemma nadd_0_n:
  forall n, nadd 0 n = n.
Proof.
  reflexivity.
Qed.

However, some of these proof will also require induction, which we'll talk about extensively during the course:

Lemma nadd_n_0:
  forall n, nadd n 0 = n.
Proof.
  intro. induction n.
  { reflexivity. }
  { simpl. rewrite -> IHn. reflexivity. }
Qed.

Question : Why did we need induction for nadd_n_0 but not for nadd_0_n ?
Consider these types for representing pairs of nats and booleans and also booleans and nats respectively:

Inductive nat_and_bool :=
| nnb : nat -> bool -> nat_and_bool.

Inductive bool_and_nat :=
| bnn : bool -> nat -> bool_and_nat.

We can write functions that swap these around:

Definition swap_nat_and_bool (x : nat_and_bool) : bool_and_nat :=
  match x with
    | nnb n b => bnn b n
  end.

Definition swap_bool_and_nat x :=
  match x with
    | bnn b n => nnb n b
  end.

We can also prove that these swaps work as we expect:

Lemma swap_swap:
  forall x, swap_nat_and_bool (swap_bool_and_nat x) = x.
Proof.
  intro. destruct x0. reflexivity.
Qed.

These definitions are overly specific though, we should define some sort of generic pair type. Unfortunately, our technique for writing parameterized definitions doesn't really cut it here: 
Definition pair x y :=
   ... (* what do we put here ?! *)
Instead we can use the type prod:

Print prod.
Inductive prod A B :=
  |  pair : A -> B -> A * B
This is an example of a parameterized type. With it we can write a generic swap function:

Definition swap (A B: Type) (p: A * B) : B * A :=
  match p with
    | pair a b => pair b a
  end.

Note that we don't have to include all the type arguments. This is due to Coq's inference mechanisms, which we will disucuss in more detail later.
We can also prove our generic swap correct:

Lemma swap_ok:
  forall A B (p: A * B),
  swap B A (swap A B p) = p.
Proof.
  intros. destruct p. reflexivity.
Qed.

One parameterized type named option is super useful for encoding partial functions:

Print option.
Inductive option (A : Type) : Type :=
  | Some : A -> option A
  | None : option A.

Definition pred (n: nat) : option nat :=
  match n with
    | O => None
    | S m => Some m
  end.

Next time we'll talk more about inductive types and how they can be used to encode syntax. However, you should check out the list type and think about it until then:

Print list.
Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.

Eval cbv in (cons 1 (cons 2 (cons 3 nil))).
This page has been generated by coqdoc