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 web-browser, #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 arrow-type buttons in the upper right-hand 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 right-hand 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 so-called ``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 extra-careful, 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 line-by-line 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 take-away 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 built-in 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 built-in 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 sub-argument 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 Attribution-ShareAlike 4.0 International License. See http://creativecommons.org/licenses/by-sa/4.0/ for details. *)