AtomSet.v

From Tealeaves Require Import
  Classes.Categorical.ContainerFunctor
  Backends.Common.Names
  Functors.List.

From Coq Require
  MSets.MSets.

Import List.ListNotations.
Import ContainerFunctor.Notations.

#[local] Open Scope list_scope.


(** * Definition of <<AtomSet>> type *)
(******************************************************************************)
Module AtomSet <: Coq.MSets.MSetInterface.WSets :=
  Coq.MSets.MSetWeakList.Make Name.

Module AtomSetProperties :=
  Coq.MSets.MSetProperties.WPropertiesOn Name AtomSet.

(** ** Notations for operations on <<AtomSet>> *)
(******************************************************************************)
Declare Scope set_scope.
Delimit Scope set_scope with set.
Open Scope set_scope.

Module Notations.

  Notation "x `∈@` S" := (AtomSet.In x S) (at level 40) : set_scope.
  Notation "x `in` S" := (AtomSet.In x S) (at level 40) : set_scope.
  Notation "x `notin` S" := (~ AtomSet.In x S) (at level 40) : set_scope.
  Notation "s [=] t" := (AtomSet.Equal s t) (at level 70, no associativity) : set_scope.
  Notation "s ⊆ t" := (AtomSet.Subset s t) (at level 70, no associativity) : set_scope.
  Notation "s ∩ t" := (AtomSet.inter s t) (at level 60, no associativity) : set_scope.
  Notation "s \\ t" := (AtomSet.diff s t) (at level 60, no associativity) : set_scope.
  Notation "s ∪ t" := (AtomSet.union s t) (at level 61, left associativity) : set_scope.
  Notation "'elements'" := (AtomSet.elements) (at level 60, no associativity) : set_scope.
  Notation "∅" := (AtomSet.empty) : set_scope.
  Notation "{{ x }}" := (AtomSet.singleton x) : set_scope.

  Tactic Notation "fsetdec" := AtomSetProperties.Dec.fsetdec.

End Notations.

Import Notations.

#[global] Instance Monoid_op_atoms: @Monoid_op AtomSet.t := AtomSet.union.
#[global] Instance Monoid_unit_atoms: @Monoid_unit AtomSet.t := AtomSet.empty.
#[global] Instance Monoid_atoms: Monoid AtomSet.t.Monoid AtomSet.t
Proof.Monoid AtomSet.t
  constructor; unfold transparent tcs; intros.x, y, z: AtomSet.t
x ∪ y ∪ z = x ∪ (y ∪ z)
x: AtomSet.t
x ∪ ∅ = x
x: AtomSet.t
∅ ∪ x = x
  (* Can't use existing monoid typeclass because
     the laws only hold up to AtomSet.Equal, not propositional equality. *)
Abort.

(** ** The [atoms] operation *)
(** <<atoms>> collects a list of atoms into an <<AtomSet>>. It is
    conceptually inverse to [AtomSet.elements], but there's no
    guarantee the operations won't disturb the order*)
(******************************************************************************)
Fixpoint atoms (l : list atom) : AtomSet.t :=
  match l with
  | nil => ∅
  | x :: xs => AtomSet.add x (atoms xs)
  end.

(** ** Rewriting rules *)
(******************************************************************************)
Create HintDb tea_rw_atoms.

Lemma atoms_nil : atoms nil = ∅.atoms [] = ∅
Proof.atoms [] = ∅
  reflexivity.
Qed.

Lemma atoms_cons : forall (x : atom) (xs : list atom),
    atoms (x :: xs) [=] {{ x }} ∪ atoms xs.forall (x : atom) (xs : list atom),
atoms (x :: xs) [=] {{x}} ∪ atoms xs
Proof.forall (x : atom) (xs : list atom),
atoms (x :: xs) [=] {{x}} ∪ atoms xs
  intros.x: atom
xs: list atom
atoms (x :: xs) [=] {{x}} ∪ atoms xs cbn.x: atom
xs: list atom
AtomSet.add x (atoms xs) [=] {{x}} ∪ atoms xs fsetdec.
Qed.

Lemma atoms_one : forall (x : atom),
    atoms [x] [=] {{ x }}.forall x : atom, atoms [x] [=] {{x}}
Proof.forall x : atom, atoms [x] [=] {{x}}
  intros.x: atom
atoms [x] [=] {{x}} cbn.x: atom
AtomSet.add x ∅ [=] {{x}} fsetdec.
Qed.

Lemma atoms_app : forall (l1 l2 : list atom),
    atoms (l1 ++ l2) [=] atoms l1 ∪ atoms l2.forall l1 l2 : list atom,
atoms (l1 ++ l2) [=] atoms l1 ∪ atoms l2
Proof.forall l1 l2 : list atom,
atoms (l1 ++ l2) [=] atoms l1 ∪ atoms l2
  induction l1.forall l2 : list atom,
atoms ([] ++ l2) [=] atoms [] ∪ atoms l2
a: atom
l1: list atom
IHl1: forall l2 : list atom,
atoms (l1 ++ l2) [=] atoms l1 ∪ atoms l2
forall l2 : list atom,
atoms ((a :: l1) ++ l2) [=] atoms (a :: l1) ∪ atoms l2
  -forall l2 : list atom,
atoms ([] ++ l2) [=] atoms [] ∪ atoms l2 cbn.forall l2 : list atom, atoms l2 [=] ∅ ∪ atoms l2 List.simpl_list.forall l2 : list atom, atoms l2 [=] ∅ ∪ atoms l2 fsetdec.
  -a: atom
l1: list atom
IHl1: forall l2 : list atom,
atoms (l1 ++ l2) [=] atoms l1 ∪ atoms l2
forall l2 : list atom,
atoms ((a :: l1) ++ l2) [=] atoms (a :: l1) ∪ atoms l2 cbn.a: atom
l1: list atom
IHl1: forall l2 : list atom,
atoms (l1 ++ l2) [=] atoms l1 ∪ atoms l2
forall l2 : list atom,
AtomSet.add a (atoms (l1 ++ l2))
[=] AtomSet.add a (atoms l1) ∪ atoms l2 introv.a: atom
l1: list atom
IHl1: forall l2 : list atom,
atoms (l1 ++ l2) [=] atoms l1 ∪ atoms l2
l2: list atom
AtomSet.add a (atoms (l1 ++ l2))
[=] AtomSet.add a (atoms l1) ∪ atoms l2 rewrite (IHl1 l2).a: atom
l1: list atom
IHl1: forall l2 : list atom,
atoms (l1 ++ l2) [=] atoms l1 ∪ atoms l2
l2: list atom
AtomSet.add a (atoms l1 ∪ atoms l2)
[=] AtomSet.add a (atoms l1) ∪ atoms l2 fsetdec.
Qed.

#[export] Hint Rewrite atoms_nil atoms_cons atoms_one atoms_app : tea_rw_atoms.

Lemma in_atoms_nil : forall x, x `in` atoms nil <-> False.forall x : AtomSet.elt, x `in` atoms [] <-> False
Proof.forall x : AtomSet.elt, x `in` atoms [] <-> False
  cbn.forall x : AtomSet.elt, x `in` ∅ <-> False fsetdec.
Qed.

Lemma in_atoms_cons : forall (y : atom) (x : atom) (xs : list atom),
    y `in` atoms (x :: xs) <-> y = x \/ y `in` atoms xs.forall (y x : atom) (xs : list atom),
y `in` atoms (x :: xs) <-> y = x \/ y `in` atoms xs
Proof.forall (y x : atom) (xs : list atom),
y `in` atoms (x :: xs) <-> y = x \/ y `in` atoms xs
   intros.y, x: atom
xs: list atom
y `in` atoms (x :: xs) <-> y = x \/ y `in` atoms xs autorewrite with tea_rw_atoms.y, x: atom
xs: list atom
y `in` ({{x}} ∪ atoms xs) <-> y = x \/ y `in` atoms xs fsetdec.
Qed.

Lemma in_atoms_one : forall (y x : atom),
    y `in` atoms [x] <-> y = x.forall y x : atom, y `in` atoms [x] <-> y = x
Proof.forall y x : atom, y `in` atoms [x] <-> y = x
  intros.y, x: atom
y `in` atoms [x] <-> y = x autorewrite with tea_rw_atoms.y, x: atom
y `in` {{x}} <-> y = x fsetdec.
Qed.

Lemma in_atoms_app : forall (x : atom) (l1 l2 : list atom),
    x `in` atoms (l1 ++ l2) <-> x `in` atoms l1 \/ x `in` atoms l2.forall (x : atom) (l1 l2 : list atom),
x `in` atoms (l1 ++ l2) <->
x `in` atoms l1 \/ x `in` atoms l2
Proof.forall (x : atom) (l1 l2 : list atom),
x `in` atoms (l1 ++ l2) <->
x `in` atoms l1 \/ x `in` atoms l2
   intros.x: atom
l1, l2: list atom
x `in` atoms (l1 ++ l2) <->
x `in` atoms l1 \/ x `in` atoms l2 autorewrite with tea_rw_atoms.x: atom
l1, l2: list atom
x `in` (atoms l1 ∪ atoms l2) <->
x `in` atoms l1 \/ x `in` atoms l2 fsetdec.
Qed.

#[export] Hint Rewrite in_atoms_nil in_atoms_cons in_atoms_one in_atoms_app : tea_rw_atoms.

Lemma in_singleton_iff : forall (x : atom) (y : atom),
    y `in` {{ x }} <-> y = x.forall x y : atom, y `in` {{x}} <-> y = x
Proof.forall x y : atom, y `in` {{x}} <-> y = x
  intros.x, y: atom
y `in` {{x}} <-> y = x fsetdec.
Qed.

Lemma in_union_iff : forall (x : atom) (s1 s2 : AtomSet.t),
    x `in` (s1 ∪ s2) <-> x `in` s1 \/ x `in` s2.forall (x : atom) (s1 s2 : AtomSet.t),
x `in` (s1 ∪ s2) <-> x `in` s1 \/ x `in` s2
Proof.forall (x : atom) (s1 s2 : AtomSet.t),
x `in` (s1 ∪ s2) <-> x `in` s1 \/ x `in` s2
  intros.x: atom
s1, s2: AtomSet.t
x `in` (s1 ∪ s2) <-> x `in` s1 \/ x `in` s2 fsetdec.
Qed.

(** ** Relating <<AtomSet.t>> and <<list atom>> *)
(******************************************************************************)
Lemma in_elements_iff : forall (s : AtomSet.t) (x : atom),
    x `in` s <-> x ∈ elements s.forall (s : AtomSet.t) (x : atom),
x `in` s <-> x ∈ (elements) s
Proof.forall (s : AtomSet.t) (x : atom),
x `in` s <-> x ∈ (elements) s
  intros.s: AtomSet.t
x: atom
x `in` s <-> x ∈ (elements) s rewrite <- AtomSet.elements_spec1.s: AtomSet.t
x: atom
SetoidList.InA eq x ((elements) s) <->
x ∈ (elements) s induction (elements s).s: AtomSet.t
x: atom
SetoidList.InA eq x [] <-> x ∈ []
s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
SetoidList.InA eq x (a :: l) <-> x ∈ (a :: l)
  -s: AtomSet.t
x: atom
SetoidList.InA eq x [] <-> x ∈ [] cbv.s: AtomSet.t
x: atom
(SetoidList.InA eq x [] -> False) /\
(False -> SetoidList.InA eq x []) split; intro H; inversion H.
  -s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
SetoidList.InA eq x (a :: l) <-> x ∈ (a :: l) cbn.s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
SetoidList.InA eq x (a :: l) <-> a = x \/ List.In x l split; intro H; inversion H.s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: SetoidList.InA eq x (a :: l)
y: atom
l0: list atom
H1: x = a
H0: y = a
H2: l0 = l
a = x \/ List.In x l
s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: SetoidList.InA eq x (a :: l)
y: atom
l0: list atom
H1: SetoidList.InA eq x l
H0: y = a
H2: l0 = l
a = x \/ List.In x l
s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: a = x \/ List.In x l
H0: a = x
SetoidList.InA eq x (a :: l)
s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: a = x \/ List.In x l
H0: List.In x l
SetoidList.InA eq x (a :: l)
    +s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: SetoidList.InA eq x (a :: l)
y: atom
l0: list atom
H1: x = a
H0: y = a
H2: l0 = l
a = x \/ List.In x l subst.s: AtomSet.t
a: AtomSet.elt
l: list AtomSet.elt
H: SetoidList.InA eq a (a :: l)
IHl: SetoidList.InA eq a l <-> a ∈ l
a = a \/ List.In a l now left.
    +s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: SetoidList.InA eq x (a :: l)
y: atom
l0: list atom
H1: SetoidList.InA eq x l
H0: y = a
H2: l0 = l
a = x \/ List.In x l subst.s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: SetoidList.InA eq x (a :: l)
H1: SetoidList.InA eq x l
a = x \/ List.In x l destruct H.s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
y: atom
l0: list atom
H: x = y
H1: SetoidList.InA eq x l
a = x \/ List.In x l
s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
y: atom
l0: list atom
H: SetoidList.InA eq x l0
H1: SetoidList.InA eq x l
a = x \/ List.In x l
      subst.s: AtomSet.t
a: AtomSet.elt
l: list AtomSet.elt
y: atom
IHl: SetoidList.InA eq y l <-> y ∈ l
l0: list atom
H1: SetoidList.InA eq y l
a = y \/ List.In y l
s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
y: atom
l0: list atom
H: SetoidList.InA eq x l0
H1: SetoidList.InA eq x l
a = x \/ List.In x l rewrite IHl in H1.s: AtomSet.t
a: AtomSet.elt
l: list AtomSet.elt
y: atom
IHl: SetoidList.InA eq y l <-> y ∈ l
l0: list atom
H1: y ∈ l
a = y \/ List.In y l
s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
y: atom
l0: list atom
H: SetoidList.InA eq x l0
H1: SetoidList.InA eq x l
a = x \/ List.In x l now right.s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
y: atom
l0: list atom
H: SetoidList.InA eq x l0
H1: SetoidList.InA eq x l
a = x \/ List.In x l
      rewrite IHl in H1.s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
y: atom
l0: list atom
H: SetoidList.InA eq x l0
H1: x ∈ l
a = x \/ List.In x l now right.
    +s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: a = x \/ List.In x l
H0: a = x
SetoidList.InA eq x (a :: l) subst.s: AtomSet.t
x: atom
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: x = x \/ List.In x l
SetoidList.InA eq x (x :: l) now left.
    +s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: a = x \/ List.In x l
H0: List.In x l
SetoidList.InA eq x (a :: l) right.s: AtomSet.t
x: atom
a: AtomSet.elt
l: list AtomSet.elt
IHl: SetoidList.InA eq x l <-> x ∈ l
H: a = x \/ List.In x l
H0: List.In x l
SetoidList.InA eq x l now rewrite IHl.
Qed.

Lemma in_atoms_iff : forall (l : list atom) (x : atom), x ∈ l <-> x `in` atoms l.forall (l : list atom) (x : atom),
x ∈ l <-> x `in` atoms l
Proof.forall (l : list atom) (x : atom),
x ∈ l <-> x `in` atoms l
  intros.l: list atom
x: atom
x ∈ l <-> x `in` atoms l induction l.x: atom
x ∈ [] <-> x `in` atoms []
a: atom
l: list atom
x: atom
IHl: x ∈ l <-> x `in` atoms l
x ∈ (a :: l) <-> x `in` atoms (a :: l)
  -x: atom
x ∈ [] <-> x `in` atoms [] easy.
  -a: atom
l: list atom
x: atom
IHl: x ∈ l <-> x `in` atoms l
x ∈ (a :: l) <-> x `in` atoms (a :: l) autorewrite with tea_rw_atoms tea_list.a: atom
l: list atom
x: atom
IHl: x ∈ l <-> x `in` atoms l
x = a \/ x ∈ l <-> x = a \/ x `in` atoms l
    now rewrite IHl.
Qed.