Exploring equality via homotopy and proof assistants - Day 2 - Equality in Coq

Note: You may use either the lab computers, or your laptop. Coq may not be installed on the Windows computers, you should use the Macs. If the Macs do not have CoqIDE installed, you can go to https://coq.inria.fr/coq-85, download CoqIDE_8.5beta2.dmg, open it, and run CoqIDE directly, without installing it. This file contains the exercises for Day 2. Some are explicitly marked as "Homework"; the rest can be done either in class or for homework. When doing exercises on your own, feel free to skip around; there are some interesting puzzles near the bottom (around J_implies_UIP). If you feel like you know exactly how a proof will go, but find it painful and tedious to write out the proof terms explicitly, come find me. Coq has a lot of support for automation and taking care of things that are easy and verbose, so you don't have to. Proving should feel like a game. If it doesn't, I can probably help you with that. N.B. There are many theorem provers out there, e.g., Agda, Idris, NuPRL, Otter, Twelf, Isabelle/HOL, Mizar, Metamath The following are placeholders; admit indicates that something should be filled in later.

Tautologies

We'll fill in these first few together. Any ideas for how to to prove something like this?

We can also write the colon on a line of its own; I set up this file in this way so that I can use a large font in my presentation.

N.B. A → (B → C) and A → B → C are the same; → associates to the right.

We can also fill in the functions bit by bit, as follows:

These two are exercises to do individually or with the people sitting next to you.

Optional Homework Problems for More Practice

This one is a bit different; one of the arguments has a ∀

Challenge Homework Problems Come ask me about disjunction and negation during TAU if you are interested in playing with these. Prove that the Law of Excluded Middle implies Double Negation Elimination

Prove that Double Negation Elimination implies Peirce's Law

Prove that Peirce's Law implies the Law of Excluded Middle

Judgmental equality.

We allow writing refl for eq_refl.

Interesting question: Are all proofs of equality themselves equal? Keep this in the back of your mind as we define what equality is. To do this we need to define two notions of equality: judgmental, and propositional. Coq knows some things about equality. If Coq judges that two things are equal (and equally trivially), then you can prove them (propositionally) equal by reflexivity, with refl. In this case, we say that they are also judgmentally equal. For example: Propositional equality is denoted as x = y. Definition of judgmental equality, version 1: intuitively, x and y are judgmentally equal if there is a really stupid, trivial proof that x = y. Definition of judgmental equality, version 2: x and y are judgmentally equal if (Coq says that) refl proves x = y.

Just so that you don't think Coq believes everything is equal:

This gives

The command has indeed failed with message:
=> Error: The term "refl" has type "?30 = ?30"
    while it is expected to have type "1 = 0".

You can see the "normal form" of something with Compute:

Definition of judgmental equality, version 3: x and y are judgmentally equal if Compute gives you the same normal form for x and y. N.B. This is equivalent to what Coq is doing internally. Note that equality is homogeneous; the things you're comparing for equality need to already have the same type. You can ask if a statement is valid using Check:

A note on syntax

Pattern matching is case analysis, on things that are defined by cases (like, bool, nat). This is a technical meaning for "pattern matching" or "case analysis", namely, "using a match ... with ... end statement in Coq".

unit is a type with one element.

But refl does not prove that all units are equal.

But we can pattern match

Optional Homework for More Practice This should send true to false, and false to true.

This should implement the truth table for "and":

  A B │ A ∧ B
  ────┼──────
  T T │   T
  T F │   F
  F T │   F
  F F │   F

This should implement the truth table for "or":

  A B │ A ∨ B
  ────┼──────
  T T │   T
  T F │   T
  F T │   T
  F F │   F

This should implement the truth table for "xor":

  A B │ A ⊕ B
  ────┼──────
  T T │   F
  T F │   T
  F T │   T
  F F │   F

This should implement the truth table for "implication":

  A B │ A → B
  ────┼──────
  T T │   T
  T F │   F
  F T │   T
  F F │   T

This should implement the truth table for "biconditional":

  A B │ A ↔ B
  ────┼──────
  T T │   T
  T F │   F
  F T │   F
  F F │   T

Recall: Are all proofs of equality themselves equal? Here we define what equality is, i.e., how to use it. We can prove the J-rule by pattern matching. We start off with the simpler version, called the "non-dependent" version.

If you want to not always have to pass all of the arguments to J explicitly, you can uncomment the following lines, removing the and , to make A, x, and y be inferred automatically.

Arguments J_nondep {A} {x} {y} H P _.

Recall the blackboard proof of symmetry, that x = y → y = x. Someone remind me how it goes. First prove this by passing arguments to J_nondep.

Now prove this by pattern matching.

We allow writing sym p to mean sym _ _ _ p

First prove this by passing arguments to J_nondep.

Now prove this by pattern matching.

First prove this by passing arguments to J_nondep.

First prove this by pattern matching.

Now the version with more bells and whistles, again provable by pattern matching.

J also has a computation rule, which holds judgmentally. We start with the rule for J_nondep.

If you want to not always have to pass all of the arguments to J explicitly, you can uncomment the following lines, removing the and , to make A, x, and y be inferred automatically.

Arguments J {A} {x} {y} H P _.
Arguments J_computes {A x} P k.
Arguments J_non_computes {A x} P k.

First prove this by passing arguments to J.

Now prove this by pattern matching.

Exercises to do individually, or with the people next to you. First prove this by filling in arguments to J explicitly.

Now prove this by pattern matching.

Recall the informal proof from yesterday's homework, which "proved" that all proofs of x = y are themselves equal: The J rule says informally that if you have a proof p of x = y, it suffices to assume that y is x (to substitute x for y in what you are trying to prove), and to assume that p is refl x (to substitute refl x for p in what you are trying to prove). Suppose we have a type A, two inhabitants x and y of type A, and two proofs p and q that x = y. By J, it suffices to assume that y is x, that p is refl x, and hence it suffices to prove that refl x = q, where q now has type x = x. To prove this, again by J, it suffices to assume that x is x (it already is) and that q is refl x, and hence it suffices to prove refl x = refl x. We can prove this by refl (refl x). Thus for any proofs p and q that x = y, we have p = q. Qed. Try to formalize this proof in Coq, and see what goes wrong. It may help to use refine so that you can construct the proof sentence by sentence. If you are having trouble figuring out how to instantiate J for a proof of equality H : x = y, you can ask Coq to figure it out for you by running destruct H.. You can see what it did by typing Show Proof. afterwards.

The rest of these are explicitly Homework; feel free to take a break now, or to keep going. Recall from yesterday's homework that the K rule says:

Prove that K implies uniqueness of identity proofs. If you do this interactively with refine, you may find it useful to unfold K_rule_type in × to see the definition of K in your goals window.

Note that it's impossible to prove K from J. See if you can get any insight into this by attempting to construct a proof. Hint: Think about what these things (and UIP) mean in the paths interpretation of equality, and remember that all of our functions are continuous.

Can you write down three "different" proofs of transitivity (they should all be judgmentally different; refl should not prove any two of them the same.

Now we have Coq check that they are not the same; these lines should compile unmodified.

Now prove that these are all equal (propositionally, but not judgmentally.

We can also prove associativity.

Category theory

Those of you familiar with category theory might find the following properties interesting. All exercises in this section are optional homework. We can look at ap as describing the action on morphisms (equality proofs) of any function; the type of morphisms from x : A to y : A is the type x = y; the action of f : A → B on a morphism m : x = y is ap f m : f x = f y. We can prove the relevant functoriality properties. Action on identity:

Action on composition:

Action on inverses (additional rule for groupoids):

Furthermore, every function that specifies the action of a natural transformation on objects is automatically natural:

Further exploration:

These are completely optional, and moderately challenging. If you are interested, here are some problems that draw interesting connections between this material and category theory. 1. Can you find and prove a statement relating sym_sym to sym_trans? 2. Can you find and prove a statement relating sym to trans_assoc and sym_trans via ap? 3. The equality relation on a type forms a weak ω-groupoid (sometimes written as a weak ∞-groupoid). This means that there is structure at every level. The first few levels are given by refl, sym, and trans (level 1); sym_sym, sym_trans, trans_assoc, sym_refl, trans_1p, trans_p1, trans_pV, and trans_Vp (level 2). The theorem statements in general are known as the Stasheff polyhedra or Stasheff associahedra. Can you discover more of these rules?