Library Coq.FSets.FSetPositive


Efficient implementation of FSetInterface.S for positive keys, inspired from the FMapPositive module.
This module was adapted by Alexandre Ren, Damien Pous, and Thomas Braibant (2010, LIG, CNRS, UMR 5217), from the FMapPositive module of Pierre Letouzey and Jean-Christophe Filliâtre, which in turn comes from the FMap framework of a work by Xavier Leroy and Sandrine Blazy (used for building certified compilers).

Require Import Bool BinPos OrderedType OrderedTypeEx FSetInterface.

Set Implicit Arguments.

Local Open Scope lazy_bool_scope.
Local Open Scope positive_scope.

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

  Module E:=PositiveOrderedTypeBits.

  Definition elt := positive.

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

  Scheme tree_ind := Induction for tree Sort Prop.

  Definition t := tree.

  Definition empty := 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) : 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.

helper function to avoid creating empty trees that are not leaves

  Definition node l (b: bool) r :=
    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) : 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) :=
    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) :=
    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) :=
    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.

reverses y and concatenate it with x

  Fixpoint rev_append y x :=
    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.

the additional argument, i, records the current path, in reverse order (this should be more efficient: we reverse this argument only at present nodes only, rather than at each node of the tree). we also use this convention in all functions below

    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) :=
      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) :=
      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.

uses a to accumulate values rather than doing a lot of concatenations

  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.

  Definition omap (f: elt -> elt) x :=
    match x with
      | None => None
      | Some i => Some (f i)
    end.

would it be more efficient to use a path like in the above functions ?

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

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

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

lexicographic product, defined using a notation to keep things lazy

  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_fun (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_fun l l´) (compare_fun 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_fun m m´ = Lt.

Specification of In

  Lemma In_1: forall s x y, E.eq x y -> In x s -> In y s.

Specification of eq

  Lemma eq_refl: forall s, eq s s.

  Lemma eq_sym: forall s s´, eq s s´ -> eq s´ s.

  Lemma eq_trans: forall s s´ s´´, eq s s´ -> eq s´ s´´ -> eq s s´´.

Specification of mem

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

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

Additional lemmas for mem

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

Specification of empty

  Lemma empty_1 : Empty empty.

Specification of node

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

Specification of is_empty

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

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

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

Specification of subset

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

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

  Lemma subset_1: forall s s´, Subset s s´ -> subset s s´ = true.

  Lemma subset_2: forall s s´, subset s s´ = true -> Subset s s´.

Specification of equal (via subset)

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

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

  Lemma equal_1: forall s s´, Equal s s´ -> equal s s´ = true.

  Lemma equal_2: forall s s´, equal s s´ = true -> Equal s s´.

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

(Specified) definition of compare

  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_fun s s´ = CompOpp (compare_fun 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_fun s s´ = Eq <-> equal s s´ = true.

  Lemma compare_gt: forall s s´, compare_fun s s´ = Gt -> lt s´ s.

  Lemma compare_eq: forall s s´, compare_fun s s´ = Eq -> eq s s´.

  Lemma compare : forall s s´ : t, Compare lt eq 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_fun s Leaf = if is_empty s then Eq else Gt.

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

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

  Lemma ct_compare_fun:
    forall a b c, ct (compare_fun a b) (compare_fun b c) (compare_fun a c).

  End lt_spec.

  Lemma lt_trans: forall s s´ s´´, lt s s´ -> lt s´ s´´ -> lt s s´´.

  Lemma lt_not_eq: forall s s´, lt s s´ -> ~ eq s s´.

Specification of add

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

  Lemma add_1: forall s x y, x = y -> In y (add x s).

  Lemma add_2: forall s x y, In y s -> In y (add x s).

  Lemma add_3: forall s x y, x<>y -> In y (add x s) -> In y s.

Specification of remove

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

  Lemma remove_1: forall s x y, x=y -> ~ In y (remove x s).

  Lemma remove_2: forall s x y, x<>y -> In y s -> In y (remove x s).

  Lemma remove_3: forall s x y, In y (remove x s) -> In y s.

Specification of singleton

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

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

Specification of union

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

  Lemma union_1: forall s s´ x, In x (union s s´) -> In x s \/ In x s´.

  Lemma union_2: forall s s´ x, In x s -> In x (union s s´).

  Lemma union_3: forall s s´ x, In x s´ -> In x (union s s´).

Specification of inter

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

  Lemma inter_1: forall s s´ x, In x (inter s s´) -> In x s.

  Lemma inter_2: forall s s´ x, In x (inter s s´) -> In x s´.

  Lemma inter_3: forall s s´ x, In x s -> In x s´ -> In x (inter s s´).

Specification of diff

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

  Lemma diff_1: forall s s´ x, In x (diff s s´) -> In x s.

  Lemma diff_2: forall s s´ x, In x (diff s s´) -> ~ In x s´.

  Lemma diff_3: forall s s´ x, In x s -> ~ In x s´ -> In x (diff s s´).

Specification of fold

  Lemma fold_1: 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.

Specification of cardinal

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

Specification of filter

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

  Lemma filter_1 : forall s x f, compat_bool E.eq f ->
    In x (filter f s) -> In x s.

  Lemma filter_2 : forall s x f, compat_bool E.eq f ->
    In x (filter f s) -> f x = true.

  Lemma filter_3 : forall s x f, compat_bool E.eq f -> In x s ->
    f x = true -> In x (filter f s).

Specification of for_all

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

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

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

Specification of exists

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

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

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

Specification of partition

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

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

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

Specification of elements

  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_1: forall s x, In x s -> InL x (elements s).

  Lemma elements_2: 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_3: forall s, sort E.lt (elements s).

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

Specification of choose

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

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

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

  Lemma choose_3´: forall s s´, Equal s s´ -> choose s = choose s´.

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

Specification of min_elt

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

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

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

Specification of max_elt

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

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

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

End PositiveSet.