coq_lecture
Require Import Coq.Init.Prelude.
Introduction
Why do we want this?
 Mathematicians are people (too!) and so make mistakes. In
mathematics we're (usually) only interested in things that are true
or correct. Sometimes the mathematics involved is so complicated
that nobody wants to check it, sometimes nobody but the author even
can check it! (These cases are bad for other reasons).
 Working in mathematics can be, as i'm sure you'll agree, challenging
and difficult. Sometimes keeping track of all the details can be
overwhelming, and at times even distracting.
 In a related way, sometimes the details aren't really important and
are mechanical (``just check these five calculations''), but
verifying them is still time consuming and difficult.
 Not everyone agrees on what is easy or difficult in mathematics, and sometimes the details provided in a proof aren't sufficient for every purpose.
What is Coq?
Using this document
(** Blaf *)is a ``comment'' and will be ignored by Coq. Here is something that is not a comment, notice how it lives outside of the blue boxes, or in the raw version has different colours.
Check (5).
Using https://x80.org/collacoq/
Check (6).
Check (127).
Check (57).
As you can see, Coq told us some things in the lower righthand
side window. This is the ``Response'' window, and above it is the
``Goals'' window. We'll learn about these later, but for now know that
they're there and will serve as locations of Coq output.
Finally, Collacoq supports saving your work. If you press the save
icon in the ``hastebin'' area above, you'll notice that the URL has
changed to reflect your document id. Copying this URL allows you and
others to retrieve the document at a later date.
Warning: I have no idea how long Collacoq retains documents.
A primer on notation
Types
In Coq we will often deal with things which look likestuff : ThingThe way we read this aloud is stuff is of type Thing. Unfortunately that's not very insightful so instead we mostly say
Check (5).
Then in the ``Response'' window we'll see that Coq tells us
Here's another example:
5 : natTry pronouncing this as above, 5 is a nat.
Check (Prop).
Based on the output in the ``Response'' window we can say Prop is
a Type ... perhaps we didn't learn anything.
So what's a type?
For our purposes a type should be thought of as a collection, in some
ways like a set. Types have terms in the same way that sets have
elements, and if you find this confusing you'll do no harm right now in
calling them the same thing. In fact, let's ask Coq what nat is
supposed to be.
Check (nat).
So we see that nat is a Set, but for some reason Prop is a
Type. This is a technical distinction and we won't dwell on it now.
The summary is that we think of nat and Prop as the same sort of thing,
they're both collections.
nat is the collection of natural numbers 0, 1, 2, ...
So of what is Prop the collection?
Propositions
In Coq, Prop represents the collection of all propositions  those logical statements which may be proven or disproven and on which we developed all of our logical operations: and, or, not, implies, ...Section section1.
Variable (P : Prop).
Coq says some confusing stuff in the ``Response'' window, and who
knows what this notation means, but now we're living in a world where
Coq knows that P is a Prop.
The thing that makes propositions interesting is that they may be
proven. What does it mean to prove a proposition true in Coq?
Unlike natural numbers which are somehow atomic, a proposition may
have elements all its own. This is a little confusing at first. Let's
tell Coq that we want to assume that P is true.
Variable (p : P).
What does the following do?
Check (Prop).
Check (P).
Check (p).
We're told:
Above we said that we only mostly pronounce `:' as ``is a''. This is
one of the cases where we don't want to do that.
Instead we read p : P as: P is true because of p.
Elements of a proposition are proofs that it's true. So you can think
of propositions in Coq as convenient containers which store proofs of
their truth. We're just going to get rid of our variables quickly.
 Prop is a Type, just like before
 P is a Prop, this still makes sense
 p is a P? This doesn't seem to work.
End section1.
How to read arrows `>'
Check S.
Coq tells us
S is a nat > nat.
Hmm, well the problem seem to lie in the fact that we don't know how
to read nat > nat. What is it?
S : nat > natLet's try to apply our pronounciation to this, shall we?
Check (nat > nat).
Coq tells us that nat > nat is a Set. Well that didn't tell us
much except perhaps that it might be instructive to think about what
its elements, like S, are supposed to be.
In Coq we think of nat > nat as the collection of functions from nat to
nat.
So an element of nat > nat, like S above, is a function which takes a
nat and produces a nat. To be sure, let's ask Coq to work out a few
cases of successor
Compute (S 0).
Compute (S 1).
Compute (S 162).
Thinking about functions, here's a weird case to consider. We said
that if P Q : Prop then both P and Q have elements  proofs of
their truths , so it makes sense to ask: what are the elements of P
> Q?
First lets ask Coq what P > Q even is. We have to introduce some
variables for this to make sense.
Section section2.
Variable (P Q : Prop).
Check (P > Q).
End section2.
Umm what? Coq says that P > Q is a Prop. That means that, by
our first guide, if we had imp : P > Q then we would be forced to
read this as P > Q is true because of imp.
But by our guide for functions, imp : P > Q would be read as
imp is a function from P to Q. So which is it?
The answer is both! When P Q : Prop we can read P > Q as the
collection of proofs that P implies Q. What does it mean for P
to imply Q? It means that if we assume that P is true then we can
derive that Q is true.
What does it mean to assume that P is true? It means that we have p
: P.
What does it mean for Q to be true? It means to give some q : Q.
What does it mean to derive that Q is true from a proof that P is
true? It means to take as input a p : P and provide as output a q :
Q  a function!
A function between propositions is an implication!
So now we may happily read P > Q as the collection of proofs for the
logical implication P implies Q or, as before, as the collection
of functions from P to Q.
This is perhaps the most important concept we'll meet. Let's make
sure you understand it!
With the understanding that A > B is the collection of functions
from A to B, how would we read A > B > C?
Here's a hint, let's see what Coq makes of the following:
How to read more arrows
Check plus.
When we think of the function plus on nat, we think of it as a
function that takes two arguments, say m and n, and returns their
sum, m+n.
They way that Coq writes this for us is nat > nat > nat. Thus, to read
this in a compatible way we say plus is a function from nat to nat
to nat with the understanding that all but the last bit is the input.
In general then, In_1 > In_2 > ... > In_k > Out is the collection of
functions which take as input elements of type In_1 through In_k
and produce an output of type Out. We'll see another example of this
shortly.
Our starting point for computer assisted proofs is propositional
calculus, just as it was when we were learning mathematics `by
hand' originally.
The first topic we'll learn about is logical conjunction, `and'.
In Coq this means that given propositions P and Q we may form the
proposition `P and Q'. Let's ask Coq what it thinks `and' is:
Propositional calculus
Conjunctions, P /\ Q
Check (and).
Coq says,
By our pronounciation guide above, this says and is a function
from Prop to Prop to Prop.
That is, `and' is a machine which takes in a proposition, and another
proposition and gives us a resulting proposition.
Coq has convenient notation for `and', which we will use. If P and Q
are propositions, or in Coq's language, P Q : Prop  note the space
separating the propositions P and Q , then we may write P /\ Q
where we might want ``P and Q'' and it means exactly the same thing.
Alright, but how do we prove a conjunction? We have learnt that to
prove P /\ Q we must give a proof of P as well as a proof of Q. The
corresponding idea in Coq is called `conj'. Let's see,
and : Prop > Prop > Prop
Check (conj).
Coq says,
We read this as follows:
For all propositions A and B, to give a proof of A /\ B we may give
a proof of A as well as a proof of B.
That is, `conj' is a machine which takes a proof of A, a proof of B
and produces a proof of A /\ B.
In fact at this point we have enough to prove our first theorem.
conj : forall A B : Prop, A > B > A /\ B
Our first theorem
This won't be especially thrilling for its mathematical content, but we do rather have to start somewhere. Our first target is a theorem whose truth we should all recognise:Let P be a proposition. If P then P /\ P.
The paper proof
If we wanted to prove this on paper, and we wanted to be extracareful, we might proceed like this.Goal: P > P /\ P Context:1. To give a proof of the form A > B we may assume A and derive B.
Goal: P /\ P Context: P2. To give a proof of P /\ P we must give a proof of P, as well as a poof of P.
Goals: P, P Context: P3. Now we have two goals, so lets deal with them individually.
Goal: P Context: P4a. By hypothesis we have a proof of P, exactly what we need for this goal
Goal: P Context: P4b. By hypothesis we have a proof of P, so we have exactly what we need.
QED.5. We have no more goals so we are done.
The Coq proof
Now suppose instead we wanted to leverage the power of the Coq computer proof assistant system, how would our proof look? In what follows we'll intersperse the Coq instructions with explanations, just like before. Run this document in Collacoq only up to the start of every comment block so that you're following along at the desired pace.Stating our theorem
We'll begin by writing down what we want to prove, so that Coq can help us keep track of our argument. If we want to begin to prove the same theorem as before, we might tell Coq the following.Theorem our_first_theorem (P : Prop) : (P > P /\ P).
Proof.
Let's analyse this linebyline and learn some things as we go.
The takeaway here is:
To introduce a theorem and begin to prove it we write
Theorem name_of_theorem (context) : (statement).
Proof.
 On the first line, Theorem our_first_theorem (P : Prop) : (P > P /\ P).
we say many things at once.
 tell Coq we're going to be starting a theorem by using the Theorem
keyword,
 name our theorem, in this case our_first_theorem,
 tell Coq the context in which the theorem is stated. In the
case of our theorem, we're reasoning about a proposition P and
so we write (P : Prop) next to the name,
 tell Coq what our result should be. In this case we want to state
``If P then (P and P)'', which we would turn into the symbols
P > P /\ P
 tell Coq we're going to be starting a theorem by using the Theorem
keyword,
 On the second line we tell Coq that we're about to prove the result by using the Proof. keyword.
To introduce a theorem and begin to prove it we write
Theorem name_of_theorem (context) : (statement).
Proof.
Interactive theorem proving in Coq
1 subgoal P : Prop ============================ P > P /\ P
intro proof_of_P.
In step (1.) of the paper proof we reasoned that to prove A > B
it's enough to suppose A and derive B. The analagous idea is
achieved in Coq by introducing an hypothesis.
You should now see that the ``Goals'' window states
What have we done?
We have told Coq to hypothesise that we have a proof named
proof_of_p of our proposition P. Coq obliged and added that to our
hypotheses, as we can see above.
When the goal is of the form A > B, intro proof_of_A. will add the hypothesis proof_of_A to our context so that we may conclude B.
Remember: We think of a term of a proposition as a proof of
its truth, so proof_of_P : P reads ``P is true because of
proof_of_P''.
In step (2) of the paper proof we used reasoned that in order to
construct a proof of A /\ B it was enough to give a proof of A as
well as a proof of B. In the world of Coq, applying this sort of
reasoning is achieved as follows.
1 subgoal P : Prop proof_of_P : P ============================ P > P /\ P
When the goal is of the form A > B, intro proof_of_A. will add the hypothesis proof_of_A to our context so that we may conclude B.
apply (conj).
Here we have told Coq to apply conj to our goal. Recall that
conj : forall A B : Prop, A > B > A /\ B
and so Coq figured out that, because our goal was of the form P /\ P
we wanted to use conj with A and B both as P. It then applied it
to our goal to allow us to reduce the task of giving a proof of P /\
P to that of giving a proof of P as well as a proof of P.
We might summarise this by saying that when we write apply (thing). apply moves our goal backwards through thing.
To reflect this fact the ``Goals'' window now says
Just as in the paper proof, Coq now tells us that we have two goals.
In the same way that we attended to each one individually in the paper
proof, so too do we have a way to focus Coq's attention to a
particular subgoal. We do this as follows:
conj : forall A B : Prop, A > B > A /\ B
We might summarise this by saying that when we write apply (thing). apply moves our goal backwards through thing.
2 subgoals P : Prop proof_of_P : P ============================ P subgoal 2 is0 P

That's right, it's a dash (or minus sign), as though we are
starting a list. We've now narrowed Coq's attention to the first
subgoal we had before. Observe that the ``Goals'' window now says
To focus on the next subgoal in the list, write 
With that, we can start to wrap up this proof. Coq is telling us,
just as we had in (4b.) above, that we need to prove P and that we
have, as part of our hypotheses, a proof of P, namely proof_of_P :
P.
How do we tell Coq to use this proof_of_P?
1 subgoals P : Prop proof_of_P : P ============================ P
To focus on the next subgoal in the list, write 
exact (proof_of_P).
By doing this we are telling Coq that we have exactly what we need
to achieve our goal.
Whenever we have a thing in context that satisfies our goal we can tell Coq to use it by writing exact (thing).
The ``Response'' window will then happily announce:
This is Coq reminding us that while we have proven our first goal,
there are others. We do as it suggests and focus on the next goal with
another 
Whenever we have a thing in context that satisfies our goal we can tell Coq to use it by writing exact (thing).
This subproof is complete, but there are some unfocused goals. Focus next goal with bullet .

This is step (4b.) of the paper proof, and this is exactly the
same as the previous case, so we can conclude it in the same way.
exact (proof_of_P).
Hurrah! At this point the ``Goals'' window says
No more subgoals.We have nothing left to prove at this point, and so we conclude the proving session with an emphatic ...
Qed.
Coq understands that this means that we are done, and will commit
our theorem to its memory.
To end a proof and store have Coq store your work in its memory write Qed.
To be extra sure, we can now ask Coq about our_first_theorem
To end a proof and store have Coq store your work in its memory write Qed.
Check (our_first_theorem).
In the ``Response'' window we see
All in all, without the giant comment blocks in the way, the Coq code
we gave for this theorem and its proof is this:
our_first_theorem : forall P : Prop, P > P /\ Pwhich is a little difficult to read in its present form, and so we break it up mentally like this instead.
our_first_theorem says (forall P : Prop), P > P /\ P
Theorem our_first_theorem (P : Prop) : (P > P /\ P).
Proof.
intro proof_of_P.
apply (conj).
 exact (proof_of_P).
 exact (proof_of_P).
Qed.
More about conjunctions
We know that A /\ B > A in particular, and this fact is represented in Coq by the following two names. (Can you work out what the 1 and 2 mean? Check them and try!)Check (proj1).
Check (proj2).
Using these we're going to try to prove the theorem:
We know that our opening line will have to look something like
So we fill these in and tell Coq that we'd like to prove this theorem.
Let A and B be propositions. If (A and B) then (B and A).But this time we're not going to do it by hand first.
Our second theorem
To begin we must translate this natural language statement into symbols and quantifiers, and tell Coq what we're trying to prove.Theorem our_second_theorem (context?) : (statement?).But what goes where?
 Our theorem begins with ``Let A and B be propositions'', so we
recognise that our context is A B : Prop. Note the space separating
the names of things, not a comma.
 Formally said, the statement of our theorem is A /\ B > B /\ A.
Theorem our_second_theorem (A B : Prop) : (A /\ B > B /\ A).
Proof.
According to the ``Goals'' window we are aiming for A /\ B > B /\
A and so, as before, we proceed by claminig that to prove an
implication it is enough to assume that the antecedent is true and
derive the consequent. In Coq this means
intro proof_of_conjunction.
Now we need to prove a conjunction, B /\ A in specific, and so
the only way we know how to do that is by applying conj. In doing so
we will give ourselves two new goals: one for B and one for A.
apply (conj).
Coq reminds us that we have two subgoals at this point, and so we
focus the first.

We appear to be a little stuck now. It's not immediately obvious
how we can proceed given our current state:
Let's Check something again
1 subgoal A, B : Prop proof_of_conjunction : A /\ B ============================ BBut we know that A /\ B > B holds, that is, given a proof of A /\ B we may derive a proof of B. How do we tell Coq about this proof of B?
Check (proj2).
Remember that we read this as a machine which takes proofs of the
conjunction and gives us proofs of the second conjunct. So, what
happens if we feed this machine proof_of_conjunction? To do this we
simply write the name of the thing we want to feed to proj2 after
proj2 itself:
Check (proj2 proof_of_conjunction).
proj2 proof_of_conjunction : BIs the response that Coq gives us. That is, proj2 proof_of_conjunction is a proof of B.
To apply a function to arguments we write (function_name argument_one argument_two)
pose (proof_of_B := (proj2 proof_of_conjunction)).
Coq has a keyword pose which adds a definition to our context.
In this case proof_of_B is added to our context, giving us
To add a name to our context with a chosen definition we write pose (name := definition).
We recognise this position. We have exactly what we need to achieve
our goal.
1 subgoal A, B : Prop proof_of_conjunction : A /\ B proof_of_B := proj2 proof_of_conjunction : B ============================ B
To add a name to our context with a chosen definition we write pose (name := definition).
exact (proof_of_B).
Coq helpfully reminds us that we're not done yet, and so we focus
on the next goal.

This subgoal is just like the previous one, but with A and
B swapped. We know how to deal with it:
pose (proof_of_A := (proj1 proof_of_conjunction)).
exact (proof_of_A).
... and that's it!
Qed.
The Check statements we used in the proof didn't actually change
anything, they just helped us produce the proof in the first place. So
if we wanted to compact the proof and remove all commentry we can
safely write
Theorem our_second_theorem (A B : Prop) : (A /\ B > B /\ A).
Proof.
intro proof_of_conjunction.
apply (conj).
 pose (proof_of_B := (proj2 proof_of_conjunction)).
exact (proof_of_B).
 pose (proof_of_A := (proj1 proof_of_conjunction)).
exact (proof_of_A).
Qed.
Some reading fluency exercises
Theorem exc1 (P : Prop) : (P > P).
Proof.
intro Hp.
exact (Hp).
Qed.
Theorem exc2 (P Q : Prop) : ((P > Q) > P > Q).
Proof.
intro imp.
intro Hp.
pose (proof_of_Q := (imp Hp)).
exact (proof_of_Q).
Qed.
Theorem exc3 (P Q : Prop) : ((P > Q) > P > Q).
Proof.
intro imp.
intro Hp.
exact (imp Hp).
Qed.
What's the difference between exc2 and exc3?
Theorem exc4 (P Q : Prop) : ((P > Q) /\ P > Q).
Proof.
intro conjunction.
pose (imp := (proj1 conjunction)).
pose (Hp := (proj2 conjunction)).
exact (imp Hp).
Qed.
These are more difficult, but that much more rewarding.
Theorem exc5 (P Q R : Prop) : ((P > Q > R) > (P /\ Q > R)).
Proof.
intro curry.
intro conjunction.
pose (proof_of_P := (proj1 conjunction)).
pose (proof_of_Q := (proj2 conjunction)).
pose (proof_of_R := (curry proof_of_P proof_of_Q)).
exact (proof_of_R).
Qed.
Theorem exc6 (P Q R : Prop) : ((P /\ Q > R) > (P > Q > R)).
Proof.
intro imp.
intro Hp.
intro Hq.
pose (proof_of_conjunction := (conj Hp Hq)).
pose (proof_of_R := (imp proof_of_conjunction)).
exact (proof_of_R).
Qed.
For this last one we're going to prove a biconditional. In Coq,
much as in class, this is called ``iff''. It's even defined the same
way,
``A iff B'' is (A > B) /\ (B > A).
Coq has some builtin notation for this, A <> B.
Theorem exc7 (A B C : Prop) : ((A > B > C) <> (A /\ B > C)).
Proof.
apply (conj).
 exact (exc5 A B C).
 exact (exc6 A B C).
Qed.
Disjunctions, P \/ Q
Check (or).
Much like in the case of and, Coq has builtin notation for the
disjunction of two propositions.
Section ornotation.
Variable (P Q : Prop).
Check (P \/ Q).
End ornotation.
Our first stopping point with disjunctions is the consideration of
how they are proven. We know that to prove P /\ Q we must give both a
proof of P as well as a proof of Q. However, for P \/ Q we know
that it suffices to give a proof of either P or Q. That is, we are
familiar with the implications P > P \/ Q and Q > P \/ Q. Coq has
these too,
Check (or_introl).
Check (or_intror).
Try reading those aloud. With this, we're equipped to prove our
first theorem about disjunctions.
Let P and Q be propositions. If (P and Q) then (P or Q).We begin by stating our theorem in Coq and using intro as we wish to prove an implication.
Theorem disj_to_conj1 (P Q : Prop) : (P /\ Q > P \/ Q).
Proof.
intro proof_of_conj.
Now we know that to prove P \/ Q it suffices to give a proof of,
say, P. That implication was called or_introl and we ask Coq to
apply this reasoning.
apply (or_introl).
We are left with extracting a proof of P from a proof of P /\
Q, but thinking back to last time we remember that this is done with
proj1.
exact (proj1 proof_of_conj).
Qed.
Note how we didn't bother giving a name to the intermediate proof
of P and instead used it directly in our exact statement.
Of course, we made a choice in this proof. We could equally well have
proven this statement by instead supplying a proof of Q. How would
that go?
Theorem disj_to_conj2 (P Q : Prop) : (P /\ Q > P \/ Q).
Proof.
intro proof_of_conj.
apply (or_intror).
exact (proj2 proof_of_conj).
Qed.
Questions: Are these two proofs the same? What should
that mean?
We could keep playing around with proving disjunctions, but this would
come at the cost of not exposing the most important feature of
disjunctions.
To introduce the idea of arguing by cases, consider the following
theorem and its paper proof.
4. There are no more cases now on our hypothesis P \/ Q, and we have
completed our goal in each case. Qed.
Question: Could we have done this proof if, before step (2),
we had instead chosen that to prove P \/ Q we were going to give a
proof of P?
Let's try to imitate this proof in Coq. We begin with the usual
incantations, specifically using intro as we wish to prove an implication.
Arguing by cases
Let P and Q be propositions. If (P or Q) then (Q or P).How would we prove this? We might proceed as follows.
Goal: P \/ Q > Q \/ P Context:1. To prove an implication it suffices to assume the antecedent and derive the consequent.
Goal: Q \/ P Context: P \/ Q2. When our hypothesis is of the form P \/ Q, we may argue by cases. In the first case let us suppose that P is true.
Goal: Q \/ P Context: P3a. In order to give a proof of Q \/ P it suffices to give a proof of P, but we have exactly this by hypothesis and so we conclude this case. For the next case let us suppose that Q is true.
Goal: Q \/ P Context: Q3b. In order to give a proof of Q \/ P it suffices to give a proof of Q, but we have exactly this by hypothesis and so we conclude this case.
Theorem disj_commute (P Q : Prop) : (P \/ Q > Q \/ P).
Proof.
intro hyp.
Now we need to perform the analogue of arguing by cases. It was
easy to miss in the paper proof, but arguing by cases is unlike
anything we have encountered so far. It does not give us more
subgoals, instead it splits our entire argument in two.
In order to argue by cases on P \/ Q we must provide two, complete
arguments for the same goal.
In order to perform this in Coq we make use of the induction
keyword. If you have seen induction before you may be wondering why
this is called induction, after all there don't seem to be any natural
numbers about. It turns out that, is some deep and satisfying way,
that other induction and this induction are really two manifestations
of the same concept. Unfortunately that might not help you, so for now
we'll just have to live with it. Here's the summary:
To argue by cases on an hypothesis hyp : A \/ B write induction (hyp)., and then we focus each subargument with a  (minus).
To argue by cases on an hypothesis hyp : A \/ B write induction (hyp)., and then we focus each subargument with a  (minus).
induction (hyp).
You may notice that our context has changed. Coq has understood
that we wanted to argue by cases on hyp : P \/ Q and so has chosen
the case of P for us at first, and added the hypothesis H : P
reflecting the assumption that P is true. This is step (2) above.
Now we are ready to focus this case and proceed with the proof. In
(3a) we argued that to prove Q \/ P it was enough to prove P. To
apply this reasoning in Coq we write:
 apply (or_intror).
Note the or_intror, we really want to prove P here and not
Q. Well, as in (3a) above we have exactly what we need.
exact (H).
With that achieved Coq helpfully reminds us that we have another
subgoal, and so we focus to that case.

Notice how Coq has automatically given us H : Q, it's helping us
argue by cases! How does the proof of this subgoal go?
apply (or_introl).
exact (H).
Qed.
After the exact (H). Coq told us that we had no more subgoals,
that is, we were done arguing by cases! All in all, our proof was
Theorem disj_commute (P Q : Prop) : (P \/ Q > Q \/ P).
Proof.
intro hyp.
induction (hyp).
 apply (or_intror).
exact (H).
 apply (or_introl).
exact (H).
Qed.
Theorem disj_commute (P Q : Prop) : (P \/ Q > Q \/ P).
Proof.
intro hyp.
induction (hyp).
 apply (or_intror).
exact (H).
 apply (or_introl).
exact (H).
Qed.
Now let's be more ambitious and try to understand the following
exercises.
Theorem exc8 (P Q R : Prop) : (P /\ (Q \/ R) > (P /\ Q) \/ (P /\ R)).
Proof.
intro hyp.
pose (proof_of_P := (proj1 hyp)).
pose (proof_of_Q_or_R := (proj2 hyp)).
induction (proof_of_Q_or_R).
 apply (or_introl).
exact (conj proof_of_P H).
 apply (or_intror).
exact (conj proof_of_P H).
Qed.
Theorem exc9 (P Q R : Prop) : (P /\ (Q \/ R) > (P /\ Q) \/ (P /\ R)).
Proof.
intro hyp.
pose (proof_of_P := (proj1 hyp)).
pose (proof_of_Q_or_R := (proj2 hyp)).
induction (proof_of_Q_or_R).
 apply (or_introl).
apply (conj).
+ exact (proof_of_P).
+ exact (H).
 apply (or_intror).
apply (conj).
+ exact (proof_of_P).
+ exact (H).
Qed.
The implication the other way is potentially scary.
Theorem exc10 (P Q R : Prop) : ((P /\ Q) \/ (P /\ R) > P /\ (Q \/ R)).
Proof.
intro hyp.
induction (hyp).
 pose (proof_of_P := (proj1 H)).
pose (proof_of_Q := (proj2 H)).
apply (conj).
+ exact (proof_of_P).
+ apply (or_introl).
exact (proof_of_Q).
 pose (proof_of_P := (proj1 H)).
pose (proof_of_R := (proj2 H)).
apply (conj).
+ exact (proof_of_P).
+ apply (or_intror).
exact (proof_of_R).
Qed.
If we drop some names of things we can make it look smaller.
Theorem exc11 (P Q R : Prop) : ((P /\ Q) \/ (P /\ R) > P /\ (Q \/ R)).
Proof.
intro hyp.
induction (hyp).
 apply (conj).
+ exact (proj1 H).
+ apply (or_introl).
exact (proj2 H).
 apply (conj).
+ exact (proj1 H).
+ apply (or_intror).
exact (proj2 H).
Qed.
The smallest proof by far ;)
Theorem exc12 (P Q R : Prop) : ((P /\ Q) \/ (P /\ R) > P /\ (Q \/ R)).
Proof.
tauto.
Qed.
This page has been generated by coqdoc