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.