RelProperties of Relations
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export IndProp.
From LF Require Export IndProp.
Relations
Somewhat confusingly, the Coq standard library hijacks the generic
term "relation" for this specific instance of the idea. To
maintain consistency with the library, we will do the same. So,
henceforth, the Coq identifier relation will always refer to a
binary relation on some set (between the set and itself),
whereas in ordinary mathematical English the word "relation" can
refer either to this specific concept or the more general concept
of a relation between any number of possibly different sets. The
context of the discussion should always make clear which is
meant.
An example relation on nat is le, the less-than-or-equal-to
relation, which we usually write n1 ≤ n2.
Print le.
(* ====> Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m *)
Check le : nat → nat → Prop.
Check le : relation nat.
(* ====> Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m *)
Check le : nat → nat → Prop.
Check le : relation nat.
(Why did we write it this way instead of starting with Inductive
le : relation nat...? Because we wanted to put the first nat
to the left of the :, which makes Coq generate a somewhat nicer
induction principle for reasoning about ≤.)
Basic Properties
Partial Functions
For example, the next_nat relation is a partial function.
Inductive next_nat : nat → nat → Prop :=
| nn n : next_nat n (S n).
Check next_nat : relation nat.
Theorem next_nat_partial_function :
partial_function next_nat.
| nn n : next_nat n (S n).
Check next_nat : relation nat.
Theorem next_nat_partial_function :
partial_function next_nat.
However, the ≤ relation on numbers is not a partial
function. (Assume, for a contradiction, that ≤ is a partial
function. But then, since 0 ≤ 0 and 0 ≤ 1, it follows that
0 = 1. This is nonsense, so our assumption was
contradictory.)
Exercise: 2 stars, standard, optional (total_relation_not_partial_function)
Show that the total_relation defined in (an exercise in) IndProp is not a partial function.
Inductive total_relation : nat → nat → Prop :=
(* FILL IN HERE *)
.
Theorem total_relation_not_partial_function :
¬ (partial_function total_relation).
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
.
Theorem total_relation_not_partial_function :
¬ (partial_function total_relation).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (empty_relation_partial_function)
Show that the empty_relation defined in (an exercise in) IndProp is a partial function.
Inductive empty_relation : nat → nat → Prop :=
(* FILL IN HERE *)
.
Theorem empty_relation_partial_function :
partial_function empty_relation.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *)
.
Theorem empty_relation_partial_function :
partial_function empty_relation.
Proof.
(* FILL IN HERE *) Admitted.
☐
Reflexive Relations
Definition reflexive {X: Type} (R: relation X) :=
∀ a : X, R a a.
Theorem le_reflexive :
reflexive le.
∀ a : X, R a a.
Theorem le_reflexive :
reflexive le.
Definition transitive {X: Type} (R: relation X) :=
∀ a b c : X, (R a b) → (R b c) → (R a c).
Theorem le_trans :
transitive le.
Theorem lt_trans:
transitive lt.
∀ a b c : X, (R a b) → (R b c) → (R a c).
Theorem le_trans :
transitive le.
Proof.
intros n m o Hnm Hmo.
induction Hmo.
- (* le_n *) apply Hnm.
- (* le_S *) apply le_S. apply IHHmo. Qed.
intros n m o Hnm Hmo.
induction Hmo.
- (* le_n *) apply Hnm.
- (* le_S *) apply le_S. apply IHHmo. Qed.
Theorem lt_trans:
transitive lt.
Exercise: 2 stars, standard, optional (le_trans_hard_way)
We can also prove lt_trans more laboriously by induction, without using le_trans. Do this.
Theorem lt_trans' :
transitive lt.
Proof.
(* Prove this by induction on evidence that m is less than o. *)
unfold lt. unfold transitive.
intros n m o Hnm Hmo.
induction Hmo as [| m' Hm'o].
(* FILL IN HERE *) Admitted.
☐
transitive lt.
Proof.
(* Prove this by induction on evidence that m is less than o. *)
unfold lt. unfold transitive.
intros n m o Hnm Hmo.
induction Hmo as [| m' Hm'o].
(* FILL IN HERE *) Admitted.
☐
Theorem lt_trans'' :
transitive lt.
transitive lt.
Proof.
unfold lt. unfold transitive.
intros n m o Hnm Hmo.
induction o as [| o'].
(* FILL IN HERE *) Admitted.
unfold lt. unfold transitive.
intros n m o Hnm Hmo.
induction o as [| o'].
(* FILL IN HERE *) Admitted.
☐
The transitivity of le, in turn, can be used to prove some facts
that will be useful later (e.g., for the proof of antisymmetry
below)...
Exercise: 2 stars, standard, optional (le_Sn_n_inf)
Provide an informal proof of the following theorem:
(* FILL IN HERE *)
☐
☐
Symmetric and Antisymmetric Relations
Partial Orders and Preorders
A preorder is almost like a partial order, but doesn't have to be
antisymmetric.
Definition preorder {X:Type} (R: relation X) :=
(reflexive R) ∧ (transitive R).
Theorem le_order :
order le.
(reflexive R) ∧ (transitive R).
Theorem le_order :
order le.
Proof.
unfold order. split.
- (* refl *) apply le_reflexive.
- split.
+ (* antisym *) apply le_antisymmetric.
+ (* transitive. *) apply le_trans. Qed.
unfold order. split.
- (* refl *) apply le_reflexive.
- split.
+ (* antisym *) apply le_antisymmetric.
+ (* transitive. *) apply le_trans. Qed.
Reflexive, Transitive Closure
Inductive clos_refl_trans {A: Type} (R: relation A) : relation A :=
| rt_step x y (H : R x y) : clos_refl_trans R x y
| rt_refl x : clos_refl_trans R x x
| rt_trans x y z
(Hxy : clos_refl_trans R x y)
(Hyz : clos_refl_trans R y z) :
clos_refl_trans R x z.
| rt_step x y (H : R x y) : clos_refl_trans R x y
| rt_refl x : clos_refl_trans R x x
| rt_trans x y z
(Hxy : clos_refl_trans R x y)
(Hyz : clos_refl_trans R y z) :
clos_refl_trans R x z.
For example, the reflexive and transitive closure of the
next_nat relation coincides with the le relation.
Theorem next_nat_closure_is_le : ∀ n m,
(n ≤ m) ↔ ((clos_refl_trans next_nat) n m).
(n ≤ m) ↔ ((clos_refl_trans next_nat) n m).
Proof.
intros n m. split.
- (* -> *)
intro H. induction H.
+ (* le_n *) apply rt_refl.
+ (* le_S *)
apply rt_trans with m. apply IHle. apply rt_step.
apply nn.
- (* <- *)
intro H. induction H.
+ (* rt_step *) inversion H. apply le_S. apply le_n.
+ (* rt_refl *) apply le_n.
+ (* rt_trans *)
apply le_trans with y.
apply IHclos_refl_trans1.
apply IHclos_refl_trans2. Qed.
intros n m. split.
- (* -> *)
intro H. induction H.
+ (* le_n *) apply rt_refl.
+ (* le_S *)
apply rt_trans with m. apply IHle. apply rt_step.
apply nn.
- (* <- *)
intro H. induction H.
+ (* rt_step *) inversion H. apply le_S. apply le_n.
+ (* rt_refl *) apply le_n.
+ (* rt_trans *)
apply le_trans with y.
apply IHclos_refl_trans1.
apply IHclos_refl_trans2. Qed.
The above definition of reflexive, transitive closure is natural:
it says, explicitly, that the reflexive and transitive closure of
R is the least relation that includes R and that is closed
under rules of reflexivity and transitivity. But it turns out
that this definition is not very convenient for doing proofs,
since the "nondeterminism" of the rt_trans rule can sometimes
lead to tricky inductions. Here is a more useful definition:
Inductive clos_refl_trans_1n {A : Type}
(R : relation A) (x : A)
: A → Prop :=
| rt1n_refl : clos_refl_trans_1n R x x
| rt1n_trans (y z : A)
(Hxy : R x y) (Hrest : clos_refl_trans_1n R y z) :
clos_refl_trans_1n R x z.
(R : relation A) (x : A)
: A → Prop :=
| rt1n_refl : clos_refl_trans_1n R x x
| rt1n_trans (y z : A)
(Hxy : R x y) (Hrest : clos_refl_trans_1n R y z) :
clos_refl_trans_1n R x z.
Our new definition of reflexive, transitive closure "bundles"
the rt_step and rt_trans rules into the single rule step.
The left-hand premise of this step is a single use of R,
leading to a much simpler induction principle.
Before we go on, we should check that the two definitions do
indeed define the same relation...
First, we prove two lemmas showing that clos_refl_trans_1n mimics
the behavior of the two "missing" clos_refl_trans
constructors.
Lemma rsc_trans :
∀ (X:Type) (R: relation X) (x y z : X),
clos_refl_trans_1n R x y →
clos_refl_trans_1n R y z →
clos_refl_trans_1n R x z.
Proof.
(* FILL IN HERE *) Admitted.
☐
∀ (X:Type) (R: relation X) (x y z : X),
clos_refl_trans_1n R x y →
clos_refl_trans_1n R y z →
clos_refl_trans_1n R x z.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, optional (rtc_rsc_coincide)
Theorem rtc_rsc_coincide :
∀ (X:Type) (R: relation X) (x y : X),
clos_refl_trans R x y ↔ clos_refl_trans_1n R x y.
Proof.
(* FILL IN HERE *) Admitted.
☐
∀ (X:Type) (R: relation X) (x y : X),
clos_refl_trans R x y ↔ clos_refl_trans_1n R x y.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* 2024-08-25 14:45 *)