Library ATBR.Model_StdRelations

Require Import Common.
Require Import Classes.
Require Converse.

Require Import Relations.


Section Def.

  Context {A: Type}.

  Definition comp (R S: relation A): relation A :=
    fun i k => exists j, R i j /\ S j k.
  Definition empty: relation A := fun x y => False.

  Program Instance rel_Graph: Graph := {
    T := unit;
    X n m := relation A;
    equal n m := same_relation A
  }.

  Instance rel_SemiLattice_Ops: SemiLattice_Ops rel_Graph := {
    plus n m := union A;
    zero n m := empty
  }.

  Instance rel_Monoid_Ops: Monoid_Ops rel_Graph := {
    dot n m p := comp;
    one n := @eq A
  }.

  Instance rel_Star_Op: Star_Op rel_Graph := {
    star n := clos_refl_trans A
  }.

  Instance rel_Converse_Op: Converse_Op rel_Graph := {
    conv n m := transp A
  }.

  Transparent equal.

  Instance rel_SemiLattice: SemiLattice rel_Graph.


  Ltac destruct_ex :=
    repeat
      match goal with
        | H : ex _ |- _ => destruct H
        | H : ex2 _ _ |- _ => destruct H
        | H : ?A \/ ?B |- _ => destruct H
        | H : ?A , H' : (forall (x : ?A), _ ) |- _ =>
          specialize (H' H); intuition
      end.

  Instance rel_ConverseSemiRing: ConverseIdemSemiRing rel_Graph.

  Definition rel_IdemSemiRing: IdemSemiRing rel_Graph := Converse.CISR_ISR.

  Lemma rel_leq n m: forall (a b: @X rel_Graph n m),
    a<==b <-> forall x y, a x y -> b x y.

  Instance rel_ConverseKleeneAlgebra: ConverseKleeneAlgebra rel_Graph.

  Definition rel_KleeneAlgebra: KleeneAlgebra rel_Graph := Converse.CKA_KA.

End Def.

Module Load.


  Canonical Structure rel_Graph.

  Transparent equal plus dot one zero star.

  Ltac fold_relAlg A :=
    change (same_relation A) with (@equal (@rel_Graph A) tt tt);
    change (@eq A) with (@one (@rel_Graph A) rel_Monoid_Ops tt);
    change (@comp A) with (@dot (@rel_Graph A) rel_Monoid_Ops tt tt tt);
    change (union A) with (@plus (@rel_Graph A) rel_SemiLattice_Ops tt tt);
    change (@empty A) with (@zero (@rel_Graph A) rel_SemiLattice_Ops tt tt);
    change (clos_refl_trans A) with (@star (@rel_Graph A) rel_Star_Op tt).


End Load.