Coq for SSFT'2018 - Type Theory exercises - Level 3
Crash course in Coq

first-order logic, basics

Open the file firstorder.v in Proof General and start feeding the commands to Coq.

First-order logic is based on a notion of terms, here modelled as inhabitants of a type declared by Variable term:Type.

The next commands illustrate how to declare your signature: constants, function symbols, and predicate symbols.

Preliminary remarks: the goal display and the ∀ quantifier

The first Theorem illustrates how to manipulate the ∀ quantifier of first-order logic. Let's see how it works.

When ∀ quantifiers are involved, they form proper items of the stack or of the context, and they can be moved about in the same way we move hypotheses about. For instance after 

Theorem fa: forall n m, (forall p, Rel p m) -> Rel n m.
Proof.
  move => n.
you get the sequent 
n : term
============================
∀m : term, (∀p : term, Rel p m) → Rel n m
with 1 element in the context ("n is of type term" is the same as "n is a label for term") and 2 elements in the stack.

Justification for command move => n: in order to build a proof of ∀n F, it is sufficient to prove F, whilst making no particular assumption about n.
The converse property being true, move => n is reversible and move: n will get you back where you started, just like with implication.
You now know how to manipulate ∀ when it is below the bar.

When you find it above the bar, the same tactic as for implication works again:
apply:h here matches Rel p m against your goal Rel n m,
and will conclude that if Rel p m for all n (as stated by hypothesis h), then in particular it is true when p is instantiated as n, which is exactly what we want to prove. In other words, in this example, apply automatically finds out from your goal that it should instantiate p with n.

In other examples, apply might not be as smart and might not know how to instantiate a ∀ above the bar. In that case, a possible fallback plan for you is to do some forward-reasoning.

Exercise: prove the next theorems b and c.

∃ quantifier

Look at the proof of the next theorem, it illustrates how Finish the proof as an exercise.

Exercise: prove the next theorems d and a', noticing that the latter is a variant of axiom a) of Definition 6.6.
a) itself cannot be proved, again because Coq works in constructive logic while INF412 addressed classical logic. More on this in lecture 5.

Example: the theory of equality

Now we show how Coq handles the theory of equality.

The first axiom (forall x:term, x=x) is trivially proved by Coq, it is built-in.

The other axioms of equality for the signature consisting of the term symbol f of arity 2 and of the predicate symbol F of arity 1, are:

∀x1 x1' x2 : term, x1 = x1' → f x1 x2 = f x1' x2
∀x1 x2 x2' : term, x2 = x2' → f x1 x2 = f x1 x2'
∀x1 x1' : term, x1 = x1' → F x1' → F x1

The proof of the first of those three axioms should give you enough clues for the others.

Prove the other two axioms.

Prove the next statements.

Remark: with the axioms you have proved, it should be clear to you that, when an equality h:a=b is in your context, you can use it to replace a by b in your goal (with rewrite h) but also vice versa, replace b by a in your goal. In order to do this, you can of course invoke the fact that equality is commutative, but you can more simply write rewrite -h, as described in your cheat sheet 1.

Final remark: we have seen that, when you have a hypothesis h:∀x1 ∀x2 ∀x3... A in your context, apply:h is often able to automatically instantiate x1 x2 x3... by matching A against your goal.
This is also true of rewrite: When you have h:∀x1 ∀x2 ∀x3... t1=t2 in your context, rewrite h is often able to automatically instantiate x1 x2 x3... by matching t1 against (a subterm of) your goal.
Otherwise, you can always do some forward reasoning.

It's now time that you get the second cheat sheet that will give you more tricks on bookkeeping and other topics.