Library ATBR.Model_Relations

Require Import Common.
Require Import Classes.
Require Converse.

Section Def.

  Definition rel A B := A -> B -> Prop.
  Definition rel_equal A B (R S: rel A B) := forall x y, R x y <-> S x y.
  Definition rel_union A B (R S: rel A B): rel A B := fun x y => R x y \/ S x y.
  Definition rel_inter A B (R S: rel A B): rel A B := fun x y => R x y /\ S x y.
  Definition rel_comp A B C (R: rel A B) (S: rel B C): rel A C := fun x z => exists2 y, R x y & S y z.
  Definition rel_conv A B (R: rel A B): rel B A := fun x y => R y x.
  Definition rel_id A: rel A A := @eq A.
  Definition rel_empty A B: rel A B := fun x y => False.
  Definition rel_top A B: rel A B := fun x y => True.
  Fixpoint rel_iter A (R: rel A A) n: rel A A :=
    match n with
      | 0 => @rel_id A
      | S n => rel_comp (rel_iter R n) R
    end.
  Definition rel_star A (R: rel A A): rel A A := fun x y => exists n, rel_iter R n x y.

  Program Instance rel_Graph: Graph := {
    T := Type;
    X := rel;
    equal := rel_equal
  }.

  Instance rel_SemiLattice_Ops: SemiLattice_Ops rel_Graph := {
    plus := rel_union;
    zero := rel_empty
  }.

  Instance rel_Monoid_Ops: Monoid_Ops rel_Graph := {
    dot := rel_comp;
    one := rel_id
  }.

  Instance rel_Star_Op: Star_Op rel_Graph := {
    star := rel_star
  }.

  Instance rel_Converse_Op: Converse_Op rel_Graph := {
    conv := rel_conv
  }.

  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 A B: forall (a b: @X (rel_Graph) A B), 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 :=
    change rel_equal with (@equal rel_Graph);
      change rel_id with (@one rel_Graph rel_Monoid_Ops);
        change rel_comp with (@dot rel_Graph rel_Monoid_Ops);
          change rel_union with (@plus rel_Graph rel_SemiLattice_Ops);
            change rel_empty with (@zero rel_Graph rel_SemiLattice_Ops);
              change rel_star with (@star rel_Graph rel_Star_Op).

End Load.