Library zoo.common.relations

From stdpp Require Export
  relations.

From zoo Require Import
  prelude.
From zoo Require Import
  options.

Section relation.
  Context {A} (R : relation A).

  Lemma transitive_tc `{!Transitive R} x1 x2 :
    tc R x1 x2 ↔
    R x1 x2.
  Lemma preorder_rtc `{!Reflexive R} `{!Transitive R} x1 x2 :
    rtc R x1 x2 ↔
    R x1 x2.

  #[global] Instance transitive_tc_antisymm `{!Transitive R} `{!AntiSymm R' R} :
    AntiSymm R' (tc R).
  #[global] Instance preorder_rtc_antisymm `{!Reflexive R} `{!Transitive R} `{!AntiSymm R' R} :
    AntiSymm R' (rtc R).

  Lemma rtc_equivalence_antisymm R' `{!Equivalence R'} `{!AntiSymm (=) (rtc R)} :
    AntiSymm R' (rtc R).
End relation.

Class Initial {A} (R : relation A) :=
  { initial : A
  ; initial_lb a :
      R initial a
  }.
#[global] Arguments Build_Initial {_ _} _ _ : assert.
#[global] Arguments initial {_ _ _} : assert.

#[global] Program Instance rtc_initial `(R : relation A) `{!Initial R} : Initial (rtc R) :=
  {| initial := initial |}.