MorePropMore about Propositions and Evidence


Require Export "Prop".

Relations

Just as a single-argument proposition defines a 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

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

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?
      pred (S O) = O
(1) Prop
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable
What is the type of the following expression?
      ∀n:nat, pred (S n) = n
(1) Prop
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable
What is the type of the following expression?
      ∀n:nat, S (pred n) = n
(1) Prop
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable
What is the type of the following expression?
      ∀n:nat, pred (S n)
(1) Prop
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable
What is the type of the following expression?
      fun n:nat ⇒ pred (S n)
(1) Prop
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable
What is the type of the following expression?
      fun n:nat ⇒ pred (S n) = n
(1) Prop
(2) nat→Prop
(3) ∀ n:nat, Prop
(4) nat→nat
(5) Not typeable

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