Library EVMOpSem.Lem.lem_relation

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.

Require Import coqharness.

Open Scope nat_scope.
Open Scope string_scope.

Require Import lem_bool.
Require Export lem_bool.
Require Import lem_basic_classes.
Require Export lem_basic_classes.
Require Import lem_tuple.
Require Export lem_tuple.
Require Import lem_set.
Require Export lem_set.
Require Import lem_num.
Require Export lem_num.


Definition rel_pred (a: Type) (b: Type) : Type := a -> b -> bool .
Definition rel_pred_default {a: Type} {b: Type} : rel_pred a b := (fun (x151 : a) => (fun (x152 : b) => bool_default)).
Definition rel_set (a: Type) (b: Type) : Type := set ((a * b) % type).
Definition rel_set_default {a: Type} {b: Type} : rel_set a b := DAEMON.


Definition rel (a: Type) (b: Type) : Type := rel_set a b.
Definition rel_default {a: Type} {b: Type} : rel a b := DAEMON.



Definition relEq {a b : Type} `{SetType a} `{SetType b} (r1 : set ((a*b) % type)) (r2 : set ((a*b) % type)) : bool := ( (set_equal_by (pairCompare setElemCompare setElemCompare)r1 r2)).


Definition relToPred {a b : Type} `{SetType a} `{SetType b} `{Eq a} `{Eq b} (r : set ((a*b) % type)) : a -> b -> bool := (fun (x : a) (y : b) => (set_member_by (pairCompare setElemCompare setElemCompare) (x, y) r)).
Definition relFromPred {a b : Type} `{SetType a} `{SetType b} `{Eq a} `{Eq b} (xs : set a) (ys : set b) (p : a -> b -> bool ) : set ((a*b) % type):= lem_set.filter (
  fun (p0 : (a*b) % type) => match ( (p0) ) with ( (x, y)) => p x y end) (cross xs ys).




Definition relIdOn {a : Type} `{SetType a} `{Eq a} (s : set a) : set ((a*a) % type):= relFromPred s s (fun x y => x = y).




Definition relComp {a b c : Type} `{SetType a} `{SetType b} `{SetType c} `{Eq a} `{Eq b} (r1 : set ((a*b) % type)) (r2 : set ((b*c) % type)) : set ((a*c) % type):= let x2 :=
  [] in set_fold
   (fun (p : (a*b) % type) (x2 : set ((a*c) % type)) =>
      match ( (p ,x2) ) with ((e1, e2) , x2) =>
        set_fold
          (fun (p : (b*c) % type) (x2 : set ((a*c) % type)) =>
             match ( (p ,x2) ) with ((e2', e3) , x2) =>
               if e2 = e2' then set_add (e1, e3) x2 else x2 end) (r2)
        x2 end) (r1) x2.

Definition relRestrict {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : set ((a*a) % type):= (let x2 :=
  [] in set_fold
   (fun (a1 : a) (x2 : set ((a*a) % type)) =>
      set_fold
        (fun (b : a) (x2 : set ((a*a) % type)) =>
           if (set_member_by (pairCompare setElemCompare setElemCompare)
                 (a1, b) r) then set_add (a1, b) x2 else x2) s x2) s
 x2).

Definition relConverse {a b : Type} `{SetType a} `{SetType b} (r : set ((a*b) % type)) : set ((b*a) % type):= (lem_set.map (
  fun (p : (a*b) % type) => match ( (p) ) with ( (v1, v2)) => (v2, v1) end) (r)).

Definition relDomain {a b : Type} `{SetType a} `{SetType b} (r : set ((a*b) % type)) : set a:= lem_set.map (fun (x : (a*b) % type) => (@ fst _ _) x) (r).

Definition relRange {a b : Type} `{SetType a} `{SetType b} (r : set ((a*b) % type)) : set b:= lem_set.map (fun (x : (a*b) % type) => (@ snd _ _) x) (r).


Definition relOver {a : Type} `{SetType a} (r : set ((a*a) % type)) (s : set a) : bool := ( (set_subset_by setElemCompare(( (set_union_by setElemCompare(relDomain r) (relRange r)))) s)).

Definition relApply {a b : Type} `{SetType a} `{SetType b} `{Eq a} (r : set ((a*b) % type)) (s : set a) : set b:= let x2 :=
  [] in set_fold
   (fun (p : (a*b) % type) (x2 : set b) =>
      match ( (p ,x2) ) with ((x, y) , x2) =>
        if (set_member_by setElemCompare x s) then set_add y x2 else x2 end)
   (r) x2.


Definition isReflexiveOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := (set_for_all
  (fun (e : a) =>
     (set_member_by (pairCompare setElemCompare setElemCompare) (e, e) r)) s).


Definition isIrreflexiveOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := (set_for_all
  (fun (e : a) =>
     negb
       ( (set_member_by (pairCompare setElemCompare setElemCompare) (e, e) r))) s).

Definition isIrreflexive {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) : bool := (set_for_all
  (fun (p : (a*a) % type) =>
     match ( (p) ) with ( (e1, e2)) => negb (e1 = e2) end) (r)).

Definition isSymmetricOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := (set_for_all
  (fun (e1 : a) =>
     set_for_all
       (fun (e2 : a) =>
          ((negb
              ( (set_member_by (pairCompare setElemCompare setElemCompare)
                   (e1, e2) r))) ||
           ( (set_member_by (pairCompare setElemCompare setElemCompare)
                (e2, e1) r)))) s) s).

Definition isSymmetric {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) : bool := (set_for_all
  (fun (p : (a*a) % type) =>
     match ( (p) ) with ( (e1, e2)) =>
       (set_member_by (pairCompare setElemCompare setElemCompare) (e2, e1) r)
     end) r).

Definition isAntisymmetricOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := (set_for_all
  (fun (e1 : a) =>
     set_for_all
       (fun (e2 : a) =>
          ((negb
              ( (set_member_by (pairCompare setElemCompare setElemCompare)
                   (e1, e2) r))) ||
           ((negb
               ( (set_member_by (pairCompare setElemCompare setElemCompare)
                    (e2, e1) r))) || (e1 = e2)))) s) s).

Definition isAntisymmetric {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) : bool := (set_for_all
  (fun (p : (a*a) % type) =>
     match ( (p) ) with ( (e1, e2)) =>
       ((negb
           ( (set_member_by (pairCompare setElemCompare setElemCompare)
                (e2, e1) r))) || (e1 = e2)) end) r).

Definition isTransitiveOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := (set_for_all
  (fun (e1 : a) =>
     set_for_all
       (fun (e2 : a) =>
          set_for_all
            (fun (e3 : a) =>
               ((negb
                   ( (set_member_by
                        (pairCompare setElemCompare setElemCompare) (e1, e2)
                        r))) ||
                ((negb
                    ( (set_member_by
                         (pairCompare setElemCompare setElemCompare)
                       (e2, e3) r))) ||
                 ( (set_member_by (pairCompare setElemCompare setElemCompare)
                      (e1, e3) r))))) s) s) s).

Definition isTransitive {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) : bool := (set_for_all
  (fun (p : (a*a) % type) =>
     match ( (p) ) with ( (e1, e2)) =>
       set_for_all
         (fun (e3 : a) =>
            (set_member_by (pairCompare setElemCompare setElemCompare)
               (e1, e3) r)) (relApply r [e2]) end) r).

Definition isTotalOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := (set_for_all
  (fun (e1 : a) =>
     set_for_all
       (fun (e2 : a) =>
          ( (set_member_by (pairCompare setElemCompare setElemCompare)
               (e1, e2) r)) ||
          ( (set_member_by (pairCompare setElemCompare setElemCompare)
               (e2, e1) r))) s) s).


Definition isTrichotomousOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := (set_for_all
  (fun (e1 : a) =>
     set_for_all
       (fun (e2 : a) =>
          ( (set_member_by (pairCompare setElemCompare setElemCompare)
               (e1, e2) r)) ||
          ((e1 = e2) ||
           ( (set_member_by (pairCompare setElemCompare setElemCompare)
                (e2, e1) r)))) s) s).


Definition isSingleValued {a b : Type} `{SetType a} `{SetType b} `{Eq a} `{Eq b} (r : set ((a*b) % type)) : bool := (set_for_all
  (fun (p : (a*b) % type) =>
     match ( (p) ) with ( (e1, e2a)) =>
       set_for_all (fun (e2b : b) => e2a = e2b) (relApply r [e1]) end) r).

Definition isEquivalenceOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := isReflexiveOn r s && (isSymmetricOn r s && isTransitiveOn r s).



Definition isPreorderOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := isReflexiveOn r s && isTransitiveOn r s.


Definition isPartialOrderOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := isReflexiveOn r s && (isTransitiveOn r s && isAntisymmetricOn r s).

Definition isStrictPartialOrderOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := isIrreflexiveOn r s && isTransitiveOn r s.

Definition isStrictPartialOrder {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) : bool := isIrreflexive r && isTransitive r.


Definition isTotalOrderOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := isPartialOrderOn r s && isTotalOn r s.

Definition isStrictTotalOrderOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : bool := isStrictPartialOrderOn r s && isTrichotomousOn r s.






Definition transitiveClosureAdd {a : Type} `{SetType a} `{Eq a} (x : a) (y : a) (r : set ((a*a) % type)) : set ((a*a) % type):=
  (( (set_union_by (pairCompare setElemCompare setElemCompare)(((set_add (x,y) (r)))) ((( (set_union_by (pairCompare setElemCompare setElemCompare)((let x2 :=
  [] in set_fold
   (fun (z : a) (x2 : set ((a*a) % type)) =>
      if (set_member_by (pairCompare setElemCompare setElemCompare) (y, z) r) then
        set_add (x, z) x2 else x2) (relRange r) x2)) ((let x2 := [] in set_fold
   (fun (z : a) (x2 : set ((a*a) % type)) =>
      if (set_member_by (pairCompare setElemCompare setElemCompare) (z, x) r) then
        set_add (z, y) x2 else x2) (relDomain r) x2))))))))).

Definition reflexiveTransitiveClosureOn {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) (s : set a) : set ((a*a) % type):= (set_tc (fun x y => x = y) (( (set_union_by (pairCompare setElemCompare setElemCompare)(r) ((relIdOn s)))))).


Definition withoutTransitiveEdges {a : Type} `{SetType a} `{Eq a} (r : set ((a*a) % type)) : set ((a*a) % type):=
  let tc := (set_tc (fun x y => x = y) r) in
  let x2 := [] in set_fold
   (fun (p : (a*a) % type) (x2 : set ((a*a) % type)) =>
      match ( (p ,x2) ) with ((a1, c) , x2) =>
        if set_for_all
             (fun (b : a) =>
                ((negb ((a1 <> b) && (b <> c))) ||
                 negb
                   ( (set_member_by
                        (pairCompare setElemCompare setElemCompare) (a1, b)
                        tc) &&
                     (set_member_by
                        (pairCompare setElemCompare setElemCompare) (b, c)
                      tc)))) (relRange r) then set_add (a1, c) x2 else
        x2 end) r x2.