logical-foundations/Rel.v

398 lines
13 KiB
Coq
Raw Permalink Normal View History

2020-06-04 02:46:06 +00:00
(** * Rel: Properties of Relations *)
(** This short (and optional) chapter develops some basic definitions
and a few theorems about binary relations in Coq. The key
definitions are repeated where they are actually used (in the
[Smallstep] chapter of _Programming Language Foundations_),
so readers who are already comfortable with these ideas can safely
skim or skip this chapter. However, relations are also a good
source of exercises for developing facility with Coq's basic
reasoning facilities, so it may be useful to look at this material
just after the [IndProp] chapter. *)
Set Warnings "-notation-overridden,-parsing".
From LF Require Export IndProp.
(* ################################################################# *)
(** * Relations *)
(** A binary _relation_ on a set [X] is a family of propositions
parameterized by two elements of [X] -- i.e., a proposition about
pairs of elements of [X]. *)
Definition relation (X: Type) := X -> X -> Prop.
(** 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 between some set and itself, whereas the English word
"relation" can refer either to the specific Coq 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.
(** (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 *)
(** As anyone knows who has taken an undergraduate discrete math
course, there is a lot to be said about relations in general,
including ways of classifying relations (as reflexive, transitive,
etc.), theorems that can be proved generically about certain sorts
of relations, constructions that build one relation from another,
etc. For example... *)
(* ----------------------------------------------------------------- *)
(** *** Partial Functions *)
(** A relation [R] on a set [X] is a _partial function_ if, for every
[x], there is at most one [y] such that [R x y] -- i.e., [R x y1]
and [R x y2] together imply [y1 = y2]. *)
Definition partial_function {X: Type} (R: relation X) :=
forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
(** For example, the [next_nat] relation defined earlier 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. (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. {
apply Hc with (x := 0).
- apply le_n.
- apply le_S. apply le_n. }
discriminate Nonsense. Qed.
(** **** Exercise: 2 stars, standard, optional (total_relation_not_partial)
Show that the [total_relation] defined in (an exercise in)
[IndProp] is not a partial function. *)
(* FILL IN HERE
[] *)
(** **** Exercise: 2 stars, standard, optional (empty_relation_partial)
Show that the [empty_relation] defined in (an exercise in)
[IndProp] is a partial function. *)
(* FILL IN HERE
[] *)
(* ----------------------------------------------------------------- *)
(** *** Reflexive Relations *)
(** 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) :=
forall a : X, R a a.
Theorem le_reflexive :
reflexive le.
Proof.
unfold reflexive. intros n. apply le_n. Qed.
(* ----------------------------------------------------------------- *)
(** *** Transitive Relations *)
(** 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) :=
forall 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.
Theorem lt_trans:
transitive lt.
Proof.
unfold lt. unfold transitive.
intros n m o Hnm Hmo.
apply le_S in Hnm.
apply le_trans with (a := (S n)) (b := (S m)) (c := o).
apply Hnm.
apply Hmo. Qed.
(** **** 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.
(** [] *)
(** **** Exercise: 2 stars, standard, optional (lt_trans'')
Prove the same thing again by induction on [o]. *)
Theorem lt_trans'' :
transitive lt.
Proof.
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)... *)
Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
Proof.
intros n m H. apply le_trans with (S n).
- apply le_S. apply le_n.
- apply H.
Qed.
(** **** Exercise: 1 star, standard, optional (le_S_n) *)
Theorem le_S_n : forall n m,
(S n <= S m) -> (n <= m).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard, optional (le_Sn_n_inf)
Provide an informal proof of the following theorem:
Theorem: For every [n], [~ (S n <= n)]
A formal proof of this is an optional exercise below, but try
writing an informal proof without doing the formal proof first.
Proof: *)
(* FILL IN HERE
[] *)
(** **** Exercise: 1 star, standard, optional (le_Sn_n) *)
Theorem le_Sn_n : forall n,
~ (S n <= n).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** 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, let's look at a few other common ones... *)
(* ----------------------------------------------------------------- *)
(** *** Symmetric and Antisymmetric Relations *)
(** A relation [R] is _symmetric_ if [R a b] implies [R b a]. *)
Definition symmetric {X: Type} (R: relation X) :=
forall a b : X, (R a b) -> (R b a).
(** **** Exercise: 2 stars, standard, optional (le_not_symmetric) *)
Theorem le_not_symmetric :
~ (symmetric le).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** 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) :=
forall a b : X, (R a b) -> (R b a) -> a = b.
(** **** Exercise: 2 stars, standard, optional (le_antisymmetric) *)
Theorem le_antisymmetric :
antisymmetric le.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard, optional (le_step) *)
Theorem le_step : forall n m p,
n < m ->
m <= S p ->
n <= p.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(* ----------------------------------------------------------------- *)
(** *** Equivalence Relations *)
(** 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).
(* ----------------------------------------------------------------- *)
(** *** Partial Orders and Preorders *)
(** 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).
Theorem le_order :
order le.
Proof.
unfold order. split.
- (* refl *) apply le_reflexive.
- split.
+ (* antisym *) apply le_antisymmetric.
+ (* transitive. *) apply le_trans. Qed.
(* ################################################################# *)
(** * Reflexive, Transitive Closure *)
(** The _reflexive, transitive closure_ of a relation [R] is the
smallest relation that contains [R] and that is both reflexive and
transitive. Formally, it is defined like this in the Relations
module of the Coq standard library: *)
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.
(** For example, the reflexive and transitive closure of the
[next_nat] relation coincides with the [le] relation. *)
Theorem next_nat_closure_is_le : forall 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.
(** 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.
(** 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_R : forall (X:Type) (R:relation X) (x y : X),
R x y -> clos_refl_trans_1n R x y.
Proof.
intros X R x y H.
apply rt1n_trans with y. apply H. apply rt1n_refl. Qed.
(** **** Exercise: 2 stars, standard, optional (rsc_trans) *)
Lemma rsc_trans :
forall (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.
(** [] *)
(** Then we use these facts to prove that the two definitions of
reflexive, transitive closure do indeed define the same
relation. *)
(** **** Exercise: 3 stars, standard, optional (rtc_rsc_coincide) *)
Theorem rtc_rsc_coincide :
forall (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.
(** [] *)
(* Wed Jan 9 12:02:46 EST 2019 *)