PropPropositions and Evidence

Require Export MoreCoq.

So far, all of our theorems have concluded with an equality proposition of the form e1 = e2. But Coq supports a much broader range of primitive propositions.

Inductively Defined Propositions

As a running example, let's define a simple property of natural numbers — we'll call it "beautiful."
Informally, a number is beautiful if it is 0, 3, 5, or the sum of two beautiful numbers.
More pedantically, we can define beautiful numbers by giving four rules:
  • Rule b_0: The number 0 is beautiful.
  • Rule b_3: The number 3 is beautiful.
  • Rule b_5: The number 5 is beautiful.
  • Rule b_sum: If n and m are both beautiful, then so is their sum.
Such definitions are often presented using inference rules:

beautiful 0

beautiful 3

beautiful 5
beautiful n     beautiful m (b_sum)  

beautiful (n+m)
The following proof tree demonstrates that 8 is beautiful:
         ----------- (b_3)   ----------- (b_5)
         beautiful 3         beautiful 5
         ------------------------------- (b_sum)
                   beautiful 8   
Of course, there are other ways of using these rules to argue that 8 is beautiful, for instance:
         ----------- (b_5)   ----------- (b_3)
         beautiful 5         beautiful 3
         ------------------------------- (b_sum)
                   beautiful 8   

How many different ways are there to show that 8 is beautiful?
(1) one
(2) two
(3) three
(4) four
(5) five
(6) infinitely many

In Coq, we can express the definition of beautiful as follows:

Inductive beautiful : nat Prop :=
  b_0 : beautiful 0
| b_3 : beautiful 3
| b_5 : beautiful 5
| b_sum : n m, beautiful n beautiful m beautiful (n+m).

The first line declares that beautiful is a proposition — or, more formally, a family of propositions "indexed by" natural numbers. (That is, for each number n, the claim that "n is beautiful" is a proposition.) Such a family of propositions is often called a property of numbers. Each of the remaining lines embodies one of the rules for beautiful numbers.
The rules introduced this way have the same status as proven theorems; that is, they are true axiomatically. So we can use Coq's apply tactic with the rule names to prove that particular numbers are beautiful.

Theorem three_is_beautiful: beautiful 3.
   apply b_3.

Theorem eight_is_beautiful: beautiful 8.
   apply b_sum with (n:=3) (m:=5).
   apply b_3.
   apply b_5.

As you would expect, we can also prove theorems that have hypotheses about beautiful.

Theorem beautiful_plus_eight: n, beautiful n beautiful (8+n).
  intros n B.
  apply b_sum with (n:=8) (m:=n).
  apply eight_is_beautiful.
  apply B.

Exercise: 2 stars (b_timesm)

Theorem b_timesm: n m, beautiful n beautiful (m×n).
   (* FILL IN HERE *) Admitted.

Induction Over Evidence

Besides constructing evidence that numbers are beautiful, we can also reason about such evidence.
The fact that we introduced beautiful with an Inductive declaration tells Coq not only that the constructors b_0, b_3, b_5 and b_sum are ways to build evidence, but also that these two constructors are the only ways to build evidence that numbers are beautiful.
In other words, if someone gives us evidence E for the assertion beautiful n, then we know that E must have one of four shapes:
  • E is b_0 (and n is O),
  • E is b_3 (and n is 3),
  • E is b_5 (and n is 5), or
  • E is b_sum n1 n2 E1 E2 (and n is n1+n2, where E1 is evidence that n1 is beautiful and E2 is evidence that n2 is beautiful).
This permits us to analyze any hypothesis of the form beautiful n to see how it was constructed, using the tactics we already know. In particular, we can use the induction tactic that we have already seen for reasoning about inductively defined data to reason about inductively defined evidence.
To illustrate this, let's define another property of numbers:

Inductive gorgeous : nat Prop :=
  g_0 : gorgeous 0
| g_plus3 : n, gorgeous n gorgeous (3+n)
| g_plus5 : n, gorgeous n gorgeous (5+n).

Now let's prove that every gorgeous number is also beautiful.

Theorem gorgeous__beautiful : n,
  gorgeous n beautiful n.
   intros n H.
   induction H as [|n'|n'].
   Case "g_0".
       apply b_0.
   Case "g_plus3".
       apply b_sum. apply b_3.
       apply IHgorgeous.
   Case "g_plus5".
       apply b_sum. apply b_5. apply IHgorgeous.

Notice that the argument proceeds by induction on the evidence H!

From Boolean Functions to Propositions

In chapter Basics we defined a function evenb that tests a number for evenness, yielding true if so. We can use this function to define the proposition that some number n is even:

Definition even (n:nat) : Prop :=
  evenb n = true.

That is, we can define "n is even" to mean "the function evenb returns true when applied to n."
Note that here we have given a name to a proposition using a Definition, just as we have given names to expressions of other sorts. This isn't a fundamentally new kind of proposition; it is still just an equality.
A different way to talk about evenness is to define an inductively defined proposition ev n.

Inductive ev : nat Prop :=
  | ev_0 : ev O
  | ev_SS : n:nat, ev n ev (S (S n)).

How many different proof objects for ev 0 are there?
(1) 0
(2) 1
(3) 2
(4) 4
(5) Infinitely many
What about for ev 1?
(1) 0
(2) 1
(3) 2
(4) 4
(5) Infinitely many
What about for ev 2?
(1) 0
(2) 1
(3) 2
(4) 4
(5) Infinitely many
What about for an arbitrary n? How many proof objects for ev n are there?
(1) Depending on the value of n, there could be any finite number of proofs (including zero).
(2) Depending on the value of n, there could be any number of proofs (including zero or infinitely many).
(3) At most one.
(4) Exactly one.

Discussion: Computational vs. Inductive Definitions

Many concepts (like evenness) can be defined in Coq in two different ways:
  • as a recursive function returning a boolean
  • as an inductively defined predicate
Both methods have advantages:
  • Functions can be easier to work with because they are subject to Coq's machinery for simplifying expressions
    • evenb 1000 = true definitionally
    • ev 1000 must be justified by a largeish proof
  • Inductively defined predicates are more flexible
    • not subject to the requirement that Fixpoints always terminate
    • suitable for properties that are awkward, unnatural, or impossible to define as recursive functions (e.g. beautiful)
Sometimes it is helpful to define a given concept both ways, prove that they are equivalent ( n. evenb n = true ev n), and then switch back and forth as convenient.

Inversion on Evidence

Another situation where we want to analyze evidence for evenness is when proving that, if n is even, then pred (pred n)) is too. In this case, we don't need to do an inductive proof. The right tactic turns out to be inversion.

Theorem ev_minus2: n,
  ev n ev (pred (pred n)).
  intros n E.
  inversion E as [| n' E'].
  Case "E = ev_0". simpl. apply ev_0.
  Case "E = ev_SS n' E'". simpl. apply E'. Qed.

Another example, in which inversion helps narrow down to the relevant cases.

Theorem SSev__even : n,
  ev (S (S n)) ev n.
  intros n E.
  inversion E as [| n' E'].
  apply E'. Qed.

The tactic inversion actually works on any I:P where P is defined by Inductive:
  • For each constructor of P, make a subgoal and replace I by how exactly this constructor could have been used to prove P.
  • Discard contradictory subgoals (such as ev_0 above).
  • Generate auxiliary equalities (as with ev_SS above).