Coq for SSFT'2018 - Type Theory exercises - Level 3

`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.

`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 mwith 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.

`b`

and `c`

.

`∃`

quantifier- tactic
`case`

manipulates the existential quantifier above the bar. - tactic
`exists`

(again) manipulates the existential quantifier below the bar.

`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.

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.

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.