Library MyFset

Require Import FSetExtra FSetWeakNotin Setoids.Setoid.
Require Export TLC.LibRelation TLC.LibTactics Omega TLC.LibLogic.

Defining atoms

Atoms are structureless objects such that we can always generate one fresh from a finite collection. Equality on atoms is eq and decidable. We use Coq's module system to make abstract the implementation of atoms.

Require Import OrderedTypeEx.

Module Import IndexSetImpl : FSetExtra.Sfun Nat_as_OT :=
FSetExtra.Make Nat_as_OT.

Notation indices :=
IndexSetImpl.t.

The AtomSetDecide module provides the fsetdec tactic for solving facts about finite sets of atoms.

Module Export IndexSetDecide := CoqFSetDecide.WDecide_fun Nat_as_OT IndexSetImpl.

The AtomSetNotin module provides the destruct_notin and solve_notin for reasoning about non-membership in finite sets of atoms, as well as a variety of lemmas about non-membership.

Module Export IndexSetNotin := FSetWeakNotin.Notin_fun Nat_as_OT IndexSetImpl.

Given the fsetdec tactic, we typically do not need to refer to specific lemmas about finite sets. However, instantiating functors from the FSets library makes a number of setoid rewrites available. These rewrites are crucial to developments since they allow us to replace a set with an extensionally equal set (see the Equal relation on finite sets) in propositions about finite sets.

Module IndexSetFacts := FSetFacts.WFacts_fun Nat_as_OT IndexSetImpl.
Module IndexSetProperties := FSetProperties.WProperties_fun Nat_as_OT IndexSetImpl.

Export IndexSetFacts.

Notation add := IndexSetImpl.add.
Notation empty := IndexSetImpl.empty.
Notation remove := IndexSetImpl.remove.
Notation singleton := IndexSetImpl.singleton.
Notation union := IndexSetImpl.union.
Notation diff := IndexSetImpl.diff.
Notation inter := IndexSetImpl.inter.
Notation filter := IndexSetImpl.filter.

Notation "E [=] F" :=
  (IndexSetImpl.Equal E F)
  (at level 70, no associativity)
  : set_scope.

Notation "E \c F" :=
  (IndexSetImpl.Subset E F)
  (at level 70, no associativity)
  : set_scope.

Notation "\{}" :=
  (IndexSetImpl.empty)
  : set_scope.

Notation "\{ x }" :=
  (IndexSetImpl.singleton x)
  : set_scope.

Notation "x \in E" :=
  (IndexSetImpl.In x E)
  (at level 70)
  : set_scope.

Notation "x \notin E" :=
  (¬ IndexSetImpl.In x E)
  (at level 70)
  : set_scope.

Notation "E \u F" :=
  (IndexSetImpl.union E F)
  (at level 65, right associativity, format "E \u '/' F")
  : set_scope.

Notation "F \- E" :=
  (IndexSetImpl.diff F E)
  (at level 70)
  : set_scope.

Notation "F \n E" :=
  (IndexSetImpl.inter F E)
  (at level 70)
  : set_scope.

Open Scope set_scope.

Lemma subset_trans: ∀ E F G, E \c F → F \c G → E \c G.
Proof.
  fsetdec.
Qed.

Definition map f E := fold (fun n E ⇒ \{ f n } \u E) E \{}.

Lemma map_spec : ∀ E f x, x \in map f E ↔ ∃ y, f y = x ∧ y \in E.
Proof.
  split.
  - unfold map. apply IndexSetProperties.fold_rec_bis; intros.
    × destruct (H0 H1). ∃ x0. split; intuition. fsetdec.
    × fsetdec.
    × rewrite union_iff in H2. destruct H2. rewrite singleton_iff in H2. ∃ x0. intuition.
      destruct (H1 H2). ∃ x1. split; intuition.
  - unfold map. apply IndexSetProperties.fold_rec_bis; intros.
    × apply H0. destruct H1. ∃ x0; intuition. fsetdec.
    × fsetdec.
    × do 2 (destruct H2). rewrite add_iff in H3. destruct H3; try fsetdec.
      rewrite union_iff. right. apply H1. ∃ x1; auto.
Qed.

Hint Extern 1 (SetoidList.compat_bool Logic.eq _) ⇒ unfold SetoidList.compat_bool; Morphisms.solve_proper:fs.

Hint Rewrite map_spec filter_iff union_iff inter_iff Compare_dec.leb_iff diff_iff:fs.

Ltac destruct_hyps :=
  repeat match goal with H: ?T |- _ ⇒
    match T with
    | _ ∧ _ ⇒ destruct H
    | ∃ a, _ ⇒ destruct H
    end
  end.

Ltac simplfs :=
  repeat (autorewrite with fs in *; auto with fs; destruct_hyps).

Lemma map_id : ∀ E, map (fun x ⇒ x) E [=] E.
Proof.
  split; simplfs; intuition. simplfs. subst; auto.
  eexists; intuition.
Qed.

Lemma filter_id : ∀ E, filter (fun x ⇒ true) E [=] E.
Proof.
  split; simplfs; intuition; auto with fs.
Qed.

Lemma map_empty : ∀ f, map f \{} = \{}.
Proof.
  unfold map. intros. apply IndexSetProperties.fold_empty.
Qed.

Lemma map_singleton : ∀ f x, map f (\{ x }) [=] \{ f x }.
Proof.
  intros. split; intros; simplfs. fsetdec. ∃ x. fsetdec.
Qed.

Lemma map_union : ∀ E F f, map f (E \u F) [=] map f E \u map f F.
Proof.
  intros. split; intros; simplfs.
  destruct H0; [ left | right]; ∃ x; fsetdec.
  destruct H; simplfs; ∃ x; fsetdec.
Qed.

Lemma map_subset : ∀ f E F, E \c F → map f E \c map f F.
Proof.
  intros f E F H1 H2 H3. simplfs. ∃ x; intuition.
Qed.

Lemma map_eq : ∀ f g E, (∀ x, x \in E → f x = g x ) → map f E [=] map g E.
Proof.
  intros. intros a. split; repeat rewrite map_spec; intros; destruct_hyps; ∃ x; intuition; [rewrite <- H; auto | rewrite H; auto].
Qed.

Lemma map_inter : ∀ E E' f, injective f → map f (E \n E') [=] (map f E \n map f E').
Proof.
  intros. intros a. split.
    simplfs. intros. destruct_hyps. simplfs. split; ∃ x; intuition.
    simplfs. intros. destruct_hyps. rewrite <- H1 in H0. forwards*: H H0. subst. ∃ x; intuition.
Qed.

Lemma filter_subset : ∀ f E F, E \c F → filter f E \c filter f F.
Proof.
  intros f E F H1 H2 H3. simplfs.
Qed.

Lemma filter_union : ∀ f E F, filter f (E \u F) [=] (filter f E \u filter f F ).
Proof.
  split; simplfs; intuition.
Qed.

Add Parametric Morphism (f:nat → nat) : (map f)
  with signature (Equal ) ==> (Equal ) as map_morphism.
Proof.
  intros. split; simplfs; intros; destruct H0; ∃ x0; fsetdec.
Qed.

Hint Rewrite map_id map_empty map_singleton filter_id:fs.

Notation cardinal := IndexSetImpl.cardinal.
Notation max_elt := IndexSetImpl.max_elt.

Lemma max_elt_spec : ∀ E n, max_elt E = Some n ↔ n \in E ∧ ∀ y, y \in E → y ≤ n.
Proof.
  split; intros. split. apply× IndexSetImpl.max_elt_1. intros. forwards*: IndexSetImpl.max_elt_2. omega.
  destruct H. absurds. intros. remember (max_elt E) as m. destruct m. assert (bla:=Heqm). symmetry in Heqm, bla.
  apply IndexSetImpl.max_elt_1 in Heqm. forwards*: H0 n0. forwards*: IndexSetImpl.max_elt_2 n0 n. assert (n=n0) by omega.
  intuition. symmetry in Heqm. apply IndexSetImpl.max_elt_3 in Heqm. fsetdec.
Qed.

Lemma max_elt_spec_empty : ∀ E, max_elt E = None ↔ IndexSetImpl.Empty E.
Proof.
  split; intros. apply× IndexSetImpl.max_elt_3.
  absurds. intros. remember (max_elt E) as m. destruct m; auto. symmetry in Heqm.
  apply IndexSetImpl.max_elt_1 in Heqm. fsetdec.
Qed.