Library NameSet

Require Import SfLib.
Require Import LibTactics.
Require Import BisimTheory.
Require Import Coq.MSets.MSetList.
Require Import Coq.MSets.MSetFacts.
Require Import Coq.MSets.MSetProperties.
Require Import Coq.FSets.FMapPositive.
Require Import Coq.FSets.FMapFacts.
Require Import Coq.PArith.BinPos.
Module PMapFacts := FMapFacts.WFacts_fun PositiveMap.E PositiveMap.

Definition name := positive.
Definition name_eq := Pos.eq_dec.

Module Pos_OWL <: OrderedTypeWithLeibniz.
  Include BinPos.Pos.
  Definition eq_leibniz: ∀ (x y:name), eq x y → x = y. introv H; exact H. Qed.
End Pos_OWL.

Module NameSet := MSetList.MakeWithLeibniz Pos_OWL.
Module NameSetFacts := MSetFacts.WFacts NameSet.
Module NameSetProps := MSetProperties.WProperties NameSet.

Definition nameset := NameSet.t.

Delimit Scope nameset_scope with nameset.
Bind Scope nameset_scope with NameSet.t.

Module Notation.

  Notation "l / a" := (NameSet.remove a l) : nameset_scope.
  Notation "'∅'" := (NameSet.empty) : nameset_scope.
  Notation "a ∈ b" := (NameSet.In a b) (no associativity, at level 19) : nameset_scope.
  Notation "a ⋃ b" := (NameSet.union a b) (left associativity, at level 21) : nameset_scope.
  Notation "a ⋂ b" := (NameSet.inter a b) (left associativity, at level 21) : nameset_scope.
  Notation "a ⊆ b" := (NameSet.Subset a b) (left associativity, at level 40) : nameset_scope.

End Notation.

Import Notation.
Open Scope nameset_scope.

Section Sets.

  Lemma NameSet_union_remove: ∀ a ns ns1 ns2,
    NameSet.Equal ns (NameSet.union ns1 ns2) →
    NameSet.Equal (NameSet.remove a ns) (NameSet.union (NameSet.remove a ns1) (NameSet.remove a ns2)).
  Proof.
    intros.
    unfold NameSet.Equal in ×.
    setoid_rewrite NameSet.union_spec.
    setoid_rewrite NameSet.union_spec in H.
    setoid_rewrite NameSet.remove_spec.
    intros a0; destruct (H a0); intuition.
  Qed.

  Lemma NameSet_Subset_inter: ∀ s1 s2 s3 s4,
    NameSet.Subset s1 s3 → NameSet.Subset s2 s4 →
    NameSet.Subset (NameSet.inter s1 s2) (NameSet.inter s3 s4).
  Proof.
    intros.
    transitivity (NameSet.inter s1 s4).
    apply NameSetProps.inter_subset_3.
    apply NameSetProps.inter_subset_1.
    transitivity s2; auto.
    apply NameSetProps.inter_subset_2.
    apply NameSetProps.inter_subset_3.
    transitivity s1; auto.
    apply NameSetProps.inter_subset_1.
    apply NameSetProps.inter_subset_2.
  Qed.

  Lemma NameSet_diff_add: ∀ a n1 n2,
    NameSet.Equal (NameSet.diff n1 (NameSet.add a n2)) (NameSet.remove a (NameSet.diff n1 n2)).
  Proof.
    intros; intro; intros.
    rewrite NameSetProps.Dec.F.remove_iff.
    rewrite NameSet.diff_spec.
    rewrite NameSet.diff_spec.
    rewrite NameSet.add_spec.
    intuition.
  Qed.

End Sets.