Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

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

For le: Argument scopes are [nat_scope nat_scope]
For le_n: Argument scope is [nat_scope]
For le_S: Argument scopes are [nat_scope nat_scope _]
Check le : nat -> nat -> Prop.le : nat -> nat -> Prop
     : nat -> nat -> Prop
Check le : relation nat.le : relation nat
     : 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 : nat -> nat -> Prop :=
    nn : forall n : nat, next_nat n (S n)

For next_nat: Argument scopes are [nat_scope
                nat_scope]
For nn: Argument scope is [nat_scope]

Check next_nat : relation nat.next_nat : relation nat
     : relation nat

Theorem next_nat_partial_function :
   partial_function next_nat.partial_function next_nat
Proof.partial_function next_nat
  unfold partial_function.forall x y1 y2 : nat,
next_nat x y1 -> next_nat x y2 -> y1 = y2
  intros x y1 y2 H1 H2.x, y1, y2:nat
H1:next_nat x y1
H2:next_nat x y2
y1 = y2
  inversion H1.x, y1, y2:nat
H1:next_nat x y1
H2:next_nat x y2
n:nat
H:n = x
H0:S x = y1
S x = y2 inversion H2.x, y1, y2:nat
H1:next_nat x y1
H2:next_nat x y2
n:nat
H:n = x
H0:S x = y1
n0:nat
H3:n0 = x
H4:S x = y2
S x = S x
  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).~ partial_function le
Proof.~ partial_function le
  unfold not.partial_function le -> False unfold partial_function.(forall x y1 y2 : nat, x <= y1 -> x <= y2 -> y1 = y2) ->
False intros Hc.Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
False
  assert (0 = 1) as Nonsense.Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
0 = 1
Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
Nonsense:0 = 1
False {Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
0 = 1
    apply Hc with (x := 0).Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
0 <= 0
Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
0 <= 1
    -Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
0 <= 0 apply le_n.
    -Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
0 <= 1 apply le_S.Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
0 <= 0 apply le_n. }Hc:forall x y1 y2 : nat,
x <= y1 -> x <= y2 -> y1 = y2
Nonsense:0 = 1
False
  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.reflexive le
Proof.reflexive le
  unfold reflexive.forall a : nat, a <= a intros n.n:nat
n <= 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.transitive le
Proof.transitive le
  intros n m o Hnm Hmo.n, m, o:nat
Hnm:n <= m
Hmo:m <= o
n <= o
  induction Hmo.n, m:nat
Hnm:n <= m
n <= m
n, m:nat
Hnm:n <= m
m0:nat
Hmo:m <= m0
IHHmo:n <= m0
n <= S m0
  - (* le_n *)n, m:nat
Hnm:n <= m
n <= m apply Hnm.
  - (* le_S *)n, m:nat
Hnm:n <= m
m0:nat
Hmo:m <= m0
IHHmo:n <= m0
n <= S m0 apply le_S.n, m:nat
Hnm:n <= m
m0:nat
Hmo:m <= m0
IHHmo:n <= m0
n <= m0 apply IHHmo.  Qed.

Theorem lt_trans:
  transitive lt.transitive lt
Proof.transitive lt
  unfold lt.transitive (fun n m : nat => S n <= m) unfold transitive.forall a b c : nat, S a <= b -> S b <= c -> S a <= c
  intros n m o Hnm Hmo.n, m, o:nat
Hnm:S n <= m
Hmo:S m <= o
S n <= o
  apply le_S in Hnm.n, m, o:nat
Hnm:S n <= S m
Hmo:S m <= o
S n <= o
  apply le_trans with (a := (S n)) (b := (S m)) (c := o).n, m, o:nat
Hnm:S n <= S m
Hmo:S m <= o
S n <= S m
n, m, o:nat
Hnm:S n <= S m
Hmo:S m <= o
S m <= o
  apply Hnm.n, m, o:nat
Hnm:S n <= S m
Hmo:S m <= o
S m <= o
  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.transitive lt
Proof.transitive lt
  (* Prove this by induction on evidence that [m] is less than [o]. *)
  unfold lt.transitive (fun n m : nat => S n <= m) unfold transitive.forall a b c : nat, S a <= b -> S b <= c -> S a <= c
  intros n m o Hnm Hmo.n, m, o:nat
Hnm:S n <= m
Hmo:S m <= o
S n <= o
  induction Hmo as [| m' Hm'o].n, m:nat
Hnm:S n <= m
S n <= S m
n, m:nat
Hnm:S n <= m
m':nat
Hm'o:S m <= m'
IHHm'o:S n <= m'
S n <= S m'
    (* 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.transitive lt
Proof.transitive lt
  unfold lt.transitive (fun n m : nat => S n <= m) unfold transitive.forall a b c : nat, S a <= b -> S b <= c -> S a <= c
  intros n m o Hnm Hmo.n, m, o:nat
Hnm:S n <= m
Hmo:S m <= o
S n <= o
  induction o as [| o'].n, m:nat
Hnm:S n <= m
Hmo:S m <= 0
S n <= 0
n, m, o':nat
Hnm:S n <= m
Hmo:S m <= S o'
IHo':S m <= o' -> S n <= o'
S n <= S 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.forall n m : nat, S n <= m -> n <= m
Proof.forall n m : nat, S n <= m -> n <= m
  intros n m H.n, m:nat
H:S n <= m
n <= m apply le_trans with (S n).n, m:nat
H:S n <= m
n <= S n
n, m:nat
H:S n <= m
S n <= m
  -n, m:nat
H:S n <= m
n <= S n apply le_S.n, m:nat
H:S n <= m
n <= n apply le_n.
  -n, m:nat
H:S n <= m
S n <= m apply H.
Qed.

Exercise: 1 star, standard, optional (le_S_n)

Theorem le_S_n : forall n m,
  (S n <= S m) -> (n <= m).forall n m : nat, S n <= S m -> n <= m
Proof.forall n m : nat, S n <= S m -> n <= m
  (* 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).forall n : nat, ~ S n <= n
Proof.forall n : nat, ~ S n <= n
  (* 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).~ symmetric le
Proof.~ symmetric le
  (* 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.antisymmetric le
Proof.antisymmetric le
  (* 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.forall n m p : nat, n < m -> m <= S p -> n <= p
Proof.forall n m p : nat, n < m -> m <= S p -> n <= p
  (* 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.order le
Proof.order le
  unfold order.reflexive le /\ antisymmetric le /\ transitive le split.reflexive le
antisymmetric le /\ transitive le
    - (* refl *)reflexive le apply le_reflexive.
    -antisymmetric le /\ transitive le split.antisymmetric le
transitive le
      + (* antisym *)antisymmetric le apply le_antisymmetric.
      + (* transitive. *)transitive le 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).forall n m : nat,
n <= m <-> clos_refl_trans next_nat n m
Proof.forall n m : nat,
n <= m <-> clos_refl_trans next_nat n m
  intros n m.n, m:nat
n <= m <-> clos_refl_trans next_nat n m split.n, m:nat
n <= m -> clos_refl_trans next_nat n m
n, m:nat
clos_refl_trans next_nat n m -> n <= m
  - (* -> *)n, m:nat
n <= m -> clos_refl_trans next_nat n m
    intro H.n, m:nat
H:n <= m
clos_refl_trans next_nat n m induction H.n:nat
clos_refl_trans next_nat n n
n, m:nat
H:n <= m
IHle:clos_refl_trans next_nat n m
clos_refl_trans next_nat n (S m)
    + (* le_n *)n:nat
clos_refl_trans next_nat n n apply rt_refl.
    + (* le_S *)n, m:nat
H:n <= m
IHle:clos_refl_trans next_nat n m
clos_refl_trans next_nat n (S m)
      apply rt_trans with m.n, m:nat
H:n <= m
IHle:clos_refl_trans next_nat n m
clos_refl_trans next_nat n m
n, m:nat
H:n <= m
IHle:clos_refl_trans next_nat n m
clos_refl_trans next_nat m (S m) apply IHle.n, m:nat
H:n <= m
IHle:clos_refl_trans next_nat n m
clos_refl_trans next_nat m (S m) apply rt_step.n, m:nat
H:n <= m
IHle:clos_refl_trans next_nat n m
next_nat m (S m)
      apply nn.
  - (* <- *)n, m:nat
clos_refl_trans next_nat n m -> n <= m
    intro H.n, m:nat
H:clos_refl_trans next_nat n m
n <= m induction H.x, y:nat
H:next_nat x y
x <= y
x:nat
x <= x
x, y, z:nat
H:clos_refl_trans next_nat x y
H0:clos_refl_trans next_nat y z
IHclos_refl_trans1:x <= y
IHclos_refl_trans2:y <= z
x <= z
    + (* rt_step *)x, y:nat
H:next_nat x y
x <= y inversion H.x, y:nat
H:next_nat x y
n:nat
H0:n = x
H1:S x = y
x <= S x apply le_S.x, y:nat
H:next_nat x y
n:nat
H0:n = x
H1:S x = y
x <= x apply le_n.
    + (* rt_refl *)x:nat
x <= x apply le_n.
    + (* rt_trans *)x, y, z:nat
H:clos_refl_trans next_nat x y
H0:clos_refl_trans next_nat y z
IHclos_refl_trans1:x <= y
IHclos_refl_trans2:y <= z
x <= z
      apply le_trans with y.x, y, z:nat
H:clos_refl_trans next_nat x y
H0:clos_refl_trans next_nat y z
IHclos_refl_trans1:x <= y
IHclos_refl_trans2:y <= z
x <= y
x, y, z:nat
H:clos_refl_trans next_nat x y
H0:clos_refl_trans next_nat y z
IHclos_refl_trans1:x <= y
IHclos_refl_trans2:y <= z
y <= z
      apply IHclos_refl_trans1.x, y, z:nat
H:clos_refl_trans next_nat x y
H0:clos_refl_trans next_nat y z
IHclos_refl_trans1:x <= y
IHclos_refl_trans2:y <= z
y <= z
      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.forall (X : Type) (R : relation X) (x y : X),
R x y -> clos_refl_trans_1n R x y
Proof.forall (X : Type) (R : relation X) (x y : X),
R x y -> clos_refl_trans_1n R x y
  intros X R x y H.X:Type
R:relation X
x, y:X
H:R x y
clos_refl_trans_1n R x y
  apply rt1n_trans with y.X:Type
R:relation X
x, y:X
H:R x y
R x y
X:Type
R:relation X
x, y:X
H:R x y
clos_refl_trans_1n R y y apply H.X:Type
R:relation X
x, y:X
H:R x y
clos_refl_trans_1n R y y 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.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.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
  (* 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.forall (X : Type) (R : relation X) (x y : X),
clos_refl_trans R x y <-> clos_refl_trans_1n R x y
Proof.forall (X : Type) (R : relation X) (x y : X),
clos_refl_trans R x y <-> clos_refl_trans_1n R x y
  (* FILL IN HERE *) Admitted.

☐

(* Wed Jan 9 12:02:46 EST 2019 *)