# Library Prop

Section prop.

A proposition is a definitive statement which we may be able to prove. In Coq we write P : Prop to express that P is a proposition.

We will later introduce ways to construct interesting propositions, but in the moment we will use propositional variables instead. We declare in Coq:

Variables P Q R : Prop.

This means that the P,Q,R are atomic propositions which may
be substituted by any concrete propositions. In the moment it is helpful to think of them as statements
like "The sun is shining" or "We go to the zoo."

We are going to introduce a number of connectives and logical constants to construct propositions:

- Implication ->, read P -> Q as if P then Q.
- Conjunction /\, read P /\ Q as P and Q.
- Disjunction \/, read P \/ Q as P or Q.
- False, read False as "Pigs can fly".
- True, read True as "It sometimes rains in England."
- Negation ~, read ~ P as not P. We define ~ P as P -> False.
- Equivalence, <->, read P <-> Q as P is equivalent to Q. We define P <-> Q as (P -> Q) /\ (Q -> P).

- Implication is right associative, i.e. we read P -> Q -> R as P -> (Q -> R).
- Implication and equivalence bind weaker than conjunction and disjunction. E.g. we read P \/ Q -> R as (P \/ Q) -> R.
- Conjunction binds stronger than disjunction. E.g. we read P /\ Q \/ R as (P /\ Q) \/ R.
- Negation binds stronger than all the other connectives, e.g. we read ~ P /\ Q as (~ P) /\ Q.

We will now discuss how to prove propositions in Coq. If we are
proving a statement containing propositional variables then this means
that the statement is true for all replacements of the variables with
actual propositions. We say it is a tautology.

We start with a very simple tautology P -> P, i.e. if P then P.
To start a proof we write:

Lemma I : P -> P.

It is useful to run the source of this document in Coq to see what
happens. Coq enters a proof state and shows what we are going to prove
under what assumptions. In the moment our assumptions are that
P,Q,R are propositions and our goal is P -> P. To
prove an implication we add the left hand side to the assumptions and
continue to prove the right hand side - this is done using the intro
tactic. We also choose a name for the assumption, let's call it p.

intro p.

This changes the proof state: we now have to prove P but we also
have a new assumption p : P. We can finish the proof by using this
assumption. In Coq this can done by using the exact tactic.

exact p.

This finishes the proof. We only have to instruct Coq to save the
proof under the name we have indicated in the beginning, in this case I.

Qed.

Qed stands for "Quod erat demonstrandum". This is Latin for "What was to be shown."

Next we will prove another tautology, namely
(P -> Q) -> (Q -> R) -> P -> R.
Try to understand why this is intuitively true for any propositions P,Q and R.

To prove this in Coq we need to know how to use an implication which we have assumed. This can be done using the apply tactic: if we have assumed P -> Q and we want to prove Q then we can use the assumption to reduce (hopefully) the problem to proving P. Clearly, using this step is only sensible if P is actually easier to prove than Q. Step through the next proof to see how this works in practice!

To prove this in Coq we need to know how to use an implication which we have assumed. This can be done using the apply tactic: if we have assumed P -> Q and we want to prove Q then we can use the assumption to reduce (hopefully) the problem to proving P. Clearly, using this step is only sensible if P is actually easier to prove than Q. Step through the next proof to see how this works in practice!

Lemma C : (P -> Q) -> (Q -> R) -> P -> R.

We have to prove an implication, hence we will be using intro.
Because -> is right associative the proposition can be written as
(P -> Q) -> ((Q -> R) -> P -> R). Hence we are going to assume P -> Q.

intro pq.

we continue assuming...

intro qr.

intro p.

Now we have three assumptions P -> Q, Q -> R and P.
It remains to prove R. We cannot use intro any more because our goal is not
an implication. Instead we need to use our assumptions. The only assumption which
could help us to prove R is Q -> R. We use the apply tactic.

apply qr.

Apply uses Q -> R to reduce the problem to prove R to the problem to prove Q.
Which in turn can be further reduced to proving P using P -> Q.

apply pq.

And now it only remains to prove P which is one of our assumptions - hence we can use exact again.

exact p.

Qed.

Qed.

We observe that there are two types of proof steps (tactics):

- introduction: How can we prove a proposition? In the case of an implication this is intro. To prove P -> Q, we assume P and prove Q.
- elimination: How can we use an assumption? In the case of implication this is apply. If we know P -> Q and we want to prove Q it is sufficient to prove P.

There is also a 3rd kind of steps: structural steps.
An example is exact which we can use when we want to refer to an assumption.
We can also use assumption then we don't even have to give the name of the assumption.

If we want to combine several intro steps we can use intros. We can also use intros without parameters in which case Coq does
as many intro as possible and invents the names itself.

How to prove a conjunction? To prove P /\ Q we need to prove P and Q. This is achieved using the split tactic. We look at a simple example.

Lemma pair : P -> Q -> P /\ Q.

On the top level we have to prove an implication.

intros p q.

now to prove P /\ Q we use split.

split.

This creates two subgoals. We do the first

exact p.

And then the 2nd

exact q.

Qed.

How do we use an assumption P /\ Q. We use destruct to split it into two assumptions.
As an example we prove that P /\ Q -> Q /\ P.

Lemma andCom : P /\ Q -> Q /\ P.

intro pq.

destruct pq as [p q].

split.

Now we need to use the assumption P /\ Q. We destruct it into two assumptions: P and Q.
destruct allows us to name the new assumptions.

exact q.

exact p.

Qed.

Can you see a shorter proof of the same theorem ?

To summarize for conjunction we have:

- introduction: split: to prove P /\ Q we prove both P and Q.
- elimination: destruct: to prove something from P /\ Q we prove it from assuming both P and Q.

Maybe you have already noticed that a statement like P -> Q -> R
basically means that R can be proved from assuming both P and Q.
Indeed, it is equivalent to P /\ Q -> R. We can show this formally by using
<-> for the first time.

All the steps we have already explained so I won't comment. It is a good idea to step through the proof using Coq.

All the steps we have already explained so I won't comment. It is a good idea to step through the proof using Coq.

Lemma curry : (P /\ Q -> R) <-> (P -> Q -> R).

unfold iff.

split.

intros H p q.

apply H.

split.

exact p.

exact q.

intros pqr pq.

apply pqr.

destruct pq as [p q].

exact p.

destruct pq as [p q].

exact q.

Qed.

I call this the currying theorem, because this is the logical counterpart of currying in functional programming: i.e. that a function with several parameters can be reduced to a function which returns a function. So in Haskell addition has the type Int -> Int -> Int.

To prove a disjunction like P \/ Q we can either prove P or Q. This is done via the tactics left and right. As an example we prove P -> P \/ Q.

Lemma inl : P -> P \/ Q.

intros p.

Clearly, here we have to use left.

left.

exact p.

Qed.

To use a disjunction P \/ Q to prove something we have to prove it from both P and Q. The tactic we use is also called destruct but in this case destruct creates two subgoals. This can be compared to case analysis in functional programming. Indeed we can prove the following theorem.

Lemma case : P \/ Q -> (P -> R) -> (Q -> R) -> R.

intros pq pr qr.

destruct pq as [p | q].

The syntax for destruct for disjunction is different if we want to name the assumption we have to separate them with |. Indeed each of them will be visible in a different part of the proof.
First we assume P.

apply pr.

exact p.

And then we assume Q

apply qr.

exact q.

Qed.

So again to summarize: For disjunction we have:

- introduction: there are two ways to prove a disjunction P \/ Q. We use left to prove it from P and right to prove it from Q.
- elimination: If we have assumed P \/ Q then we can use destruct to prove our current goal from assuming P and from assuming Q.

As an example of how to combine the proof steps for conjunction
and disjunction we show that distributivity holds, i.e. P /\ (Q \/
R) is logically equivalent to (P /\ Q) \/ (P /\ R). This is
reminiscent of the principle in algebra that x * (y + z) = x * y + x * z.

Lemma andOrDistr : P /\ (Q \/ R)

<-> (P /\ Q) \/ (P /\ R).

split.

intro pqr.

destruct pqr as [p qr].

destruct qr as [q | r].

left.

split.

exact p.

exact q.

right.

split.

exact p.

exact r.

intro pqpr.

destruct pqpr as [pq | pr].

split.

destruct pq as [p q].

exact p.

left.

destruct pq as [p q].

exact q.

destruct pr as [p r].

split.

exact p.

right.

exact r.

Qed.

As before: to understand the working of this script it is advisable to step through it using Coq.

True is just a conjunction with no arguments as opposed to /\ which has two. Similarity False is a disjunction with no arguments. As a consequence we already know the proof rules for True and False.

We can prove True without any assumptions.

We can prove True without any assumptions.

Lemma triv : True.

split.

Here we split but instead of two subgoals we get none.

Qed.

On the other had we can prove anything from False. This is called "ex falso quod libet" in Latin.

Lemma exFalso : False -> P.

intro f.

destruct f.

Here instead of two subgoals we get none.

Qed.

In terms of introduction and elimination steps we may summarize:

- True: There is one introduction rule but no elimination.
- False: There is one elimination rule but no introduction.

~ P is defined as P -> False. Using this we can establish some basic theorems about negation. First we show that we cannot have both P and ~ P, that is we prove ~ (P /\ ~ P).

Lemma incons : ~ ( P /\ ~ P).

unfold not.

intro h.

destruct h as [p np].

apply np.

exact p.

Qed.

Another example is to show that P implies ~ ~ P.

Lemma p2nnp : P -> ~ ~ P.

unfold not.

intros p np.

apply np.

exact p.

Qed.

You may expect that we can also prove the other direction ~ ~ P -> P and that indeed P <-> ~ ~ P.
We can reason that P is either True or False and in both cases ~ ~ P will be the same. However,
this reasoning is not possible using the principles we have introduced so far. The reason is that Coq is based
on intuitionistic logic, and the above proposition is not provable intuitionistically.

However, we can use an additional axiom, which corresponds to the principle that every proposition is either True or False, this is the Principle of the Excluded Middle P \/ ~ P. In Coq this can be achieved by:

However, we can use an additional axiom, which corresponds to the principle that every proposition is either True or False, this is the Principle of the Excluded Middle P \/ ~ P. In Coq this can be achieved by:

Require Import Coq.Logic.Classical.

This means we are now using Classical Logic instead of Intuitionistic Logic. The only difference is that we have an
axiom classic which proves the principle of the excluded middle for any proposition. We can use this to prove
~ ~ P -> P.

Lemma nnpp : ~~P -> P.

intro nnp.

Here we use a particular instance of classic for P.

destruct (classic P) as [p | np].

First case P holds

exact p.

2nd case ~ P holds. Here we appeal to exFalso.

apply exFalso.

Notice that we have shown exFalso only for P. We should have shown it for any proposition but this would
involve quantification over all propositions and we haven't done this yet.

apply nnp.

exact np.

Qed.

Unless stated otherwise we will try to prove propositions intuitionsitically, that is without using classic.
An intuitionistic proof provides a positive reason why something is true, while a classical proof may be
quite indirect and not so easily acceptable intuitively. Another advantage of intuitionistic reasoning is that it
is constructive, that is whenever we prove the existence of a certain object we can also explicitly construct it.
This is not true in intuitionistic logic. Moreover, in intuitionistic logic we can make differences which disappear
when using classical logic. For example we can explicit state when a property is decidable, i.e. can be computed
by a computer program.

This is a good point to introduce another structural rule: the cut rule.
Cutting a proof means to introduce an intermediate goal, then you prove
your current goal from this intermediate goal, and you prove theintermediate goal.
This is particularly useful when you use the intermediate goal several times.

In Coq this can be achieved by using assert. assert h : H introduces H as a new subgoal and after you have proven this you can use an assumption h : H to prove your original goal.

The following (artificial) example demonstrates the use of assert.

In Coq this can be achieved by using assert. assert h : H introduces H as a new subgoal and after you have proven this you can use an assumption h : H to prove your original goal.

The following (artificial) example demonstrates the use of assert.

Lemma usecut : (P /\ ~P) -> Q.

intro pnp.

If we had a generic version of exFalso we could use this.
Instead we can introduce False as an intermediate goal.

assert (f : False).

which is easy to prove

destruct pnp as [p np].

apply np.

exact p.

apply np.

exact p.

and using False it is easy to prove Q.

destruct f.

Qed.

Qed.

This example also shows that sometimes we have to cut (i.e. use assert) to prove something.