# Library bin_rels

Require Import UsefulTypes.

Definition bin_rel (T : Type) := TT[univ].

Definition trans_rel {T} (R : bin_rel T) :=
x y z, R x yR y zR x z.

Definition symm_rel {T} (R : bin_rel T) :=
x y, R x yR y x.

Definition refl_rel {T} (R : bin_rel T) :=
x, R x x.

defines when a binary relation is Less or Equal
Definition le_bin_rel {T:Type} (R1 R2: @bin_rel T) : [univ] :=
(a b : T), R1 a bR2 a b.

Definition eq_bin_rel {T} (R1 R2 : bin_rel T) :=
le_bin_rel R1 R2 # le_bin_rel R2 R1.

Definition is_ge_any_rel_sat {T:[univ]} (R: @bin_rel T)
(C: (@bin_rel T)->[univ]) : [univ] :=
(Rp: @bin_rel T), C Rple_bin_rel Rp R.

Definition is_greatest_rel_sat {T:[univ]} (R: @bin_rel T)
(C: (@bin_rel T)->[univ]) : [univ] :=
C R # is_ge_any_rel_sat R C.

Definition bin_rel_and {T} (R1 R2:bin_rel T ):=
fun x yR1 x y # R2 x y.

Definition indep_bin_rel {T:Type} (Rl Rr: T[univ]) : ( @bin_rel T)
:= fun x y ⇒ (Rl x # Rr y).

Lemma lift_bin_rel_if : {T:[univ]} (R : bin_rel T) (b:bool)
nl1 nl2 nr1 nr2,
R nl1 nr1
→ R nl2 nr2
→ R (if b then nl1 else nl2) (if b then nr1 else nr2).
Proof.
intros. cases_if; sp.
Qed.

Lemma lift_bin_rel_ifdp : {T:[univ]} {Pl Pr : Prop} (R : bin_rel T)
(b: (@sumbool Pl Pr))
nl1 nl2 nr1 nr2,
R nl1 nr1
→ R nl2 nr2
→ R (if b then nl1 else nl2) (if b then nr1 else nr2).
Proof.
intros. cases_if; sp.
Qed.