We have now seen many examples of factual claims (propositions) and ways of presenting evidence of their truth (proofs). In particular, we have worked extensively with equality propositions (e₁ = e₂), implications (P → Q), and quantified propositions (∀ x, P). In this chapter, we will see how Coq can be used to carry out other familiar forms of logical reasoning. Before diving into details, we should talk a bit about the status of mathematical statements in Coq. Recall that Coq is a typed language, which means that every sensible expression has an associated type. Logical claims are no exception: any statement we might try to prove in Coq has a type, namely Prop, the type of propositions. We can see this with the Check command:

Note that all syntactically well-formed propositions have type Prop in Coq, regardless of whether they are true. Simply being a proposition is one thing; being provable is a different thing!

Indeed, propositions not only have types: they are first-class entities that can be manipulated in all the same ways as any of the other things in Coq's world. So far, we've seen one primary place that propositions can appear: in Theorem (and Lemma and Example) declarations.

But propositions can be used in other ways. For example, we can give a name to a proposition using a Definition, just as we give names to other kinds of expressions.

We can later use this name in any situation where a proposition is expected -- for example, as the claim in a Theorem declaration.

We can also write parameterized propositions -- that is, functions that take arguments of some type and return a proposition. For instance, the following function takes a number and returns a proposition asserting that this number is equal to three:

In Coq, functions that return propositions are said to define properties of their arguments. For instance, here's a (polymorphic) property defining the familiar notion of an injective function.

The equality operator = is a (binary) function that returns a Prop. The expression n = m is syntactic sugar for eq n m (defined in Coq's standard library using the Notation mechanism). Because eq can be used with elements of any type, it is also polymorphic:

(Notice that we wrote @eq instead of eq: The type argument A to eq is declared as implicit, and we need to turn off the inference of this implicit argument to see the full type of eq.)

Logical Connectives

Conjunction

The conjunction, or logical and, of propositions A and B is written A ∧ B, representing the claim that both A and B are true.

To prove a conjunction, use the split tactic. It will generate two subgoals, one for each part of the statement:

For any propositions A and B, if we assume that A is true and that B is true, we can conclude that A ∧ B is also true.

Since applying a theorem with hypotheses to some goal has the effect of generating as many subgoals as there are hypotheses for that theorem, we can apply and_intro to achieve the same effect as split.

Exercise: 2 stars, standard (plus_is_O)

So much for proving conjunctive statements. To go in the other direction -- i.e., to use a conjunctive hypothesis to help prove something else -- we employ the destruct tactic. When the current proof context contains a hypothesis H of the form A ∧ B, writing destruct H as [HA HB] will remove H from the context and replace it with two new hypotheses: HA, stating that A is true, and HB, stating that B is true.

As usual, we can also destruct H right when we introduce it, instead of introducing and then destructing it:

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:

For this specific 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 larger developments. Here's a simple example:

Another common situation with conjunctions is that we know A ∧ B but in some context we need just A or just B. In such cases we can do a destruct (possibly as part of an intros) and use an underscore pattern _ to indicate that the unneeded conjunct should just be thrown away.

Exercise: 1 star, standard, optional (proj2)

Finally, we sometimes need to rearrange the order of conjunctions and/or the grouping of multi-way conjunctions. We can see this at work in the proofs of the following commutativity and associativity theorems

Exercise: 1 star, standard (and_assoc)

(In the following proof of associativity, notice how the nested intros pattern breaks the hypothesis H : P ∧ (Q ∧ R) down into HP : P, HQ : Q, and HR : R. Finish the proof from there.)

By the way, the infix notation ∧ is actually just syntactic sugar for and A B. That is, and is a Coq operator that takes two propositions as arguments and yields a proposition.

Disjunction

Another important connective is the disjunction, or logical or, of two propositions: A ∨ B is true when either A or B is. (This infix notation stands for or A B, where or : Prop → Prop → Prop.) To use a disjunctive hypothesis in a proof, we proceed by case analysis -- which, as with other data types like nat, can be done explicitly with destruct or implicitly with an intros pattern:

We can see in this example that, when we perform case analysis on a disjunction A ∨ B, we must separately satisfy two proof obligations, each showing that the conclusion holds under a different assumption -- A in the first subgoal and B in the second. Note that the case analysis pattern [Hn | Hm] allows us to name the hypotheses that are generated for the subgoals. Conversely, to show that a disjunction holds, it suffices to show that one of its sides holds. This can be done via two tactics, left and right. As their names imply, the first one requires proving the left side of the disjunction, while the second requires proving its right side. Here is a trivial use...

... and here is a slightly more interesting example requiring both left and right:

Exercise: 1 star, standard (mult_is_O)

Exercise: 1 star, standard (or_commut)

Falsehood and Negation

So far, we have mostly been concerned with proving "positive" statements -- addition is commutative, appending lists is associative, etc. Of course, we may also be interested in negative results, demonstrating that some given proposition is not true. Such statements are expressed with the logical negation operator ¬. To see how negation works, recall the principle of explosion from the Tactics chapter, which 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 (but equivalent) choice, defining ¬ P as P → False, where False is a specific contradictory proposition defined in the standard library.

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:

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)

Show that Coq's definition of negation implies the intuitive one mentioned above. Hint: while getting accustomed to Coq's definition of not, you might find it helpful to unfold not near the beginning of proofs.

Inequality is a frequent enough form of negated statement that there is a special notation for it, x ≠ y:
      Notation "x <> y" := (~(x = y)). We can use not to state that 0 and 1 are different elements of nat:

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.)

To prove an inequality, we may assume the opposite equality...

... 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.

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 make Coq understand it! Here are proofs of a few familiar facts to get you warmed up.

Exercise: 2 stars, advanced (double_neg_informal)

Write an informal proof of double_neg: Theorem: P implies ~~P, for any proposition P.

Exercise: 2 stars, standard, especially useful (contrapositive)

Exercise: 1 star, standard (not_both_true_and_false)

Exercise: 1 star, advanced (not_PNP_informal)

Write an informal proof (in English) of the proposition ∀ P : Prop, ~(P ∧ ¬P).

Exercise: 2 stars, standard (de_morgan_not_or)

De Morgan's Laws, named for Augustus De Morgan, describe how negation interacts with conjunction and disjunction. The following law says that "the negation of a disjunction is the conjunction of the negations." There is a dual law de_morgan_not_and_not to which we will return at the end of this chapter.

Since inequality involves a negation, it also 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 x≠y.

Since reasoning with ex_falso_quodlibet is quite common, Coq provides a built-in tactic, exfalso, for applying it.

Truth

Besides False, Coq's standard library also defines True, a proposition that is trivially true. To prove it, we use the constant I : True, which is also defined in the standard library:

Unlike False, which is used extensively, True is used relatively rarely, since it is trivial (and therefore uninteresting) to prove as a goal, and conversely it provides no interesting information when used as a hypothesis. However, True can be quite useful when defining complex Props using conditionals or as a parameter to higher-order Props. We'll come back to this later. For now, let's take a look at how we can use True and False to achieve a similar effect as the discriminate tactic, without literally using discriminate. Pattern-matching lets us do different things for different constructors. If the result of applying two different constructors were hypothetically equal, then we could use match to convert an unprovable statement (like False) to one that is provable (like True).

To generalize this to other constructors, we simply have to provide the appropriate generalization of disc_fn. To generalize it to other conclusions, we can use exfalso to replace them with False. The built-in discriminate tactic takes care of all this for us!

Exercise: 2 stars, advanced, optional (nil_is_not_cons)

Use the same technique as above to show that nil ≠ x :: xs. Do not use the discriminate tactic.

Logical Equivalence

The handy "if and only if" connective, which asserts that two propositions have the same truth value, is simply the conjunction of two implications.

The apply tactic can also be used with ↔. We can use apply on an ↔ in either direction, without explicitly thinking about the fact that it is really an and underneath.

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.

Exercise: 3 stars, standard (or_distributes_over_and)

Setoids and Logical Equivalence

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 have to import the Coq library that supports it:

A "setoid" is a set equipped with an equivalence relation -- that is, a relation that is reflexive, symmetric, and transitive. When two elements of a set are equivalent according to the relation, rewrite can be used to replace one element with the other. We've seen that already with the equality relation = in Coq: when x = y, we can use rewrite to replace x with y, or vice-versa. Similarly, the logical equivalence relation ↔ is reflexive, symmetric, and transitive, so we can use it to replace one part of a proposition with another: if P ↔ Q, then we can use rewrite to replace P with Q, or vice-versa. Here is a simple example demonstrating how these tactics work with iff. First, let's prove a couple of basic iff equivalences.

We can now use these facts with rewrite and reflexivity to give smooth proofs of statements involving equivalences. For example, here is a ternary version of the previous mult_0 result: