RelProperties of Relations
(* $Date: 2013-04-01 09:15:45 -0400 (Mon, 01 Apr 2013) $ *)
Require Export SfLib.
A (binary) relation on a set X is a proposition parameterized by two
Xs — i.e., it is a logical assertion involving two values from
the set X.
Definition relation (X: Type) := X→X→Prop.
An example relation on nat is le, the less-that-or-equal-to
relation which we usually write like this 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.
Basic Properties of Relations
Definition partial_function {X: Type} (R: relation X) :=
∀x y1 y2 : X, R x y1 → R x y2 → y1 = y2.
For example, the next_nat relation defined in Logic.v is a
partial function.
(* Print next_nat.
(* ====>
Inductive next_nat (n : nat) : nat -> Prop :=
nn : next_nat n (S n)
*)
Check next_nat : relation nat.
Theorem next_nat_partial_function :
partial_function next_nat.
Proof.
unfold partial_function.
intros x y1 y2 H1 H2.
inversion H1. inversion H2.
reflexivity. Qed. *)
However, the ≤ relation on numbers is not a partial function.
This can be shown by contradiction. In short: 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.
Theorem le_not_a_partial_function :
¬ (partial_function le).
Proof.
unfold not. unfold partial_function. intros Hc.
assert (0 = 1) as Nonsense.
Case "Proof of assertion".
apply Hc with (x := 0).
apply le_n.
apply le_S. apply le_n.
inversion Nonsense. Qed.
A reflexive relation on a set X is one for which every element
of X is related to itself.
Definition reflexive {X: Type} (R: relation X) :=
∀a : X, R a a.
Theorem le_reflexive :
reflexive le.
Proof.
unfold reflexive. intros n. apply le_n. Qed.
A relation R is transitive if R a c holds whenever R a b
and R b c do.
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.
Proof.
intros n m o Hnm Hmo.
induction Hmo.
Case "le_n". apply Hnm.
Case "le_S". apply le_S. apply IHHmo. Qed.
Reflexivity and transitivity are the main concepts we'll need for
later chapters, but, for a bit of additional practice working with
relations in Coq, here are a few more common ones.
A relation R is symmetric if R a b implies R b a.
Definition symmetric {X: Type} (R: relation X) :=
∀a b : X, (R a b) → (R b a).
A relation R is antisymmetric if R a b and R b a together
imply a = b — that is, if the only "cycles" in R are trivial
ones.
Definition antisymmetric {X: Type} (R: relation X) :=
∀a b : X, (R a b) → (R b a) → a = b.
A relation is an equivalence if it's reflexive, symmetric, and
transitive.
Definition equivalence {X:Type} (R: relation X) :=
(reflexive R) ∧ (symmetric R) ∧ (transitive R).
A relation is a partial order when it's reflexive,
anti-symmetric, and transitive. In the Coq standard library
it's called just "order" for short.
Definition order {X:Type} (R: relation X) :=
(reflexive R) ∧ (antisymmetric R) ∧ (transitive R).
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).
Reflexive, Transitive Closure
Inductive clos_refl_trans {A: Type} (R: relation A) : relation A :=
| rt_step : ∀x y, R x y → clos_refl_trans R x y
| rt_refl : ∀x, clos_refl_trans R x x
| rt_trans : ∀x y z,
clos_refl_trans R x y →
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).
Proof.
intros n m. split.
Case "→".
intro H. induction H.
SCase "le_n". apply rt_refl.
SCase "le_S".
apply rt_trans with m. apply IHle. apply rt_step. apply nn.
Case "←".
intro H. induction H.
SCase "rt_step". inversion H. apply le_S. apply le_n.
SCase "rt_refl". apply le_n.
SCase "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 — the "nondeterminism" of the rt_trans rule can sometimes
lead to tricky inductions.
Here is a more useful definition...
Inductive refl_step_closure {X:Type} (R: relation X) : relation X :=
| rsc_refl : ∀(x : X), refl_step_closure R x x
| rsc_step : ∀(x y z : X),
R x y →
refl_step_closure R y z →
refl_step_closure R x z.
(Note that, aside from the naming of the constructors, this
definition is the same as the multi step relation used in many
other chapters.)
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 refl_step_closure mimics
the behavior of the two "missing" clos_refl_trans
constructors.
Theorem rsc_R : ∀(X:Type) (R:relation X) (x y : X),
R x y → refl_step_closure R x y.
Proof.
intros X R x y H.
apply rsc_step with y. apply H. apply rsc_refl. Qed.
Theorem rsc_trans :
∀(X:Type) (R: relation X) (x y z : X),
refl_step_closure R x y →
refl_step_closure R y z →
refl_step_closure R x z.
Proof.
(* FILL IN HERE *) Admitted.
∀(X:Type) (R: relation X) (x y z : X),
refl_step_closure R x y →
refl_step_closure R y z →
refl_step_closure R x z.
Proof.
(* FILL IN HERE *) Admitted.
☐
Then we use these facts to prove that the two definitions of
reflexive, transitive closure do indeed define the same
relation.
Exercise: 3 stars, optional (rtc_rsc_coincide)
Theorem rtc_rsc_coincide :
∀(X:Type) (R: relation X) (x y : X),
clos_refl_trans R x y ↔ refl_step_closure R x y.
Proof.
(* FILL IN HERE *) Admitted.
∀(X:Type) (R: relation X) (x y : X),
clos_refl_trans R x y ↔ refl_step_closure R x y.
Proof.
(* FILL IN HERE *) Admitted.
☐