# MorePropMore about Propositions and Evidence

Require Export "Prop".

# Relations

*property*, a two-argument proposition defines a

*relation*.

One useful example is the "less than or equal to"
relation on numbers.

Inductive le : nat → nat → Prop :=

| le_n : ∀n, le n n

| le_S : ∀n m, (le n m) → (le n (S m)).

Notation "m ≤ n" := (le m n).

Some sanity checks...

Theorem test_le1 :

3 ≤ 3.

Proof.

(* WORK IN CLASS *) Admitted.

Theorem test_le2 :

3 ≤ 6.

Proof.

(* WORK IN CLASS *) Admitted.

Theorem test_le3 :

(2 ≤ 1) → 2 + 2 = 5.

Proof.

(* WORK IN CLASS *) Admitted.

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

Definition lt (n m:nat) := le (S n) m.

Notation "m < n" := (lt m n).

Here are a few more simple relations on numbers:

Inductive square_of : nat → nat → Prop :=

sq : ∀n:nat, square_of n (n × n).

Inductive next_nat (n:nat) : nat → Prop :=

| nn : next_nat n (S n).

Inductive next_even (n:nat) : nat → Prop :=

| ne_1 : ev (S n) → next_even n (S n)

| ne_2 : ev (S (S n)) → next_even n (S (S n)).

# Programming with Propositions

*proposition*is a factual claim. In Coq, propositions are expressions of type Prop.

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

We've mainly 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 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.

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

Propositions — including parameterized propositions — are
first-class citizens in Coq. For example, we can define functions
from numbers to propositions...

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

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

Definition natural_number_induction_valid : Prop :=

∀(P:nat→Prop),

true_for_zero P →

preserved_by_S P →

true_for_all_numbers P.

What is the type of the following expression?
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable

pred (S O) = O

(1) Prop
What is the type of the following expression?
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable

∀n:nat, pred (S n) = n

(1) Prop
What is the type of the following expression?
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable

∀n:nat, S (pred n) = n

(1) Prop
What is the type of the following expression?
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable

∀n:nat, pred (S n)

(1) Prop
What is the type of the following expression?
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable

fun n:nat ⇒ pred (S n)

(1) Prop
What is the type of the following expression?
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable

fun n:nat ⇒ pred (S n) = n

(1) Prop
Which of the following is not a proposition?
(1) 3 + 2 = 4
(2) 3 + 2 = 5
(3) beq_nat (3+2) 5
(4) beq_nat (3+2) 4 = false
(5) ∀ n, beq_nat (3+2) n = true → n = 5
(6) none of the above