Cases

Require Export DMFP.Propositions.
Today is a long day: we're going to teach you several tactics and proof methods. There are a few more exercises than usual, too. So: please start early and ask for help if you need it!

Proofs Within Proofs

In Coq, as in informal mathematics, large proofs are often broken into a sequence of theorems, with later proofs referring to earlier theorems. But sometimes a proof will require some miscellaneous fact that is too trivial and of too little general interest to bother giving it its own top-level name. In such cases, it is convenient to be able to simply state and prove the needed "sub-theorem" right at the point where it is used. The assert tactic allows us to do this. For example, our earlier proof of the mult_0_plus theorem referred to a previous theorem named plus_O_n. We could instead use assert to state and prove plus_O_n in-line:
Theorem mult_0_plus' : n m : nat,
  (0 + n) × m = n × m.
Proof.
  intros n m.
  assert (H: 0 + n = n). { reflexivity. }
  rewriteH.
  reflexivity. Qed.
The assert tactic introduces two sub-goals. The first is the assertion itself; by prefixing it with H: we name the assertion H. (We can also name the assertion with as just as we did above with destruct and induction, i.e., assert (0 + n = n) as H.) Note that we surround the proof of this assertion with curly braces { ... }, both for readability and so that, when using Coq interactively, we can see more easily when we have finished this sub-proof. The second goal is the same as the one at the point where we invoke assert except that, in the context, we now have the assumption H that 0 + n = n. That is, assert generates one subgoal where we must prove the asserted fact and a second subgoal where we can use the asserted fact to make progress on whatever we were trying to prove in the first place.

Unfolding Definitions

It sometimes happens that we need to manually unfold a Definition so that we can manipulate its right-hand side. We've already met the unfold tactic when talking about not, but it's generally useful. For example, if we define...
Definition square n := n × n.
... and try to prove a simple fact about square...
Lemma square_mult : n m,
    ( n m o, n × (m × o) = (n × m) × o) (* we'll prove this later *)
    ( n m, n × m = m × n) (* same *)
    square (n × m) = square n × square m.
Proof.
  intros n m mult_assoc mult_comm.
  simpl mult.
  simpl square.
... we get stuck: simpl doesn't simplify anything at this point no matter what we try, and since we haven't proved any other facts about square, there is nothing we can apply or rewrite with.
To make progress, we can manually unfold the definition of square:
  unfold square.
Now we have plenty to work with: both sides of the equality are expressions involving multiplication, and we have lots of facts about multiplication at our disposal. In particular, we know that it is commutative and associative, and from these facts it is not hard to finish the proof.
  rewrite mult_assoc.
  assert (H : n × m × n = n × n × m).
  { rewrite mult_comm. apply mult_assoc. }
  rewrite H. rewrite mult_assoc. reflexivity.
Qed.

Proof by Case Analysis

Of course, not everything can be proved by simple calculation and rewriting: In general, unknown, hypothetical values (arbitrary numbers, booleans, lists, etc.) can block simplification. For example, if we try to prove the following fact using the simpl tactic as above, we get stuck. (We then use the Abort command to give up on it for the moment.)
Theorem plus_1_neq_0_firsttry : n : nat,
  eqb (n + 1) 0 = false.
Proof.
  intros n.
  simpl plus. (* does nothing! *)
  simpl eqb. (* does nothing! *)
Abort.
The reason for this is that the definitions of both eqb and + begin by performing a match on their first argument. But here, the first argument to + is the unknown number n and the argument to eqb is the compound expression n + 1; neither can be simplified.
To make progress, we need to consider the possible forms of n separately. If n is O, then we can calculate the final result of eqb (n + 1) 0 and check that it is, indeed, false. And if n = S n' for some n', then, although we don't know exactly what number n + 1 yields, we can calculate that, at least, it will begin with one S, and this is enough to calculate that, again, eqb (n + 1) 0 will yield false.
The tactic that tells Coq to consider, separately, the cases where n = O and where n = S n' is called destruct.
Theorem plus_1_neq_0 : n : nat,
  eqb (n + 1) 0 = false.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - reflexivity.
  - reflexivity. Qed.
The destruct generates two subgoals, which we must then prove, separately, in order to get Coq to accept the theorem. The annotation "as [| n']" is called an intro pattern. It tells Coq what variable names to introduce in each subgoal. In general, what goes between the square brackets is a list of lists of names, separated by |. In this case, the first component is empty, since the O constructor is nullary (it doesn't have any arguments). The second component gives a single name, n', since S is a unary constructor.
It's worth contrasting intro patterns with match patterns, i.e., what we write in match expressions. A match pattern in a branch of a match expression names each constructor and its arguments, with a | before each one, e.g.:

Definition minustwo (n : nat) : nat :=
  match n with
    | OO
    | S OO
    | S (S n') ⇒ n'
  end.
In contrast, an intro pattern names only the arguments of each constructor, leaving out the constructor name itself, as in:

   destruct n as [| n'].
You can nest patterns, e.g., to do case analysis on n and n' simultaneously, write:

   destruct n as [| [| n']].
There will be three subgoals: n = O, n = S O, and n = S (S n').
When doing case analysis with destruct, in each subgoal, Coq remembers the assumption about n that is relevant for this subgoal -- either n = 0 or n = S n' for some n'. The eqn:E annotation tells destruct to give the name E to this equation. Leaving off the eqn:E annotation causes Coq to elide these assumptions in the subgoals. This slightly streamlines proofs where the assumptions are not explicitly used, but it is better practice to keep them for the sake of documentation, as they can help keep you oriented when working with the subgoals.
The - signs on the second and third lines are called bullets, and they mark the parts of the proof that correspond to each generated subgoal. The proof script that comes after a bullet is the entire proof for a subgoal. In this example, each of the subgoals is easily proved by a single use of reflexivity, which itself performs some simplification -- e.g., the first one simplifies eqb (S n' + 1) 0 to false by first rewriting (S n' + 1) to S (n' + 1), then unfolding eqb, and then simplifying the match.
Marking cases with bullets is entirely optional: if bullets are not present, Coq simply asks you to prove each subgoal in sequence, one at a time. But it is a good idea to use bullets. For one thing, they make the structure of a proof apparent, making it more readable. Also, bullets instruct Coq to ensure that a subgoal is complete before trying to verify the next one, preventing proofs for different subgoals from getting mixed up. These issues become especially important in large developments, where fragile proofs lead to long debugging sessions.
There are no hard and fast rules for how proofs should be formatted in Coq -- in particular, where lines should be broken and how sections of the proof should be indented to indicate their nested structure. However, if the places where multiple subgoals are generated are marked with explicit bullets at the beginning of lines, then the proof will be readable almost no matter what choices are made about other aspects of layout.
This is also a good place to mention one other piece of somewhat obvious advice about line lengths. Beginning Coq users sometimes tend to the extremes, either writing each tactic on its own line or writing entire proofs on one line. Good style lies somewhere in the middle. One reasonable convention is to limit yourself to 80-character lines.
The destruct tactic can be used with any inductively defined datatype. For example, we use it next to prove that boolean negation is involutive -- i.e., that negation is its own inverse.
  • Theorem: For any natural number n,

          eqb (n + 1) 0 = false.
    Proof: Let n be given (intros n). We go by cases on n (destruct n as [| n']):
    • First, suppose n=0. We must show that eqb (0 + 1) 0 = false, which we have by definition (reflexivity).
    • Next, suppose n=S n'. We must show that eqb ((S n') + 1) 0 = false, which holds by the definition of eqb (reflexivity).
    Qed.
Notice how the destruct lines up with what we say in the paper proof. We open with announcing our intention---to do case analysis on n. While Coq wants to know the names of any possible subparts of n up front, in the as pattern of the destruct; in the paper proof, we find out the names when we write out which case we're in explicitly: each subcase is written as its own bullet, where we announce the case we're in.
We've encounted our first significant divergence (of many!) between how Coq and paper proofs work. Coq keeps track of the context for you, so Coq proof scripts can leave quite a bit implicit. Paper proofs are meant to communicate an idea from one human to another, so it's important to check in and make sure everyone is on the same page---by, for example, saying what each case is up front.
Finally, note that we're not "transliterating" the Coq: the two uses of reflexivity in each branch are written slightly differently in the paper proof.
Theorem negb_involutive : b : bool,
  negb (negb b) = b.
Proof.
  intros b. destruct b eqn:E.
  - reflexivity.
  - reflexivity. Qed.
Note that the destruct here has no as clause because none of the subcases of the destruct need to bind any variables, so there is no need to specify any names. (We could also have written as [ | ], or as [].) In fact, we can omit the as clause from any destruct and Coq will fill in variable names automatically. This is generally considered bad style, since Coq often makes confusing choices of names when left to its own devices. In a paper proof, it'd be good to announce that b=false in the first case and b=true in the second case.
It is sometimes useful to invoke destruct inside a subgoal, generating yet more proof obligations. In this case, we use different kinds of bullets to mark goals on different "levels." For example:

Exercise: 2 stars, standard (negb_involutive_informal)

(* As we did last week, give an informal proof in comments showing negb_involutive.
   Follow the proof of plus_1_neq_0 for inspiration.
 *)

(* Do not modify the following line: *)
Definition manual_grade_for_negb_involutive_informal : option (nat×string) := None.
Print complement. (* Just to remind you. *)

Lemma complement_involutive : (b : base),
    complement (complement b) = b.
Proof.
  intros b. destruct b eqn:E.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

Theorem andb_commutative : b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.
Each pair of calls to reflexivity corresponds to the subgoals that were generated after the execution of the destruct c line right above it.
Besides - and +, we can use × (asterisk) as a third kind of bullet. We can also enclose sub-proofs in curly braces, which is useful in case we ever encounter a proof that generates more than three levels of subgoals:
Theorem andb_commutative' : b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  { destruct c eqn:Ec.
    { reflexivity. }
    { reflexivity. } }
  { destruct c eqn:Ec.
    { reflexivity. }
    { reflexivity. } }
Qed.
Since curly braces mark both the beginning and the end of a proof, they can be used for multiple subgoal levels, as this example shows. Furthermore, curly braces allow us to reuse the same bullet shapes at multiple levels in a proof:
Theorem andb3_exchange :
   b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
  intros b c d. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
Qed.
As you may have noticed, many proofs perform case analysis on a variable right after introducing it:
       intros x y. destruct y as [|y]. This pattern is so common that Coq provides a shorthand for it: we can perform case analysis on a variable when introducing it by using an intro pattern instead of a variable name. For instance, here is a shorter proof of the plus_1_neq_0 theorem above.
Theorem plus_1_neq_0' : n : nat,
  eqb (n + 1) 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity. Qed.

Exercise: 1 star, standard (minus_n_O)

Lemma minus_n_O : n : nat, n = n - 0.
Proof.
  (* FILL IN HERE *) Admitted.
If there are no arguments to name, we can just write [].
Theorem andb_commutative'' :
   b c, andb b c = andb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

Exercise: 2 stars, standard (andb_true_elim2)

Prove the following claim, marking cases (and subcases) with bullets when you use destruct.
Theorem andb_true_elim2 : b c : bool,
  andb b c = true c = true.
Proof.
  (* FILL IN HERE *) Admitted.
At this point, a deeper discussion of unfolding and simplification is in order.
You may already have observed that tactics like simpl, reflexivity, and apply will often unfold the definitions of functions automatically when this allows them to make progress. For example, if we define foo m to be the constant 5...
Definition foo (x: nat) := 5.
then the simpl plus in the following proof (or the reflexivity, if we omit the simpl plus) will unfold foo m to (fun x 5) m and then further simplify this expression to just 5.
Fact silly_fact_1 : m, foo m + 1 = foo (m + 1) + 1.
Proof.
  intros m.
  simpl plus.
  reflexivity.
Qed.
However, this automatic unfolding is rather conservative. For example, if we define a slightly more complicated function involving a pattern match...
Definition bar x :=
  match x with
  | O ⇒ 5
  | S _ ⇒ 5
  end.
...then the analogous proof will get stuck:
Fact silly_fact_2_FAILED : m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  simpl bar. (* Does nothing! *)
Abort.
The reason that simpl bar doesn't make progress here is that it notices that, after tentatively unfolding bar m, it is left with a match whose scrutinee, m, is a variable, so the match cannot be simplified further. (It is not smart enough to notice that the two branches of the match are identical.) So it gives up on unfolding bar m and leaves it alone. Similarly, tentatively unfolding bar (m+1) leaves a match whose scrutinee is a function application (that, itself, cannot be simplified, even after unfolding the definition of +), so simpl bar leaves it alone.
At this point, there are two ways to make progress. One is to use destruct m to break the proof into two cases, each focusing on a more concrete choice of m (O vs S _). In each case, the match inside of bar can now make progress, and the proof is easy to complete.
Fact silly_fact_2 : m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  destruct m.
  - simpl bar. reflexivity.
  - simpl bar. reflexivity.
Qed.
This approach works, but it depends on our recognizing that the match hidden inside bar is what was preventing us from making progress.
A more straightforward way to make progress is to explicitly tell Coq to unfold bar.
Fact silly_fact_2' : m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  unfold bar.
Now it is apparent that we are stuck on the match expressions on both sides of the =, and we can use destruct to finish the proof without thinking too hard.
  destruct m.
  - reflexivity.
  - reflexivity.
Qed.
Finally, it's often useful to do the unfold/fold 1-2 punch: unfolding a recursive definition and then immediately folding it back up will reveal the work one step of recursion is doing without doing any simplification.
Fixpoint funny_rec (n : nat) : nat :=
  match n with
  | O ⇒ 0
  | S n'if evenb n then 0 else funny_rec n'
  end.

Exercise: 2 stars, standard (funny_rec_evenb_0)

In the n = S n' case, notice that simpl gives you an annoying answer, but unfold/fold works a treat.
Lemma funny_rec_evenb_0 : n,
    evenb n = true
    funny_rec n = 0.
Proof.
  (* FILL IN HERE *) Admitted.
We can formalize this trick in a new tactic (yet another programming language inside of Coq!). Now, we can say step funny_rec to go through one level of its recursion.
step here does the work of unfold followed by fold. The notations defined below mean we can also use step on hypotheses.
Ltac step_goal A := unfold A; fold A.
Ltac step_in A H := unfold A in H; fold A in H.
Tactic Notation "step" constr(A) := step_goal A.
Tactic Notation "step" constr(A) "in" hyp(H) := step_in A H.

Logical Connectives

Now that we've seen destruct, we can do more with logical connectives. So far we've only proved conjunctions and disjunctions. How do you use them? And what about negation?

Conjunction

We've seen that proving a conjunction means using split to prove each part. To go in the other direction -- i.e., to use a conjunctive hypothesis to help prove something else -- we employ the destruct tactic.
If the proof context contains a hypothesis H of the form A B, writing destruct H as [HA HB] will remove H from the context and add two new hypotheses: HA, stating that A is true, and HB, stating that B is true.
The following lemmas not only show the general idea, but they're generally useful: it's a common situation to know A B but only really need just A (or just B).
Lemma proj1 : P Q : Prop,
  P Q P.
Proof.
  intros P Q [HP HQ]. (* "Let P and Q be given, and assume P /\ Q." *)
  apply HP. (* "We have to show P; but we've just assumed P, so we're done." *)
Qed.

Exercise: 1 star, standard, optional (proj2)

Lemma proj2 : P Q : Prop,
  P Q Q.
Proof.
  (* FILL IN HERE *) Admitted.
Finally, we sometimes need to rearrange the order of conjunctions and/or the grouping of multi-way conjunctions. The following commutativity and associativity theorems are handy in such cases.
Theorem and_commut : P Q : Prop,
  P Q Q P.
Proof.
  intros P Q [HP HQ].
  split.
    - (* left *) apply HQ.
    - (* right *) apply HP. Qed.

Exercise: 2 stars, standard (and_assoc)

(In the following proof of associativity, notice how the nested intro pattern breaks the hypothesis H : P (Q R) down into HP : P, HQ : Q, and HR : R. Finish the proof from there.)
Theorem and_assoc : P Q R : Prop,
  P (Q R) (P Q) R.
Proof.
  intros P Q R [HP [HQ HR]].
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard (and_assoc_informal)

(* Add comments to your proof of and_assoc above to lay it out informally.  Look at the comments in proj1 for hints and think about your earlier proofs with conjunction; or, read ahead to and_example2'.
 *)


(* Do not modify the following line: *)
Definition manual_grade_for_and_assoc_informal : option (nat×string) := None.
Lemma and_example2 :
   n m : nat, n = 0 m = 0 n + m = 0.
Proof.
  (* WORKED IN CLASS *)
  intros n m H.
  destruct H as [Hn Hm].
  rewrite Hn. rewrite Hm.
  reflexivity.
Qed.
As usual, we can also destruct H right when we introduce it, instead of introducing and then destructing it:
Lemma and_example2' :
   n m : nat, n = 0 m = 0 n + m = 0.
Proof.
  (* "Let n and m be given, and assume n = 0 and m = 0.  We
     need to show n + m = 0 " *)

  intros n m [Hn Hm].
  (* Since n is 0 and m is 0, showing n + m = 0 means showing 0 + 0 = 0, .... *)
  rewrite Hn. rewrite Hm.
  (* ... which is immediate by the definition of plus. *)
  reflexivity.
Qed.
You may wonder why we bothered packing the two hypotheses n = 0 and m = 0 into a single conjunction, since we could have also stated the theorem with two separate premises:
Lemma and_example2'' :
   n m : nat, n = 0 m = 0 n + m = 0.
Proof.
  intros n m Hn Hm.
  rewrite Hn. rewrite Hm.
  reflexivity.
Qed.
For this theorem, both formulations are fine. But it's important to understand how to work with conjunctive hypotheses because conjunctions often arise from intermediate steps in proofs, especially in bigger developments. We'll see an example on day 12.

Disjunction

Another important connective is the disjunction, or logical or of two propositions: A B is true when either A or B is. (Alternatively, we can write or A B, where or : Prop Prop Prop.)
Recall that we used left and right to choose which branch of disjunction to prove. Just as for conjunction, we use destruct to ask: if we know P Q, which one holds?
Theorem or_commut : P Q : Prop,
  P Q Q P.
Proof.
  (* Let P, Q be given, and assume P \/ Q. We go by cases... *)
  intros P Q HPQ. destruct HPQ as [HP | HQ].
  - (* If P is true, we have to show ... *) right. apply HP.
  - (* If Q is true, we have to show ... *) left. apply HQ.
Qed.

Theorem or_commut' : P Q : Prop,
  P Q Q P.
Proof.
  intros P Q [HP | HQ].
  - (* left *) right. apply HP.
  - (* right *) left. apply HQ. Qed.
... and a slightly more interesting example requiring both left and right:
Lemma zero_or_succ :
   n : nat, n = 0 n = S (pred n).
Proof.
  (* WORKED IN CLASS *)
  intros [|n].
  - left. reflexivity.
  - right. reflexivity.
Qed.

Exercise: 2 stars, standard (zero_or_succ_informal)

(* Add comments here to give an informal proof of zero_or_succ.  You can work by translating the proof we did in class, or you can do it _without_ a Coq proof handy for practice!
 *)


(* Do not modify the following line: *)
Definition manual_grade_for_zero_or_succ_informal : option (nat×string) := None.

Falsehood and Negation

So far, we have mostly been concerned with proving that certain things are true -- addition is commutative, appending lists is associative, etc. Of course, we may also be interested in negative results, showing that certain propositions are not true. In Coq, such negative statements are expressed with the negation operator ¬.
To see how negation works, recall the discussion of the principle of explosion from the Tactics chapter; it asserts that, if we assume a contradiction, then any other proposition can be derived. Following this intuition, we could define ¬ P ("not P") as Q, P Q. Coq actually makes a slightly different choice, defining ¬ P as P False, where False is a specific contradictory proposition defined in the standard library.
Module MyNot.

Definition not (P:Prop) := P False.

Notation "~ x" := (not x) : type_scope.

Check not.
(* ===> Prop -> Prop *)

End MyNot.
PROP ::= EXPR1 = EXPR2 | forall x : TYPE, PROP | PROP1 -> PROP2 | PROP1 /\ PROP2 | PROP1 \/ PROP2 | True | ~ PROP | False
Since False is a contradictory proposition, the principle of explosion also applies to it. If we get False into the proof context, we can use destruct on it to complete any goal:
Theorem ex_falso_quodlibet : (P:Prop),
  False P.
Proof.
  (* WORKED IN CLASS *)
  intros P contra.
  destruct contra. Qed.

Theorem not_False :
  ¬ False.
Proof.
  (* We must show ¬ False.  Towards a contradiction, assume False.  *)
  unfold not. intros H.
  (* But we've already assumed something impossible---that False
    holds!  By the principle of explosion, the original claim of ¬ False must be true. *)

  destruct H. (* Or... apply H! *)
Qed.
The Latin ex falso quodlibet means, literally, "from falsehood follows whatever you like"; this is another common name for the principle of explosion.

Exercise: 2 stars, standard, optional (not_implies_our_not)

(Optionally) show that Coq's definition of negation implies the intuitive one mentioned above:
Fact not_implies_our_not : (P:Prop),
  ¬ P ( (Q:Prop), P Q).
Proof.
  (* FILL IN HERE *) Admitted.
It takes a little practice to get used to working with negation in Coq. Even though you can see perfectly well why a statement involving negation is true, it can be a little tricky at first to get things into the right configuration so that Coq can understand it! Here are proofs of a few familiar facts to get you warmed up.
Especially as you're getting used to our notion of negation, using the unfold tactic is helpful: it will turn a negation into an implication. (You can use unfold and its partner, fold, on any Definition or Fixpoint, not just not!)
Theorem double_neg : P : Prop,
  P ~~P.
Proof.
  (* WORKED IN CLASS *)
  intros P H. unfold not. intros G. apply G. apply H.
Qed.

Exercise: 2 stars, standard (contrapositive)

Theorem contrapositive : (P Q : Prop),
  (P Q) (¬Q ¬P).
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard (contrapositive_informal)

(* Add comments to your proof of contrapositive above to lay it out informally.
 *)


(* Do not modify the following line: *)
Definition manual_grade_for_contrapositive_informal : option (nat×string) := None.

More Exercises

Exercise: 2 stars, standard, optional (boolean_functions)

Use the tactics you have learned so far to prove the following theorem about boolean functions.
Theorem identity_fn_applied_twice :
   (f : bool bool),
  ( (x : bool), f x = x)
   (b : bool), f (f b) = b.
Proof.
  (* FILL IN HERE *) Admitted.
Now state and prove a theorem in Coq; call it negation_fn_applied_twice. It should be similar to the previous one but where the second hypothesis says that the function f has the property that f x = negb x.
Just like for definitions, the autograder will reject your program if you don't define this theorem at the correct type! If you're having trouble, talk to Prof. or a TA.
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_negation_fn_applied_twice : option (nat×string) := None.

The injection and discriminate Tactics

Recall the definition of natural numbers:
     Inductive nat : Type :=
       | O
       | S (n : nat).
This definition asserts that every number has one of two forms: either it is the constructor O or it is built by applying the constructor S to another number. But there is more here than meets the eye: implicit in the definition are two more facts:
  • The constructor S is injective, or one-to-one. That is, if S n = S m, it must be that n = m.
  • The constructors O and S are disjoint. That is, O is not equal to S n for any n.
Similar principles apply to all inductively defined types: all constructors are injective, and the values built from distinct constructors are never equal. For lists, the cons constructor is injective and nil is different from every non-empty list. For booleans, true and false are different. (Since true and false take no arguments, their injectivity is neither here nor there.) And so on.
For example, we can prove the injectivity of S by using the pred function defined in Basics.v.
Theorem S_injective : (n m : nat),
  S n = S m
  n = m.
Proof.
  intros n m H1.
  (* Our use of assert here 'captures' n: we're proving this just
     for the n we have, not for all n (though it's true for all
     n). *)

  assert (H2: n = pred (S n)). { reflexivity. }
  (* For "obvious" properties like this, we might prefer to write
     assert (H2: n = pred (S n)) by reflexivity., avoiding the
     nested proof. *)

  rewrite H2. rewrite H1. reflexivity.
Qed.
This technique can be generalized to any constructor by writing the equivalent of pred -- i.e., writing a function that "undoes" one application of the constructor. As a more convenient alternative, Coq provides a tactic called injection that allows us to exploit the injectivity of any constructor. Here is an alternate proof of the above theorem using injection:
Theorem S_injective' : (n m : nat),
  S n = S m
  n = m.
Proof.
  intros n m H.
By writing injection H as Hmn at this point, we are asking Coq to generate all equations that it can infer from H using the injectivity of constructors (in the present example, the equation n = m). Each such equation is added as a hypothesis (with the name Hmn in this case) into the context.
Informally, we might say "by the injectivity of S, we know n = m".
  injection H as Hnm. apply Hnm.
Qed.
Here's a more interesting example that shows how injection can derive multiple equations at once.
Theorem injection_ex1 : (n m o : nat),
  [n; m] = [o; o]
  [n] = [m].
Proof.
  intros n m o H.
  (* WORKED IN CLASS *)
  injection H as H1 H2.
  rewrite H1. rewrite H2. reflexivity.
Qed.
Alternatively, if you just say injection H with no as clause, then all the equations will be turned into hypotheses at the beginning of the goal.
Theorem injection_ex2 : (n m o : nat),
  [n; m] = [o; o]
  [n] = [m].
Proof.
  (* Let n, m, and o be given; assume [n;m] = [o;o]. *)
  intros n m o H.
  (* By this assumption and the injectivity of cons, n must be o and
  m must also be o. *)

  injection H.
  (* WORKED IN CLASS *)
  intros H1 H2. rewrite H1. rewrite H2.
  (* So [n] = [m] is just [o]=[o], which is immediate. *)
  reflexivity.
Qed.

Exercise: 3 stars, standard, optional (injection_ex3)

Example injection_ex3 : (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j
  j = z :: l
  x = y.
Proof.
  (* FILL IN HERE *) Admitted.
So much for injectivity of constructors. What about disjointness?
The principle of disjointness says that two terms beginning with different constructors (like O and S, or true and false) can never be equal. This means that, any time we find ourselves in a context where we've assumed that two such terms are equal, we are justified in concluding anything we want, since the assumption is nonsensical.
The discriminate tactic embodies this principle: It is used on a hypothesis involving an equality between different constructors (e.g., S n = O), and it solves the current goal immediately. Here is an example:
Theorem eqb_0_l : n,
   eqb 0 n = true n = 0.
Proof.
  intros n.
We can proceed by case analysis on n. The first case is trivial.
  destruct n as [| n'] eqn:E.
  - (* n = 0 *)
    intros H. reflexivity.
However, the second one doesn't look so simple: assuming eqb 0 (S n') = true, we must show S n' = 0! The way forward is to observe that the assumption itself is nonsensical:
  - (* n = S n' *)
    simpl eqb.
If we use discriminate on this hypothesis, Coq confirms that the subgoal we are working on is impossible and removes it from further consideration.
    intros H. discriminate H.
Qed.
The discriminate tactic is an instance of the logical principle we met earlier: the principle of explosion.
Theorem discriminate_ex1 : (n : nat),
  S n = O
  2 + 2 = 5.
Proof.
  (* Let n be given, and assume S n = 0. *)
  intros n contra.
  (* But by the disjointness of the constructors for nat, this is
  impossible---S of anything can't possibly be O.  So we have a
  contradiction. *)

  discriminate contra. Qed.

Theorem discriminate_ex2 : (n m : nat),
  false = true
  [n] = [m].
Proof.
  intros n m contra. discriminate contra. Qed.
If you find the principle of explosion confusing, remember that these proofs are not showing that the conclusion of the statement holds. Rather, they are showing that, if the nonsensical situation described by the premise did somehow arise, then the nonsensical conclusion would also follow, because we'd be living in an inconsistent universe where every statement is true. We'll explore the principle of explosion in more detail later on.

Exercise: 1 star, standard (discriminate_ex3)

Example discriminate_ex3 :
   (X : Type) (x y z : X) (l j : list X),
    x :: y :: l = []
    x = z.
Proof.
  (* FILL IN HERE *) Admitted.
This is how we use not to state that 0 and 1 are different elements of nat:
Theorem zero_not_one : ~(0 = 1).
Proof.
The proposition 0 1 is exactly the same as ~(0 = 1), that is not (0 = 1), which unfolds to (0 = 1) False. (We use unfold not explicitly here to illustrate that point, but generally it can be omitted.)
  unfold not.
To prove an inequality, we may assume the opposite equality...
  intros contra.
... and deduce a contradiction from it. Here, the equality O = S O contradicts the disjointness of constructors O and S, so discriminate takes care of it.
  discriminate contra.
Qed.
Such inequality statements are frequent enough to warrant a special notation, x y:
Check (0 1).
(* ===> Prop *)

Theorem zero_not_one' : 0 1.
Proof.
  intros H. discriminate H.
Qed.
Similarly, since inequality involves a negation, it requires a little practice to be able to work with it fluently. Here is one useful trick. If you are trying to prove a goal that is nonsensical (e.g., the goal state is false = true), apply ex_falso_quodlibet to change the goal to False. This makes it easier to use assumptions of the form ¬P that may be available in the context -- in particular, assumptions of the form xy.
Theorem not_true_is_false : b : bool,
  b true b = false.
Proof.
  (* Let b be given, and assume b true. Observe that b is either true or false. *)
  intros b H. destruct b.
  - (* b = true *)
    (* If b is true, we must show b = false. But we've already
    assumed b true, so this case will never arise. *)

    unfold not in H.
    apply ex_falso_quodlibet.
    apply H. reflexivity.
  - (* b = false *)
    (* If b is false, we have our goal of b = false immediately. *)
    reflexivity.
Qed.
Since reasoning with ex_falso_quodlibet is quite common, Coq provides a built-in tactic, exfalso, for applying it.
Theorem not_true_is_false' : b : bool,
  b true b = false.
Proof.
  intros [] H.
  - (* b = false *)

    unfold not in H.
    exfalso. (* <=== *)
    apply H. reflexivity.
  - (* b = true *) reflexivity.
Qed.

Theorem contradiction_implies_anything : P Q : Prop,
  (P ¬P) Q.
Proof.
  (* WORKED IN CLASS *)
  intros P Q [HP HNA]. unfold not in HNA.
  apply HNA in HP. destruct HP. Qed.

Exercise: 1 star, standard, optional (not_both_true_and_false)

Some (optional!) practice with logical connectives.
Theorem not_both_true_and_false : P : Prop,
  ¬ (P ¬P).
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard (injection_discriminate_informal)

(* In comments, write an _informal_ proof of the following property,
   which will require both injection (by the injectivity of ...) and
   discriminate (by the disjointness of ...) to prove.  You don't have
   to prove it in Coq first, but you may if you like.

   Try to solve it without any apply-ing of previous theorems.  Case
   analysis is ok.  This may be the longest proof you've done yet.

   Before you get started, think about what you know, how injection
   could help, how to do proofs making use of andb or leb.  Reasoning
   by the injectivity of S will be one of your first moves. *)


Theorem injection_discriminate : (n m : nat) (b c:bool),
    andb b c = leb n m S n = S 0 b = c.
Proof.
  (* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_injection_discriminate_informal : option (nat×string) := None.

Logical Equivalence

The handy "if and only if" a/k/a iff connective, which asserts that two propositions have the same truth value, is just the conjunction of two implications.
PROP ::= EXPR1 = EXPR2 | forall x : TYPE, PROP | PROP1 -> PROP2 | PROP1 /\ PROP2 | PROP1 \/ PROP2 | True | ~ PROP | False | PROP1 <-> PROP2
Module MyIff.

Definition iff (P Q : Prop) := (P Q) (Q P).

Notation "P <-> Q" := (iff P Q)
                      (at level 95, no associativity)
                      : type_scope.

End MyIff.

Theorem iff_sym : P Q : Prop,
  (P Q) (Q P).
Proof.
  (* WORKED IN CLASS *)
  intros P Q [HAB HBA].
  split.
  - (* -> *) apply HBA.
  - (* <- *) apply HAB. Qed.

Exercise: 1 star, standard, optional (iff_properties)

Using the above proof that is symmetric (iff_sym) as a guide, prove that it is also reflexive and transitive.
Theorem iff_refl : P : Prop,
  P P.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem iff_trans : P Q R : Prop,
  (P Q) (Q R) (P R).
Proof.
  (* FILL IN HERE *) Admitted.
Some of Coq's tactics treat iff statements specially, avoiding the need for some low-level proof-state manipulation. In particular, rewrite and reflexivity can be used with iff statements, not just equalities. To enable this behavior, we imported a "Setoid" Coq library on Day11.
Here is a simple example demonstrating how these tactics work with iff. First, let's prove a couple of basic iff equivalences...
Lemma orb_true_iff : b1 b2,
  b1 || b2 = true b1 = true b2 = true.
Proof.
  (* We proceed by cases on b1. *)
  intros [].
  - (* Assuming b1 = true, we must show true || b2 = true true = true b2 = true. *)
    (* By the definition of orb, this is the same as showing true = true true = true b2 = true. *)
    simpl orb. intros b2.
    (* We will prove each direction of the biconditional. *)
    split.
    + (* Assume true = true.  We must show true = true b2 = true, and the left disjunct is immediate from our assumption. *)
      intros _. left. reflexivity.
    + (* Now assume true = true b2 = true. We must show true = true; but this is immediate anyhow. *)
      intros _. reflexivity.
  - (* Assuming b1 = false, we must show false || b2 = true false = true b2 = true.  By the definition of orb this is the same as showing b2 = true false = true b2 = true. *)
    simpl orb. intros []. (* We go by cases on b2. *)
    + (* If b2 is true, we must show true = true false = true true = true.  We prove each direction separately. *)
      split.
      × (* Assuming true = true, we must show false = true true = true.  The right hand of the disjunction is immediate. *)
        intros _. right. reflexivity.
      × (* Assuming false = true true = true, we must show true = true, but that's immediate. *)
        intros _. reflexivity.
    + (* If b2 is false, we must show false = true false = true false = true. *)
      (* We prove each direction separately. *)
      split.
      × (* Assuming false = true, we must show false = true false = true.  But we've just assumed that false = true, which is a contradiction by the disjointness of the constructors of bool. *)
        intros H. discriminate H.
      × (* Now assume false = true false = true.  Either assumption is contradictory by the disjointness of constructors for bool. *)
        intros [H | H].
        { discriminate H. }
        { discriminate H. }
Qed.

Lemma or_assoc :
   P Q R : Prop, P (Q R) (P Q) R.
Proof.
  intros P Q R. split.
  - intros [H | [H | H]].
    + left. left. apply H.
    + left. right. apply H.
    + right. apply H.
  - intros [[H | H] | H].
    + left. apply H.
    + right. left. apply H.
    + right. right. apply H.
Qed.
We can now use these facts with rewrite and reflexivity to give smooth proofs of statements involving equivalences. Here is a ternary version of the orb_true_iff result:
Lemma orb_true_3 :
   a b c : bool, a || b || c = true a = true b = true c = true.
Proof.
  intros n m p.
  rewrite orb_true_iff. rewrite orb_true_iff. rewrite or_assoc.
  reflexivity.
Qed.
The apply tactic can also be used with . When given an equivalence as its argument, apply tries to guess which side of the equivalence to use.
Lemma apply_iff_example :
   a b : bool, a || b = true a = true b = true.
Proof.
  intros n m H. apply orb_true_iff. apply H.
Qed.

Lemma not_true_iff_false : b,
  b true b = false.
Proof.
  (* WORKED IN CLASS *)
  intros b. split.
  - (* -> *) apply not_true_is_false.
  - (* <- *)
    intros H. rewrite H. intros H'. discriminate H'.
Qed.
It's common to use iff to relate functions to propositions---like we already saw for orb_true_iff. Here we relate the eq_base function to the = proposition. All of these are good practice, but we leave them optional.

Exercise: 1 star, standard, optional (eq_base_refl)

Lemma eq_base_refl : (b : base),
    eq_base b b = true.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard, optional (eq_base_true)

Lemma eq_base_true : (b1 b2 : base),
    eq_base b1 b2 = true b1 = b2.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard, optional (eq_base_iff)

Prove a theorem characterizing equality on DNA bases.
Proofs relating equality predicates (i.e., functions) to the equality proposition tend to take this form: one direction is simply reflexivity (if b1 = b2, then you need only show that eq_blah b1 b1 = true) and the other is more involved (if eq_blah b1 b2 = true, then b1 = b2 for real).
Lemma eq_base_iff : (b1 b2 : base),
    eq_base b1 b2 = true b1 = b2.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard (not_P__P_true)

This lemma is particularly useful for when we have computational characterizations of interesting properties.
Lemma not_P__P_true : P b,
    b = true P
    b = false ¬P.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard, optional (andb_true_iff)

The following lemma relates the conjunction to the corresponding boolean operations.
Lemma andb_true_iff : b1 b2:bool,
  b1 && b2 = true b1 = true b2 = true.
Proof.
  (* FILL IN HERE *) Admitted.

Using Tactics on Hypotheses

By default, most tactics work on the goal formula and leave the context unchanged. However, many tactics also have a variant that performs a similar operation on a statement in the context.
For example, the tactic simpl ... in H performs simplification in the hypothesis named H in the context.
Theorem S_inj : (n m : nat) (b : bool),
     eqb (S n) (S m) = b
     eqb n m = b.
Proof.
  intros n m b H. simpl eqb in H. apply H. Qed.
Similarly, apply L in H matches some conditional statement L (of the form L1 L2, say) against a hypothesis H in the context. However, unlike ordinary apply (which rewrites a goal matching L2 into a subgoal L1), apply L in H matches H against L1 and, if successful, replaces it with L2.
In other words, apply L in H gives us a form of "forward reasoning": from L1 L2 and a hypothesis matching L1, it produces a hypothesis matching L2. By contrast, apply L is "backward reasoning": it says that if we know L1L2 and we are trying to prove L2, it suffices to prove L1.
Here is a variant of a proof from above, using forward reasoning throughout instead of backward reasoning.
Theorem silly3' : (n : nat),
  (eqb n 5 = true eqb (S (S n)) 7 = true)
  true = eqb n 5
  true = eqb (S (S n)) 7.
Proof.
  intros n eq H.
  symmetry in H. apply eq in H. symmetry in H.
  apply H. Qed.
Forward reasoning starts from what is given (premises, previously proven theorems) and iteratively draws conclusions from them until the goal is reached. Backward reasoning starts from the goal, and iteratively reasons about what would imply the goal, until premises or previously proven theorems are reached. If you've seen informal proofs before (for example, in a math class), they probably used forward reasoning. They might have even told you that backward reasoning was wrong or not allowed! In general, idiomatic use of Coq tends to favor backward reasoning, but in some situations the forward style can be easier to think about.

Using destruct on Compound Expressions

We have seen many examples where destruct is used to perform case analysis of the value of some variable. But sometimes we need to reason by cases on the result of some expression. We can also do this with destruct.
Here are some examples:
Definition sillyfun (n : nat) : bool :=
  if eqb n 3 then false
  else if eqb n 5 then false
       else false.

Theorem sillyfun_false : (n : nat),
    sillyfun n = false.
Proof.
  intros n. unfold sillyfun.
  destruct (eqb n 3).
  - (* eqb n 3 = true *) reflexivity.
  - (* eqb n 3 = false *) destruct (eqb n 5).
    + (* eqb n 5 = true *) reflexivity.
    + (* eqb n 5 = false *) reflexivity. Qed.
After unfolding sillyfun in the above proof, we find that we are stuck on if (eqb n 3) then ... else .... But either n is equal to 3 or it isn't, so we can use destruct (eqb n 3) to let us reason about the two cases.
Informally, we might read the proof above like so:
We want to show that for any number n, sillyfun n = false. Let a number n be given. Observe that sillyfun is defined so that when eqb n 3 = true the result is false, when eqb n 5 = true the result is false, and if both are false then the result is false. We handle each case in turn.
First, suppose that eqb n 3 = true. Then we hit the first branch of sillyfun and return false, and false = false is immediate.
Second, suppose that eqb n 5 = true. Then we hit the second branch of sillyfun and likewise return false.
Finally, suppose that neither of those cases hold. Then sillyfun also returns false and the same reasoning holds.
In general, the destruct tactic can be used to perform case analysis of the results of arbitrary computations. If e is an expression whose type is some inductively defined type T, then, for each constructor c of T, destruct e generates a subgoal in which all occurrences of e (in the goal and in the context) are replaced by c.
More practically, we can use these case analyses to reason about the complex decisions made in programs. As a rule of thumb, you will need this trick whenever you are stuck on a match or an if which depends on the result of some function call rather than some ready-to-hand value.
Here's a function that computes the minimum of three arguments. First, let's make sure we have a good leb defined.
Fixpoint leb (n m : nat) : bool :=
  match n with
  | Otrue
  | S n'
      match m with
      | Ofalse
      | S m'leb n' m'
      end
  end.

Definition min3 (n1 n2 n3 : nat) : nat :=
  if leb n1 n2
  then if leb n1 n3
       then n1
       else n3
  else if leb n2 n3
       then n2
       else n3.

Definition argmin3 {A:Type} (cost : A nat) (o1 o2 o3 : A) : A :=
  let c1 := cost o1 in
  let c2 := cost o2 in
  let c3 := cost o3 in
  if leb c1 c2
  then if leb c1 c3
       then o1
       else o3
  else if leb c2 c3
       then o2
       else o3.

Exercise: 2 stars, standard (argmin3_min3_eqs)

Relate min3 to argmin3. Your proof will need to navigate why argmin3 should go one direction or another by using destruct with a compound term relevant to the decision-making process of arg3min.
Lemma argmin3_min3_eqs : {A:Type} (cost : A nat) (o1 o2 o3 : A) (n1 n2 n3 : nat),
    cost o1 = n1
    cost o2 = n2
    cost o3 = n3
    cost (argmin3 cost o1 o2 o3) = min3 n1 n2 n3.
Proof.
  (* FILL IN HERE *) Admitted.
To prove this one, you should be able to just use argmin3_min3_eqs.
Corollary argmin3_min3 : {A:Type} (cost : A nat) (o1 o2 o3 : A),
    cost (argmin3 cost o1 o2 o3) = min3 (cost o1) (cost o2) (cost o3).
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard (argmin3_min3_eqs_informal)

(* As before, add comments to your proof of argmin3_min3_eqs above
   (either line by line or in one large block) to provide an informal
   proof.  You can use language like "by cases on whether cost o1 <=
   cost o2" or "observe that either cost o1 <= cost o2 or cost o2 <
   cost o1; we go by cases."  *)


(* Do not modify the following line: *)
Definition manual_grade_for_argmin3_min3_eqs_informal : option (nat×string) := None.
However, destructing compound expressions requires a bit of care, as such destructs can sometimes erase information we need to complete a proof. For example, suppose we define a function sillyfun1 like this:
Definition sillyfun1 (n : nat) : bool :=
  if eqb n 3 then true
  else if eqb n 5 then true
       else false.
Now suppose that we want to convince Coq of the (rather obvious) fact that sillyfun1 n yields true only when n is odd. By analogy with the proofs we did with sillyfun above, it is natural to start the proof like this:
Theorem sillyfun1_odd_FAILED : (n : nat),
    ( n m, eqb n m = true n = m)
    sillyfun1 n = true
    oddb n = true.
Proof.
  intros n eqb_true eq. unfold sillyfun1 in eq.
  destruct (eqb n 3).
  (* stuck... *)
Abort.
We get stuck at this point because the context does not contain enough information to prove the goal! The problem is that the substitution performed by destruct is too brutal -- it threw away every occurrence of eqb n 3, but we need to keep some memory of this expression and how it was destructed, because we need to be able to reason that, since eqb n 3 = true in this branch of the case analysis, it must be that n = 3, from which it follows that n is odd.
What we would really like is to substitute away all existing occurences of eqb n 3, but at the same time add an equation to the context that records which case we are in. Recall that the eqn: qualifier allows us to introduce such an equation, giving it a name that we choose.
Theorem sillyfun1_odd : (n : nat),
    ( n m, eqb n m = true n = m)
    sillyfun1 n = true
    oddb n = true.
Proof.
  (* Let n be given, and assume that for all n and m, if eqb n m = true then n = m.  Also assume sillyfun1 n = true.  *)
  intros n eqb_true eq. unfold sillyfun1 in eq.
  (* "Observe that eqb n 3 is either true or false." *)
  destruct (eqb n 3) eqn:Heqe3.
  (* Now we have the same state as at the point where we got
     stuck above, except that the context contains an extra equality
     assumption, which is exactly what we need to make progress. *)

  - (* e3 = true *) apply eqb_true in Heqe3.
    (* If it is true, then we know that n = 3 by our earlier assumption. *)
    rewriteHeqe3. reflexivity.
  - (* e3 = false *)
    (* Otherwise, eqb n 5 is also either true or false. *)
    (* When we come to the second equality test in the body of
       the function we are reasoning about, we can use eqn: again in
       the same way, allow us to finish the proof. *)

    destruct (eqb n 5) eqn:Heqe5.
    + (* e5 = true *)
      (* If it is true, then we know n = 5. *)
      apply eqb_true in Heqe5.
      rewriteHeqe5. reflexivity.
    + (* e5 = false *)
      (* If n is neither 3 nor 5, sillyfun1 could not possibly
         have returned true, so we have a contradiction in our
         assumptions. *)

      discriminate eq. Qed.

(* 2022-01-12 10:20 *)