include "basics/types.ma".
include "basics/lists/list.ma".
include "arithmetics/nat.ma".
include "ASM/Util.ma".

axiom set: Type[0] → Type[0].

inductive set (elt_type: Type[0]): Type[0] ≝
  | empty: set elt_type
  | node : nat → set elt_type → elt_type → set elt_type → set elt_type.

axiom set_empty: ∀elt_type. set elt_type.

axiom set_size: ∀elt_type. set elt_type → nat.
axiom set_to_list: ∀elt_type. set elt_type → list elt_type.
axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type.
axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type.
axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool.
axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool.
axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool.
axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type.
axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a.
axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type  → a → a.
axiom set_equal: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
  set elt_type → set elt_type → bool.

(* XXX: define in terms of primitives *)
axiom set_diff: ∀elt_type: Type[0]. set elt_type → set elt_type → set elt_type.

definition set_is_empty ≝
  λelt_type: Type[0].
  λset: set elt_type.
    eq_nat (set_size elt_type set) 0.

definition set_singleton ≝
  λelt_type: Type[0].
  λelt     : elt_type.
    set_insert elt_type elt (set_empty elt_type).

definition set_from_list ≝
  λelt_type: Type[0].
  λthe_list: list elt_type.
    foldr … (set_insert elt_type) (set_empty elt_type) the_list.

definition set_split ≝
  λelt_type: Type[0].
  λpred    : elt_type → bool.
  λthe_set : set elt_type.
  let left  ≝ set_filter elt_type pred the_set in
  let npred ≝ λx. ¬ (pred x) in
  let right ≝ set_filter elt_type npred the_set in
    〈left, right〉.

definition set_subset ≝
  λelt_type: Type[0].
  λeq      : elt_type → elt_type → bool.
  λleft    : set elt_type.
  λright   : set elt_type.
    set_forall elt_type (λelt. set_member elt_type eq elt right) left.

definition set_subseteq ≝
  λelt_type: Type[0].
  λeq      : elt_type → elt_type → bool.
  λleft    : set elt_type.
  λright   : set elt_type.
    set_equal elt_type eq left right ∧ (set_subset elt_type eq left right).

definition set_union ≝
  λelt_type: Type[0].
  λleft    : set elt_type.
  λright   : set elt_type.
    set_fold elt_type (set elt_type) (set_insert elt_type) left right.

definition set_intersection ≝
  λelt_type: Type[0].
  λeq      : elt_type → elt_type → bool.
  λleft    : set elt_type.
  λright   : set elt_type.
    set_filter elt_type (λelt. set_member elt_type eq elt right) left.