Library zoo.common.relations

Require Export stdpp.relations.

Require Import zoo.prelude.
Require Import zoo.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
  |}.