# 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

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

*inference rules*:

(b_0) | |

beautiful 0 |

(b_3) | |

beautiful 3 |

(b_5) | |

beautiful 5 |

beautiful n beautiful m | (b_sum) |

beautiful (n+m) |

*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:
beautiful 3 beautiful 5

------------------------------- (b_sum)

beautiful 8

----------- (b_5) ----------- (b_3)

beautiful 5 beautiful 3

------------------------------- (b_sum)

beautiful 8

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

*property*of numbers. Each of the remaining lines embodies one of the rules for beautiful numbers.Theorem three_is_beautiful: beautiful 3.

Proof.

apply b_3.

Qed.

Theorem eight_is_beautiful: beautiful 8.

Proof.

apply b_sum with (n:=3) (m:=5).

apply b_3.

apply b_5.

Qed.

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

Theorem beautiful_plus_eight: ∀n, beautiful n → beautiful (8+n).

Proof.

intros n B.

apply b_sum with (n:=8) (m:=n).

apply eight_is_beautiful.

apply B.

Qed.

Theorem b_timesm: ∀n m, beautiful n → beautiful (m×n).

Proof.

(* FILL IN HERE *) Admitted.

Proof.

(* FILL IN HERE *) Admitted.

☐

## Induction Over Evidence

*constructing*evidence that numbers are beautiful, we can also

*reason about*such evidence.

*only*ways to build evidence that numbers are beautiful.

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

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

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.

Proof.

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.

Qed.

Notice that the argument proceeds by induction on the

*evidence*H!## From Boolean Functions to Propositions

*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
(3) At most one.
(4) Exactly one.

*any*number of proofs (including zero or infinitely many).### Discussion: Computational vs. Inductive Definitions

- as a recursive
*function*returning a boolean - as an inductively defined
*predicate*

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

## Inversion on Evidence

Theorem ev_minus2: ∀n,

ev n → ev (pred (pred n)).

Proof.

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.

Proof.

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