Preliminaries

Instructor's Name: Jason Username: espuser Password: !Splash2014 How to install Coq: Open up a terminal, and type

    tellme root
    sudo apt-get install coq coqide emacs proofgeneral-coq

At home, you can download it from https://coq.inria.fr/. You can download this file from: http://web.mit.edu/jgross/Public/2014-splash/equality/exercises.v

Warmup - Getting used to Coq

Let's see how to prove some things. You may find http://andrej.com/coq/cheatsheet.pdf helpful. Here's a partial list:

• simpl simplifies things
• compute shows you the normal form
• intro x
• destruct x, case x, induction x do case analysis on x
• reflexivity proves a goal of the form x = x
• apply H makes use of a hypothesis H
• rewrite H replaces x with y when H is of type x = y
• rewrite <- H replaces y with x when H is of type x = y
• split is used to prove _ ∧ _ (conjunction)
• left and right are used to prove _ ∨ _ (disjunction)

We use a cheating axiom as a placeholder. Your code should not end with any admits. We use curly braces to not have to give T explicitly.

We begin by defining equality:

This says the following:

• To ask the question, "is x equal to y?", x and y must both have the same type A.
• The only way to construct a proof of equality is by reflexivity, which proves, for all x, that x = x.
• The way to make use of an equality e : x = y is to replace y with x and e with refl. This is formalized in eq_rect:

 eq_rect
     : forall (A : Type) (x : A) (P : forall a : A, x = a -> Type),
       P x refl -> forall (y : A) (e : x = y), P y e

This says that if you are trying to prove P y e for any y : A and e : x = y, it sufficies to prove P x refl, i.e., it sufficies to replace y with x and e with refl and prove the resulting statement. Using the tactic destruct e or induction e will perform this step in a proof. Furthermore, there is a computation rule, which says that when y is already x and e is already refl, the eq_rect disappears from your proof, and the resulting term of type P y e *is* the same as the term of type P x refl. Let's see that this obeys our intuitions.

You'll want to use case or destruct here, to do case analysis on the "proof of False". (Hint: There are no proofs of False. So if you have one, you can do trivial case analysis, and there are no cases.)

Let's prove some simple lemmas.

We make a notation, so that sym e can be written e^ or e⁻¹. Switch the order of these if you want it to display as e^.

We make another notation for trans, which can be thought of as concatenating or composing equality proofs.

When are two proofs of equality themselves equal? Since refl proves x = x, we have that any proof of equality is equal to itself.

Our computation rules also give us that refl⁻¹ = refl and refl • refl = refl.

unfold sym

plug arguments into functions

compute pattern matches

We can prove the following in two different ways: By doing case analysis on b1 then b2, or by doing case analysis on b2 then b1. N.B. There are more ways to prove this theorem, which might not all be equal.

We can prove that these two proofs are equal, by case analysis on b1 and b2.

We can, in fact, prove this in another way, too.

And we can prove that these two ways are equal...

What other properties can we prove?

There are also rules for how ap plays with trans and sym. Try to state and prove them.

Now back to the rules not involving ap.

We can relate trans_1p, trans_p1, and trans_assoc in a commutative triangle:

    (p • refl) • q == p • (refl • q)
           \\          //
             \\      //
               \\  //
                p • q

There is a similar pentagon relating the two different ways of proving that p @ (q @ (r @ s)) = ((p @ q) @ r) @ s using chains of trans_assoc. Write down the five legs of this pentagon, and prove that the two paths are equal.

  ((p @ q) @ r) @ s ======= (p @ (q @ r)) @ s
          ||                    ||
          ||                    ||
          ||                    ||
   (p @ q) @ (r @ s)         p @ ((q @ r) @ s)
          \\                   //
            \\               //
              \\           //
                \\       //
             p @ (q @ (r @ s))

There are higher dimensional rules, too, that relate the triangle and the pentagon. They are known as Stasheff polyhedra or associahedra. Let's look at more complicated things. We can proof that all proofs of False are equal Hint 1: There are no such proofs. Hint 2: You can use exfalso to say "it sufficies to prove False".

We can prove that all proofs of false = true are equal.

We can proof that all proofs of equality of things of type unit are equal, but we need to prove something more general.

It sufficies to prove that all x : unit are equal to tt. To do this, we need to construct a canonical proof of tt = x for all x.

Note: to see the result of applying a theorem to an argument, you can use pose proof (thm args) as H.

It is possible to prove that all proofs of true = true are equal, but we have to prove a more general theorem. Namely, we need to prove a fact for all b : bool and p : true = b at once. In the case that b is true, we prove that p = refl. In the case that b is false, we prove absurdity (False).

UIP stands for "uniqueness of identity proofs".

More generally, we can prove uniqueness of identity proofs for booleans.

It is possible to prove that UIP goes up levels.

Can you prove this in general? We can try to ask: "Are all proofs of equality equal to reflexivity?" But this question does not typecheck. There are subtle reasons for this, and it ends up being important.

We can instead try to prove that any proof of x = x is refl.