# MorePropMore about Propositions and Evidence

Require Export "Prop".

# Programming with Propositions

*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 mentioned it explicitly, we have already seen numerous examples.

Check (2 + 2 = 4).

(* ===> 2 + 2 = 4 : Prop *)

Check (ble_nat 3 2 = false).

(* ===> ble_nat 3 2 = false : Prop *)

Check (beautiful 8).

(* ===> beautiful 8 : Prop *)

Both provable and unprovable claims are perfectly good
propositions. Simply

*being*a proposition is one thing; being*provable*is something else!Check (2 + 2 = 5).

(* ===> 2 + 2 = 5 : Prop *)

Check (beautiful 4).

(* ===> beautiful 4 : Prop *)

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

Theorem plus_2_2_is_4 :

2 + 2 = 4.

Proof. reflexivity. Qed.

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

Definition plus_fact : Prop := 2 + 2 = 4.

Check plus_fact.

(* ===> plus_fact : Prop *)

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

Theorem plus_fact_is_true :

plus_fact.

Proof. reflexivity. Qed.

We've seen several ways of constructing propositions.
We have also seen

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

*parameterized propositions*, such as even and beautiful.Check (even 4).

(* ===> even 4 : Prop *)

Check (even 3).

(* ===> even 3 : Prop *)

Check even.

(* ===> even : nat -> Prop *)

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

*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."Definition between (n m o: nat) : Prop :=

andb (ble_nat n o) (ble_nat o m) = true.

... and then partially apply them:

Definition teen : nat→Prop := between 13 19.

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

Definition true_for_zero (P:nat→Prop) : Prop :=

P 0.

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.

Definition true_for_all_numbers (P:nat→Prop) : Prop :=

∀n, P n.

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*:Definition preserved_by_S (P:nat→Prop) : Prop :=

∀n', P n' → P (S n').

#### 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.Definition combine_odd_even (Podd Peven : nat → Prop) : nat → Prop :=

(* FILL IN HERE *) admit.

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

Theorem combine_odd_even_intro :

∀(Podd Peven : nat → Prop) (n : nat),

(oddb n = true → Podd n) →

(oddb n = false → Peven n) →

combine_odd_even Podd Peven n.

Proof.

(* FILL IN HERE *) Admitted.

Theorem combine_odd_even_elim_odd :

∀(Podd Peven : nat → Prop) (n : nat),

combine_odd_even Podd Peven n →

oddb n = true →

Podd n.

Proof.

(* FILL IN HERE *) Admitted.

Theorem combine_odd_even_elim_even :

∀(Podd Peven : nat → Prop) (n : nat),

combine_odd_even Podd Peven n →

oddb n = false →

Peven n.

Proof.

(* FILL IN HERE *) Admitted.

☐

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

Fixpoint true_upto_n__true_everywhere

(* FILL IN HERE *)

Example true_upto_n_example :

(true_upto_n__true_everywhere 3 (fun n => even n))

= (even 3 -> even 2 -> even 1 -> forall m : nat, even m).

Proof. reflexivity. Qed.

*)

☐

(* $Date: 2013-02-06 21:18:41 -0500 (Wed, 06 Feb 2013) $ *)