Relations

A proposition parameterized by a number (such as ev or beautiful) can be thought of as a property — i.e., it defines a subset of nat, namely those numbers for which the proposition is provable. In the same way, a two-argument proposition can be thought of as a relation — i.e., it defines a set of pairs for which the proposition is provable.

One useful example is the "less than or equal to" relation on numbers. The following definition should be fairly intuitive. It says that there are two ways to give evidence that one number is less than or equal to another: either observe that they are the same number, or give evidence that the first is less than or equal to the predecessor of the second.

Proofs of facts about ≤ using the constructors le_n and le_S follow the same patterns as proofs about properties, like ev in chapter Prop. We can apply the constructors to prove ≤ goals (e.g., to show that 3≤3 or 3≤6), and we can use tactics like inversion to extract information from ≤ hypotheses in the context (e.g., to prove that (2 ≤ 1) → 2+2=5.) Here are some sanity checks on the definition. (Notice that, although these are the same kind of simple "unit tests" as we gave for the testing functions we wrote in the first few lectures, we must construct their proofs explicitly — simpl and reflexivity don't do the job, because the proofs aren't just a matter of simplifying computations.)

The "strictly less than" relation n < m can now be defined in terms of le.

Here are a few more simple relations on numbers:

Exercise: 2 stars (total_relation)

Define an inductive binary relation total_relation that holds between every pair of natural numbers.

☐

Exercise: 2 stars (empty_relation)

Define an inductive binary relation empty_relation (on numbers) that never holds.

☐

Exercise: 2 stars, optional (le_exercises)

Here are a number of facts about the ≤ and < relations that we are going to need later in the course. The proofs make good practice exercises.

Exercise: 3 stars (R_provability)

We can define three-place relations, four-place relations, etc., in just the same way as binary relations. For example, consider the following three-place relation on numbers:

• Which of the following propositions are provable?
  • R 1 1 2
  • R 2 2 6
• If we dropped constructor c5 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.
• If we dropped constructor c4 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.

(* FILL IN HERE *)
☐

Exercise: 3 stars, optional (R_fact)

Relation R actually encodes a familiar function. State and prove two theorems that formally connects the relation and the function. That is, if R m n o is true, what can we say about m, n, and o, and vice versa?

☐

Programming with Propositions

A proposition is a statement expressing a factual claim, like "two plus two equals four." In Coq, propositions are written as expressions of type Prop. Although we haven't discussed this explicitly, we have already seen numerous examples.

Both provable and unprovable claims are perfectly good propositions. Simply being a proposition is one thing; being provable is something else!

Both 2 + 2 = 4 and 2 + 2 = 5 are legal expressions of type Prop. We've mainly seen one place that propositions can appear in Coq: in Theorem (and Lemma and Example) declarations.

But they can be used in many other ways. For example, we have also seen that we can give a name to a proposition using a Definition, just as we have given names to expressions of other sorts.

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

We've seen several ways of constructing propositions.

• We can define a new proposition primitively using Inductive.
• Given two expressions e1 and e2 of the same type, we can form the proposition e1 = e2, which states that their values are equal.
• We can combine propositions using implication and quantification.

We have also seen parameterized propositions, such as even and beautiful.

The type of even, i.e., nat→Prop, can be pronounced in three equivalent ways: (1) "even is a function from numbers to propositions," (2) "even is a family of propositions, indexed by a number n," or (3) "even is a property of numbers." Propositions — including parameterized propositions — are first-class citizens in Coq. For example, we can define functions from numbers to propositions...

... and then partially apply them:

We can even pass propositions — including parameterized propositions — as arguments to functions:

Here are two more examples of passing parameterized propositions as arguments to a function. The first function, true_for_all_numbers, takes a proposition P as argument and builds the proposition that P is true for all natural numbers.

The second, preserved_by_S, takes P and builds the proposition that, if P is true for some natural number n', then it is also true by the successor of n' — i.e. that P is preserved by successor:

Finally, we can put these ingredients together to define a proposition stating that induction is valid for natural numbers:

Exercise: 3 stars (combine_odd_even)

Complete the definition of the combine_odd_even function below. It takes as arguments two properties of numbers Podd and Peven. As its result, it should return a new property P such that P n is equivalent to Podd n when n is odd, and equivalent to Peven n otherwise.

To test your definition, see whether you can prove the following facts:

☐

One more quick digression, for adventurous souls: if we can define parameterized propositions using Definition, then can we also define them using Fixpoint? Of course we can! However, this kind of "recursive parameterization" doesn't correspond to anything very familiar from everyday mathematics. The following exercise gives a slightly contrived example.

Exercise: 4 stars, optional (true_upto_n__true_everywhere)

Define a recursive function true_upto_n__true_everywhere that makes true_upto_n_example work.

☐