Require Import Coq.Init.Prelude.
(** * Introduction *)
(** ** Why do we want this?
Let's briefly discuss what a computer proof assistant can bring to the
following situations.
 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?
Coq is an interactive theorem prover, meaning that it allows the user
to enter mathematical statements and their proofs and will check,
assist in the writing of, and in some cases automatically find, these
proofs.
Coq is available from its website #https://coq.inria.fr/# under the
terms of the #GNU
Lesser General Public License Version 2.1# free software license.
Most flavours of Linux have Coq in their software repositories (and if
not, it may be built from source), and there are installers for
Windows. The situation for Mac is somewhat nuanced.
In any event, it won't prove necessary to have Coq or its IDE running
locally on your machine because in this class we will make use of an
online interface so all you'll need is a webbrowser, #https://x80.org/collacoq#. *)
(** *** Using this document
As you may have noticed, some portions of this document are not in
blue boxes at all. Those are the bits corresponding to Coq code. In
order to following along, you can copy and paste those into your Coq
interpreter and execute them one line at a time, observing the
changes.
As it happens, this document was generated directly from Coq code, and
if you prefer you can copy and paste the entire raw version of this
document into your Coq interpreter. In Coq, everything that looks like
this
<<
(** 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/#
Familiarise yourself with the three arrowtype buttons in the upper
righthand side of the screen. If you hover over these buttons you'll
see that they have descriptions: ``Up'', ``Down'', and ``To cursor''.
Those buttons  explained in reverse order here  tell Coq to focus
on everything up to the cursor, one line further, and one line prior.
These have keyboard shortcuts, where ``Meta'' is ``Alt'' on most
keyboards. The easiest way to understand that is to enter the
following three lines and see what the buttons do. *)
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
As you have seen above, a basic way we can interact with the Coq proof
assistant is through the use of the [Check (thing).] command. This
will instruct Coq to look at [thing] and tell you what it knows about
it. In the coming sections we'll learn to interpret this output.
*)
(** *** Types
In Coq we will often deal with things which look like
<<
stuff : Thing
>>
The way we read this aloud is _[stuff] is of type [Thing]_. Unfortunately
that's not very insightful so instead we mostly say
_[stuff] is a [Thing]_.
Here's an example, if we run this line through Coq ...
*)
Check (5).
(** Then in the ``Response'' window we'll see that Coq tells us
<<
5
: nat
>>
Try pronouncing this as above, _[5] is a [nat]_.
Here's another example:
*)
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, ...
Let's introduce a proposition temporarily. *)
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:
 _[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.
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. *)
End section1.
(** *** How to read arrows `>'
There's another aspect of Coq with which we'll need to become familiar
if we're to use it for proving things.
On the natural numbers we can define the socalled ``successor''
function, S(n):=n+1, taking one natural number to the next. This
function is built into Coq under the same name, [S].
Let's see what Coq thinks about the successor function from [nat] to
[nat].*)
Check S.
(** Coq tells us
<<
S
: nat > nat
>>
Let's try to apply our pronounciation to this, shall we?
_[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? *)
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! *)
(** *** How to read more arrows
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:
*)
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.*)
(** * Propositional calculus *)
(** Our starting point for computer assisted proofs is propositional
calculus, just as it was when we were learning mathematics `by
hand' originally. *)
(** ** Conjunctions, P /\ Q *)
(** 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: *)
Check (and).
(** Coq says,
<<
and
: Prop > Prop > Prop
>> *)
(** 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, *)
Check (conj).
(** Coq says,
<<
conj
: forall A B : Prop, A > B > A /\ B
>>*)
(** 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. *)
(* *)
(** ** 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: P
>>
2. 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: P
>>
3. Now we have two goals, so lets deal with them individually.
<<
Goal: P
Context: P
>>
4a. By hypothesis we have a proof of [P], exactly what we need for
this goal
<<
Goal: P
Context: P
>>
4b. 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.
 On the first line, [Theorem our_first_theorem (P : Prop) : (P > P /\ P).]
we say many things at once.
We:
 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]
 On the second line we tell Coq that we're about to prove the result
by using the [Proof.] keyword.
The takeaway here is:

To introduce a theorem and begin to prove it we write
[[
Theorem name_of_theorem (context) : (statement).
Proof.
]]

*)
(* *)
(** *** Interactive theorem proving in Coq
You may have noticed that the ``Goals'' window of Coq now says
<<
1 subgoal
P : Prop
============================
P > P /\ P
>>
What does this mean?
This is _exactly_ the Goal/Context setup we
had before. Our current goal is listed below the line, and everything
we know is above it. Moreover, Coq reminds us that we presently have
only one goal. How do we proceed?
*)
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
<<
1 subgoal
P : Prop
proof_of_P : P
============================
P > P /\ P
>>
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, _apply_ing this sort of
reasoning is achieved as follows.
*)
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
<<
2 subgoals
P : Prop
proof_of_P : P
============================
P
subgoal 2 is0
P
>>
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:
*)

(** 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
<<
1 subgoals
P : Prop
proof_of_P : P
============================
P
>>

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]? *)
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 subproof is complete, but there are some unfocused goals.
Focus next goal with bullet .
>>
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 
*)

(** 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] *)
Check (our_first_theorem).
(** In the ``Response'' window we see
<<
our_first_theorem
: forall P : Prop, P > P /\ P
>>
which 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
>>
All in all, without the giant comment blocks in the way, the Coq code
we gave for this theorem and its proof is this:*)
(* *)
(**

[[
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:
<<
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.
We know that our opening line will have to look something like
<<
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].
So we fill these in and tell Coq that we'd like to prove this theorem.
*)
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:
<<
1 subgoal
A, B : Prop
proof_of_conjunction : A /\ B
============================
B
>>
But 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]?
Let's [Check] something again
*)
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
: B
>>
Is 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)]

This is what we need, but how do we add it to our context? *)
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
<<
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).]

We recognise this position. We have _exact_ly what we need to achieve
our goal.
*)
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
By stepping through the following theorems and proofs, can you
understand what they're saying and how they work? *)
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
Now that we have some understanding of conjunctions, we're going to
look at disjunctions. We understand that, if [P] and [Q] are
propositions, then so too is [P \/ Q]. In Coq the way to construct the
proposition corresponding to the disjunction of two other propositions
is by using [or]. Let's ask Coq what it is. *)
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. *)
(** *** Arguing by cases
To introduce the idea of arguing by cases, consider the following
theorem and its paper proof.
<<
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 \/ Q
>>
2. 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: P
>>
3a. 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: Q
>>
3b. 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.
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.*)
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).
 *)
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.
]]
*)
(* *)
(** 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 work is made available under the terms of the Creative
Commons AttributionShareAlike 4.0 International License. See
http://creativecommons.org/licenses/bysa/4.0/ for details. *)