Library Coq.MSets.MSetPositive

Require Import Bool BinPos Orders OrdersEx MSetInterface.

Set Implicit Arguments.
Local Open Scope lazy_bool_scope.
Local Open Scope positive_scope.

Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.

  Module E:=PositiveOrderedTypeBits.

  Definition elt := positive : Type.

  Inductive tree :=
    | Leaf : tree
    | Node : tree -> bool -> tree -> tree.

  Scheme tree_ind := Induction for tree Sort Prop.

  Definition t := tree : Type.

  Definition empty : t := Leaf.

  Fixpoint is_empty (m : t) : bool :=
   match m with
    | Leaf => true
    | Node l b r => negb b &&& is_empty l &&& is_empty r
   end.

  Fixpoint mem (i : positive) (m : t) {struct m} : bool :=
    match m with
    | Leaf => false
    | Node l o r =>
        match i with
        | 1 => o
        | i~0 => mem i l
        | i~1 => mem i r
        end
    end.

  Fixpoint add (i : positive) (m : t) : t :=
    match m with
    | Leaf =>
        match i with
        | 1 => Node Leaf true Leaf
        | i~0 => Node (add i Leaf) false Leaf
        | i~1 => Node Leaf false (add i Leaf)
        end
    | Node l o r =>
        match i with
        | 1 => Node l true r
        | i~0 => Node (add i l) o r
        | i~1 => Node l o (add i r)
        end
    end.

  Definition singleton i := add i empty.

  Definition node (l : t) (b: bool) (r : t) : t :=
    if b then Node l b r else
     match l,r with
       | Leaf,Leaf => Leaf
       | _,_ => Node l false r end.

  Fixpoint remove (i : positive) (m : t) {struct m} : t :=
    match m with
      | Leaf => Leaf
      | Node l o r =>
        match i with
          | 1 => node l false r
          | i~0 => node (remove i l) o r
          | i~1 => node l o (remove i r)
        end
    end.

  Fixpoint union (m m': t) : t :=
    match m with
      | Leaf => m'
      | Node l o r =>
        match m' with
          | Leaf => m
          | Node l' o' r' => Node (union l l') (o||o') (union r r')
        end
    end.

  Fixpoint inter (m m': t) : t :=
    match m with
      | Leaf => Leaf
      | Node l o r =>
        match m' with
          | Leaf => Leaf
          | Node l' o' r' => node (inter l l') (o&&o') (inter r r')
        end
    end.

  Fixpoint diff (m m': t) : t :=
    match m with
      | Leaf => Leaf
      | Node l o r =>
        match m' with
          | Leaf => m
          | Node l' o' r' => node (diff l l') (o&&negb o') (diff r r')
        end
    end.

  Fixpoint equal (m m': t): bool :=
    match m with
      | Leaf => is_empty m'
      | Node l o r =>
        match m' with
          | Leaf => is_empty m
          | Node l' o' r' => eqb o o' &&& equal l l' &&& equal r r'
        end
    end.

  Fixpoint subset (m m': t): bool :=
    match m with
      | Leaf => true
      | Node l o r =>
        match m' with
          | Leaf => is_empty m
          | Node l' o' r' => (negb o ||| o') &&& subset l l' &&& subset r r'
        end
    end.

  Fixpoint rev_append (y x : elt) : elt :=
    match y with
      | 1 => x
      | y~1 => rev_append y x~1
      | y~0 => rev_append y x~0
    end.
  Infix "@" := rev_append (at level 60).
  Definition rev x := x@1.

  Section Fold.

    Variables B : Type.
    Variable f : positive -> B -> B.

    Fixpoint xfold (m : t) (v : B) (i : positive) :=
      match m with
        | Leaf => v
        | Node l true r =>
          xfold r (f (rev i) (xfold l v i~0)) i~1
        | Node l false r =>
          xfold r (xfold l v i~0) i~1
      end.
    Definition fold m i := xfold m i 1.

  End Fold.

  Section Quantifiers.

    Variable f : positive -> bool.

    Fixpoint xforall (m : t) (i : positive) :=
      match m with
        | Leaf => true
        | Node l o r =>
          (negb o ||| f (rev i)) &&& xforall r i~1 &&& xforall l i~0
      end.
    Definition for_all m := xforall m 1.

    Fixpoint xexists (m : t) (i : positive) :=
      match m with
        | Leaf => false
        | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0
      end.
    Definition exists_ m := xexists m 1.

    Fixpoint xfilter (m : t) (i : positive) : t :=
      match m with
        | Leaf => Leaf
        | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1)
      end.
    Definition filter m := xfilter m 1.

    Fixpoint xpartition (m : t) (i : positive) : t * t :=
      match m with
        | Leaf => (Leaf,Leaf)
        | Node l o r =>
          let (lt,lf) := xpartition l i~0 in
          let (rt,rf) := xpartition r i~1 in
             if o then
               let fi := f (rev i) in
                 (node lt fi rt, node lf (negb fi) rf)
             else
                 (node lt false rt, node lf false rf)
      end.
    Definition partition m := xpartition m 1.

  End Quantifiers.

  Fixpoint xelements (m : t) (i : positive) (a: list positive) :=
    match m with
      | Leaf => a
      | Node l false r => xelements l i~0 (xelements r i~1 a)
      | Node l true r => xelements l i~0 (rev i :: xelements r i~1 a)
    end.

  Definition elements (m : t) := xelements m 1 nil.

  Fixpoint cardinal (m : t) : nat :=
    match m with
      | Leaf => O
      | Node l false r => (cardinal l + cardinal r)%nat
      | Node l true r => S (cardinal l + cardinal r)
    end.

  Fixpoint choose (m: t) : option elt :=
    match m with
      | Leaf => None
      | Node l o r => if o then Some 1 else
        match choose l with
          | None => option_map xI (choose r)
          | Some i => Some i~0
        end
    end.

  Fixpoint min_elt (m: t) : option elt :=
    match m with
      | Leaf => None
      | Node l o r =>
        match min_elt l with
          | None => if o then Some 1 else option_map xI (min_elt r)
          | Some i => Some i~0
        end
    end.

  Fixpoint max_elt (m: t) : option elt :=
    match m with
      | Leaf => None
      | Node l o r =>
        match max_elt r with
          | None => if o then Some 1 else option_map xO (max_elt l)
          | Some i => Some i~1
        end
    end.

  Notation lex u v := match u with Eq => v | Lt => Lt | Gt => Gt end.

  Definition compare_bool a b :=
    match a,b with
      | false, true => Lt
      | true, false => Gt
      | _,_ => Eq
    end.

  Fixpoint compare (m m': t): comparison :=
    match m,m' with
      | Leaf,_ => if is_empty m' then Eq else Lt
      | _,Leaf => if is_empty m then Eq else Gt
      | Node l o r,Node l' o' r' =>
        lex (compare_bool o o') (lex (compare l l') (compare r r'))
    end.

  Definition In i t := mem i t = true.
  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
  Definition Subset s s' := forall a : elt, In a s -> In a s'.
  Definition Empty s := forall a : elt, ~ In a s.
  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.

  Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
  Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).

  Definition eq := Equal.
  Definition lt m m' := compare m m' = Lt.

#[global]
  Instance In_compat : Proper (E.eq==>Logic.eq==>iff) In.

  Lemma mem_spec: forall s x, mem x s = true <-> In x s.

  Lemma mem_Leaf: forall x, mem x Leaf = false.

  Lemma empty_spec : Empty empty.

  Lemma mem_node: forall x l o r, mem x (node l o r) = mem x (Node l o r).
  Local Opaque node.

  Lemma is_empty_spec: forall s, is_empty s = true <-> Empty s.

  Lemma subset_Leaf_s: forall s, Leaf [<=] s.

  Lemma subset_spec: forall s s', subset s s' = true <-> s [<=] s'.

  Lemma equal_subset: forall s s', equal s s' = subset s s' && subset s' s.

  Lemma equal_spec: forall s s', equal s s' = true <-> Equal s s'.

  Lemma eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.

  Lemma lex_Opp: forall u v u' v', u = CompOpp u' -> v = CompOpp v' ->
    lex u v = CompOpp (lex u' v').

  Lemma compare_bool_inv: forall b b',
    compare_bool b b' = CompOpp (compare_bool b' b).

  Lemma compare_inv: forall s s', compare s s' = CompOpp (compare s' s).

  Lemma lex_Eq: forall u v, lex u v = Eq <-> u=Eq /\ v=Eq.

  Lemma compare_bool_Eq: forall b1 b2,
    compare_bool b1 b2 = Eq <-> eqb b1 b2 = true.

  Lemma compare_equal: forall s s', compare s s' = Eq <-> equal s s' = true.

  Lemma compare_gt: forall s s', compare s s' = Gt -> lt s' s.

  Lemma compare_eq: forall s s', compare s s' = Eq -> eq s s'.

  Lemma compare_spec : forall s s' : t, CompSpec eq lt s s' (compare s s').

  Section lt_spec.

  Inductive ct: comparison -> comparison -> comparison -> Prop :=
  | ct_xxx: forall x, ct x x x
  | ct_xex: forall x, ct x Eq x
  | ct_exx: forall x, ct Eq x x
  | ct_glx: forall x, ct Gt Lt x
  | ct_lgx: forall x, ct Lt Gt x.

  Lemma ct_cxe: forall x, ct (CompOpp x) x Eq.

  Lemma ct_xce: forall x, ct x (CompOpp x) Eq.

  Lemma ct_lxl: forall x, ct Lt x Lt.

  Lemma ct_gxg: forall x, ct Gt x Gt.

  Lemma ct_xll: forall x, ct x Lt Lt.

  Lemma ct_xgg: forall x, ct x Gt Gt.

  Local Hint Constructors ct: ct.
  Local Hint Resolve ct_cxe ct_xce ct_lxl ct_xll ct_gxg ct_xgg: ct.
  Ltac ct := trivial with ct.

  Lemma ct_lex: forall u v w u' v' w',
    ct u v w -> ct u' v' w' -> ct (lex u u') (lex v v') (lex w w').

  Lemma ct_compare_bool:
    forall a b c, ct (compare_bool a b) (compare_bool b c) (compare_bool a c).

  Lemma compare_x_Leaf: forall s,
    compare s Leaf = if is_empty s then Eq else Gt.

  Lemma compare_empty_x: forall a, is_empty a = true ->
    forall b, compare a b = if is_empty b then Eq else Lt.

  Lemma compare_x_empty: forall a, is_empty a = true ->
    forall b, compare b a = if is_empty b then Eq else Gt.

  Lemma ct_compare:
    forall a b c, ct (compare a b) (compare b c) (compare a c).

  End lt_spec.

#[global]
  Instance lt_strorder : StrictOrder lt.


#[global]
  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.

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

  Lemma remove_spec: forall s x y, In y (remove x s) <-> In y s /\ y<>x.

  Lemma singleton_spec : forall x y, In y (singleton x) <-> y=x.

  Lemma union_spec: forall s s' x, In x (union s s') <-> In x s \/ In x s'.

  Lemma inter_spec: forall s s' x, In x (inter s s') <-> In x s /\ In x s'.

  Lemma diff_spec: forall s s' x, In x (diff s s') <-> In x s /\ ~ In x s'.

  Lemma fold_spec: forall s (A : Type) (i : A) (f : elt -> A -> A),
      fold f s i = fold_left (fun a e => f e a) (elements s) i.

  Lemma cardinal_spec: forall s, cardinal s = length (elements s).

  Lemma xfilter_spec: forall f s x i,
    In x (xfilter f s i) <-> In x s /\ f (i@x) = true.

  Lemma filter_spec: forall s x f, @compat_bool elt E.eq f ->
    (In x (filter f s) <-> In x s /\ f x = true).

  Lemma xforall_spec: forall f s i,
    xforall f s i = true <-> For_all (fun x => f (i@x) = true) s.

  Lemma for_all_spec: forall s f, @compat_bool elt E.eq f ->
    (for_all f s = true <-> For_all (fun x => f x = true) s).

  Lemma xexists_spec: forall f s i,
    xexists f s i = true <-> Exists (fun x => f (i@x) = true) s.

  Lemma exists_spec : forall s f, @compat_bool elt E.eq f ->
    (exists_ f s = true <-> Exists (fun x => f x = true) s).

  Lemma partition_filter : forall s f,
    partition f s = (filter f s, filter (fun x => negb (f x)) s).

  Lemma partition_spec1 : forall s f, @compat_bool elt E.eq f ->
      Equal (fst (partition f s)) (filter f s).

  Lemma partition_spec2 : forall s f, @compat_bool elt E.eq f ->
      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).

  Notation InL := (InA E.eq).

  Lemma xelements_spec: forall s j acc y,
    InL y (xelements s j acc)
    <->
    InL y acc \/ exists x, y=(j@x) /\ mem x s = true.

  Lemma elements_spec1: forall s x, InL x (elements s) <-> In x s.

  Lemma lt_rev_append: forall j x y, E.lt x y -> E.lt (j@x) (j@y).

  Lemma elements_spec2: forall s, sort E.lt (elements s).

  Lemma elements_spec2w: forall s, NoDupA E.eq (elements s).

  Lemma choose_spec1: forall s x, choose s = Some x -> In x s.

  Lemma choose_spec2: forall s, choose s = None -> Empty s.

  Lemma choose_empty: forall s, is_empty s = true -> choose s = None.

  Lemma choose_spec3': forall s s', Equal s s' -> choose s = choose s'.

  Lemma choose_spec3: forall s s' x y,
    choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y.

  Lemma min_elt_spec1: forall s x, min_elt s = Some x -> In x s.

  Lemma min_elt_spec3: forall s, min_elt s = None -> Empty s.

  Lemma min_elt_spec2: forall s x y, min_elt s = Some x -> In y s -> ~ E.lt y x.

  Lemma max_elt_spec1: forall s x, max_elt s = Some x -> In x s.

  Lemma max_elt_spec3: forall s, max_elt s = None -> Empty s.

  Lemma max_elt_spec2: forall s x y, max_elt s = Some x -> In y s -> ~ E.lt x y.

End PositiveSet.