Library CoLoR.Util.FSet.FSetUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2008-02-22

Lemmas and tactics extending Coq's library FSet.

Set Implicit Arguments.

Module Make (Export XSet : FSetInterface.S).

  Module Export XSetEqProps := EqProperties XSet.
  Module Export XSetProps := Properties XSet.
  Module Export XSetFacts := Facts XSet.
  Module Export XSetOrdProps := OrdProperties XSet.

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

  Ltac eq_dec x y := unfold eqb; destruct (P.FM.eq_dec x y).

database of Equal-ity lemmas.

  Hint Rewrite union_assoc inter_assoc diff_inter_empty diff_inter_all : Equal.
  Hint Rewrite <- add_union_singleton : Equal.

  Ltac Equal := autorewrite with Equal.

database of equality lemmas on mem.

  Hint Rewrite empty_b singleton_b remove_b add_b union_b inter_b diff_b
    : mem.

  Ltac mem := autorewrite with mem.

Tactic putting a set built from intersections and unions into a "disjunctive normal form", i.e. a union of intersections.

  Ltac dnf := repeat
    match goal with
      | |- context [inter (union ?a _) _] => rewrite union_inter_1 with (s:=a)
      | |- context [inter ?a (union _ _)] =>
        rewrite inter_sym with (s:=a), union_inter_1 with (s'':=a)

Tactic for proving simple membership propositions.

  Ltac fset := intro; set_iff; tauto.

boolean equality on X

  Lemma eqb_ok x y : eqb x y = true <-> E.eq x y.

  Lemma eqb_refl x : eqb x x = true.

  Hint Rewrite eqb_refl : mem.

  Lemma eqb_sym : forall x y, eqb x y = eqb y x.


  Lemma is_empty_eq s : is_empty s = true <-> s [=] empty.

  Lemma mem_is_empty {x s} : mem x s = true -> is_empty s = false.

  Lemma subset_empty s : s [<=] empty -> s [=] empty.

  Lemma empty_subset s : s [=] empty <-> s [<=] empty.


  Lemma In_remove_neq x y s : In x (remove y s) -> ~E.eq y x.

  Lemma remove_3 x y s : In x (remove y s) -> In x s /\ ~E.eq y x.

  Lemma remove_singleton x : remove x (singleton x) [=] empty.

  Hint Rewrite remove_singleton : Equal.

  Lemma remove_union x s s' :
    remove x (union s s') [=] union (remove x s) (remove x s').

  Hint Rewrite remove_union : Equal.

  Lemma remove_empty x : remove x empty [=] empty.

  Hint Rewrite remove_empty : Equal.

  Lemma remove_com x y s : remove x (remove y s) [=] remove y (remove x s).

  Lemma remove_add_com x y s : ~E.eq x y ->
    add x (remove y s) [=] remove y (add x s).

  Lemma remove_add_eq x xs : remove x (add x xs) [=] remove x xs.

  Hint Rewrite remove_add_eq : Equal.

  Lemma remove_idem x xs : remove x (remove x xs) [=] remove x xs.

  Hint Rewrite remove_idem : Equal.

  Lemma remove_add_if x y xs : remove y (add x xs)
    [=] if eqb y x then remove y xs else add x (remove y xs).

  Lemma remove_inter x ys zs :
    remove x (inter ys zs) [=] inter (remove x ys) (remove x zs).


  Lemma Subset_antisym s t : s [=] t <-> (s [<=] t /\ t [<=] s).


  Lemma notin_union x s s' : ~In x (union s s') <-> ~In x s /\ ~In x s'.

  Lemma notin_singleton x y : ~In x (singleton y) <-> ~E.eq y x.

  Ltac notIn_elim := repeat
    match goal with
      | H : ~In _ (union _ _) |- _ => rewrite notin_union in H; destruct H
      | H : ~In _ (singleton _) |- _ => rewrite notin_singleton in H


  Lemma union_empty_l s : union empty s [=] s.

  Hint Rewrite union_empty_l : Equal.

  Lemma union_empty_r s : union s empty [=] s.

  Hint Rewrite union_empty_r : Equal.

  Lemma union_idem s : union s s [=] s.

  Hint Rewrite union_idem : Equal.

  Lemma union_idem_1 s t : union s (union s t) [=] union s t.

  Hint Rewrite union_idem_1 : Equal.

  Lemma union_idem_2 s t u :
    union s (union t (union s u)) [=] union s (union t u).

  Hint Rewrite union_idem_2 : Equal.

  Lemma union_idem_3 s t u :
    union (union s t) (union s u) [=] union s (union t u).

  Hint Rewrite union_idem_3 : Equal.

  Lemma union_sym_2 s t u : union s (union t u) [=] union t (union s u).

  Lemma union_empty a b :
    union a b [=] empty <-> a [=] empty /\ b [=] empty.

  Lemma union_empty_subset a b :
    union a b [<=] empty <-> (a [<=] empty /\ b [<=] empty).


  Lemma diff_union s t u :
    diff (union s t) u [=] union (diff s u) (diff t u).

  Lemma diff_empty_r s : diff s empty [=] s.

  Hint Rewrite diff_empty_r : Equal.

  Lemma diff_empty_l s : diff empty s [=] empty.

  Hint Rewrite diff_empty_l : Equal.

  Lemma remove_diff_singleton x s : remove x s [=] diff s (singleton x).

  Hint Rewrite <- remove_diff_singleton : Equal.


  Lemma inter_empty_l a : inter empty a [=] empty.

  Lemma inter_empty_r a : inter a empty [=] empty.

  Lemma inter_empty a b :
    inter a b [=] empty <-> (forall x, In x a -> ~In x b).

some equivalences

  Lemma mem_In x s : mem x s = true <-> In x s.

  Lemma subset_Subset s t : subset s t = true <-> Subset s t.

  Lemma equal_Equal s t : equal s t = true <-> Equal s t.

  Lemma rel_equal_Equal : rel_of_bool equal == Equal.

  Lemma mem_if x xs (b : bool) :
    mem x (if b then xs else empty) = b && mem x xs.

Compatibility of set operations wrt inclusion.
Monotony properties of max_elt.

  Inductive le_opt : relation (option E.t) :=
  | le_opt_1 : le_opt None None
  | le_opt_2 : forall x, le_opt None (Some x)
  | le_opt_3 : forall x y, x y \/ E.eq x y -> le_opt (Some x) (Some y).

  Instance max_elt_s : Proper (Subset ==> le_opt) max_elt.

  Instance max_elt_e : Proper (Equal ==> opt_r E.eq) max_elt.


  Section fold.

    Variables (A : Type) (eqA : relation A) (heqA : Equivalence eqA).

    Definition feq f f' :=
      forall x x', E.eq x x' -> forall a a', eqA a a' -> eqA (f x a) (f' x' a').

    Global Instance feq_Sym : Symmetric eqA -> Symmetric feq.

    Global Instance Proper_m' :
      Proper (feq ==> impl) (Proper (E.eq ==> eqA ==> eqA)).

    Global Instance transpose_feq' : Proper (feq ==> impl) (transpose eqA).

    Global Instance fold_m f : Proper (E.eq ==> eqA ==> eqA) f ->
      Proper (Equal ==> eqA ==> eqA) (fold f).

    Lemma fold_m_ext f : Proper (E.eq ==> eqA ==> eqA) f ->
      transpose eqA f ->
      forall f', feq f f' -> forall s s', s [=] s' -> forall a a', eqA a a' ->
        eqA (fold f s a) (fold f' s' a').

  End fold.


  Definition replace y z xs :=
    if mem y xs then add z (remove y xs) else xs.

  Instance replace_Subset :
    Proper (E.eq ==> E.eq ==> Subset ==> Subset) replace.

  Instance replace_Equal :
    Proper (Logic.eq ==> Logic.eq ==> Equal ==> Equal) replace.

  Lemma notin_replace x y xs : E.eq y x \/ ~In x (replace x y xs).

  Lemma replace_idem x xs : replace x x xs [=] xs.

  Lemma replace2 x y z xs :
    x = y \/ ~In y xs -> replace y z (replace x y xs) [=] replace x z xs.

End Make.