Existential Quantification

Another important logical connective is existential quantification. To say that there is some x of type T such that some property P holds of x, we write ∃ x : T, P. As with ∀, the type annotation : T can be omitted if Coq is able to infer from the context what the type of x should be. The notion of "existential" is a common one in mathematics, but you may not be familiar with its precise meaning. It might be easier to understand ∃ as the "dual" of ∀. When we say ∀ x : T, P, we mean to say that:

• Given any possible value v of type T,
• the proposition P holds when we replace x with v.

So, for example, when we say ∀ n : nat, n + 0 = n, we mean that we 0 + 0 = 0 (choosen 0 for n) and 1 + 0 = 1 (choosing 1 for n) and 47 + 0 = 47 (choosing 47 for n). When we say that ∃ x : T, P, we mean that

• There is at least one value v of type T, such that
• the proposition P holds when we replace x with v.

For example, ∃ n : nat, S n = 48 means "there is (at least one) natural number n such that the successor of n is 48". It turns out that this S n = 48 for exactly one n: 47. But it need not be so: the proposition ∃ l : list nat, length l = 1 means that "there exists a list of naturals l such that length l is 1". There are many such lists: [1] , [1337] , and so on. PROP ::= EXPR1 = EXPR2 | forall x : TYPE, PROP | PROP1 -> PROP2 | PROP1 /\ PROP2 | PROP1 \/ PROP2 | True | ~ PROP | False | PROP1 <-> PROP2 | exists x : TYPE, PROP <---- NEW! To prove a statement of the form ∃ x, P, we must show that P holds for some specific choice of value for x, known as the witness of the existential. This is done in two steps: First, we explicitly tell Coq which witness t we have in mind by invoking the tactic ∃ t. Then we prove that P holds after all occurrences of x are replaced by t.

Conversely, if we have an existential hypothesis ∃ x, P in the context, we can destruct it to obtain a witness x and a hypothesis stating that P holds of x.

Exercise: 1 star, standard, especially useful (dist_not_exists)

Prove that "P holds for all x" implies "there is no x for which P does not hold." (Hint: destruct H as [x E] works on existential assumptions!)

Exercise: 1 star, standard, especially useful (dist_not_forall)

Prove that "there exists an x for which P holds" implies "it is not the case that for all x P does not hold." (Hint: destruct H as [x E] works on existential assumptions!)

Exercise: 2 stars, standard, optional (dist_exists_or)

Prove that existential quantification distributes over disjunction.

Propositions and Booleans

We've seen two different ways of encoding logical facts in Coq: with booleans (of type bool), and with propositions (of type Prop). For instance, to claim that a number n is even, we can say either

• (1) that evenb n returns true, or
• (2) that there exists some k such that n = double k.

Indeed, these two notions of evenness are equivalent, as can easily be shown with a couple of auxiliary lemmas. Of course, it would be very strange if these two characterizations of evenness did not describe the same set of natural numbers! Fortunately, we can prove that they do... We first need three helper lemmas.

Exercise: 2 stars, standard, optional (evenb_S)

One inconvenient aspect of our definition of evenb n is the recursive call on n - 2. This makes proofs about evenb n harder when done by induction on n, since we may need an induction hypothesis about n - 2. The following lemma gives an alternative characterization of evenb (S n) that works better with induction:

Exercise: 3 stars, standard (evenb_double_conv)

In view of this theorem, we say that the boolean computation evenb n reflects the logical proposition ∃ k, n = double k. However, even when the boolean and propositional formulations of a claim are equivalent from a purely logical perspective, they need not be equivalent operationally. Equality provides an extreme example: knowing that eqb n m = true is generally of little direct help in the middle of a proof involving n and m; however, if we convert the statement to the equivalent form n = m, we can rewrite with it. The case of even numbers is also interesting. Recall that, when proving the backwards direction of even_bool_prop (i.e., evenb_double, going from the propositional to the boolean claim), we used a simple induction on k. On the other hand, the converse (the evenb_double_conv exercise) required a clever generalization, since we can't directly prove (∃ k, n = double k) → evenb n = true. For these examples, the propositional claims are more useful than their boolean counterparts, but this is not always the case. For instance, we cannot test whether a general proposition is true or not in a function definition; as a consequence, the following code fragment is rejected:

Coq complains that n = 2 has type Prop, while it expects an elements of bool (or some other inductive type with two elements). The reason for this error message has to do with the computational nature of Coq's core language, which is designed so that every function that it can express is computable and total. One reason for this is to allow the extraction of executable programs from Coq developments. As a consequence, Prop in Coq does not have a universal case analysis operation telling whether any given proposition is true or false, since such an operation would allow us to write non-computable functions. Although general non-computable properties cannot be phrased as boolean computations, it is worth noting that even many computable properties are easier to express using Prop than bool, since recursive function definitions are subject to significant restrictions in Coq. For instance, later we'll shows how to define the property that two lists are permutations of each a given string using Prop. Doing the same with bool would amount to the is_permutation_of function we wrote on day 6... which (as we'll see) is more complicated, harder to understand, and harder to reason about than the Prop we'll define. Conversely, an important side benefit of stating facts using booleans is enabling some proof automation through computation with Coq terms, a technique known as proof by reflection. Consider the following statement:

The most direct proof of this fact is to give the value of k explicitly.

On the other hand, the proof of the corresponding boolean statement is even simpler:

What is interesting is that, since the two notions are equivalent, we can use the boolean formulation to prove the other one without mentioning the value 500 explicitly:

Although we haven't gained much in terms of proof size in this case, larger proofs can often be made considerably simpler by the use of reflection. As an extreme example, the Coq proof of the famous 4-color theorem uses reflection to reduce the analysis of hundreds of different cases to a boolean computation. We won't cover reflection in any real detail, but it serves as a good example showing the complementary strengths of booleans and general propositions. As we go on to prove more interesting (and challenging!) things about our programs, the various iff lemmas relating computation to logic will surely come in handy.

Classical vs. Constructive Logic

We have seen that it is not possible to test whether or not a proposition P holds while defining a Coq function. You may be surprised to learn that a similar restriction applies to proofs! In other words, the following intuitive reasoning principle is not derivable in Coq:

To understand operationally why this is the case, recall that, to prove a statement of the form P ∨ Q, we use the left and right tactics, which effectively require knowing which side of the disjunction holds. But the universally quantified P in excluded_middle is an arbitrary proposition, which we know nothing about. We don't have enough information to choose which of left or right to apply, just as Coq doesn't have enough information to mechanically decide whether P holds or not inside a function. However, if we happen to know that P is reflected in some boolean term b, then knowing whether it holds or not is trivial: we just have to check the value of b.

In particular, the excluded middle is valid for equations n = m, between natural numbers n and m.

It may seem strange that the general excluded middle is not available by default in Coq; after all, any given claim must be either true or false. Nonetheless, there is an advantage in not assuming the excluded middle: statements in Coq can make stronger claims than the analogous statements in standard mathematics. Notably, if there is a Coq proof of ∃ x, P x, it is possible to explicitly exhibit a value of x for which we can prove P x -- in other words, every proof of existence is necessarily constructive. Logics like Coq's, which do not assume the excluded middle, are referred to as constructive logics. More conventional logical systems such as ZFC, in which the excluded middle does hold for arbitrary propositions, are referred to as classical. The following example illustrates why assuming the excluded middle may lead to non-constructive proofs: Claim: There exist irrational numbers a and b such that a ^ b is rational. Proof: It is not difficult to show that sqrt 2 is irrational. If sqrt 2 ^ sqrt 2 is rational, it suffices to take a = b = sqrt 2 and we are done. Otherwise, sqrt 2 ^ sqrt 2 is irrational. In this case, we can take a = sqrt 2 ^ sqrt 2 and b = sqrt 2, since a ^ b = sqrt 2 ^ (sqrt 2 × sqrt 2) = sqrt 2 ^ 2 = 2. ☐ Do you see what happened here? We used the excluded middle to consider separately the cases where sqrt 2 ^ sqrt 2 is rational and where it is not, without knowing which one actually holds! Because of that, we wind up knowing that such a and b exist but we cannot determine what their actual values are (at least, using this line of argument). As useful as constructive logic is, it does have its limitations: There are many statements that can easily be proven in classical logic but that have much more complicated constructive proofs, and there are some that are known to have no constructive proof at all! Fortunately, the excluded middle is known to be compatible with Coq's logic, allowing us to add it safely as an axiom. However, we will not need to do so in this book: the results that we cover can be developed entirely within constructive logic at negligible extra cost. It takes some practice to understand which proof techniques must be avoided in constructive reasoning, but arguments by contradiction, in particular, are infamous for leading to non-constructive proofs. Here's a typical example: suppose that we want to show that there exists x with some property P, i.e., such that P x. We start by assuming that our conclusion is false; that is, ¬ ∃ x, P x. From this premise, it is not hard to derive ∀ x, ¬ P x. If we manage to show that this intermediate fact results in a contradiction, we arrive at an existence proof without ever exhibiting a value of x for which P x holds! The technical flaw here, from a constructive standpoint, is that we claimed to prove ∃ x, P x using a proof of ¬ ¬ (∃ x, P x). Allowing ourselves to remove double negations from arbitrary statements is equivalent to assuming the excluded middle. Thus, this line of reasoning cannot be encoded in Coq without assuming additional axioms.

Exercise: 2 stars, standard (forall_exists)

In classical logic, ∀ and ∃ are dual: negating one gets you to the other. We saw some of this duality with dist_not_exists and dist_not_forall. Only one of the following lemmas is provable in constructive logic. Which? Why isn't the other provable?

In addition to doing one of these proofs, please briefly explain why the other doesn't work.