Module Sets

Require Import
  Utf8
  Coqlib String ToString Util
  Maps ShareTree TreeAl AdomLib
  Integers.

Local Unset Elimination Schemes.
Set Implicit Arguments.

Coercion is_true : bool >-> Sortclass.

Definition orb_left (x y: bool) : x → x || y.

Definition orb_right (x y: bool) : y → x || y.

Ltac bleft := apply orb_left.
Ltac bright := apply orb_right.

Module Type SET.
  Parameter t : Type.
  Parameter elt : Type.
  Parameter union: t -> t -> t.
  Parameter inter: t -> t -> t.
  Parameter le : t -> t -> bool.
  Parameter empty: t.
  Parameter add: elt -> t -> t.
  Parameter mem : elt -> t -> bool.

  Parameter elements : t -> list elt.

  Parameter fold : forall (A : Type) (f: elt -> A -> A), t -> A -> A.

  Parameter le_spec : forall s1 s2,
    (forall x, mem x s1 -> mem x s2) <-> le s1 s2 = true.
  Parameter mem_empty: forall x, ~mem x empty.
  Parameter mem_add: forall x y s, mem x (add y s) <-> mem x s \/ x = y.
  Parameter mem_union: forall b s1 s2,
    mem b (union s1 s2) = mem b s1 || mem b s2.
  Parameter mem_inter: forall b s1 s2,
    mem b (inter s1 s2) <-> mem b s1 /\ mem b s2.
  Parameter elements_spec : forall s x,
    mem x s <-> List.In x (elements s).
  Parameter elements_norepet : forall s, list_norepet (elements s).
  Parameter fold_spec : forall A f s a,
    @fold A f s a = List.fold_right f a (elements s).
  Hint Resolve mem_union.
End SET.

Module SetOp (S : SET).

  Definition build (l: list S.elt) : S.t :=
    List.fold_left (fun a b => S.add b a) l S.empty.

  Lemma mem_build x l :
    S.mem x (build l) <-> In x l.

  Definition singleton x := S.add x S.empty.

  Lemma mem_singleton :
    forall x y, S.mem x (singleton y) <-> x = y.

  Definition union_list (l: list S.t) : S.t :=
    List.fold_left S.union l S.empty.

  Lemma In_union_list: forall l b s,
    List.In s l -> S.mem b s -> S.mem b (union_list l).

  Instance toString `{ToString S.elt} : ToString S.t :=
    { to_string x :=
        ( "{ " ++
               List.fold_left
               (fun a e =>
                  to_string e ++ "; " ++ a
               )
               (S.elements x)
               "}"
        )%string
    }.

  Local Instance Sleb : leb_op S.t := S.le.
  Local Instance Sjoin : join_op S.t S.t := S.union.

  Lemma elements_empty : S.elements S.empty = nil.

  Definition rem s x s' : Prop :=
    (∀ y, S.mem y s → (x = y ∨ S.mem y s')) ∧
    (∀ y, S.mem y s' → x ≠ y ∧ S.mem y s).

  Lemma foldspec A f :
    ∀ P : S.t → A → A → Prop,
      (∀ s s' a b x, S.mem x s → rem s x s' → P s' a b → P s a (f x b)) →
      ∀ a, (∀ s, (∀ x, ¬ S.mem x s) → P s a a) → ∀ s, P s a (S.fold f s a).

  Definition existsb (f: S.elt → bool) (s: S.t) : bool :=
    S.fold (λ x b, b || f(x)) s false.

  Lemma existsb_exists f s :
    existsb f s = true ↔ (∃ x, S.mem x s ∧ f x = true).

  Corollary existsb_forall f s :
    existsb f s = false ↔ (∀ x, S.mem x s → f x = false).

  Inductive classify_t := Empty | Singleton (v: S.elt) | Large.
  Definition classify (s: S.t) : classify_t :=
    S.fold (λ e a, match a with Empty => Singleton e | Singleton _ | Large => Large end) s Empty.

  Lemma classify_correct s :
    match classify s with
    | Empty => ∀ x, ¬ S.mem x s
    | Singleton e => S.mem e s ∧ ∀ x, S.mem x s → x = e
    | Large => ∃ x y, x ≠ y ∧ S.mem x s ∧ S.mem y s
  end.

  Definition is_singleton (s: S.t) : option S.elt :=
    match classify s with Singleton e => Some e | _ => None end.

  Lemma is_singleton_correct s e : is_singleton s = Some e → S.mem e s ∧ ∀ x, S.mem x s → x = e.

  Definition map (f: S.elt → S.elt) (s: S.t) : S.t :=
    S.fold (fun k s => S.add (f k) s) s S.empty.

  Lemma map_in f (s: S.t) : ∀ x, S.mem x s → S.mem (f x) (map f s).

End SetOp.

Module Tree2Set (T:SHARETREE) <: SET with Definition elt := T.elt.

  Definition t := T.t unit.

  Definition elt := T.elt.

  Definition beq : t -> t -> bool := T.beq (fun _ _ => true).

  Program Definition union (x y: t) : t :=
    T.shcombine (fun _ a b => match a return _ with Some _ => a | None => b end) _ x y.

  Program Definition inter (x y: t) : t :=
    T.shcombine (fun _ a b => match a return _ with Some _ => b | None => a end) _ x y.

  Definition mem (v: elt) (x: t) : bool := match T.get v x with Some _ => true | None => false end.

  Program Definition le (x y: t) : bool :=
    T.shforall2 (fun _ a b => match a, b return _ with
                                | None, _ | Some _, Some _ => true
                                | _, _ => false
                              end)
                _ x y.

  Definition elements (x:t) : list elt :=
    T.fold (fun b v _ => v::b) x nil.

  Definition empty := T.empty unit.

  Definition add x s := T.set x tt s.

  Definition rem x s : t := T.remove x s.

  Definition fold A (f: elt -> A -> A) : t -> A -> A :=
    T.fold (fun a e _ => f e a).

  Lemma le_spec : forall s1 s2,
    (forall x, mem x s1 -> mem x s2) <-> le s1 s2 = true.

  Lemma mem_empty: forall x, ~mem x empty.

  Lemma mem_add: forall x y s, mem x (add y s) <-> mem x s \/ x = y.

  Lemma mem_rem: forall x y s, mem x (rem y s) <-> mem x s /\ x <> y.

  Lemma mem_union: forall b s1 s2,
    mem b (union s1 s2) = mem b s1 || mem b s2.

  Lemma mem_inter: forall b s1 s2,
    mem b (inter s1 s2) <-> mem b s1 /\ mem b s2.

  Lemma elements_spec : forall s x,
    mem x s <-> List.In x (elements s).

  Lemma elements_norepet : forall s, list_norepet (elements s).

  Lemma fold_spec A f s (a: A) :
    fold f s a = List.fold_right f a (elements s).

End Tree2Set.

Module PSet := Tree2Set PShareTree.
Module PSetOp := SetOp PSet.

Lemma pset_beq_mem (s t: PSet.t) :
  PSet.beq s t = true →
  ∀ x: PSet.elt, PSet.mem x s = PSet.mem x t.

Module ZSet := Tree2Set ZShareTree.
Module ZSetOp := SetOp ZSet.

Global Instance ZSet_gamma : gamma_op ZSet.t int :=
  fun s i => ZSet.mem (Int.unsigned i) s.

Section NOREP.

Context (A: Type) (f: A → positive).

Fixpoint norep_aux (l: list A) (s: PSet.t) {struct l} : bool :=
  match l with
  | nil => true
  | a :: l' =>
    let h := f(a) in
    if PSet.mem h s
    then false
    else norep_aux l' (PSet.add h s)
  end.

Lemma norep_aux_correct :
  ∀ l s,
    if norep_aux l s
    then
      list_norepet (List.map f l) ∧
      ∀ h, List.In h (List.map f l) → PSet.mem h s = true → False
    else
      (¬ list_norepet (List.map f l)) ∨
      ∃ a, List.In a l ∧ PSet.mem (f a) s
    .

Definition norepet_map (l: list A) : bool :=
  norep_aux l PSet.empty.

Lemma norepet_map_iff (l: list A) :
  norepet_map l ↔ list_norepet (List.map f l).

End NOREP.