Software Foundations: Properties of Relations

Rel.v

Require Import Setoid.

Inductive le : nat -> nat -> Prop :=
| le_n : forall {n}, le n n
| le_S : forall {n m}, le n m -> le n (S m).

Notation "n <= m" := (le n m).

Definition lt n m := le (S n) m.

Notation "n < m" := (lt n m).

Definition relation A := A -> A -> Prop.

Definition partial_function {A} (R : relation A) :=
  forall x y y', R x y -> R x y' -> y = y'.

Inductive suc (n : nat) : nat -> Prop :=
| s : suc n (S n).

Theorem suc_partial_function : partial_function suc.
Proof.
  unfold partial_function.
  intros x y y' [] [].
  reflexivity.
Qed.

Theorem not_le_partial_function : ~partial_function le.
Proof.
  unfold not.
  intros.
  specialize (H 0 0 1 le_n (le_S le_n)).
  discriminate.
Qed.

Inductive total_relation : nat -> nat -> Prop :=
| total : forall {n m}, total_relation n m.

Inductive empty_relation : nat -> nat -> Prop :=.

Theorem not_total_relation_partial_function : ~partial_function total_relation.
Proof.
  unfold not.
  intros.
  specialize (H 0 0 1 total total).
  discriminate.
Qed.

Theorem empty_relation_partial_function : partial_function empty_relation.
Proof.
  unfold partial_function.
  intros.
  inversion H.
Qed.

Theorem eq_partial_function : forall {A}, partial_function (@eq A).
Proof.
  unfold partial_function.
  intros A x y y' [] [].
  reflexivity.
Qed.

Definition reflexive {A} (R : relation A) :=
  forall x, R x x.

Theorem le_reflexive : reflexive le.
Proof.
  unfold reflexive.
  intros.
  apply le_n.
Qed.

Definition transitive {A} (R : relation A) :=
  forall x y z, R x y -> R y z -> R x z.

Theorem le_transitive : transitive le.
Proof.
  unfold transitive.
  intros x y z Hxy Hyz.
  induction Hyz.
  - assumption.
  - apply le_S.
    apply IHHyz.
    assumption.
Qed.

Theorem lt_transitive : transitive lt.
Proof.
  unfold lt, transitive.
  intros x y z Hxy Hyz.
  apply le_S in Hxy.
  apply le_transitive with (x := S x) (y := S y); assumption.
Qed.

Theorem lt_transitive' : transitive lt.
Proof.
  unfold lt, transitive.
  intros x y z Hxy Hyz.
  apply le_S in Hxy.
  induction Hyz.
  - assumption.
  - apply le_S.
    apply IHHyz.
    assumption.
Qed.

Theorem lt_transitive'' : transitive lt.
Proof.
  unfold lt, transitive.
  intros x y z Hxy Hyz.
  induction z.
  - inversion Hyz.
  - apply le_S.
    inversion Hyz.
    + subst.
      assumption.
    + apply IHz.
      assumption.
Qed.

Theorem le_S_r : forall n m,
  S n <= m -> n <= m.
Proof.
  intros.
  apply le_transitive with (S n).
  - apply le_S, le_n.
  - assumption.
Qed.

Theorem le_S_S : forall n m,
  S n <= S m <-> n <= m.
Proof.
  split; intros.
  - inversion H as [| n' m' H'].
    + apply le_n.
    + apply le_S_r in H'.
      assumption.
  - induction H.
    + apply le_n.
    + apply le_S.
      assumption.
Qed.

Theorem le_Sn_n : forall n,
  ~ S n <= n.
Proof.
  unfold not.
  intros.
  induction n.
  - inversion H.
  - rewrite le_S_S in H.
    apply IHn.
    assumption.
Qed.

Definition symmetric {A} (R : relation A) :=
  forall x y, R x y -> R y x.

Theorem not_le_symmetric : ~symmetric le.
Proof.
  unfold not, symmetric.
  intros.
  specialize (H 0 1 (le_S le_n)).
  inversion H.
Qed.

Definition antisymmetric {A} (R : relation A) :=
  forall x y, R x y -> R y x -> x = y.

Tactic Notation "inversion'" hyp(H) :=
  inversion H; simpl; trivial.

Theorem le_antisymmetric : antisymmetric le.
Proof.
  unfold antisymmetric.
  induction x; destruct y; intros H H'.
  - reflexivity.
  - inversion H'.
  - inversion H.
  - rewrite le_S_S in H.
    rewrite le_S_S in H'.
    rewrite (IHx y); try assumption.
    reflexivity.
Qed.

Theorem le_step : forall n m p,
  n < m -> m <= S p -> n <= p.
Proof.
  unfold lt.
  intros n m p Hnm Hmp.
  apply le_S_S.
  apply (le_transitive _ _ _ Hnm Hmp).
Qed.

Definition equivalence {A} (R : relation A) :=
  reflexive R /\ symmetric R /\ transitive R.

Definition order {A} (R : relation A) :=
  reflexive R /\ antisymmetric R /\ transitive R.

Definition preorder {A} (R : relation A) :=
  reflexive R /\ transitive R.

Theorem le_order : order le.
Proof.
  split; try split.
  - apply le_reflexive.
  - apply le_antisymmetric.
  - apply le_transitive.
Qed.

Inductive clos_refl_trans' {A} (R : relation A) : relation A :=
| rt_step : forall x y, R x y -> clos_refl_trans' R x y
| rt_refl : forall x, clos_refl_trans' R x x
| rt_trans : forall x y z, clos_refl_trans' R x y -> clos_refl_trans' R y z -> clos_refl_trans' R x z.

Theorem suc_closure_le' : forall n m,
  n <= m <-> clos_refl_trans' suc n m.
Proof.
  split; intros.
  - induction H.
    + apply rt_refl.
    + apply rt_trans with (y := m); trivial.
      apply rt_step.
      apply s.
  - induction H.
    + destruct H.
      apply le_S, le_n.
    + apply le_n.
    + apply le_transitive with (y := y); trivial.
Qed.

Inductive clos_refl_trans {A} (R : relation A) (x : A) : A -> Prop :=
| refl : clos_refl_trans R x x
| trans y z (Hxy : R x y) (Hyz : clos_refl_trans R y z) : clos_refl_trans R x z.

Lemma rsc_R : forall A (R : relation A) x y,
  R x y -> clos_refl_trans R x y.
Proof.
  intros.
  apply trans with (y0 := y).
  - assumption.
  - apply refl.
Qed.

Lemma rsc_trans : forall A (R : relation A) x y z,
  clos_refl_trans R x y -> clos_refl_trans R y z -> clos_refl_trans R x z.
Proof.
  intros A R x y z Hxy Hyz.
  induction Hxy.
  - assumption.
  - apply trans with (y0 := y).
    + assumption.
    + apply IHHxy.
      assumption.
Qed.

Theorem rtc_rsc_coincide : forall A (R : relation A) x y,
  clos_refl_trans' R x y <-> clos_refl_trans R x y.
Proof.
  split; intros.
  - induction H.
    + apply rsc_R.
      assumption.
    + apply refl.
    + apply rsc_trans with (y := y); trivial.
  - induction H.
    + apply rt_refl.
    + apply rt_trans with (y0 := y).
      * apply rt_step.
        assumption.
      * assumption.
Qed.

Theorem rsc_le_le : forall n m,
  n <= m <-> clos_refl_trans le n m.
Proof.
  split; intros.
  - destruct H.
    + apply refl.
    + apply rsc_R.
      apply le_S.
      assumption.
  - induction H.
    + apply le_n.
    + apply le_transitive with (y := y); assumption.
Qed.