Library EVMOpSem.Lem.lem_set

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_maybe.
Require Export lem_maybe.
Require Import lem_function.
Require Export lem_function.
Require Import lem_num.
Require Export lem_num.
Require Import lem_list.
Require Export lem_list.
Require Import lem_set_helpers.
Require Export lem_set_helpers.

Require Import Coq.Lists.List.
Require Export Coq.Lists.List.




Instance x148_Eq{a: Type} `{SetType a}: Eq (set a):= {
   isEqual := (set_equal_by setElemCompare);
   isInequal s1 s2 := negb ((set_equal_by setElemCompare s1 s2))
}.

















Definition filter {a : Type} `{SetType a} (P : a -> bool ) (s : set a) : set a:= let x2 :=
  [] in set_fold (fun (e : a) (x2 : set a) => if P e then set_add e x2 else x2) s x2.

Definition partition0 {a : Type} `{SetType a} (P : a -> bool ) (s : set a) : (set a*set a) % type:= (filter P s, filter (fun (e : a) => negb (P e)) s).

Definition split {a : Type} `{SetType a} `{Ord a} (p : a) (s : set a) : (set a*set a) % type:= (filter (isGreater p) s, filter (isLess p) s).

Definition splitMember {a : Type} `{SetType a} `{Ord a} (p : a) (s : set a) : (set a*bool *set a) % type:= (filter (isLess p) s, (set_member_by setElemCompare p s), filter (isGreater p) s).








Definition bigunion {a : Type} `{SetType a} (bs : set (set a)) : set a:= let x2 :=
  [] in set_fold
   (fun (s : set a) (x2 : set a) =>
      set_fold
        (fun (x : a) (x2 : set a) => if true then set_add x x2 else x2)
      s x2) bs x2.

Definition bigintersection {a : Type} `{SetType a} (bs : set (set a)) : set a:= let x2 :=
  [] in set_fold
   (fun (x : a) (x2 : set a) =>
      if set_for_all (fun (s : set a) => (set_member_by setElemCompare x s))
           bs then set_add x x2 else x2) (bigunion bs) x2.




Definition map {a b : Type} `{SetType a} `{SetType b} (f : a -> b) (s : set a) : set b:= let x2 :=
  [] in set_fold (fun (e : a) (x2 : set b) => if true then set_add (f e) x2 else x2)
   s x2.




Definition setMapMaybe {a b : Type} `{SetType a} `{SetType b} (f : a -> option b ) (s : set a) : set b:=
  bigunion (map (fun (x : a) => match ( f x) with
                        | Some y => set_singleton y
                        | None => set_empty
                        end) s).

Definition removeMaybe {a : Type} `{SetType a} (s : set (option a )) : set a:= setMapMaybe (fun (x : option a ) => x) s.








Definition cross {a b : Type} `{SetType a} `{SetType b} (s1 : set a) (s2 : set b) : set ((a*b) % type):= let x2 :=
  [] in set_fold
   (fun (e1 : a) (x2 : set ((a*b) % type)) =>
      set_fold
        (fun (e2 : b) (x2 : set ((a*b) % type)) =>
           if true then set_add (e1, e2) x2 else x2) s2 x2) s1 x2.


Program Fixpoint leastFixedPoint {a : Type} `{SetType a} (bound : nat ) (f : set a -> set a) (x : set a) : set a:=
  match ( bound) with
  | 0%nat => x
  |S (bound') => let fx := f x in
                  if (set_subset_by setElemCompare fx x) then x
                  else leastFixedPoint bound' f ( (set_union_by setElemCompare fx x))
  end.