Library MyTheory.eq_example

Okay, so let's talk about the most important inductive type in HoTT.

We don't have to prove reflexivity because it's baked into the definition.

This proof for eq_sym is just like the other examples we've done with inductive types, there are no new principles at work here, although it takes some work to see the resemblance. It is the same basic rule of dependent pattern matching.

We don't bother introducing names for x and y because we don't need them.

Because eq is an inductive type, we can only use it by pattern matching, it's the only thing we know how to do. The reason we didn't bother introducing names for x and y above is because only reason we care about the value of x and y is to specify the return type of the function - but the only variables you can use to specify the return type of the function are the ones you introduce using the as and in keywords.

At this branch of the match statement, the variables z and z' take on more concrete, specialized values for this branch, corresponding to the constructor. By definition refl a : eq a a, so z becomes a and z' also becomes a. But now, because z and z' are both a, eq z' z is also eq a a! Again you can see this by entering tactic mode and doing a refine with the proof at this point. This means we can return refl a, which is of the correct type.

First we prove that y = z → x = z.

At this point in the code, both x' and y' are equal to a, and we want to prove that a = z → a = z. But this is trivial.

Then we apply this to eq_yz.

You can delete the type annotation as _ in eq x' y' return eq y' z → eq x' z and Coq will still accept it. The type annotations are helping us understand what Coq is doing, and helping us debug when Coq can't figure it out. Theorem: Functions preserve equality.

At this point in the code, eq x y becomes eq z z; and we are trying to return a value of type eq (f z) (f z). But this is immediate by reflexivity.

The inductive type False has no constructors.

Here we return a value for each of the constructors for False. Since there are no constructors for False, the match statement has no cases.

The inductive type True has a single constructor.

We end with a nontrivial theorem that requires a lemma, which we do using a let binding, as in Haskell or OCaml.

The proof of this goes by a standard trick. First, we define a family of dependent types on bool, P tt tt = True P ff tt = False P tt ff = False P ff ff = True

Return type of the function is now P a a

Return type of the function is now P tt tt

Return type of the function is now P ff ff

Now that we've proven that P b1 b2 has a section for all p1 p2, we just apply it to the assumptions in the question.

Again, all these type annotations are often not necessary, as Coq can infer them from context. But adding more annotations can help you get better error messages. Then once you get it to compile, you can try deleting the type annotations and see if it still compiles. We can delete the type annotation for match here but not for the lemma.