AssocList.v

From Tealeaves Require Import
  Common.Names
  Common.AtomSet
  Classes.Categorical.Monad (Return, ret)
  Classes.Categorical.Comonad (Extract, extract)
  Classes.Categorical.ShapelyFunctor
  Classes.Kleisli.TraversableFunctor
  Functors.Writer.

From Coq Require Import
  Logic.Decidable
  Sorting.Permutation.

Import Product.Notations.
Import List.ListNotations.
Import AtomSet.Notations.
Import ContainerFunctor.Notations.

Create HintDb tea_alist.

(** * The <<alist>> functor *)
(******************************************************************************)
(** An association list is a list of pairs of type <<atom * A>>.  A
functor instance is provided by mapping over <<A>>, leaving atoms
alone.  Technically the functor is the composition of [list] and
<<prod atom>>. *)
(******************************************************************************)
Module Notations.
  Notation "'one'" := (ret (T := list)).
  Notation "x ~ a" := (ret (T := list) (x, a)) (at level 50).
End Notations.

Import Notations.

Definition alist := list ∘ (atom ×).

(** ** Functor instance for <<alist>> *)
(******************************************************************************)
#[export] Instance Functor_alist : Functor alist :=
  Functor_compose list (prod atom).

(** ** DT functor instance for <<alist>> *)
(******************************************************************************)
Section DecoratedTraversableFunctor_alist.

  (*
  (** ** Traversable instance *)
  (******************************************************************************)
  #[global] Instance Dist_alist : Dist alist
    := Dist_compose.

  #[global] Instance Traversable_alist : TraversableFunctor alist
    := Traversable_compose.

  (** ** Decorated instance *)
  (******************************************************************************)
  #[global] Instance Decorate_alist :
    Decorate W (alist)
    := Decorate_zero.

  #[global] Instance DecoratedFunctor_alist :
    Algebraic.Decorated.Functor.DecoratedFunctor W (alist)
    := DecoratedFunctor_zero.

  (** ** DTM instance *)
  (******************************************************************************)
  #[global] Instance DecoratedTraversableFunctor_alist :
    DecoratedTraversableFunctor W (alist).
  Proof.
    constructor.
    typeclasses eauto.
    typeclasses eauto.
    intros.
    unfold_ops @Dist_alist @Dist_compose.
    unfold_ops @Fmap_compose.
    unfold_ops @Decorate_alist @Decorate_zero.
    reassociate <-.
    change (fmap G (fmap (list ○ prod atom) ?f))
      with (fmap (G ∘ list) (fmap (prod atom) f)).
    #[local] Set Keyed Unification.
    rewrite (natural (Natural := dist_natural list) (G := G ∘ list)).
    reassociate -> on right.
    rewrite (fun_fmap_fmap list).
    change (fmap list (fmap (prod atom) ?f)) with (fmap (list ∘ prod atom) f).
    (*
    rewrite <- (natural (Natural := dist_natural list) (G := G ∘ list)).
    rewrite (natural (Natural := dist_natural list)).
    rewrite (dist_natural (prod atom)).
    reassociate -> on left. rewrite (fun_fmap_fmap list).
    reassociate -> on left. rewrite (fun_fmap_fmap list).
    rewrite (fun_fmap_fmap (prod atom)). reflexivity.
    #[local] Unset Keyed Unification.
    *)
  Qed.
   *)

End DecoratedTraversableFunctor_alist.

(** * <<envmap>>  *)
(******************************************************************************)
(** [envmap] is just [fmap] specialized to <<alist>>. *)

Definition envmap {A B } : (A -> B) -> alist A -> alist B :=
  map (F := alist).

(** ** Rewriting principles for [envmap] *)
(******************************************************************************)
Section envmap_lemmas.

  Context
    (A B : Type).

  Implicit Types (f : A -> B) (x : atom) (a : A) (Γ : list (atom * A)).

  Lemma envmap_nil : forall f,
    envmap f (@nil (atom * A)) = nil.A, B: Type
forall f, envmap f [] = []
  Proof.A, B: Type
forall f, envmap f [] = []
    unfold envmap.A, B: Type
forall f, map f [] = [] unfold_ops @Map_compose.A, B: Type
forall f, map (map f) [] = []
    now simpl_list.
  Qed.

  Lemma envmap_one : forall f x a,
    envmap f (x ~ a) = (x ~ f a).A, B: Type
forall f x a, envmap f (x ~ a) = x ~ f a
  Proof.A, B: Type
forall f x a, envmap f (x ~ a) = x ~ f a
    reflexivity.
  Qed.

  Lemma envmap_cons : forall f x a Γ,
    envmap f ((x, a) :: Γ) = x ~ f a ++ envmap f Γ.A, B: Type
forall f x a Γ,
envmap f ((x, a) :: Γ) = x ~ f a ++ envmap f Γ
  Proof.A, B: Type
forall f x a Γ,
envmap f ((x, a) :: Γ) = x ~ f a ++ envmap f Γ
    reflexivity.
  Qed.

  Lemma envmap_app : forall f Γ1 Γ2,
    envmap f (Γ1 ++ Γ2) = envmap f Γ1 ++ envmap f Γ2.A, B: Type
forall f Γ1 Γ2,
envmap f (Γ1 ++ Γ2) = envmap f Γ1 ++ envmap f Γ2
  Proof.A, B: Type
forall f Γ1 Γ2,
envmap f (Γ1 ++ Γ2) = envmap f Γ1 ++ envmap f Γ2
    intros.A, B: Type
f: A -> B
Γ1, Γ2: list (atom * A)
envmap f (Γ1 ++ Γ2) = envmap f Γ1 ++ envmap f Γ2 unfold envmap.A, B: Type
f: A -> B
Γ1, Γ2: list (atom * A)
map f (Γ1 ++ Γ2) = map f Γ1 ++ map f Γ2 unfold_ops @Map_compose.A, B: Type
f: A -> B
Γ1, Γ2: list (atom * A)
map (map f) (Γ1 ++ Γ2) =
map (map f) Γ1 ++ map (map f) Γ2
    now simpl_list.
  Qed.

End envmap_lemmas.

Create HintDb tea_rw_envmap.
#[export] Hint Rewrite envmap_nil envmap_one
  envmap_cons envmap_app : tea_rw_envmap.

(** ** Specifications for [∈] and <<envmap>>*)
(******************************************************************************)
Section in_envmap_lemmas.

  Context
    {A B : Type}
    (l : alist A)
    (f : A -> B).

  Lemma in_envmap_iff : forall (x : atom) (b : B),
      (x, b) ∈ (envmap f l : list (atom * B)) <->
      exists a : A, (x, a) ∈ (l : list (atom * A)) /\ f a = b.A, B: Type
l: alist A
f: A -> B
forall (x : atom) (b : B),
(x, b) ∈ (envmap f l : list (atom * B)) <->
(exists a : A,
   (x, a) ∈ (l : list (atom * A)) /\ f a = b)
  Proof.A, B: Type
l: alist A
f: A -> B
forall (x : atom) (b : B),
(x, b) ∈ (envmap f l : list (atom * B)) <->
(exists a : A,
   (x, a) ∈ (l : list (atom * A)) /\ f a = b)
    intros.A, B: Type
l: alist A
f: A -> B
x: atom
b: B
(x, b) ∈ (envmap f l : list (atom * B)) <->
(exists a : A,
   (x, a) ∈ (l : list (atom * A)) /\ f a = b) unfold envmap.A, B: Type
l: alist A
f: A -> B
x: atom
b: B
(x, b) ∈ map f l <->
(exists a : A, (x, a) ∈ l /\ f a = b) unfold_ops @Map_compose @Map_reader.A, B: Type
l: alist A
f: A -> B
x: atom
b: B
(x, b) ∈ map (map_snd f) l <->
(exists a : A, (x, a) ∈ l /\ f a = b)
    rewrite (in_map_iff list).A, B: Type
l: alist A
f: A -> B
x: atom
b: B
(exists a : atom * A, a ∈ l /\ map_snd f a = (x, b)) <->
(exists a : A, (x, a) ∈ l /\ f a = b)
    split; intros; preprocess; eauto.
  Qed.

End in_envmap_lemmas.

(** ** Rewriting principles for [∈] *)
(******************************************************************************)
Section in_rewriting_lemmas.

  Context
    (A B : Type).

  Implicit Types (x : atom) (a : A) (b : B).

  Lemma in_nil_iff : forall x a,
      (x, a) ∈ nil <-> False.A, B: Type
forall x a, (x, a) ∈ [] <-> False
  Proof.A, B: Type
forall x a, (x, a) ∈ [] <-> False
    now autorewrite with tea_list.
  Qed.

  Lemma in_cons_iff : forall x y a1 a2 Γ,
      (x, a1) ∈ ((y, a2) :: Γ) <-> (x = y /\ a1 = a2) \/ (x, a1) ∈ Γ.A, B: Type
forall (x y : atom) a1 a2 (Γ : list (atom * A)),
(x, a1) ∈ ((y, a2) :: Γ) <->
x = y /\ a1 = a2 \/ (x, a1) ∈ Γ
  Proof.A, B: Type
forall (x y : atom) a1 a2 (Γ : list (atom * A)),
(x, a1) ∈ ((y, a2) :: Γ) <->
x = y /\ a1 = a2 \/ (x, a1) ∈ Γ
    introv.A, B: Type
x, y: atom
a1, a2: A
Γ: list (atom * A)
(x, a1) ∈ ((y, a2) :: Γ) <->
x = y /\ a1 = a2 \/ (x, a1) ∈ Γ autorewrite with tea_list.A, B: Type
x, y: atom
a1, a2: A
Γ: list (atom * A)
(x, a1) = (y, a2) \/ (x, a1) ∈ Γ <->
x = y /\ a1 = a2 \/ (x, a1) ∈ Γ
    now rewrite pair_equal_spec.
  Qed.

  Lemma in_one_iff : forall x y a1 a2,
      (x, a1) ∈ (y ~ a2) <-> x = y /\ a1 = a2.A, B: Type
forall (x y : atom) a1 a2,
(x, a1) ∈ (y ~ a2) <-> x = y /\ a1 = a2
  Proof.A, B: Type
forall (x y : atom) a1 a2,
(x, a1) ∈ (y ~ a2) <-> x = y /\ a1 = a2
    introv.A, B: Type
x, y: atom
a1, a2: A
(x, a1) ∈ (y ~ a2) <-> x = y /\ a1 = a2 autorewrite with tea_list.A, B: Type
x, y: atom
a1, a2: A
(x, a1) = (y, a2) <-> x = y /\ a1 = a2
    now rewrite pair_equal_spec.
  Qed.

  Lemma in_app_iff : forall x a Γ1 Γ2,
      (x, a) ∈ (Γ1 ++ Γ2) <-> (x, a) ∈ Γ1 \/ (x, a) ∈ Γ2.A, B: Type
forall x a (Γ1 Γ2 : list (atom * A)),
(x, a) ∈ (Γ1 ++ Γ2) <-> (x, a) ∈ Γ1 \/ (x, a) ∈ Γ2
  Proof.A, B: Type
forall x a (Γ1 Γ2 : list (atom * A)),
(x, a) ∈ (Γ1 ++ Γ2) <-> (x, a) ∈ Γ1 \/ (x, a) ∈ Γ2
    introv.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
(x, a) ∈ (Γ1 ++ Γ2) <-> (x, a) ∈ Γ1 \/ (x, a) ∈ Γ2 now autorewrite with tea_list.
  Qed.

End in_rewriting_lemmas.

Create HintDb tea_rw_in.
#[export] Hint Rewrite @in_nil_iff @in_cons_iff
  @in_one_iff @in_app_iff @in_envmap_iff : tea_rw_in.

(** ** Tactical lemmas for [∈] *)
(******************************************************************************)
Section in_theorems.

  Context
    (A B : Type).

  Implicit Types (x y : atom) (a b : A) (f : A -> B) (Γ : list (atom * A)).

  Lemma in_one1 : forall x a y b,
    (x, a) ∈ (y ~ b) ->
    x = y.A, B: Type
forall x a y b, (x, a) ∈ (y ~ b) -> x = y
  Proof.A, B: Type
forall x a y b, (x, a) ∈ (y ~ b) -> x = y
    introv.A, B: Type
x: atom
a: A
y: atom
b: A
(x, a) ∈ (y ~ b) -> x = y now autorewrite with tea_rw_in.
  Qed.

  Lemma in_one2 : forall x a y b,
      (x, a) ∈ (y ~ b) ->
      a = b.A, B: Type
forall x a y b, (x, a) ∈ (y ~ b) -> a = b
  Proof.A, B: Type
forall x a y b, (x, a) ∈ (y ~ b) -> a = b
    introv.A, B: Type
x: atom
a: A
y: atom
b: A
(x, a) ∈ (y ~ b) -> a = b now autorewrite with tea_rw_in.
  Qed.

  Lemma in_one_3 : forall x a,
    (x, a) ∈ (x ~ a).A, B: Type
forall x a, (x, a) ∈ (x ~ a)
  Proof.A, B: Type
forall x a, (x, a) ∈ (x ~ a)
    introv.A, B: Type
x: atom
a: A
(x, a) ∈ (x ~ a) now autorewrite with tea_rw_in.
  Qed.

  Lemma in_cons1 : forall x y a b Γ,
    (x, a) ∈ ((y, b) :: Γ) ->
    (x = y /\ a = b) \/ (x, a) ∈ Γ.A, B: Type
forall x y a b Γ,
(x, a) ∈ ((y, b) :: Γ) -> x = y /\ a = b \/ (x, a) ∈ Γ
  Proof.A, B: Type
forall x y a b Γ,
(x, a) ∈ ((y, b) :: Γ) -> x = y /\ a = b \/ (x, a) ∈ Γ
    introv.A, B: Type
x, y: atom
a, b: A
Γ: list (atom * A)
(x, a) ∈ ((y, b) :: Γ) -> x = y /\ a = b \/ (x, a) ∈ Γ now autorewrite with tea_rw_in.
  Qed.

  Lemma in_cons2 : forall x a E,
      (x, a) ∈ ((x, a) :: E).A, B: Type
forall x a (E : list (atom * A)),
(x, a) ∈ ((x, a) :: E)
  Proof.A, B: Type
forall x a (E : list (atom * A)),
(x, a) ∈ ((x, a) :: E)
    intros.A, B: Type
x: atom
a: A
E: list (atom * A)
(x, a) ∈ ((x, a) :: E) autorewrite with tea_rw_in.A, B: Type
x: atom
a: A
E: list (atom * A)
x = x /\ a = a \/ (x, a) ∈ E
    now left.
  Qed.

  Lemma in_cons_3 : forall x a y b E,
    (x, a) ∈ E ->
    (x, a) ∈ ((y, b) :: E).A, B: Type
forall x a y b (E : list (atom * A)),
(x, a) ∈ E -> (x, a) ∈ ((y, b) :: E)
  Proof.A, B: Type
forall x a y b (E : list (atom * A)),
(x, a) ∈ E -> (x, a) ∈ ((y, b) :: E)
    intros.A, B: Type
x: atom
a: A
y: atom
b: A
E: list (atom * A)
H: (x, a) ∈ E
(x, a) ∈ ((y, b) :: E) autorewrite with tea_rw_in.A, B: Type
x: atom
a: A
y: atom
b: A
E: list (atom * A)
H: (x, a) ∈ E
x = y /\ a = b \/ (x, a) ∈ E
    auto.
  Qed.

  Lemma in_app2 : forall x a Γ1 Γ2,
      (x, a) ∈ Γ1 ->
      (x, a) ∈ (Γ1 ++ Γ2).A, B: Type
forall x a Γ1 Γ2, (x, a) ∈ Γ1 -> (x, a) ∈ (Γ1 ++ Γ2)
  Proof.A, B: Type
forall x a Γ1 Γ2, (x, a) ∈ Γ1 -> (x, a) ∈ (Γ1 ++ Γ2)
    intros.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: (x, a) ∈ Γ1
(x, a) ∈ (Γ1 ++ Γ2) autorewrite with tea_rw_in.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: (x, a) ∈ Γ1
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2
    auto.
  Qed.

  Lemma in_app_3 :forall x a Γ1 Γ2,
      (x, a) ∈ Γ2 ->
      (x, a) ∈ (Γ1 ++ Γ2).A, B: Type
forall x a Γ1 Γ2, (x, a) ∈ Γ2 -> (x, a) ∈ (Γ1 ++ Γ2)
  Proof.A, B: Type
forall x a Γ1 Γ2, (x, a) ∈ Γ2 -> (x, a) ∈ (Γ1 ++ Γ2)
    intros.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: (x, a) ∈ Γ2
(x, a) ∈ (Γ1 ++ Γ2) autorewrite with tea_rw_in.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: (x, a) ∈ Γ2
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2
    auto.
  Qed.

  Lemma in_fmap_mono : forall x a f Γ,
    (x, a) ∈ Γ ->
    (x, f a) ∈ (envmap f Γ : list (atom * B)).A, B: Type
forall x a f Γ,
(x, a) ∈ Γ ->
(x, f a) ∈ (envmap f Γ : list (atom * B))
  Proof.A, B: Type
forall x a f Γ,
(x, a) ∈ Γ ->
(x, f a) ∈ (envmap f Γ : list (atom * B))
    introv hyp.A, B: Type
x: atom
a: A
f: A -> B
Γ: list (atom * A)
hyp: (x, a) ∈ Γ
(x, f a) ∈ envmap f Γ autorewrite with tea_rw_in.A, B: Type
x: atom
a: A
f: A -> B
Γ: list (atom * A)
hyp: (x, a) ∈ Γ
exists a0, (x, a0) ∈ Γ /\ f a0 = f a
    eauto.
  Qed.

End in_theorems.

#[export] Hint Resolve in_one_3 in_cons2 in_cons_3 in_app2
 in_app_3 in_fmap_mono : tea_alist.
#[export] Hint Immediate in_one1 in_one2 : tea_alist.

(** * Domain and range on alists *)
(******************************************************************************)

(** [dom] computes the list of keys of an association list. *)
Definition dom {A} (Γ : alist A) : list atom :=
  map fst Γ.

(** [domset] computes the keys as an [AtomSet.t] for use with <<fsetdec>>. *)
Definition domset {A} (Γ : alist A) : AtomSet.t :=
  atoms (dom Γ).

(** [range] computes the list of values of an association list. *)
Definition range {A} ( Γ : alist A) : list A :=
  map (extract (W := (atom ×))) Γ.

(** ** Rewriting lemmas for [dom] *)
(******************************************************************************)
Section dom_lemmas.

  Context
    (A : Type).

  Lemma dom_nil :
    dom (@nil (atom * A)) = [].A: Type
dom [] = []
  Proof.A: Type
dom [] = []
    reflexivity.
  Qed.

  Lemma dom_cons : forall (x : atom) (a : A) (E : alist A),
      dom ((x, a) :: E) = [ x ] ++ dom E.A: Type
forall (x : atom) (a : A) (E : alist A),
dom ((x, a) :: E) = [x] ++ dom E
  Proof.A: Type
forall (x : atom) (a : A) (E : alist A),
dom ((x, a) :: E) = [x] ++ dom E
    reflexivity.
  Qed.

  Lemma dom_one : forall (x : atom) (a : A),
      dom (x ~ a) = [ x ].A: Type
forall (x : atom) (a : A), dom (x ~ a) = [x]
  Proof.A: Type
forall (x : atom) (a : A), dom (x ~ a) = [x]
    reflexivity.
  Qed.

  Lemma dom_app : forall (E F : alist A),
      dom (E ++ F) = dom E ++ dom F.A: Type
forall E F : alist A, dom (E ++ F) = dom E ++ dom F
  Proof.A: Type
forall E F : alist A, dom (E ++ F) = dom E ++ dom F
    intros.A: Type
E, F: alist A
dom (E ++ F) = dom E ++ dom F unfold dom.A: Type
E, F: alist A
map fst (E ++ F) = map fst E ++ map fst F now simpl_list.
  Qed.

  Lemma dom_map : forall {B} {f : A -> B} (l : alist A),
      dom (envmap f l) = dom l.A: Type
forall (B : Type) (f : A -> B) (l : alist A),
dom (envmap f l) = dom l
  Proof.A: Type
forall (B : Type) (f : A -> B) (l : alist A),
dom (envmap f l) = dom l
    intros.A, B: Type
f: A -> B
l: alist A
dom (envmap f l) = dom l unfold dom, envmap.A, B: Type
f: A -> B
l: alist A
map fst (map f l) = map fst l compose near l on left.A, B: Type
f: A -> B
l: alist A
(map fst ∘ map f) l = map fst l
    unfold_ops @Map_compose.A, B: Type
f: A -> B
l: alist A
(map fst ∘ map (map f)) l = map fst l
    change (alist A) with (list (prod atom A)) at 1.A, B: Type
f: A -> B
l: alist A
(map fst ∘ map (map f)) l = map fst l
    rewrite (fun_map_map (F := list)).A, B: Type
f: A -> B
l: alist A
map (fst ∘ map f) l = map fst l
    fequal.A, B: Type
f: A -> B
l: alist A
fst ∘ map f = fst now ext [? ?].
  Qed.

End dom_lemmas.

Create HintDb tea_rw_dom.
#[export] Hint Rewrite dom_nil dom_cons dom_app dom_one dom_map : tea_rw_dom.

Lemma push_not : forall P Q,
    ~ (P \/ Q) <-> ~P /\ ~ Q.forall P Q : Prop, ~ (P \/ Q) <-> ~ P /\ ~ Q
Proof.forall P Q : Prop, ~ (P \/ Q) <-> ~ P /\ ~ Q
  firstorder.
Qed.

#[export] Hint Rewrite push_not : tea_rw_dom.

(** ** Rewriting lemmas for [domset] *)
(******************************************************************************)
Section domset_lemmas.

  Context
    (A : Type).

  Lemma domset_nil :
    domset (@nil (atom * A)) [=] ∅.A: Type
domset [] [=] ∅
  Proof.A: Type
domset [] [=] ∅
    reflexivity.
  Qed.

  Lemma domset_cons : forall (x : atom) (a : A) (Γ : alist A),
      domset ((x, a) :: Γ) [=] {{ x }} ∪ domset Γ.A: Type
forall (x : atom) (a : A) (Γ : alist A),
domset ((x, a) :: Γ) [=] {{x}} ∪ domset Γ
  Proof.A: Type
forall (x : atom) (a : A) (Γ : alist A),
domset ((x, a) :: Γ) [=] {{x}} ∪ domset Γ
    intros.A: Type
x: atom
a: A
Γ: alist A
domset ((x, a) :: Γ) [=] {{x}} ∪ domset Γ unfold domset.A: Type
x: atom
a: A
Γ: alist A
atoms (dom ((x, a) :: Γ)) [=] {{x}} ∪ atoms (dom Γ) autorewrite with tea_rw_dom tea_rw_atoms.A: Type
x: atom
a: A
Γ: alist A
{{x}} ∪ atoms (dom Γ) [=] {{x}} ∪ atoms (dom Γ)
    fsetdec.
  Qed.

  Lemma domset_one : forall (x : atom) (a : A),
      domset (x ~ a) [=] {{ x }}.A: Type
forall (x : atom) (a : A), domset (x ~ a) [=] {{x}}
  Proof.A: Type
forall (x : atom) (a : A), domset (x ~ a) [=] {{x}}
    intros.A: Type
x: atom
a: A
domset (x ~ a) [=] {{x}} unfold domset.A: Type
x: atom
a: A
atoms (dom (x ~ a)) [=] {{x}} autorewrite with tea_rw_dom tea_rw_atoms.A: Type
x: atom
a: A
{{x}} [=] {{x}}
    fsetdec.
  Qed.

  Lemma domset_app : forall (Γ1 Γ2 : alist A),
      domset (Γ1 ++ Γ2) [=] domset Γ1 ∪ domset Γ2.A: Type
forall Γ1 Γ2 : alist A,
domset (Γ1 ++ Γ2) [=] domset Γ1 ∪ domset Γ2
  Proof.A: Type
forall Γ1 Γ2 : alist A,
domset (Γ1 ++ Γ2) [=] domset Γ1 ∪ domset Γ2
    intros.A: Type
Γ1, Γ2: alist A
domset (Γ1 ++ Γ2) [=] domset Γ1 ∪ domset Γ2 unfold domset.A: Type
Γ1, Γ2: alist A
atoms (dom (Γ1 ++ Γ2))
[=] atoms (dom Γ1) ∪ atoms (dom Γ2) autorewrite with tea_rw_dom tea_rw_atoms.A: Type
Γ1, Γ2: alist A
atoms (dom Γ1) ∪ atoms (dom Γ2)
[=] atoms (dom Γ1) ∪ atoms (dom Γ2)
    fsetdec.
  Qed.

  Corollary domset_app_one_l : forall (Γ1 : alist A) (x : atom) (a : A),
      domset (Γ1 ++ x ~ a) [=] domset Γ1 ∪ {{ x }}.A: Type
forall (Γ1 : alist A) (x : atom) (a : A),
domset (Γ1 ++ x ~ a) [=] domset Γ1 ∪ {{x}}
  Proof.A: Type
forall (Γ1 : alist A) (x : atom) (a : A),
domset (Γ1 ++ x ~ a) [=] domset Γ1 ∪ {{x}}
    intros.A: Type
Γ1: alist A
x: atom
a: A
domset (Γ1 ++ x ~ a) [=] domset Γ1 ∪ {{x}} unfold domset.A: Type
Γ1: alist A
x: atom
a: A
atoms (dom (Γ1 ++ x ~ a)) [=] atoms (dom Γ1) ∪ {{x}} autorewrite with tea_rw_dom tea_rw_atoms.A: Type
Γ1: alist A
x: atom
a: A
atoms (dom Γ1) ∪ {{x}} [=] atoms (dom Γ1) ∪ {{x}}
    fsetdec.
  Qed.

  Lemma domset_map : forall {B} {f : A -> B} (Γ : alist A),
      domset (envmap f Γ) [=] domset Γ.A: Type
forall (B : Type) (f : A -> B) (Γ : alist A),
domset (envmap f Γ) [=] domset Γ
  Proof.A: Type
forall (B : Type) (f : A -> B) (Γ : alist A),
domset (envmap f Γ) [=] domset Γ
    intros.A, B: Type
f: A -> B
Γ: alist A
domset (envmap f Γ) [=] domset Γ unfold domset.A, B: Type
f: A -> B
Γ: alist A
atoms (dom (envmap f Γ)) [=] atoms (dom Γ) autorewrite with tea_rw_dom.A, B: Type
f: A -> B
Γ: alist A
atoms (dom Γ) [=] atoms (dom Γ)
    fsetdec.
  Qed.

End domset_lemmas.

#[export] Hint Rewrite domset_nil domset_cons
  domset_one domset_app domset_map : tea_rw_dom.

(** ** Rewriting lemmas for [range] *)
(******************************************************************************)
Section range_lemmas.

  Context
    (A : Type).

  Lemma range_nil :
    range (@nil (atom * A)) = [].A: Type
range [] = []
  Proof.A: Type
range [] = []
    reflexivity.
  Qed.

  Lemma range_one : forall (x : atom) (a : A),
      range (x ~ a) = [ a ].A: Type
forall (x : atom) (a : A), range (x ~ a) = [a]
  Proof.A: Type
forall (x : atom) (a : A), range (x ~ a) = [a]
    reflexivity.
  Qed.

  Lemma range_cons : forall (x : atom) (a : A) (Γ : alist A),
      range ((x, a) :: Γ) = [ a ] ++ range Γ.A: Type
forall (x : atom) (a : A) (Γ : alist A),
range ((x, a) :: Γ) = [a] ++ range Γ
  Proof.A: Type
forall (x : atom) (a : A) (Γ : alist A),
range ((x, a) :: Γ) = [a] ++ range Γ
    reflexivity.
  Qed.

  Lemma range_app : forall (Γ1 Γ2 : alist A),
      range (Γ1 ++ Γ2) = range Γ1 ++ range Γ2.A: Type
forall Γ1 Γ2 : alist A,
range (Γ1 ++ Γ2) = range Γ1 ++ range Γ2
  Proof.A: Type
forall Γ1 Γ2 : alist A,
range (Γ1 ++ Γ2) = range Γ1 ++ range Γ2
    intros.A: Type
Γ1, Γ2: alist A
range (Γ1 ++ Γ2) = range Γ1 ++ range Γ2 unfold range.A: Type
Γ1, Γ2: alist A
map extract (Γ1 ++ Γ2) =
map extract Γ1 ++ map extract Γ2
    now autorewrite with tea_list.
  Qed.

  Lemma range_map : forall {B} {f : A -> B} (Γ : alist A),
      range (envmap f Γ) = map f (range Γ).A: Type
forall (B : Type) (f : A -> B) (Γ : alist A),
range (envmap f Γ) = map f (range Γ)
  Proof.A: Type
forall (B : Type) (f : A -> B) (Γ : alist A),
range (envmap f Γ) = map f (range Γ)
    intros.A, B: Type
f: A -> B
Γ: alist A
range (envmap f Γ) = map f (range Γ) unfold range, envmap.A, B: Type
f: A -> B
Γ: alist A
map extract (map f Γ) = map f (map extract Γ) compose near Γ.A, B: Type
f: A -> B
Γ: alist A
(map extract ∘ map f) Γ = (map f ∘ map extract) Γ
    unfold_ops @Map_compose.A, B: Type
f: A -> B
Γ: alist A
(map extract ∘ map (map f)) Γ =
(map f ∘ map extract) Γ
    rewrite (fun_map_map (F := list) _ _ _ (map (F := prod atom) f) (extract (W := (prod atom)))).A, B: Type
f: A -> B
Γ: alist A
map (extract ∘ map f) Γ = (map f ∘ map extract) Γ
    rewrite (fun_map_map (F := list) _ _ _ extract f).A, B: Type
f: A -> B
Γ: alist A
map (extract ∘ map f) Γ = map (f ∘ extract) Γ
    fequal.A, B: Type
f: A -> B
Γ: alist A
extract ∘ map f = f ∘ extract now ext [? ?].
  Qed.

End range_lemmas.

Create HintDb tea_rw_range.
#[export] Hint Rewrite range_nil range_cons
     range_one range_app range_map : tea_rw_range.

(** ** Rewriting lemmas for [∈] [dom] *)
(******************************************************************************)
Section in_dom_lemmas.

  Context
    (A : Type).

  Lemma in_dom_nil : forall x,
      x ∈ dom (@nil (atom * A)) <-> False.A: Type
forall x : atom, x ∈ dom [] <-> False
  Proof.A: Type
forall x : atom, x ∈ dom [] <-> False
    intros; now autorewrite with tea_rw_dom.
  Qed.

  Lemma in_dom_cons : forall (x y : atom) (a : A) (Γ : alist A),
      y ∈ dom ((x, a) :: Γ) <-> y = x \/ y ∈ dom Γ.A: Type
forall (x y : atom) (a : A) (Γ : alist A),
y ∈ dom ((x, a) :: Γ) <-> y = x \/ y ∈ dom Γ
  Proof.A: Type
forall (x y : atom) (a : A) (Γ : alist A),
y ∈ dom ((x, a) :: Γ) <-> y = x \/ y ∈ dom Γ
    intros; autorewrite with tea_rw_dom.A: Type
x, y: atom
a: A
Γ: alist A
y ∈ ([x] ++ dom Γ) <-> y = x \/ y ∈ dom Γ
    rewrite @element_of_list_app.A: Type
x, y: atom
a: A
Γ: alist A
y ∈ [x] \/ y ∈ dom Γ <-> y = x \/ y ∈ dom Γ
    rewrite @element_of_list_one.A: Type
x, y: atom
a: A
Γ: alist A
y = x \/ y ∈ dom Γ <-> y = x \/ y ∈ dom Γ
    reflexivity.
  Qed.

  Lemma in_dom_one : forall (x y : atom) (a : A),
      y ∈ dom (x ~ a) <-> y = x.A: Type
forall (x y : atom) (a : A), y ∈ dom (x ~ a) <-> y = x
  Proof.A: Type
forall (x y : atom) (a : A), y ∈ dom (x ~ a) <-> y = x
    intros.A: Type
x, y: atom
a: A
y ∈ dom (x ~ a) <-> y = x now autorewrite with tea_rw_dom tea_list.
  Qed.

  Lemma in_dom_app : forall x (Γ1 Γ2 : alist A),
      x ∈ dom (Γ1 ++ Γ2) <-> x ∈ dom Γ1 \/ x ∈ dom Γ2.A: Type
forall (x : atom) (Γ1 Γ2 : alist A),
x ∈ dom (Γ1 ++ Γ2) <-> x ∈ dom Γ1 \/ x ∈ dom Γ2
  Proof.A: Type
forall (x : atom) (Γ1 Γ2 : alist A),
x ∈ dom (Γ1 ++ Γ2) <-> x ∈ dom Γ1 \/ x ∈ dom Γ2
    intros; now autorewrite with tea_rw_dom tea_list.
  Qed.

  Lemma in_dom_map : forall {B} {f : A -> B} (Γ : alist A) x,
      x ∈ dom (envmap f Γ) <-> x ∈ dom Γ.A: Type
forall (B : Type) (f : A -> B) (Γ : alist A)
  (x : atom), x ∈ dom (envmap f Γ) <-> x ∈ dom Γ
  Proof.A: Type
forall (B : Type) (f : A -> B) (Γ : alist A)
  (x : atom), x ∈ dom (envmap f Γ) <-> x ∈ dom Γ
    intros; now autorewrite with tea_rw_dom.
  Qed.

End in_dom_lemmas.

#[export] Hint Rewrite in_dom_nil in_dom_one in_dom_cons
  in_dom_app in_dom_map : tea_rw_dom.

(** ** Rewriting lemmas for [∈] [domset] *)
(******************************************************************************)
Section in_domset_lemmas.

  Context
    (A : Type).

  Lemma in_domset_nil : forall x,
      x `in` domset (@nil (atom * A)) <-> False.A: Type
forall x : AtomSet.elt, x `in` domset [] <-> False
  Proof.A: Type
forall x : AtomSet.elt, x `in` domset [] <-> False
    intros.A: Type
x: AtomSet.elt
x `in` domset [] <-> False autorewrite with tea_rw_dom.A: Type
x: AtomSet.elt
x `in` ∅ <-> False fsetdec.
  Qed.

  Lemma in_domset_one : forall (x y : atom) (a : A),
      y `in` domset (x ~ a) <-> y = x.A: Type
forall (x y : atom) (a : A),
y `in` domset (x ~ a) <-> y = x
  Proof.A: Type
forall (x y : atom) (a : A),
y `in` domset (x ~ a) <-> y = x
    intros.A: Type
x, y: atom
a: A
y `in` domset (x ~ a) <-> y = x autorewrite with tea_rw_dom.A: Type
x, y: atom
a: A
y `in` {{x}} <-> y = x
    fsetdec.
  Qed.

  Lemma in_domset_cons : forall (x y : atom) (a : A) (Γ : alist A),
      y `in` domset ((x, a) :: Γ) <-> y = x \/ y `in` domset Γ.A: Type
forall (x y : atom) (a : A) (Γ : alist A),
y `in` domset ((x, a) :: Γ) <->
y = x \/ y `in` domset Γ
  Proof.A: Type
forall (x y : atom) (a : A) (Γ : alist A),
y `in` domset ((x, a) :: Γ) <->
y = x \/ y `in` domset Γ
    intros.A: Type
x, y: atom
a: A
Γ: alist A
y `in` domset ((x, a) :: Γ) <->
y = x \/ y `in` domset Γ autorewrite with tea_rw_dom.A: Type
x, y: atom
a: A
Γ: alist A
y `in` ({{x}} ∪ domset Γ) <-> y = x \/ y `in` domset Γ fsetdec.
  Qed.

  Lemma in_domset_app : forall x (Γ1 Γ2 : alist A),
    x `in` domset (Γ1 ++ Γ2) <-> x `in` domset Γ1 \/ x `in` domset Γ2.A: Type
forall (x : AtomSet.elt) (Γ1 Γ2 : alist A),
x `in` domset (Γ1 ++ Γ2) <->
x `in` domset Γ1 \/ x `in` domset Γ2
  Proof.A: Type
forall (x : AtomSet.elt) (Γ1 Γ2 : alist A),
x `in` domset (Γ1 ++ Γ2) <->
x `in` domset Γ1 \/ x `in` domset Γ2
    intros.A: Type
x: AtomSet.elt
Γ1, Γ2: alist A
x `in` domset (Γ1 ++ Γ2) <->
x `in` domset Γ1 \/ x `in` domset Γ2 autorewrite with tea_rw_dom.A: Type
x: AtomSet.elt
Γ1, Γ2: alist A
x `in` (domset Γ1 ∪ domset Γ2) <->
x `in` domset Γ1 \/ x `in` domset Γ2 fsetdec.
  Qed.

  Lemma in_domset_map : forall {B} {f : A -> B} (l : alist A) x,
      x `in` domset (envmap f l) <-> x `in` domset l.A: Type
forall (B : Type) (f : A -> B) (l : alist A)
  (x : AtomSet.elt),
x `in` domset (envmap f l) <-> x `in` domset l
  Proof.A: Type
forall (B : Type) (f : A -> B) (l : alist A)
  (x : AtomSet.elt),
x `in` domset (envmap f l) <-> x `in` domset l
    intros.A, B: Type
f: A -> B
l: alist A
x: AtomSet.elt
x `in` domset (envmap f l) <-> x `in` domset l autorewrite with tea_rw_dom.A, B: Type
f: A -> B
l: alist A
x: AtomSet.elt
x `in` domset l <-> x `in` domset l fsetdec.
  Qed.

End in_domset_lemmas.

#[export] Hint Rewrite in_domset_nil in_domset_one
     in_domset_cons in_domset_app in_domset_map : tea_rw_dom.

(** ** Elements of [range] *)
(******************************************************************************)
Section in_range_lemmas.

  Context
    (A : Type).

  Lemma in_range_nil : forall x,
    x ∈ range (@nil (atom * A)) <-> False.A: Type
forall x : A, x ∈ range [] <-> False
  Proof.A: Type
forall x : A, x ∈ range [] <-> False
    intros; now autorewrite with tea_rw_range.
  Qed.

  Lemma in_range_cons : forall (x : atom) (a1 a2 : A) (Γ : alist A),
      a2 ∈ range ((x, a1) :: Γ) <-> a2 = a1 \/ a2 ∈ range Γ.A: Type
forall (x : atom) (a1 a2 : A) (Γ : alist A),
a2 ∈ range ((x, a1) :: Γ) <-> a2 = a1 \/ a2 ∈ range Γ
  Proof.A: Type
forall (x : atom) (a1 a2 : A) (Γ : alist A),
a2 ∈ range ((x, a1) :: Γ) <-> a2 = a1 \/ a2 ∈ range Γ
    intros; now autorewrite with tea_rw_range tea_list.
  Qed.

  Lemma in_range_one : forall (x : atom) (a1 a2 : A),
      a2 ∈ range (x ~ a1) <-> a1 = a2.A: Type
forall (x : atom) (a1 a2 : A),
a2 ∈ range (x ~ a1) <-> a1 = a2
  Proof.A: Type
forall (x : atom) (a1 a2 : A),
a2 ∈ range (x ~ a1) <-> a1 = a2
    intros; now autorewrite with tea_rw_range tea_list.
  Qed.

  Lemma in_range_app : forall x (Γ1 Γ2 : alist A),
    x ∈ range (Γ1 ++ Γ2) <-> x ∈ range Γ1 \/ x ∈ range Γ2.A: Type
forall (x : A) (Γ1 Γ2 : alist A),
x ∈ range (Γ1 ++ Γ2) <-> x ∈ range Γ1 \/ x ∈ range Γ2
  Proof.A: Type
forall (x : A) (Γ1 Γ2 : alist A),
x ∈ range (Γ1 ++ Γ2) <-> x ∈ range Γ1 \/ x ∈ range Γ2
    intros; now autorewrite with tea_rw_range tea_list.
  Qed.

  Lemma in_range_map : forall {B} {f : A -> B} (l : alist A) (b : B),
      b ∈ range (envmap f l) <-> exists a, a ∈ range l /\ f a = b.A: Type
forall (B : Type) (f : A -> B) (l : alist A) (b : B),
b ∈ range (envmap f l) <->
(exists a : A, a ∈ range l /\ f a = b)
  Proof.A: Type
forall (B : Type) (f : A -> B) (l : alist A) (b : B),
b ∈ range (envmap f l) <->
(exists a : A, a ∈ range l /\ f a = b)
    intros.A, B: Type
f: A -> B
l: alist A
b: B
b ∈ range (envmap f l) <->
(exists a : A, a ∈ range l /\ f a = b) autorewrite with tea_rw_range.A, B: Type
f: A -> B
l: alist A
b: B
b ∈ map f (range l) <->
(exists a : A, a ∈ range l /\ f a = b) now rewrite (in_map_iff list).
  Qed.

End in_range_lemmas.

#[export] Hint Rewrite in_range_nil in_range_one
  in_range_cons in_range_app in_range_map : tea_rw_range.

(** * Specifications for operations on association lists *)
(******************************************************************************)

(** ** Specifications for <<∈>> and [dom], [domset], [range] *)
(******************************************************************************)
Section in_operations_lemmas.

  Context
    {A : Type}
    (Γ : alist A).

  Ltac auto_star ::= intro; preprocess; eauto.

  Lemma in_dom_iff : forall (x : atom),
    x ∈ dom Γ <-> exists a : A, (x, a) ∈ (Γ : list (atom * A)).A: Type
Γ: alist A
forall x : atom,
x ∈ dom Γ <->
(exists a : A, (x, a) ∈ (Γ : list (atom * A)))
  Proof.A: Type
Γ: alist A
forall x : atom,
x ∈ dom Γ <->
(exists a : A, (x, a) ∈ (Γ : list (atom * A)))
    intros.A: Type
Γ: alist A
x: atom
x ∈ dom Γ <->
(exists a : A, (x, a) ∈ (Γ : list (atom * A))) unfold dom.A: Type
Γ: alist A
x: atom
x ∈ map fst Γ <-> (exists a : A, (x, a) ∈ Γ) rewrite (in_map_iff list).A: Type
Γ: alist A
x: atom
(exists a : atom * A, a ∈ Γ /\ fst a = x) <->
(exists a : A, (x, a) ∈ Γ)
    splits*.
  Qed.

  Lemma in_range_iff : forall a,
      a ∈ range Γ <-> exists x : atom, (x, a) ∈ (Γ : list (atom * A)).A: Type
Γ: alist A
forall a : A,
a ∈ range Γ <->
(exists x : atom, (x, a) ∈ (Γ : list (atom * A)))
  Proof.A: Type
Γ: alist A
forall a : A,
a ∈ range Γ <->
(exists x : atom, (x, a) ∈ (Γ : list (atom * A)))
    intros.A: Type
Γ: alist A
a: A
a ∈ range Γ <->
(exists x : atom, (x, a) ∈ (Γ : list (atom * A))) unfold range.A: Type
Γ: alist A
a: A
a ∈ map extract Γ <-> (exists x : atom, (x, a) ∈ Γ) rewrite (in_map_iff list).A: Type
Γ: alist A
a: A
(exists a0 : atom * A, a0 ∈ Γ /\ extract a0 = a) <->
(exists x : atom, (x, a) ∈ Γ)
    splits*.
  Qed.

  Lemma in_domset_iff : forall x,
      x `in` domset Γ <-> exists a : A, (x, a) ∈ (Γ : list (atom * A)).A: Type
Γ: alist A
forall x : AtomSet.elt,
x `in` domset Γ <->
(exists a : A, (x, a) ∈ (Γ : list (atom * A)))
  Proof.A: Type
Γ: alist A
forall x : AtomSet.elt,
x `in` domset Γ <->
(exists a : A, (x, a) ∈ (Γ : list (atom * A)))
    unfold domset.A: Type
Γ: alist A
forall x : AtomSet.elt,
x `in` atoms (dom Γ) <-> (exists a : A, (x, a) ∈ Γ) intro x.A: Type
Γ: alist A
x: AtomSet.elt
x `in` atoms (dom Γ) <-> (exists a : A, (x, a) ∈ Γ) rewrite <- in_atoms_iff.A: Type
Γ: alist A
x: AtomSet.elt
x ∈ dom Γ <-> (exists a : A, (x, a) ∈ Γ)
    setoid_rewrite in_dom_iff.A: Type
Γ: alist A
x: AtomSet.elt
(exists a : A, (x, a) ∈ Γ) <->
(exists a : A, (x, a) ∈ Γ) easy.
  Qed.

  Lemma in_domset_iff_dom : forall x,
      x `in` domset Γ <-> x ∈ dom Γ.A: Type
Γ: alist A
forall x : AtomSet.elt, x `in` domset Γ <-> x ∈ dom Γ
  Proof.A: Type
Γ: alist A
forall x : AtomSet.elt, x `in` domset Γ <-> x ∈ dom Γ
    intros.A: Type
Γ: alist A
x: AtomSet.elt
x `in` domset Γ <-> x ∈ dom Γ setoid_rewrite in_domset_iff.A: Type
Γ: alist A
x: AtomSet.elt
(exists a : A, (x, a) ∈ Γ) <-> x ∈ dom Γ
    setoid_rewrite in_dom_iff.A: Type
Γ: alist A
x: AtomSet.elt
(exists a : A, (x, a) ∈ Γ) <->
(exists a : A, (x, a) ∈ Γ) easy.
  Qed.

End in_operations_lemmas.

Section in_envmap_lemmas.

  Context
    {A B : Type}
    (l : alist A)
    (f : A -> B).

  Lemma in_range_envmap_iff : forall (b : B),
      b ∈ range (envmap f l) <->
      exists a : A, a ∈ range l /\ f a = b.A, B: Type
l: alist A
f: A -> B
forall b : B,
b ∈ range (envmap f l) <->
(exists a : A, a ∈ range l /\ f a = b)
  Proof.A, B: Type
l: alist A
f: A -> B
forall b : B,
b ∈ range (envmap f l) <->
(exists a : A, a ∈ range l /\ f a = b)
    intros.A, B: Type
l: alist A
f: A -> B
b: B
b ∈ range (envmap f l) <->
(exists a : A, a ∈ range l /\ f a = b) setoid_rewrite in_range_iff.A, B: Type
l: alist A
f: A -> B
b: B
(exists x : atom, (x, b) ∈ envmap f l) <->
(exists a : A,
   (exists x : atom, (x, a) ∈ l) /\ f a = b)
    setoid_rewrite in_envmap_iff.A, B: Type
l: alist A
f: A -> B
b: B
(exists (x : atom) (a : A), (x, a) ∈ l /\ f a = b) <->
(exists a : A,
   (exists x : atom, (x, a) ∈ l) /\ f a = b)
    firstorder.
  Qed.

  Lemma in_dom_envmap_iff : forall (x : atom),
      x ∈ dom (envmap f l) <-> x ∈ dom l.A, B: Type
l: alist A
f: A -> B
forall x : atom, x ∈ dom (envmap f l) <-> x ∈ dom l
  Proof.A, B: Type
l: alist A
f: A -> B
forall x : atom, x ∈ dom (envmap f l) <-> x ∈ dom l
    intros.A, B: Type
l: alist A
f: A -> B
x: atom
x ∈ dom (envmap f l) <-> x ∈ dom l setoid_rewrite in_dom_iff.A, B: Type
l: alist A
f: A -> B
x: atom
(exists a : B, (x, a) ∈ envmap f l) <->
(exists a : A, (x, a) ∈ l)
    setoid_rewrite in_envmap_iff.A, B: Type
l: alist A
f: A -> B
x: atom
(exists (a : B) (a0 : A), (x, a0) ∈ l /\ f a0 = a) <->
(exists a : A, (x, a) ∈ l)
    firstorder eauto.
  Qed.

End in_envmap_lemmas.

Section in_in.

  Context (A B : Type).
  Implicit Types (x : atom) (a : A) (b : B).

  Lemma in_in_dom : forall x a Γ,
      (x, a) ∈ Γ ->
      x ∈ dom (A := A) Γ.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> x ∈ dom Γ
  Proof.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> x ∈ dom Γ
    setoid_rewrite in_dom_iff.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> exists a0, (x, a0) ∈ Γ eauto.
  Qed.

  Lemma in_in_domset : forall x a Γ,
      (x, a) ∈ Γ ->
      x `in` domset (A := A) Γ.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> x `in` domset Γ
  Proof.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> x `in` domset Γ
    setoid_rewrite in_domset_iff.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> exists a0, (x, a0) ∈ Γ eauto.
  Qed.

  Lemma in_in_range : forall x a Γ,
      (x, a) ∈ Γ ->
      a ∈ range (A := A) Γ.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> a ∈ range Γ
  Proof.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> a ∈ range Γ
    setoid_rewrite in_range_iff.A, B: Type
forall x a (Γ : list (atom * A)),
(x, a) ∈ Γ -> exists x0, (x0, a) ∈ Γ eauto.
  Qed.

End in_in.

#[export] Hint Immediate in_in_dom in_in_domset in_in_range : tea_alist.

(** ** Support for prettifying association lists *)
(** The following rewrite rules can be used for normalizing
    alists. Note that we prefer <<one x ++ l>> to <<cons x l>>.  These
    rules are put into a rewrite hint database that can be invoked as
    <<simpl_alist>>. *)
(******************************************************************************)
Section alist_simpl_lemmas.

  Variable  X : Type.
  Variables x : X.
  Variables l l1 l2 l3 : list X.

  Lemma cons_app_one :
    cons x l = one x ++ l.X: Type
x: X
l, l1, l2, l3: list X
x :: l = one x ++ l
  Proof.X: Type
x: X
l, l1, l2, l3: list X
x :: l = one x ++ l clear.X: Type
x: X
l: list X
x :: l = one x ++ l reflexivity. Qed.

  Lemma cons_app_assoc :
    (cons x l1) ++ l2 = cons x (l1 ++ l2).X: Type
x: X
l, l1, l2, l3: list X
(x :: l1) ++ l2 = x :: l1 ++ l2
  Proof.X: Type
x: X
l, l1, l2, l3: list X
(x :: l1) ++ l2 = x :: l1 ++ l2 clear.X: Type
x: X
l1, l2: list X
(x :: l1) ++ l2 = x :: l1 ++ l2 reflexivity. Qed.

  Lemma app_assoc :
    (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).X: Type
x: X
l, l1, l2, l3: list X
(l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3
  Proof.X: Type
x: X
l, l1, l2, l3: list X
(l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3 clear.X: Type
l1, l2, l3: list X
(l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3 auto with datatypes. Qed.

  Lemma app_nil_l :
    nil ++ l = l.X: Type
x: X
l, l1, l2, l3: list X
[] ++ l = l
  Proof.X: Type
x: X
l, l1, l2, l3: list X
[] ++ l = l clear.X: Type
l: list X
[] ++ l = l reflexivity. Qed.

  Lemma app_nil_r :
    l ++ nil = l.X: Type
x: X
l, l1, l2, l3: list X
l ++ [] = l
  Proof.X: Type
x: X
l, l1, l2, l3: list X
l ++ [] = l clear.X: Type
l: list X
l ++ [] = l auto with datatypes. Qed.

End alist_simpl_lemmas.

Create HintDb tea_simpl_alist.
#[export] Hint Rewrite cons_app_one cons_app_assoc : tea_simpl_alist.
#[export] Hint Rewrite app_assoc app_nil_l app_nil_r : tea_simpl_alist.

Ltac simpl_alist :=
  autorewrite with tea_simpl_alist.
Tactic Notation "simpl_alist" "in" hyp(H) :=
  autorewrite with tea_simpl_alist in H.
Tactic Notation "simpl_alist" "in" "*" :=
  autorewrite with tea_simpl_alist in *.

(** ** Tactics for normalizing alists *)
(******************************************************************************)
(** The tactic <<change_alist>> can be used to replace an alist with
    an equivalent form, as long as the two forms are equal after
    normalizing with <<simpl_alist>>. *)
Tactic Notation "change_alist" constr(E) :=
  match goal with
    | |- context[?x] =>
      change x with E
    | |- context[?x] =>
      replace x with E;
        [| simpl_alist; reflexivity ]
  end.

Tactic Notation "change_alist" constr(E) "in" hyp(H) :=
  match type of H with
    | context[?x] =>
      change x with E in H
    | context[?x] =>
      replace x with E in H;
        [| simpl_alist; reflexivity ]
  end.

(** ** Induction principles for alists *)
(** The tactic <<alist induction>> can be used for induction on
alists. The difference between this and ordinary induction on lists is
that the induction hypothesis is stated in terms of <<one>> and <<++>>
rather than <<cons>>.*)
(******************************************************************************)
Lemma alist_ind : forall (A : Type) (P : alist A -> Type),
    P nil ->
    (forall x a xs, P xs -> P (x ~ a ++ xs)) ->
    (forall xs, P xs).forall (A : Type) (P : alist A -> Type),
P [] ->
(forall (x : atom) (a : A) (xs : alist A),
 P xs -> P (x ~ a ++ xs)) -> forall xs : alist A, P xs
Proof.forall (A : Type) (P : alist A -> Type),
P [] ->
(forall (x : atom) (a : A) (xs : alist A),
 P xs -> P (x ~ a ++ xs)) -> forall xs : alist A, P xs
  induction xs as [ | [x a] xs ].A: Type
P: alist A -> Type
X: P []
X0: forall (x : atom) (a : A) (xs : alist A),
P xs -> P (x ~ a ++ xs)
P []
A: Type
P: alist A -> Type
X: P []
X0: forall (x : atom) (a : A) (xs : alist A),
P xs -> P (x ~ a ++ xs)
x: atom
a: A
xs: list (atom * A)
IHxs: P xs
P ((x, a) :: xs)
  auto.A: Type
P: alist A -> Type
X: P []
X0: forall (x : atom) (a : A) (xs : alist A),
P xs -> P (x ~ a ++ xs)
x: atom
a: A
xs: list (atom * A)
IHxs: P xs
P ((x, a) :: xs)
  change (P (x ~ a ++ xs)).A: Type
P: alist A -> Type
X: P []
X0: forall (x : atom) (a : A) (xs : alist A),
P xs -> P (x ~ a ++ xs)
x: atom
a: A
xs: list (atom * A)
IHxs: P xs
P (x ~ a ++ xs) auto.
Defined.

Tactic Notation "alist" "induction" ident(E) :=
  try (intros until E);
  let T := type of E in
  let T := eval compute in T in
      match T with
      | list (?key * ?A) => induction E using (alist_ind A)
      end.

Tactic Notation "alist" "induction" ident(E) "as" simple_intropattern(P) :=
  try (intros until E);
  let T := type of E in
  let T := eval compute in T in
      match T with
      | list (?key * ?A) => induction E as P using (alist_ind A)
      end.

(** <<uniq l>> whenever the keys of <<l>> contain no duplicates. *)
Inductive uniq {A} : alist A -> Prop :=
| uniq_nil : uniq nil
| uniq_push : forall (x : atom) (v : A) ( Γ : alist A),
    uniq  Γ -> ~ x `in` domset  Γ -> uniq (x ~ v ++  Γ).

(** <<disjoint E F>> whenever the keys of <<E>> and <<F>> contain no
common elements. *)
Definition disjoint {A B} (Γ1 : alist A) (Γ2 : alist B) :=
  domset Γ1 ∩ domset Γ2 [=] ∅.

(** ** Rewriting principles for [disjoint] *)
(******************************************************************************)
Section disjoint_rewriting_lemmas.

  Context
    (A B C : Type).

  Lemma disjoint_sym : forall (Γ1 : alist A) (Γ2 : alist B),
    disjoint Γ1 Γ2 <-> disjoint Γ2 Γ1.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B),
disjoint Γ1 Γ2 <-> disjoint Γ2 Γ1
  Proof.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B),
disjoint Γ1 Γ2 <-> disjoint Γ2 Γ1
    intros.A, B, C: Type
Γ1: alist A
Γ2: alist B
disjoint Γ1 Γ2 <-> disjoint Γ2 Γ1 unfold disjoint.A, B, C: Type
Γ1: alist A
Γ2: alist B
domset Γ1 ∩ domset Γ2 [=] ∅ <->
domset Γ2 ∩ domset Γ1 [=] ∅ split; fsetdec.
  Qed.

  Lemma disjoint_nil_l : forall (Γ : alist A),
      disjoint (nil : alist A) Γ <-> True.A, B, C: Type
forall Γ : alist A, disjoint ([] : alist A) Γ <-> True
  Proof.A, B, C: Type
forall Γ : alist A, disjoint ([] : alist A) Γ <-> True
    unfold disjoint.A, B, C: Type
forall Γ : alist A,
domset [] ∩ domset Γ [=] ∅ <-> True fsetdec.
  Qed.

  Lemma disjoint_nil_r : forall (Γ : alist A),
      disjoint Γ (nil : alist B) <-> True.A, B, C: Type
forall Γ : alist A, disjoint Γ ([] : alist B) <-> True
  Proof.A, B, C: Type
forall Γ : alist A, disjoint Γ ([] : alist B) <-> True
    intros.A, B, C: Type
Γ: alist A
disjoint Γ ([] : alist B) <-> True rewrite disjoint_sym.A, B, C: Type
Γ: alist A
disjoint [] Γ <-> True now rewrite disjoint_nil_l.
  Qed.

  Lemma disjoint_cons_l : forall (x : atom) (a : A) (Γ1 : alist A) (Γ2 : alist B),
      disjoint ((x, a) :: Γ1) Γ2 <-> ~ x `in` domset Γ2 /\ disjoint Γ1 Γ2.A, B, C: Type
forall (x : atom) (a : A) (Γ1 : alist A)
  (Γ2 : alist B),
disjoint ((x, a) :: Γ1) Γ2 <->
x `notin` domset Γ2 /\ disjoint Γ1 Γ2
  Proof.A, B, C: Type
forall (x : atom) (a : A) (Γ1 : alist A)
  (Γ2 : alist B),
disjoint ((x, a) :: Γ1) Γ2 <->
x `notin` domset Γ2 /\ disjoint Γ1 Γ2
    intros.A, B, C: Type
x: atom
a: A
Γ1: alist A
Γ2: alist B
disjoint ((x, a) :: Γ1) Γ2 <->
x `notin` domset Γ2 /\ disjoint Γ1 Γ2 unfold disjoint.A, B, C: Type
x: atom
a: A
Γ1: alist A
Γ2: alist B
domset ((x, a) :: Γ1) ∩ domset Γ2 [=] ∅ <->
x `notin` domset Γ2 /\ domset Γ1 ∩ domset Γ2 [=] ∅ autorewrite with tea_rw_dom.A, B, C: Type
x: atom
a: A
Γ1: alist A
Γ2: alist B
({{x}} ∪ domset Γ1) ∩ domset Γ2 [=] ∅ <->
x `notin` domset Γ2 /\ domset Γ1 ∩ domset Γ2 [=] ∅
    intuition fsetdec.
  Qed.

  Lemma disjoint_cons_r : forall (x : atom) (b : B) (Γ1 : alist A) (Γ2 : alist B),
      disjoint Γ1 ((x, b) :: Γ2) <-> ~ x `in` domset Γ1 /\ disjoint Γ1 Γ2.A, B, C: Type
forall (x : atom) (b : B) (Γ1 : alist A)
  (Γ2 : alist B),
disjoint Γ1 ((x, b) :: Γ2) <->
x `notin` domset Γ1 /\ disjoint Γ1 Γ2
  Proof.A, B, C: Type
forall (x : atom) (b : B) (Γ1 : alist A)
  (Γ2 : alist B),
disjoint Γ1 ((x, b) :: Γ2) <->
x `notin` domset Γ1 /\ disjoint Γ1 Γ2
    intros.A, B, C: Type
x: atom
b: B
Γ1: alist A
Γ2: alist B
disjoint Γ1 ((x, b) :: Γ2) <->
x `notin` domset Γ1 /\ disjoint Γ1 Γ2 unfold disjoint.A, B, C: Type
x: atom
b: B
Γ1: alist A
Γ2: alist B
domset Γ1 ∩ domset ((x, b) :: Γ2) [=] ∅ <->
x `notin` domset Γ1 /\ domset Γ1 ∩ domset Γ2 [=] ∅ autorewrite with tea_rw_dom.A, B, C: Type
x: atom
b: B
Γ1: alist A
Γ2: alist B
domset Γ1 ∩ ({{x}} ∪ domset Γ2) [=] ∅ <->
x `notin` domset Γ1 /\ domset Γ1 ∩ domset Γ2 [=] ∅
    intuition fsetdec.
  Qed.

  Lemma disjoint_one_l : forall (x : atom) (a : A) (Γ2 : alist B),
      disjoint (x ~ a) Γ2 <-> ~ x `in` domset Γ2.A, B, C: Type
forall (x : atom) (a : A) (Γ2 : alist B),
disjoint (x ~ a) Γ2 <-> x `notin` domset Γ2
  Proof.A, B, C: Type
forall (x : atom) (a : A) (Γ2 : alist B),
disjoint (x ~ a) Γ2 <-> x `notin` domset Γ2
    intros.A, B, C: Type
x: atom
a: A
Γ2: alist B
disjoint (x ~ a) Γ2 <-> x `notin` domset Γ2 unfold disjoint.A, B, C: Type
x: atom
a: A
Γ2: alist B
domset (x ~ a) ∩ domset Γ2 [=] ∅ <->
x `notin` domset Γ2 autorewrite with tea_rw_dom.A, B, C: Type
x: atom
a: A
Γ2: alist B
{{x}} ∩ domset Γ2 [=] ∅ <-> x `notin` domset Γ2
    intuition fsetdec.
  Qed.

  Lemma disjoint_one_r : forall (x : atom) (b : B) (Γ1 : alist A),
      disjoint Γ1 (x ~ b) <-> ~ x `in` domset Γ1.A, B, C: Type
forall (x : atom) (b : B) (Γ1 : alist A),
disjoint Γ1 (x ~ b) <-> x `notin` domset Γ1
  Proof.A, B, C: Type
forall (x : atom) (b : B) (Γ1 : alist A),
disjoint Γ1 (x ~ b) <-> x `notin` domset Γ1
    intros.A, B, C: Type
x: atom
b: B
Γ1: alist A
disjoint Γ1 (x ~ b) <-> x `notin` domset Γ1 unfold disjoint.A, B, C: Type
x: atom
b: B
Γ1: alist A
domset Γ1 ∩ domset (x ~ b) [=] ∅ <->
x `notin` domset Γ1 autorewrite with tea_rw_dom.A, B, C: Type
x: atom
b: B
Γ1: alist A
domset Γ1 ∩ {{x}} [=] ∅ <-> x `notin` domset Γ1
    intuition fsetdec.
  Qed.

  Lemma disjoint_app_l : forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
      disjoint (Γ1 ++ Γ2) Γ3 <-> disjoint Γ1 Γ3 /\ disjoint Γ2 Γ3.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint (Γ1 ++ Γ2) Γ3 <->
disjoint Γ1 Γ3 /\ disjoint Γ2 Γ3
  Proof.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint (Γ1 ++ Γ2) Γ3 <->
disjoint Γ1 Γ3 /\ disjoint Γ2 Γ3
    intros.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
disjoint (Γ1 ++ Γ2) Γ3 <->
disjoint Γ1 Γ3 /\ disjoint Γ2 Γ3 unfold disjoint.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
domset (Γ1 ++ Γ2) ∩ domset Γ3 [=] ∅ <->
domset Γ1 ∩ domset Γ3 [=] ∅ /\
domset Γ2 ∩ domset Γ3 [=] ∅ autorewrite with tea_rw_dom.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
(domset Γ1 ∪ domset Γ2) ∩ domset Γ3 [=] ∅ <->
domset Γ1 ∩ domset Γ3 [=] ∅ /\
domset Γ2 ∩ domset Γ3 [=] ∅
    intuition fsetdec.
  Qed.

  Lemma disjoint_app_r : forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
      disjoint Γ3 (Γ1 ++ Γ2) <-> disjoint Γ1 Γ3 /\ disjoint Γ2 Γ3.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint Γ3 (Γ1 ++ Γ2) <->
disjoint Γ1 Γ3 /\ disjoint Γ2 Γ3
  Proof.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint Γ3 (Γ1 ++ Γ2) <->
disjoint Γ1 Γ3 /\ disjoint Γ2 Γ3
    intros.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
disjoint Γ3 (Γ1 ++ Γ2) <->
disjoint Γ1 Γ3 /\ disjoint Γ2 Γ3 unfold disjoint.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
domset Γ3 ∩ domset (Γ1 ++ Γ2) [=] ∅ <->
domset Γ1 ∩ domset Γ3 [=] ∅ /\
domset Γ2 ∩ domset Γ3 [=] ∅ autorewrite with tea_rw_dom.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
domset Γ3 ∩ (domset Γ1 ∪ domset Γ2) [=] ∅ <->
domset Γ1 ∩ domset Γ3 [=] ∅ /\
domset Γ2 ∩ domset Γ3 [=] ∅
    intuition fsetdec.
  Qed.

  Lemma disjoint_map_l : forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
      disjoint (envmap f Γ1) Γ2 <-> disjoint Γ1 Γ2.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
disjoint (envmap f Γ1) Γ2 <-> disjoint Γ1 Γ2
  Proof.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
disjoint (envmap f Γ1) Γ2 <-> disjoint Γ1 Γ2
    intros.A, B, C: Type
Γ1: alist A
Γ2: alist B
f: A -> C
disjoint (envmap f Γ1) Γ2 <-> disjoint Γ1 Γ2 unfold disjoint.A, B, C: Type
Γ1: alist A
Γ2: alist B
f: A -> C
domset (envmap f Γ1) ∩ domset Γ2 [=] ∅ <->
domset Γ1 ∩ domset Γ2 [=] ∅ autorewrite with tea_rw_dom.A, B, C: Type
Γ1: alist A
Γ2: alist B
f: A -> C
domset Γ1 ∩ domset Γ2 [=] ∅ <->
domset Γ1 ∩ domset Γ2 [=] ∅
    reflexivity.
  Qed.

  Lemma disjoint_map_r : forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
    disjoint Γ2 (envmap f Γ1) <-> disjoint Γ1 Γ2.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
disjoint Γ2 (envmap f Γ1) <-> disjoint Γ1 Γ2
  Proof.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
disjoint Γ2 (envmap f Γ1) <-> disjoint Γ1 Γ2
    intros.A, B, C: Type
Γ1: alist A
Γ2: alist B
f: A -> C
disjoint Γ2 (envmap f Γ1) <-> disjoint Γ1 Γ2 unfold disjoint.A, B, C: Type
Γ1: alist A
Γ2: alist B
f: A -> C
domset Γ2 ∩ domset (envmap f Γ1) [=] ∅ <->
domset Γ1 ∩ domset Γ2 [=] ∅ autorewrite with tea_rw_dom.A, B, C: Type
Γ1: alist A
Γ2: alist B
f: A -> C
domset Γ2 ∩ domset Γ1 [=] ∅ <->
domset Γ1 ∩ domset Γ2 [=] ∅
    intuition fsetdec.
  Qed.

End disjoint_rewriting_lemmas.

Create HintDb tea_rw_disj.
#[export] Hint Rewrite @disjoint_nil_l @disjoint_nil_r @disjoint_cons_l @disjoint_cons_r
     @disjoint_one_l @disjoint_one_r @disjoint_app_l @disjoint_app_r
     @disjoint_map_l @disjoint_map_r : tea_rw_disj.



(** ** Tactical lemmas for [disjoint] *)
(******************************************************************************)
Section disjoint_auto_lemmas.

  Context
    {A B C : Type}.

  Implicit Types (a : A) (b : B).

  Lemma disjoint_sym1 : forall (Γ1 : alist A) (Γ2 : alist B),
      disjoint Γ1 Γ2 ->
      disjoint Γ2 Γ1.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B),
disjoint Γ1 Γ2 -> disjoint Γ2 Γ1
  Proof.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B),
disjoint Γ1 Γ2 -> disjoint Γ2 Γ1
    intros.A, B, C: Type
Γ1: alist A
Γ2: alist B
H: disjoint Γ1 Γ2
disjoint Γ2 Γ1 now rewrite disjoint_sym.
  Qed.

  Lemma disjoint_app1 : forall  (Γ1 Γ2 : alist A) (Γ3 : alist B),
      disjoint (Γ1 ++ Γ2) Γ3 ->
      disjoint Γ1 Γ3.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint (Γ1 ++ Γ2) Γ3 -> disjoint Γ1 Γ3
  Proof.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint (Γ1 ++ Γ2) Γ3 -> disjoint Γ1 Γ3
    introv.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
disjoint (Γ1 ++ Γ2) Γ3 -> disjoint Γ1 Γ3 now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_app2 : forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
      disjoint (Γ1 ++ Γ2) Γ3 ->
      disjoint Γ2 Γ3.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint (Γ1 ++ Γ2) Γ3 -> disjoint Γ2 Γ3
  Proof.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint (Γ1 ++ Γ2) Γ3 -> disjoint Γ2 Γ3
    introv.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
disjoint (Γ1 ++ Γ2) Γ3 -> disjoint Γ2 Γ3 now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_app_3 : forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
      disjoint Γ1 Γ3 ->
      disjoint Γ2 Γ3 ->
      disjoint (Γ1 ++ Γ2) Γ3.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint Γ1 Γ3 ->
disjoint Γ2 Γ3 -> disjoint (Γ1 ++ Γ2) Γ3
  Proof.A, B, C: Type
forall (Γ1 Γ2 : alist A) (Γ3 : alist B),
disjoint Γ1 Γ3 ->
disjoint Γ2 Γ3 -> disjoint (Γ1 ++ Γ2) Γ3
    introv.A, B, C: Type
Γ1, Γ2: alist A
Γ3: alist B
disjoint Γ1 Γ3 ->
disjoint Γ2 Γ3 -> disjoint (Γ1 ++ Γ2) Γ3 now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_envmap1 : forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
      disjoint (envmap f Γ1) Γ2 ->
      disjoint Γ1 Γ2.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
disjoint (envmap f Γ1) Γ2 -> disjoint Γ1 Γ2
  Proof.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
disjoint (envmap f Γ1) Γ2 -> disjoint Γ1 Γ2
    introv.A, B, C: Type
Γ1: alist A
Γ2: alist B
f: A -> C
disjoint (envmap f Γ1) Γ2 -> disjoint Γ1 Γ2 now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_envmap2 : forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
      disjoint Γ1 Γ2 ->
      disjoint (envmap f Γ1) Γ2.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
disjoint Γ1 Γ2 -> disjoint (envmap f Γ1) Γ2
  Proof.A, B, C: Type
forall (Γ1 : alist A) (Γ2 : alist B) (f : A -> C),
disjoint Γ1 Γ2 -> disjoint (envmap f Γ1) Γ2
    introv.A, B, C: Type
Γ1: alist A
Γ2: alist B
f: A -> C
disjoint Γ1 Γ2 -> disjoint (envmap f Γ1) Γ2 now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_one_l1 : forall x a (Γ : alist B),
      disjoint (x ~ a) Γ -> ~ x `in` domset Γ.A, B, C: Type
forall (x : atom) a (Γ : alist B),
disjoint (x ~ a) Γ -> x `notin` domset Γ
  Proof.A, B, C: Type
forall (x : atom) a (Γ : alist B),
disjoint (x ~ a) Γ -> x `notin` domset Γ
    introv.A, B, C: Type
x: atom
a: A
Γ: alist B
disjoint (x ~ a) Γ -> x `notin` domset Γ now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_one_l2 : forall x a (Γ : alist B),
      ~ x `in` domset Γ -> disjoint (x ~ a) Γ.A, B, C: Type
forall (x : AtomSet.elt) a (Γ : alist B),
x `notin` domset Γ -> disjoint (x ~ a) Γ
  Proof.A, B, C: Type
forall (x : AtomSet.elt) a (Γ : alist B),
x `notin` domset Γ -> disjoint (x ~ a) Γ
    introv.A, B, C: Type
x: AtomSet.elt
a: A
Γ: alist B
x `notin` domset Γ -> disjoint (x ~ a) Γ now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_cons_hd : forall x a (Γ1 : alist A) (Γ2 : alist B),
      disjoint ((x, a) :: Γ1) Γ2 -> ~ x `in` domset Γ2.A, B, C: Type
forall (x : atom) a (Γ1 : alist A) (Γ2 : alist B),
disjoint ((x, a) :: Γ1) Γ2 -> x `notin` domset Γ2
  Proof.A, B, C: Type
forall (x : atom) a (Γ1 : alist A) (Γ2 : alist B),
disjoint ((x, a) :: Γ1) Γ2 -> x `notin` domset Γ2
    introv.A, B, C: Type
x: atom
a: A
Γ1: alist A
Γ2: alist B
disjoint ((x, a) :: Γ1) Γ2 -> x `notin` domset Γ2 now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_cons_hd_one : forall x a (Γ1 : alist A) (Γ2 : alist B),
      disjoint (x ~ a ++ Γ1) Γ2 -> ~ x `in` domset Γ2.A, B, C: Type
forall (x : atom) a (Γ1 : alist A) (Γ2 : alist B),
disjoint (x ~ a ++ Γ1) Γ2 -> x `notin` domset Γ2
  Proof.A, B, C: Type
forall (x : atom) a (Γ1 : alist A) (Γ2 : alist B),
disjoint (x ~ a ++ Γ1) Γ2 -> x `notin` domset Γ2
    introv.A, B, C: Type
x: atom
a: A
Γ1: alist A
Γ2: alist B
disjoint (x ~ a ++ Γ1) Γ2 -> x `notin` domset Γ2 now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_cons_tl : forall x a (Γ1 : alist A) (Γ2 : alist B),
      disjoint ((x, a) :: Γ1) Γ2 -> disjoint Γ1 Γ2.A, B, C: Type
forall (x : atom) a (Γ1 : alist A) (Γ2 : alist B),
disjoint ((x, a) :: Γ1) Γ2 -> disjoint Γ1 Γ2
  Proof.A, B, C: Type
forall (x : atom) a (Γ1 : alist A) (Γ2 : alist B),
disjoint ((x, a) :: Γ1) Γ2 -> disjoint Γ1 Γ2
    introv.A, B, C: Type
x: atom
a: A
Γ1: alist A
Γ2: alist B
disjoint ((x, a) :: Γ1) Γ2 -> disjoint Γ1 Γ2 now autorewrite with tea_rw_disj.
  Qed.

  Lemma disjoint_dom1 : forall x (Γ1 : alist A) (Γ2 : alist B),
      disjoint Γ1 Γ2 ->
      x `in` domset Γ1 ->
      ~ x `in` domset Γ2.A, B, C: Type
forall (x : AtomSet.elt) (Γ1 : alist A) (Γ2 : alist B),
disjoint Γ1 Γ2 ->
x `in` domset Γ1 -> x `notin` domset Γ2
  Proof.A, B, C: Type
forall (x : AtomSet.elt) (Γ1 : alist A) (Γ2 : alist B),
disjoint Γ1 Γ2 ->
x `in` domset Γ1 -> x `notin` domset Γ2
    unfold disjoint in *.A, B, C: Type
forall (x : AtomSet.elt) (Γ1 : alist A) (Γ2 : alist B),
domset Γ1 ∩ domset Γ2 [=] ∅ ->
x `in` domset Γ1 -> x `notin` domset Γ2 fsetdec.
  Qed.

  Lemma disjoint_dom2 : forall x (Γ1 : alist A) (Γ2 : alist B),
      disjoint Γ1 Γ2 ->
      x `in` domset Γ2 ->
      ~ x `in` domset Γ1.A, B, C: Type
forall (x : AtomSet.elt) (Γ1 : alist A) (Γ2 : alist B),
disjoint Γ1 Γ2 ->
x `in` domset Γ2 -> x `notin` domset Γ1
  Proof.A, B, C: Type
forall (x : AtomSet.elt) (Γ1 : alist A) (Γ2 : alist B),
disjoint Γ1 Γ2 ->
x `in` domset Γ2 -> x `notin` domset Γ1
    unfold disjoint in *.A, B, C: Type
forall (x : AtomSet.elt) (Γ1 : alist A) (Γ2 : alist B),
domset Γ1 ∩ domset Γ2 [=] ∅ ->
x `in` domset Γ2 -> x `notin` domset Γ1 fsetdec.
  Qed.

  Lemma disjoint_binds1 : forall x a (Γ1 : alist A) (Γ2 : alist A),
      disjoint Γ1 Γ2 ->
      (x, a) ∈ (Γ1 : list (prod atom A)) ->
      ~ (x, a) ∈ (Γ2 : list (prod atom A)).A, B, C: Type
forall (x : atom) a (Γ1 Γ2 : alist A),
disjoint Γ1 Γ2 ->
(x, a) ∈ (Γ1 : list (atom * A)) ->
~ (x, a) ∈ (Γ2 : list (atom * A))
  Proof.A, B, C: Type
forall (x : atom) a (Γ1 Γ2 : alist A),
disjoint Γ1 Γ2 ->
(x, a) ∈ (Γ1 : list (atom * A)) ->
~ (x, a) ∈ (Γ2 : list (atom * A))
    introv Hdisj He Hf.A, B, C: Type
x: atom
a: A
Γ1, Γ2: alist A
Hdisj: disjoint Γ1 Γ2
He: (x, a) ∈ Γ1
Hf: (x, a) ∈ Γ2
False
    apply in_in_domset in He.A, B, C: Type
x: atom
a: A
Γ1, Γ2: alist A
Hdisj: disjoint Γ1 Γ2
He: x `in` domset Γ1
Hf: (x, a) ∈ Γ2
False
    apply in_in_domset in Hf.A, B, C: Type
x: atom
a: A
Γ1, Γ2: alist A
Hdisj: disjoint Γ1 Γ2
He: x `in` domset Γ1
Hf: x `in` domset Γ2
False
    unfold disjoint in *.A, B, C: Type
x: atom
a: A
Γ1, Γ2: alist A
Hdisj: domset Γ1 ∩ domset Γ2 [=] ∅
He: x `in` domset Γ1
Hf: x `in` domset Γ2
False
    fsetdec.
  Qed.

  Lemma disjoint_binds2 : forall x a (Γ1 : alist A) (Γ2 : alist A),
      disjoint Γ1 Γ2 ->
      (x, a) ∈ (Γ1 : list (prod atom A)) ->
      ~ (x, a) ∈ (Γ2 : list (prod atom A)).A, B, C: Type
forall (x : atom) a (Γ1 Γ2 : alist A),
disjoint Γ1 Γ2 ->
(x, a) ∈ (Γ1 : list (atom * A)) ->
~ (x, a) ∈ (Γ2 : list (atom * A))
  Proof.A, B, C: Type
forall (x : atom) a (Γ1 Γ2 : alist A),
disjoint Γ1 Γ2 ->
(x, a) ∈ (Γ1 : list (atom * A)) ->
~ (x, a) ∈ (Γ2 : list (atom * A))
    introv Hd Hf.A, B, C: Type
x: atom
a: A
Γ1, Γ2: alist A
Hd: disjoint Γ1 Γ2
Hf: (x, a) ∈ Γ1
~ (x, a) ∈ Γ2
    eauto using disjoint_binds1.
  Qed.

End disjoint_auto_lemmas.

#[export] Hint Resolve disjoint_sym1 disjoint_app_3
 disjoint_envmap2 : tea_alist.

(** These introduce existential variables, so only
apply them if they immediately solve the goal. *)
#[export] Hint Immediate disjoint_app1 disjoint_app2
 disjoint_one_l1 disjoint_envmap1
 disjoint_dom1 disjoint_dom2
 disjoint_binds1 disjoint_binds2 : tea_alist.

(** ** Tactical lemmas for [uniq] *)
(** For automating proofs about uniqueness, it is typically easier to
work with (one-way) lemmas rather than rewriting principles, in
contrast to most of the other parts of Tealeaves internals. *)
(******************************************************************************)
Section uniq_auto_lemmas.

  Context
    (A B : Type)
    (Γ1 Γ2 : alist A).

  Implicit Types (x : atom) (a : A) (b : B).

  Lemma uniq_one : forall x a,
      uniq (x ~ a).A, B: Type
Γ1, Γ2: alist A
forall x a, uniq (x ~ a)
  Proof.A, B: Type
Γ1, Γ2: alist A
forall x a, uniq (x ~ a)
    intros.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
uniq (x ~ a) change_alist ((x ~ a) ++ nil).A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
uniq (x ~ a ++ [])
    constructor; [constructor | fsetdec].
  Qed.

  Lemma uniq_cons1 : forall x a,
      uniq ((x, a) :: Γ1) ->
      uniq Γ1.A, B: Type
Γ1, Γ2: alist A
forall x a, uniq ((x, a) :: Γ1) -> uniq Γ1
  Proof.A, B: Type
Γ1, Γ2: alist A
forall x a, uniq ((x, a) :: Γ1) -> uniq Γ1
    now inversion 1.
  Qed.

  Lemma uniq_cons2 : forall x a,
      uniq ((x, a) :: Γ1) ->
      ~ x `in` domset Γ1.A, B: Type
Γ1, Γ2: alist A
forall x a, uniq ((x, a) :: Γ1) -> x `notin` domset Γ1
  Proof.A, B: Type
Γ1, Γ2: alist A
forall x a, uniq ((x, a) :: Γ1) -> x `notin` domset Γ1
    now inversion 1.
  Qed.

  Lemma uniq_cons_3 : forall x a,
      ~ x `in` domset Γ1 ->
      uniq Γ1 ->
      uniq ((x, a) :: Γ1).A, B: Type
Γ1, Γ2: alist A
forall x a,
x `notin` domset Γ1 -> uniq Γ1 -> uniq ((x, a) :: Γ1)
  Proof.A, B: Type
Γ1, Γ2: alist A
forall x a,
x `notin` domset Γ1 -> uniq Γ1 -> uniq ((x, a) :: Γ1)
    intros.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
H: x `notin` domset Γ1
H0: uniq Γ1
uniq ((x, a) :: Γ1) constructor; auto.
  Qed.

  Lemma uniq_app1 :
      uniq (Γ1 ++ Γ2) ->
      uniq Γ1.A, B: Type
Γ1, Γ2: alist A
uniq (Γ1 ++ Γ2) -> uniq Γ1
  Proof.A, B: Type
Γ1, Γ2: alist A
uniq (Γ1 ++ Γ2) -> uniq Γ1
    introv Hu.A, B: Type
Γ1, Γ2: alist A
Hu: uniq (Γ1 ++ Γ2)
uniq Γ1 alist induction Γ1.A, B: Type
Γ1, Γ2: alist A
Hu: uniq ([] ++ Γ2)
uniq []
A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
Hu: uniq ((x ~ a ++ a0) ++ Γ2)
IHa: uniq (a0 ++ Γ2) -> uniq a0
uniq (x ~ a ++ a0)
    -A, B: Type
Γ1, Γ2: alist A
Hu: uniq ([] ++ Γ2)
uniq [] constructor.
    -A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
Hu: uniq ((x ~ a ++ a0) ++ Γ2)
IHa: uniq (a0 ++ Γ2) -> uniq a0
uniq (x ~ a ++ a0) simpl_alist in Hu.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
Hu: uniq (x ~ a ++ a0 ++ Γ2)
IHa: uniq (a0 ++ Γ2) -> uniq a0
uniq (x ~ a ++ a0) inverts Hu.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IHa: uniq (a0 ++ Γ2) -> uniq a0
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset (a0 ++ Γ2)
uniq (x ~ a ++ a0)
      autorewrite with tea_rw_dom in *.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IHa: uniq (a0 ++ Γ2) -> uniq a0
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset a0 /\ x `notin` domset Γ2
uniq (x ~ a ++ a0)
      constructor; tauto.
  Qed.

  Lemma uniq_app2 :
      uniq (Γ1 ++ Γ2) ->
      uniq Γ2.A, B: Type
Γ1, Γ2: alist A
uniq (Γ1 ++ Γ2) -> uniq Γ2
  Proof.A, B: Type
Γ1, Γ2: alist A
uniq (Γ1 ++ Γ2) -> uniq Γ2
    introv Hu.A, B: Type
Γ1, Γ2: alist A
Hu: uniq (Γ1 ++ Γ2)
uniq Γ2 alist induction Γ1.A, B: Type
Γ1, Γ2: alist A
Hu: uniq ([] ++ Γ2)
uniq Γ2
A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
Hu: uniq ((x ~ a ++ a0) ++ Γ2)
IHa: uniq (a0 ++ Γ2) -> uniq Γ2
uniq Γ2
    -A, B: Type
Γ1, Γ2: alist A
Hu: uniq ([] ++ Γ2)
uniq Γ2 trivial.
    -A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
Hu: uniq ((x ~ a ++ a0) ++ Γ2)
IHa: uniq (a0 ++ Γ2) -> uniq Γ2
uniq Γ2 inverts Hu.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IHa: uniq (a0 ++ Γ2) -> uniq Γ2
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset (a0 ++ Γ2)
uniq Γ2 auto.
  Qed.

  Lemma uniq_app_3 :
      uniq (Γ1 ++ Γ2) ->
      disjoint Γ1 Γ2.A, B: Type
Γ1, Γ2: alist A
uniq (Γ1 ++ Γ2) -> disjoint Γ1 Γ2
  Proof.A, B: Type
Γ1, Γ2: alist A
uniq (Γ1 ++ Γ2) -> disjoint Γ1 Γ2
    introv Hu.A, B: Type
Γ1, Γ2: alist A
Hu: uniq (Γ1 ++ Γ2)
disjoint Γ1 Γ2 unfold disjoint.A, B: Type
Γ1, Γ2: alist A
Hu: uniq (Γ1 ++ Γ2)
domset Γ1 ∩ domset Γ2 [=] ∅ alist induction Γ1 as [| ? ? ? IH].A, B: Type
Γ1, Γ2: alist A
Hu: uniq ([] ++ Γ2)
domset [] ∩ domset Γ2 [=] ∅
A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
Hu: uniq ((x ~ a ++ a0) ++ Γ2)
IH: uniq (a0 ++ Γ2) -> domset a0 ∩ domset Γ2 [=] ∅
domset (x ~ a ++ a0) ∩ domset Γ2 [=] ∅
    -A, B: Type
Γ1, Γ2: alist A
Hu: uniq ([] ++ Γ2)
domset [] ∩ domset Γ2 [=] ∅ fsetdec.
    -A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
Hu: uniq ((x ~ a ++ a0) ++ Γ2)
IH: uniq (a0 ++ Γ2) -> domset a0 ∩ domset Γ2 [=] ∅
domset (x ~ a ++ a0) ∩ domset Γ2 [=] ∅ inverts Hu.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IH: uniq (a0 ++ Γ2) -> domset a0 ∩ domset Γ2 [=] ∅
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset (a0 ++ Γ2)
domset (x ~ a ++ a0) ∩ domset Γ2 [=] ∅ autorewrite with tea_rw_dom in *.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IH: uniq (a0 ++ Γ2) -> domset a0 ∩ domset Γ2 [=] ∅
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset a0 /\ x `notin` domset Γ2
({{x}} ∪ domset a0) ∩ domset Γ2 [=] ∅
      lapply IH.A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IH: uniq (a0 ++ Γ2) -> domset a0 ∩ domset Γ2 [=] ∅
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset a0 /\ x `notin` domset Γ2
domset a0 ∩ domset Γ2 [=] ∅ ->
({{x}} ∪ domset a0) ∩ domset Γ2 [=] ∅
A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IH: uniq (a0 ++ Γ2) -> domset a0 ∩ domset Γ2 [=] ∅
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset a0 /\ x `notin` domset Γ2
uniq (a0 ++ Γ2)
      +A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IH: uniq (a0 ++ Γ2) -> domset a0 ∩ domset Γ2 [=] ∅
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset a0 /\ x `notin` domset Γ2
domset a0 ∩ domset Γ2 [=] ∅ ->
({{x}} ∪ domset a0) ∩ domset Γ2 [=] ∅ fsetdec.
      +A, B: Type
Γ1, Γ2: alist A
x: atom
a: A
a0: alist A
IH: uniq (a0 ++ Γ2) -> domset a0 ∩ domset Γ2 [=] ∅
H1: uniq (a0 ++ Γ2)
H3: x `notin` domset a0 /\ x `notin` domset Γ2
uniq (a0 ++ Γ2) auto.
  Qed.

  Lemma uniq_app_4 : forall C (Γx : alist C) (Γy : alist C),
      uniq Γx ->
      uniq Γy ->
      disjoint Γx Γy ->
      uniq (Γx ++ Γy).A, B: Type
Γ1, Γ2: alist A
forall (C : Type) (Γx Γy : alist C),
uniq Γx ->
uniq Γy -> disjoint Γx Γy -> uniq (Γx ++ Γy)
  Proof.A, B: Type
Γ1, Γ2: alist A
forall (C : Type) (Γx Γy : alist C),
uniq Γx ->
uniq Γy -> disjoint Γx Γy -> uniq (Γx ++ Γy)
    intros.A, B: Type
Γ1, Γ2: alist A
C: Type
Γx, Γy: alist C
H: uniq Γx
H0: uniq Γy
H1: disjoint Γx Γy
uniq (Γx ++ Γy) alist induction Γx as [| ? ? Γz ?].A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
H: uniq []
H0: uniq Γy
H1: disjoint [] Γy
uniq ([] ++ Γy)
A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H: uniq (x ~ a ++ Γz)
H0: uniq Γy
H1: disjoint (x ~ a ++ Γz) Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
uniq ((x ~ a ++ Γz) ++ Γy)
    -A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
H: uniq []
H0: uniq Γy
H1: disjoint [] Γy
uniq ([] ++ Γy) cbn.A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
H: uniq []
H0: uniq Γy
H1: disjoint [] Γy
uniq Γy assumption.
    -A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H: uniq (x ~ a ++ Γz)
H0: uniq Γy
H1: disjoint (x ~ a ++ Γz) Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
uniq ((x ~ a ++ Γz) ++ Γy) change_alist (x ~ a ++ (Γz ++ Γy)).A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H: uniq (x ~ a ++ Γz)
H0: uniq Γy
H1: disjoint (x ~ a ++ Γz) Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
uniq (x ~ a ++ Γz ++ Γy)
      inverts H.A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H0: uniq Γy
H1: disjoint (x ~ a ++ Γz) Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
H4: uniq Γz
H6: x `notin` domset Γz
uniq (x ~ a ++ Γz ++ Γy) autorewrite with tea_rw_disj in *.A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H0: uniq Γy
H1: x `notin` domset Γy /\ disjoint Γz Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
H4: uniq Γz
H6: x `notin` domset Γz
uniq (x ~ a ++ Γz ++ Γy) constructor.A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H0: uniq Γy
H1: x `notin` domset Γy /\ disjoint Γz Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
H4: uniq Γz
H6: x `notin` domset Γz
uniq (Γz ++ Γy)
A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H0: uniq Γy
H1: x `notin` domset Γy /\ disjoint Γz Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
H4: uniq Γz
H6: x `notin` domset Γz
x `notin` domset (Γz ++ Γy)
      +A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H0: uniq Γy
H1: x `notin` domset Γy /\ disjoint Γz Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
H4: uniq Γz
H6: x `notin` domset Γz
uniq (Γz ++ Γy) tauto.
      +A, B: Type
Γ1, Γ2: alist A
C: Type
Γy: alist C
x: atom
a: C
Γz: alist C
H0: uniq Γy
H1: x `notin` domset Γy /\ disjoint Γz Γy
IHΓx: uniq Γz -> disjoint Γz Γy -> uniq (Γz ++ Γy)
H4: uniq Γz
H6: x `notin` domset Γz
x `notin` domset (Γz ++ Γy) now autorewrite with tea_rw_dom.
  Qed.

  Lemma uniq_app_5 : forall x a Γ,
      uniq (x ~ a ++ Γ) ->
      ~ x `in` domset Γ.A, B: Type
Γ1, Γ2: alist A
forall x a (Γ : list (atom * A)),
uniq (x ~ a ++ Γ) -> x `notin` domset Γ
  Proof.A, B: Type
Γ1, Γ2: alist A
forall x a (Γ : list (atom * A)),
uniq (x ~ a ++ Γ) -> x `notin` domset Γ
    now inversion 1.
  Qed.

  (* For some reason, [uniq_app_4] will not be applied
     by auto on this goal. *)
  Lemma uniq_symm :
      uniq (Γ1 ++ Γ2) ->
      uniq (Γ2 ++ Γ1).A, B: Type
Γ1, Γ2: alist A
uniq (Γ1 ++ Γ2) -> uniq (Γ2 ++ Γ1)
  Proof.A, B: Type
Γ1, Γ2: alist A
uniq (Γ1 ++ Γ2) -> uniq (Γ2 ++ Γ1)
    intros.A, B: Type
Γ1, Γ2: alist A
H: uniq (Γ1 ++ Γ2)
uniq (Γ2 ++ Γ1) eapply uniq_app_4.A, B: Type
Γ1, Γ2: alist A
H: uniq (Γ1 ++ Γ2)
uniq Γ2
A, B: Type
Γ1, Γ2: alist A
H: uniq (Γ1 ++ Γ2)
uniq Γ1
A, B: Type
Γ1, Γ2: alist A
H: uniq (Γ1 ++ Γ2)
disjoint Γ2 Γ1
    all: eauto using uniq_app_4, uniq_app2,
         uniq_app1, uniq_app_3, disjoint_sym1.
  Qed.

  Lemma uniq_envmap1 : forall (f : A -> B),
      uniq (envmap f Γ1) ->
      uniq Γ1.A, B: Type
Γ1, Γ2: alist A
forall f : A -> B, uniq (envmap f Γ1) -> uniq Γ1
  Proof.A, B: Type
Γ1, Γ2: alist A
forall f : A -> B, uniq (envmap f Γ1) -> uniq Γ1
    introv Hu.A, B: Type
Γ1, Γ2: alist A
f: A -> B
Hu: uniq (envmap f Γ1)
uniq Γ1 alist induction Γ1.A, B: Type
Γ1, Γ2: alist A
f: A -> B
Hu: uniq (envmap f [])
uniq []
A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
Hu: uniq (envmap f (x ~ a ++ a0))
IHa: uniq (envmap f a0) -> uniq a0
uniq (x ~ a ++ a0)
    -A, B: Type
Γ1, Γ2: alist A
f: A -> B
Hu: uniq (envmap f [])
uniq [] constructor.
    -A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
Hu: uniq (envmap f (x ~ a ++ a0))
IHa: uniq (envmap f a0) -> uniq a0
uniq (x ~ a ++ a0) autorewrite with tea_rw_envmap in *.A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
Hu: uniq (x ~ f a ++ envmap f a0)
IHa: uniq (envmap f a0) -> uniq a0
uniq (x ~ a ++ a0) inverts Hu.A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq (envmap f a0) -> uniq a0
H1: uniq (envmap f a0)
H3: x `notin` domset (envmap f a0)
uniq (x ~ a ++ a0)
      constructor.A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq (envmap f a0) -> uniq a0
H1: uniq (envmap f a0)
H3: x `notin` domset (envmap f a0)
uniq a0
A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq (envmap f a0) -> uniq a0
H1: uniq (envmap f a0)
H3: x `notin` domset (envmap f a0)
x `notin` domset a0
      +A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq (envmap f a0) -> uniq a0
H1: uniq (envmap f a0)
H3: x `notin` domset (envmap f a0)
uniq a0 auto.
      +A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq (envmap f a0) -> uniq a0
H1: uniq (envmap f a0)
H3: x `notin` domset (envmap f a0)
x `notin` domset a0 now autorewrite with tea_rw_dom in *.
  Qed.

  Lemma uniq_envmap2 : forall (f : A -> B),
      uniq Γ1 ->
      uniq (envmap f Γ1).A, B: Type
Γ1, Γ2: alist A
forall f : A -> B, uniq Γ1 -> uniq (envmap f Γ1)
  Proof.A, B: Type
Γ1, Γ2: alist A
forall f : A -> B, uniq Γ1 -> uniq (envmap f Γ1)
    introv Hu.A, B: Type
Γ1, Γ2: alist A
f: A -> B
Hu: uniq Γ1
uniq (envmap f Γ1) alist induction Γ1.A, B: Type
Γ1, Γ2: alist A
f: A -> B
Hu: uniq []
uniq (envmap f [])
A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
Hu: uniq (x ~ a ++ a0)
IHa: uniq a0 -> uniq (envmap f a0)
uniq (envmap f (x ~ a ++ a0))
    -A, B: Type
Γ1, Γ2: alist A
f: A -> B
Hu: uniq []
uniq (envmap f []) constructor.
    -A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
Hu: uniq (x ~ a ++ a0)
IHa: uniq a0 -> uniq (envmap f a0)
uniq (envmap f (x ~ a ++ a0)) autorewrite with tea_rw_envmap.A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
Hu: uniq (x ~ a ++ a0)
IHa: uniq a0 -> uniq (envmap f a0)
uniq (x ~ f a ++ envmap f a0) inverts Hu.A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq a0 -> uniq (envmap f a0)
H1: uniq a0
H3: x `notin` domset a0
uniq (x ~ f a ++ envmap f a0)
      constructor.A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq a0 -> uniq (envmap f a0)
H1: uniq a0
H3: x `notin` domset a0
uniq (envmap f a0)
A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq a0 -> uniq (envmap f a0)
H1: uniq a0
H3: x `notin` domset a0
x `notin` domset (envmap f a0)
      +A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq a0 -> uniq (envmap f a0)
H1: uniq a0
H3: x `notin` domset a0
uniq (envmap f a0) auto.
      +A, B: Type
Γ1, Γ2: alist A
f: A -> B
x: atom
a: A
a0: alist A
IHa: uniq a0 -> uniq (envmap f a0)
H1: uniq a0
H3: x `notin` domset a0
x `notin` domset (envmap f a0) now autorewrite with tea_rw_dom in *.
  Qed.

  Lemma uniq_map1 : forall (f : A -> B),
      uniq (map (F := list ∘ prod atom) f Γ1) ->
      uniq Γ1.A, B: Type
Γ1, Γ2: alist A
forall f : A -> B, uniq (map f Γ1) -> uniq Γ1
  Proof.A, B: Type
Γ1, Γ2: alist A
forall f : A -> B, uniq (map f Γ1) -> uniq Γ1
    intros.A, B: Type
Γ1, Γ2: alist A
f: A -> B
H: uniq (map f Γ1)
uniq Γ1 eapply uniq_envmap1.A, B: Type
Γ1, Γ2: alist A
f: A -> B
H: uniq (map f Γ1)
uniq (envmap ?f Γ1) exact H.
  Qed.

  Lemma uniq_map2 : forall (f : A -> B),
      uniq Γ1 ->
      uniq (map (F := list ∘ prod atom) f Γ1).A, B: Type
Γ1, Γ2: alist A
forall f : A -> B, uniq Γ1 -> uniq (map f Γ1)
  Proof.A, B: Type
Γ1, Γ2: alist A
forall f : A -> B, uniq Γ1 -> uniq (map f Γ1)
    intros.A, B: Type
Γ1, Γ2: alist A
f: A -> B
H: uniq Γ1
uniq (map f Γ1) now apply uniq_envmap2.
  Qed.

End uniq_auto_lemmas.

#[export] Hint Resolve uniq_nil uniq_push uniq_one
 uniq_cons_3 uniq_app_3 uniq_app_4 uniq_envmap2 uniq_symm : tea_alist.

(** These introduce existential variables *)
#[export] Hint Immediate uniq_cons1
 uniq_cons2 uniq_app1 uniq_app2
 uniq_app_5 uniq_envmap1 : tea_alist.

(** ** Rewriting principles for [uniq] *)
(* *********************************************************************** *)
Section uniq_rewriting_lemmas.

  Context
    (A B : Type).

  Implicit Types (x : atom) (a : A) (b : B) (Γ : alist A).

  Lemma uniq_nil_iff :
    uniq ([] : list (atom * A)) <-> True.A, B: Type
uniq ([] : list (atom * A)) <-> True
  Proof.A, B: Type
uniq ([] : list (atom * A)) <-> True
    split; auto with tea_alist.
  Qed.

  Lemma uniq_cons_iff : forall x a Γ,
      uniq ((x, a) :: Γ) <->  ~ x `in` domset Γ /\ uniq Γ.A, B: Type
forall x a Γ,
uniq ((x, a) :: Γ) <-> x `notin` domset Γ /\ uniq Γ
  Proof.A, B: Type
forall x a Γ,
uniq ((x, a) :: Γ) <-> x `notin` domset Γ /\ uniq Γ
    split.A, B: Type
x: atom
a: A
Γ: alist A
uniq ((x, a) :: Γ) -> x `notin` domset Γ /\ uniq Γ
A, B: Type
x: atom
a: A
Γ: alist A
x `notin` domset Γ /\ uniq Γ -> uniq ((x, a) :: Γ)
    -A, B: Type
x: atom
a: A
Γ: alist A
uniq ((x, a) :: Γ) -> x `notin` domset Γ /\ uniq Γ eauto with tea_alist.
    -A, B: Type
x: atom
a: A
Γ: alist A
x `notin` domset Γ /\ uniq Γ -> uniq ((x, a) :: Γ) intuition auto with tea_alist.
  Qed.

  Lemma uniq_one_iff : forall x b,
      uniq (x ~ b) <-> True.A, B: Type
forall x b, uniq (x ~ b) <-> True
  Proof.A, B: Type
forall x b, uniq (x ~ b) <-> True
    split; auto with tea_alist.
  Qed.

  Lemma uniq_app_iff : forall Γ1 Γ2,
      uniq (Γ1 ++ Γ2) <-> uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2.A, B: Type
forall Γ1 Γ2,
uniq (Γ1 ++ Γ2) <->
uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
  Proof.A, B: Type
forall Γ1 Γ2,
uniq (Γ1 ++ Γ2) <->
uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
    intuition eauto with tea_alist.
  Qed.

  Lemma uniq_envmap_iff : forall Γ1 (f : A -> B),
      uniq (envmap f Γ1) <-> uniq Γ1.A, B: Type
forall Γ1 (f : A -> B), uniq (envmap f Γ1) <-> uniq Γ1
  Proof.A, B: Type
forall Γ1 (f : A -> B), uniq (envmap f Γ1) <-> uniq Γ1
    intuition eauto with tea_alist.
  Qed.

  Lemma uniq_map_iff : forall Γ1 (f : A -> B),
      uniq (map (F := list ∘ prod atom) f Γ1) <-> uniq Γ1.A, B: Type
forall Γ1 (f : A -> B), uniq (map f Γ1) <-> uniq Γ1
  Proof.A, B: Type
forall Γ1 (f : A -> B), uniq (map f Γ1) <-> uniq Γ1
    intros.A, B: Type
Γ1: alist A
f: A -> B
uniq (map f Γ1) <-> uniq Γ1 now rewrite uniq_envmap_iff.
  Qed.

End uniq_rewriting_lemmas.

Create HintDb tea_rw_uniq.
#[export] Hint Rewrite uniq_nil_iff uniq_cons_iff
     uniq_one_iff uniq_app_iff uniq_envmap_iff uniq_map_iff : tea_rw_uniq.

(** ** More facts about [uniq] *)
(* *********************************************************************** *)
Section uniq_theorems.

  Context
    (A : Type).

  Implicit Types (x : atom) (a b : A) (Γ : list (atom * A)).

  Lemma uniq_insert_mid : forall x a Γ1 Γ2,
    uniq (Γ1 ++ Γ2) ->
    ~ x `in` domset Γ1 ->
    ~ x `in` domset Γ2 ->
    uniq (Γ1 ++ x ~ a ++ Γ2).A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ Γ2) ->
x `notin` domset Γ1 ->
x `notin` domset Γ2 -> uniq (Γ1 ++ x ~ a ++ Γ2)
  Proof.A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ Γ2) ->
x `notin` domset Γ1 ->
x `notin` domset Γ2 -> uniq (Γ1 ++ x ~ a ++ Γ2)
    intros.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq (Γ1 ++ Γ2)
H0: x `notin` domset Γ1
H1: x `notin` domset Γ2
uniq (Γ1 ++ x ~ a ++ Γ2) autorewrite with tea_rw_uniq tea_rw_disj in *.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
H0: x `notin` domset Γ1
H1: x `notin` domset Γ2
uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
    rewrite disjoint_sym.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
H0: x `notin` domset Γ1
H1: x `notin` domset Γ2
uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ1 Γ2 intuition.
  Qed.

  Lemma uniq_remove_mid : forall Γ1 Γ2 Γ3,
    uniq (Γ1 ++ Γ3 ++ Γ2) ->
    uniq (Γ1 ++ Γ2).A: Type
forall Γ1 Γ2 Γ3,
uniq (Γ1 ++ Γ3 ++ Γ2) -> uniq (Γ1 ++ Γ2)
  Proof.A: Type
forall Γ1 Γ2 Γ3,
uniq (Γ1 ++ Γ3 ++ Γ2) -> uniq (Γ1 ++ Γ2)
    intros.A: Type
Γ1, Γ2, Γ3: list (atom * A)
H: uniq (Γ1 ++ Γ3 ++ Γ2)
uniq (Γ1 ++ Γ2)
    autorewrite with tea_rw_uniq tea_rw_disj in *.A: Type
Γ1, Γ2, Γ3: list (atom * A)
H: uniq Γ1 /\
(uniq Γ3 /\ uniq Γ2 /\ disjoint Γ3 Γ2) /\
disjoint Γ3 Γ1 /\ disjoint Γ2 Γ1
uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
    unfold disjoint.A: Type
Γ1, Γ2, Γ3: list (atom * A)
H: uniq Γ1 /\
(uniq Γ3 /\ uniq Γ2 /\ disjoint Γ3 Γ2) /\
disjoint Γ3 Γ1 /\ disjoint Γ2 Γ1
uniq Γ1 /\ uniq Γ2 /\ domset Γ1 ∩ domset Γ2 [=] ∅ intuition.A: Type
Γ1, Γ2, Γ3: list (atom * A)
H0: uniq Γ1
H1: uniq Γ3
H: disjoint Γ3 Γ1
H4: disjoint Γ2 Γ1
H2: uniq Γ2
H5: disjoint Γ3 Γ2
domset Γ1 ∩ domset Γ2 [=] ∅
    now rewrite disjoint_sym in H4.
  Qed.

  Lemma uniq_reorder1 : forall Γ1 Γ2,
    uniq (Γ1 ++ Γ2) ->
    uniq (Γ2 ++ Γ1).A: Type
forall Γ1 Γ2, uniq (Γ1 ++ Γ2) -> uniq (Γ2 ++ Γ1)
  Proof.A: Type
forall Γ1 Γ2, uniq (Γ1 ++ Γ2) -> uniq (Γ2 ++ Γ1)
    intros.A: Type
Γ1, Γ2: list (atom * A)
H: uniq (Γ1 ++ Γ2)
uniq (Γ2 ++ Γ1) now apply uniq_symm.
  Qed.

  Lemma uniq_reorder2 : forall Γ1 Γ2 Γ3,
    uniq (Γ1 ++ Γ3 ++ Γ2) ->
    uniq (Γ1 ++ Γ2 ++ Γ3).A: Type
forall Γ1 Γ2 Γ3,
uniq (Γ1 ++ Γ3 ++ Γ2) -> uniq (Γ1 ++ Γ2 ++ Γ3)
  Proof.A: Type
forall Γ1 Γ2 Γ3,
uniq (Γ1 ++ Γ3 ++ Γ2) -> uniq (Γ1 ++ Γ2 ++ Γ3)
    intros.A: Type
Γ1, Γ2, Γ3: list (atom * A)
H: uniq (Γ1 ++ Γ3 ++ Γ2)
uniq (Γ1 ++ Γ2 ++ Γ3) autorewrite with tea_rw_uniq tea_rw_disj in *.A: Type
Γ1, Γ2, Γ3: list (atom * A)
H: uniq Γ1 /\
(uniq Γ3 /\ uniq Γ2 /\ disjoint Γ3 Γ2) /\
disjoint Γ3 Γ1 /\ disjoint Γ2 Γ1
uniq Γ1 /\
(uniq Γ2 /\ uniq Γ3 /\ disjoint Γ2 Γ3) /\
disjoint Γ2 Γ1 /\ disjoint Γ3 Γ1
    unfold disjoint.A: Type
Γ1, Γ2, Γ3: list (atom * A)
H: uniq Γ1 /\
(uniq Γ3 /\ uniq Γ2 /\ disjoint Γ3 Γ2) /\
disjoint Γ3 Γ1 /\ disjoint Γ2 Γ1
uniq Γ1 /\
(uniq Γ2 /\ uniq Γ3 /\ domset Γ2 ∩ domset Γ3 [=] ∅) /\
domset Γ2 ∩ domset Γ1 [=] ∅ /\
domset Γ3 ∩ domset Γ1 [=] ∅ rewrite <- (disjoint_sym _ _ Γ2 Γ3) in *.A: Type
Γ1, Γ2, Γ3: list (atom * A)
H: uniq Γ1 /\
(uniq Γ3 /\ uniq Γ2 /\ disjoint Γ2 Γ3) /\
disjoint Γ3 Γ1 /\ disjoint Γ2 Γ1
uniq Γ1 /\
(uniq Γ2 /\ uniq Γ3 /\ domset Γ2 ∩ domset Γ3 [=] ∅) /\
domset Γ2 ∩ domset Γ1 [=] ∅ /\
domset Γ3 ∩ domset Γ1 [=] ∅
    intuition.
  Qed.

  Lemma uniq_map_app_l : forall Γ1 Γ2 (f : A -> A),
    uniq (Γ1 ++ Γ2) ->
    uniq (envmap f Γ1 ++ Γ2).A: Type
forall Γ1 Γ2 (f : A -> A),
uniq (Γ1 ++ Γ2) -> uniq (envmap f Γ1 ++ Γ2)
  Proof.A: Type
forall Γ1 Γ2 (f : A -> A),
uniq (Γ1 ++ Γ2) -> uniq (envmap f Γ1 ++ Γ2)
    intros.A: Type
Γ1, Γ2: list (atom * A)
f: A -> A
H: uniq (Γ1 ++ Γ2)
uniq (envmap f Γ1 ++ Γ2) autorewrite with tea_rw_uniq tea_rw_disj in *.A: Type
Γ1, Γ2: list (atom * A)
f: A -> A
H: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
    tauto.
  Qed.

  Lemma fresh_mid_tail : forall x a Γ1 Γ2,
    uniq (Γ1 ++ x ~ a ++ Γ2) ->
    ~ x `in` domset Γ2.A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ x ~ a ++ Γ2) -> x `notin` domset Γ2
  Proof.A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ x ~ a ++ Γ2) -> x `notin` domset Γ2
    intros.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq (Γ1 ++ x ~ a ++ Γ2)
x `notin` domset Γ2 autorewrite with tea_rw_uniq tea_rw_disj in *.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
x `notin` domset Γ2
    tauto.
  Qed.

  Lemma fresh_mid_head : forall x a Γ1 Γ2,
    uniq (Γ1 ++ x ~ a ++ Γ2) ->
    ~ x `in` domset Γ1.A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ x ~ a ++ Γ2) -> x `notin` domset Γ1
  Proof.A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ x ~ a ++ Γ2) -> x `notin` domset Γ1
    intros.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq (Γ1 ++ x ~ a ++ Γ2)
x `notin` domset Γ1 autorewrite with tea_rw_uniq tea_rw_disj in *.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
x `notin` domset Γ1
    tauto.
  Qed.

End uniq_theorems.

(** ** Stronger theorems for <<∈>> on [uniq] lists *)
(******************************************************************************)
Section in_theorems_uniq.

  Context
    (A B : Type).

  Implicit Types (x : atom) (a : A) (b : B).

  Lemma in_app_uniq_iff : forall x a Γ1 Γ2,
      uniq (Γ1 ++ Γ2) ->
      (x, a) ∈ (Γ1 ++ Γ2) <->
      ((x, a) ∈ Γ1 /\ ~ x `in` domset Γ2) \/
      ((x, a) ∈ Γ2 /\ ~ x `in` domset Γ1).A, B: Type
forall x a (Γ1 Γ2 : list (atom * A)),
uniq (Γ1 ++ Γ2) ->
(x, a) ∈ (Γ1 ++ Γ2) <->
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1
  Proof.A, B: Type
forall x a (Γ1 Γ2 : list (atom * A)),
uniq (Γ1 ++ Γ2) ->
(x, a) ∈ (Γ1 ++ Γ2) <->
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1
    introv H.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq (Γ1 ++ Γ2)
(x, a) ∈ (Γ1 ++ Γ2) <->
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1 autorewrite with tea_rw_uniq tea_rw_in in *.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2 <->
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1
    destructs H.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2 <->
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1 split.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2 ->
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1
A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1 ->
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2
    -A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2 ->
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1 intros [inΓ1|inΓ2].A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ1: (x, a) ∈ Γ1
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1
A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ2: (x, a) ∈ Γ2
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1
      +A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ1: (x, a) ∈ Γ1
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1 left.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ1: (x, a) ∈ Γ1
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 split.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ1: (x, a) ∈ Γ1
(x, a) ∈ Γ1
A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ1: (x, a) ∈ Γ1
x `notin` domset Γ2
        *A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ1: (x, a) ∈ Γ1
(x, a) ∈ Γ1 auto.
        *A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ1: (x, a) ∈ Γ1
x `notin` domset Γ2 eauto using disjoint_dom1 with tea_alist.
      +A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ2: (x, a) ∈ Γ2
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1 right.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ2: (x, a) ∈ Γ2
(x, a) ∈ Γ2 /\ x `notin` domset Γ1 split.A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ2: (x, a) ∈ Γ2
(x, a) ∈ Γ2
A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ2: (x, a) ∈ Γ2
x `notin` domset Γ1
        *A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ2: (x, a) ∈ Γ2
(x, a) ∈ Γ2 auto.
        *A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
inΓ2: (x, a) ∈ Γ2
x `notin` domset Γ1 eauto using disjoint_dom1 with tea_alist.
    -A, B: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H0: uniq Γ2
H1: disjoint Γ1 Γ2
(x, a) ∈ Γ1 /\ x `notin` domset Γ2 \/
(x, a) ∈ Γ2 /\ x `notin` domset Γ1 ->
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2 tauto.
  Qed.

  Lemma in_cons_uniq_iff : forall x y (a b : A) Γ,
    uniq ((y, b) :: Γ) ->
    (x, a) ∈ ((y, b) :: Γ) <->
     (x = y /\ a = b /\ ~ x `in` domset Γ) \/
     ((x, a) ∈ Γ /\ x <> y).A, B: Type
forall (x y : atom) (a b : A) (Γ : list (atom * A)),
uniq ((y, b) :: Γ) ->
(x, a) ∈ ((y, b) :: Γ) <->
x = y /\ a = b /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x <> y
  Proof.A, B: Type
forall (x y : atom) (a b : A) (Γ : list (atom * A)),
uniq ((y, b) :: Γ) ->
(x, a) ∈ ((y, b) :: Γ) <->
x = y /\ a = b /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x <> y
    introv.A, B: Type
x, y: atom
a, b: A
Γ: list (atom * A)
uniq ((y, b) :: Γ) ->
(x, a) ∈ ((y, b) :: Γ) <->
x = y /\ a = b /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x <> y change_alist (y ~ b ++ Γ).A, B: Type
x, y: atom
a, b: A
Γ: list (atom * A)
uniq (y ~ b ++ Γ) ->
(x, a) ∈ (y ~ b ++ Γ) <->
x = y /\ a = b /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x <> y
    intro.A, B: Type
x, y: atom
a, b: A
Γ: list (atom * A)
H: uniq (y ~ b ++ Γ)
(x, a) ∈ (y ~ b ++ Γ) <->
x = y /\ a = b /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x <> y rewrite in_app_uniq_iff; auto.A, B: Type
x, y: atom
a, b: A
Γ: list (atom * A)
H: uniq (y ~ b ++ Γ)
(x, a) ∈ (y ~ b) /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x `notin` domset (y ~ b) <->
x = y /\ a = b /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x <> y
    autorewrite with tea_rw_in tea_rw_dom.A, B: Type
x, y: atom
a, b: A
Γ: list (atom * A)
H: uniq (y ~ b ++ Γ)
(x = y /\ a = b) /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x <> y <->
x = y /\ a = b /\ x `notin` domset Γ \/
(x, a) ∈ Γ /\ x <> y
    tauto.
  Qed.

End in_theorems_uniq.

(** * Facts about [binds] *)
(* *********************************************************************** *)
Section binds_theorems.

  Context
    (A : Type).

  Implicit Types
    (x y : atom)
    (a b : A)
    (Γ : list (atom * A)).

  Lemma in_decide : forall x a Γ,
    (forall a b : A, {a = b} + {a <> b}) ->
    {(x, a) ∈ Γ} + {~ (x, a) ∈ Γ}.A: Type
forall x a Γ,
(forall a0 b, {a0 = b} + {a0 <> b}) ->
{(x, a) ∈ Γ} + {~ (x, a) ∈ Γ}
  Proof.A: Type
forall x a Γ,
(forall a0 b, {a0 = b} + {a0 <> b}) ->
{(x, a) ∈ Γ} + {~ (x, a) ∈ Γ}
    clear.A: Type
forall x a Γ,
(forall a0 b, {a0 = b} + {a0 <> b}) ->
{(x, a) ∈ Γ} + {~ (x, a) ∈ Γ} intros.A: Type
x: atom
a: A
Γ: list (atom * A)
X: forall a b, {a = b} + {a <> b}
{(x, a) ∈ Γ} + {~ (x, a) ∈ Γ} alist induction Γ.A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
{(x, a) ∈ []} + {~ (x, a) ∈ []}
A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
IHΓ: {(x, a) ∈ xs} + {~ (x, a) ∈ xs}
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)}
    -A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
{(x, a) ∈ []} + {~ (x, a) ∈ []} right.A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
~ (x, a) ∈ [] auto.
    -A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
IHΓ: {(x, a) ∈ xs} + {~ (x, a) ∈ xs}
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)} destruct IHΓ.A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
e: (x, a) ∈ xs
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)}
A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)}
      +A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
e: (x, a) ∈ xs
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)} left.A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
e: (x, a) ∈ xs
(x, a) ∈ (x0 ~ a0 ++ xs) simpl_list.A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
e: (x, a) ∈ xs
(x, a) = (x0, a0) \/ (x, a) ∈ xs now right.
      +A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)} compare values x and x0.A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
{(x0, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x0, a) ∈ (x0 ~ a0 ++ xs)}
A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)}
        {A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
{(x0, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x0, a) ∈ (x0 ~ a0 ++ xs)} destruct (X a a0); subst.A: Type
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a0) ∈ xs
DESTR_EQs: x0 = x0
{(x0, a0) ∈ (x0 ~ a0 ++ xs)} +
{~ (x0, a0) ∈ (x0 ~ a0 ++ xs)}
A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
n0: a <> a0
{(x0, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x0, a) ∈ (x0 ~ a0 ++ xs)}
          -A: Type
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a0) ∈ xs
DESTR_EQs: x0 = x0
{(x0, a0) ∈ (x0 ~ a0 ++ xs)} +
{~ (x0, a0) ∈ (x0 ~ a0 ++ xs)} left.A: Type
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a0) ∈ xs
DESTR_EQs: x0 = x0
(x0, a0) ∈ (x0 ~ a0 ++ xs) now left.
          -A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
n0: a <> a0
{(x0, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x0, a) ∈ (x0 ~ a0 ++ xs)} right.A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
n0: a <> a0
~ (x0, a) ∈ (x0 ~ a0 ++ xs) simpl_list.A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
n0: a <> a0
~ ((x0, a) = (x0, a0) \/ (x0, a) ∈ xs) intros [hyp|hyp].A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
n0: a <> a0
hyp: (x0, a) = (x0, a0)
False
A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
n0: a <> a0
hyp: (x0, a) ∈ xs
False
            inversion hyp; contradiction.A: Type
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x0, a) ∈ xs
DESTR_EQs: x0 = x0
n0: a <> a0
hyp: (x0, a) ∈ xs
False contradiction. }A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)}
        {A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
{(x, a) ∈ (x0 ~ a0 ++ xs)} +
{~ (x, a) ∈ (x0 ~ a0 ++ xs)} right.A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
~ (x, a) ∈ (x0 ~ a0 ++ xs) intros [hyp|hyp].A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
hyp: (x0, a0) = (x, a)
False
A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
hyp: ToSubset_list (atom * A) ([] ++ xs) (x, a)
False
          inversion hyp; contradiction.A: Type
x: atom
a: A
X: forall a b, {a = b} + {a <> b}
x0: atom
a0: A
xs: alist A
n: ~ (x, a) ∈ xs
DESTR_NEQ: x <> x0
DESTR_NEQs: x0 <> x
hyp: ToSubset_list (atom * A) ([] ++ xs) (x, a)
False contradiction. }
  Defined.

  Lemma in_lookup : forall x Γ,
    {a : A | (x, a) ∈ Γ} + (forall a, ~ (x, a) ∈ Γ).A: Type
forall x Γ,
{a : A | (x, a) ∈ Γ} + (forall a, ~ (x, a) ∈ Γ)
  Proof.A: Type
forall x Γ,
{a : A | (x, a) ∈ Γ} + (forall a, ~ (x, a) ∈ Γ)
    clear.A: Type
forall x Γ,
{a : A | (x, a) ∈ Γ} + (forall a, ~ (x, a) ∈ Γ) intros.A: Type
x: atom
Γ: list (atom * A)
{a : A | (x, a) ∈ Γ} + (forall a, ~ (x, a) ∈ Γ) induction Γ.A: Type
x: atom
{a : A | (x, a) ∈ []} + (forall a, ~ (x, a) ∈ [])
A: Type
x: atom
a: atom * A
Γ: list (atom * A)
IHΓ: {a : A | (x, a) ∈ Γ} + (forall a, ~ (x, a) ∈ Γ)
{a0 : A | (x, a0) ∈ (a :: Γ)} +
(forall a0, ~ (x, a0) ∈ (a :: Γ))
    -A: Type
x: atom
{a : A | (x, a) ∈ []} + (forall a, ~ (x, a) ∈ []) simpl_list; cbn; now right.
    -A: Type
x: atom
a: atom * A
Γ: list (atom * A)
IHΓ: {a : A | (x, a) ∈ Γ} + (forall a, ~ (x, a) ∈ Γ)
{a0 : A | (x, a0) ∈ (a :: Γ)} +
(forall a0, ~ (x, a0) ∈ (a :: Γ)) destruct a as [y a].A: Type
x, y: atom
a: A
Γ: list (atom * A)
IHΓ: {a : A | (x, a) ∈ Γ} + (forall a, ~ (x, a) ∈ Γ)
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ)) destruct IHΓ.A: Type
x, y: atom
a: A
Γ: list (atom * A)
s: {a : A | (x, a) ∈ Γ}
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ))
A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ))
      +A: Type
x, y: atom
a: A
Γ: list (atom * A)
s: {a : A | (x, a) ∈ Γ}
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ)) destruct s.A: Type
x, y: atom
a: A
Γ: list (atom * A)
x0: A
e: (x, x0) ∈ Γ
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ)) left.A: Type
x, y: atom
a: A
Γ: list (atom * A)
x0: A
e: (x, x0) ∈ Γ
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} eexists.A: Type
x, y: atom
a: A
Γ: list (atom * A)
x0: A
e: (x, x0) ∈ Γ
(x, ?a) ∈ ((y, a) :: Γ) right.A: Type
x, y: atom
a: A
Γ: list (atom * A)
x0: A
e: (x, x0) ∈ Γ
ToSubset_list (atom * A) Γ (x, ?a) eauto.
      +A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ)) compare values x and y.A: Type
y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (y, a) ∈ Γ
DESTR_EQs: y = y
{a0 : A | (y, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (y, a0) ∈ ((y, a) :: Γ))
A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ))
        {A: Type
y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (y, a) ∈ Γ
DESTR_EQs: y = y
{a0 : A | (y, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (y, a0) ∈ ((y, a) :: Γ)) left.A: Type
y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (y, a) ∈ Γ
DESTR_EQs: y = y
{a0 : A | (y, a0) ∈ ((y, a) :: Γ)} exists a.A: Type
y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (y, a) ∈ Γ
DESTR_EQs: y = y
(y, a) ∈ ((y, a) :: Γ) now left. }A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ))
        {A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
{a0 : A | (x, a0) ∈ ((y, a) :: Γ)} +
(forall a0, ~ (x, a0) ∈ ((y, a) :: Γ)) right.A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
forall a0, ~ (x, a0) ∈ ((y, a) :: Γ) introv.A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
a0: A
~ (x, a0) ∈ ((y, a) :: Γ) simpl_list.A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
a0: A
~ ((x, a0) = (y, a) \/ (x, a0) ∈ Γ)
          intros [contra|contra].A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
a0: A
contra: (x, a0) = (y, a)
False
A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
a0: A
contra: (x, a0) ∈ Γ
False
          -A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
a0: A
contra: (x, a0) = (y, a)
False inversion contra; subst.A: Type
y: atom
a: A
Γ: list (atom * A)
DESTR_NEQs, DESTR_NEQ: y <> y
n: forall a, ~ (y, a) ∈ Γ
contra: (y, a) = (y, a)
False contradiction.
          -A: Type
x, y: atom
a: A
Γ: list (atom * A)
n: forall a, ~ (x, a) ∈ Γ
DESTR_NEQ: x <> y
DESTR_NEQs: y <> x
a0: A
contra: (x, a0) ∈ Γ
False eapply n; eauto.
        }
  Defined.

  Lemma in_decidable : forall x Γ,
    decidable (exists a, (x, a) ∈ Γ).A: Type
forall x Γ, decidable (exists a, (x, a) ∈ Γ)
  Proof with intuition eauto.A: Type
forall x Γ, decidable (exists a, (x, a) ∈ Γ)
    intros.A: Type
x: atom
Γ: list (atom * A)
decidable (exists a, (x, a) ∈ Γ) unfold decidable.A: Type
x: atom
Γ: list (atom * A)
(exists a, (x, a) ∈ Γ) \/ ~ (exists a, (x, a) ∈ Γ)
    destruct (in_lookup x Γ) as [[? ?] | ?]...A: Type
x: atom
Γ: list (atom * A)
n: forall a, (x, a) ∈ Γ -> False
(exists a, (x, a) ∈ Γ) \/
((exists a, (x, a) ∈ Γ) -> False)
    right.A: Type
x: atom
Γ: list (atom * A)
n: forall a, (x, a) ∈ Γ -> False
(exists a, (x, a) ∈ Γ) -> False intros [? ?]...
  Defined.

  Lemma in_weaken1 : forall x a Γ1 Γ2 Γ3,
    (x, a) ∈ (Γ1 ++ Γ3) ->
    (x, a) ∈ (Γ1 ++ Γ2 ++ Γ3).A: Type
forall x a Γ1 Γ2 Γ3,
(x, a) ∈ (Γ1 ++ Γ3) -> (x, a) ∈ (Γ1 ++ Γ2 ++ Γ3)
  Proof.A: Type
forall x a Γ1 Γ2 Γ3,
(x, a) ∈ (Γ1 ++ Γ3) -> (x, a) ∈ (Γ1 ++ Γ2 ++ Γ3)
    clear.A: Type
forall x a Γ1 Γ2 Γ3,
(x, a) ∈ (Γ1 ++ Γ3) -> (x, a) ∈ (Γ1 ++ Γ2 ++ Γ3) intros.A: Type
x: atom
a: A
Γ1, Γ2, Γ3: list (atom * A)
H: (x, a) ∈ (Γ1 ++ Γ3)
(x, a) ∈ (Γ1 ++ Γ2 ++ Γ3) simpl_list in *.A: Type
x: atom
a: A
Γ1, Γ2, Γ3: list (atom * A)
H: (x, a) ∈ Γ1 \/ (x, a) ∈ Γ3
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2 \/ (x, a) ∈ Γ3 intuition.
  Qed.

  Lemma binds_mid_eq : forall x a b Γ1 Γ2,
    (x, a) ∈ (Γ1 ++ (x ~ b) ++ Γ2) ->
    uniq (Γ1 ++ (x ~ b) ++ Γ2) ->
    a = b.A: Type
forall x a b Γ1 Γ2,
(x, a) ∈ (Γ1 ++ x ~ b ++ Γ2) ->
uniq (Γ1 ++ x ~ b ++ Γ2) -> a = b
  Proof.A: Type
forall x a b Γ1 Γ2,
(x, a) ∈ (Γ1 ++ x ~ b ++ Γ2) ->
uniq (Γ1 ++ x ~ b ++ Γ2) -> a = b
    introv J ?.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
J: (x, a) ∈ (Γ1 ++ x ~ b ++ Γ2)
H: uniq (Γ1 ++ x ~ b ++ Γ2)
a = b
    autorewrite with tea_rw_uniq tea_rw_disj in *.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
J: (x, a) ∈ (Γ1 ++ x ~ b ++ Γ2)
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b
    simpl_list in *.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
J: (x, a) ∈ Γ1 \/ (x, a) = (x, b) \/ (x, a) ∈ Γ2
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b destruct J.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ1
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b
A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) = (x, b) \/ (x, a) ∈ Γ2
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b
    -A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ1
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b intuition.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ1
H1: uniq Γ1
H2: True
H: x `in` domset Γ1 -> False
H5: disjoint Γ2 Γ1
H3: uniq Γ2
H6: x `in` domset Γ2 -> False
a = b contradiction H.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ1
H1: uniq Γ1
H2: True
H: x `in` domset Γ1 -> False
H5: disjoint Γ2 Γ1
H3: uniq Γ2
H6: x `in` domset Γ2 -> False
x `in` domset Γ1 rewrite in_domset_iff.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ1
H1: uniq Γ1
H2: True
H: x `in` domset Γ1 -> False
H5: disjoint Γ2 Γ1
H3: uniq Γ2
H6: x `in` domset Γ2 -> False
exists a, (x, a) ∈ Γ1 eauto.
    -A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) = (x, b) \/ (x, a) ∈ Γ2
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b destruct H0; subst.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) = (x, b)
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b
A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ2
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b
      +A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) = (x, b)
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b now inversion H0.
      +A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ2
H: uniq Γ1 /\
(True /\ uniq Γ2 /\ x `notin` domset Γ2) /\
x `notin` domset Γ1 /\ disjoint Γ2 Γ1
a = b intuition.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ2
H1: uniq Γ1
H2: True
H: x `in` domset Γ1 -> False
H5: disjoint Γ2 Γ1
H3: uniq Γ2
H6: x `in` domset Γ2 -> False
a = b contradiction H6.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ2
H1: uniq Γ1
H2: True
H: x `in` domset Γ1 -> False
H5: disjoint Γ2 Γ1
H3: uniq Γ2
H6: x `in` domset Γ2 -> False
x `in` domset Γ2 rewrite in_domset_iff.A: Type
x: atom
a, b: A
Γ1, Γ2: list (atom * A)
H0: (x, a) ∈ Γ2
H1: uniq Γ1
H2: True
H: x `in` domset Γ1 -> False
H5: disjoint Γ2 Γ1
H3: uniq Γ2
H6: x `in` domset Γ2 -> False
exists a, (x, a) ∈ Γ2 eauto.
  Qed.

  Lemma binds_remove_mid : forall x y a b Γ1 Γ2,
    (x, a) ∈ (Γ1 ++ (y ~ b) ++ Γ2) ->
    x <> y ->
    (x, a) ∈ (Γ1 ++ Γ2).A: Type
forall x y a b Γ1 Γ2,
(x, a) ∈ (Γ1 ++ y ~ b ++ Γ2) ->
x <> y -> (x, a) ∈ (Γ1 ++ Γ2)
  Proof.A: Type
forall x y a b Γ1 Γ2,
(x, a) ∈ (Γ1 ++ y ~ b ++ Γ2) ->
x <> y -> (x, a) ∈ (Γ1 ++ Γ2)
    introv J.A: Type
x, y: atom
a, b: A
Γ1, Γ2: list (atom * A)
J: (x, a) ∈ (Γ1 ++ y ~ b ++ Γ2)
x <> y -> (x, a) ∈ (Γ1 ++ Γ2) simpl_list in *.A: Type
x, y: atom
a, b: A
Γ1, Γ2: list (atom * A)
J: (x, a) ∈ Γ1 \/ (x, a) = (y, b) \/ (x, a) ∈ Γ2
x <> y -> (x, a) ∈ Γ1 \/ (x, a) ∈ Γ2
    intros.A: Type
x, y: atom
a, b: A
Γ1, Γ2: list (atom * A)
J: (x, a) ∈ Γ1 \/ (x, a) = (y, b) \/ (x, a) ∈ Γ2
H: x <> y
(x, a) ∈ Γ1 \/ (x, a) ∈ Γ2 intuition (preprocess; easy).
  Qed.

  Lemma in_unique : forall x a b Γ,
    (x, a) ∈ Γ ->
    (x, b) ∈ Γ ->
    uniq Γ ->
    a = b.A: Type
forall x a b Γ,
(x, a) ∈ Γ -> (x, b) ∈ Γ -> uniq Γ -> a = b
  Proof.A: Type
forall x a b Γ,
(x, a) ∈ Γ -> (x, b) ∈ Γ -> uniq Γ -> a = b
    introv hyp1 hyp2 Hu.A: Type
x: atom
a, b: A
Γ: list (atom * A)
hyp1: (x, a) ∈ Γ
hyp2: (x, b) ∈ Γ
Hu: uniq Γ
a = b alist induction Γ as [ | ? ? Γ' IH ].A: Type
x: atom
a, b: A
hyp1: (x, a) ∈ []
hyp2: (x, b) ∈ []
Hu: uniq []
a = b
A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) ∈ (x0 ~ a0 ++ Γ')
hyp2: (x, b) ∈ (x0 ~ a0 ++ Γ')
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b
    -A: Type
x: atom
a, b: A
hyp1: (x, a) ∈ []
hyp2: (x, b) ∈ []
Hu: uniq []
a = b inversion hyp1.
    -A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) ∈ (x0 ~ a0 ++ Γ')
hyp2: (x, b) ∈ (x0 ~ a0 ++ Γ')
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b simpl_list in *.A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) = (x0, a0) \/ (x, a) ∈ Γ'
hyp2: (x, b) = (x0, a0) \/ (x, b) ∈ Γ'
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b destruct hyp1 as [hyp1|hyp1];
                         destruct hyp2 as [hyp2|hyp2].A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) = (x0, a0)
hyp2: (x, b) = (x0, a0)
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b
A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) = (x0, a0)
hyp2: (x, b) ∈ Γ'
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b
A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) ∈ Γ'
hyp2: (x, b) = (x0, a0)
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b
A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) ∈ Γ'
hyp2: (x, b) ∈ Γ'
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b
      +A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) = (x0, a0)
hyp2: (x, b) = (x0, a0)
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b inverts hyp1.A: Type
b: A
x0: atom
a0: A
Γ': alist A
hyp2: (x0, b) = (x0, a0)
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x0, a0) ∈ Γ' ->
(x0, b) ∈ Γ' -> uniq Γ' -> a0 = b
a0 = b now inverts hyp2.
      +A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) = (x0, a0)
hyp2: (x, b) ∈ Γ'
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b inverts hyp1.A: Type
b: A
x0: atom
a0: A
Γ': alist A
hyp2: (x0, b) ∈ Γ'
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x0, a0) ∈ Γ' ->
(x0, b) ∈ Γ' -> uniq Γ' -> a0 = b
a0 = b inverts Hu.A: Type
b: A
x0: atom
a0: A
Γ': alist A
hyp2: (x0, b) ∈ Γ'
IH: (x0, a0) ∈ Γ' ->
(x0, b) ∈ Γ' -> uniq Γ' -> a0 = b
H1: uniq Γ'
H3: x0 `notin` domset Γ'
a0 = b
        now (apply in_in_domset in hyp2).
      +A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) ∈ Γ'
hyp2: (x, b) = (x0, a0)
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b inverts hyp2.A: Type
a: A
x0: atom
a0: A
Γ': alist A
hyp1: (x0, a) ∈ Γ'
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x0, a) ∈ Γ' ->
(x0, a0) ∈ Γ' -> uniq Γ' -> a = a0
a = a0 inverts Hu.A: Type
a: A
x0: atom
a0: A
Γ': alist A
hyp1: (x0, a) ∈ Γ'
IH: (x0, a) ∈ Γ' ->
(x0, a0) ∈ Γ' -> uniq Γ' -> a = a0
H1: uniq Γ'
H3: x0 `notin` domset Γ'
a = a0
        now (apply in_in_domset in hyp1).
      +A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) ∈ Γ'
hyp2: (x, b) ∈ Γ'
Hu: uniq (x0 ~ a0 ++ Γ')
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
a = b inverts Hu.A: Type
x: atom
a, b: A
x0: atom
a0: A
Γ': alist A
hyp1: (x, a) ∈ Γ'
hyp2: (x, b) ∈ Γ'
IH: (x, a) ∈ Γ' -> (x, b) ∈ Γ' -> uniq Γ' -> a = b
H1: uniq Γ'
H3: x0 `notin` domset Γ'
a = b auto.
  Qed.

  Lemma fresh_app_l : forall x a Γ1 Γ2,
    uniq (Γ1 ++ Γ2) ->
    (x, a) ∈ Γ1 ->
    ~ x `in` (domset Γ2).A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ Γ2) -> (x, a) ∈ Γ1 -> x `notin` domset Γ2
  Proof.A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ Γ2) -> (x, a) ∈ Γ1 -> x `notin` domset Γ2
    intros.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq (Γ1 ++ Γ2)
H0: (x, a) ∈ Γ1
x `notin` domset Γ2 autorewrite with tea_rw_uniq in *.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
H0: (x, a) ∈ Γ1
x `notin` domset Γ2
    preprocess.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H1: uniq Γ2
H2: disjoint Γ1 Γ2
H0: (x, a) ∈ Γ1
x `notin` domset Γ2 apply in_in_domset in H0.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H1: uniq Γ2
H2: disjoint Γ1 Γ2
H0: x `in` domset Γ1
x `notin` domset Γ2
    eauto with tea_alist.
  Qed.

  Lemma fresh_app_r : forall x a Γ1 Γ2,
    uniq (Γ1 ++ Γ2) ->
    (x, a) ∈ Γ2 ->
    ~ x `in` domset Γ1.A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ Γ2) -> (x, a) ∈ Γ2 -> x `notin` domset Γ1
  Proof.A: Type
forall x a Γ1 Γ2,
uniq (Γ1 ++ Γ2) -> (x, a) ∈ Γ2 -> x `notin` domset Γ1
    intros.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq (Γ1 ++ Γ2)
H0: (x, a) ∈ Γ2
x `notin` domset Γ1 autorewrite with tea_rw_uniq in *.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
H0: (x, a) ∈ Γ2
x `notin` domset Γ1
    preprocess.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H1: uniq Γ2
H2: disjoint Γ1 Γ2
H0: (x, a) ∈ Γ2
x `notin` domset Γ1 apply in_in_domset in H0.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H1: uniq Γ2
H2: disjoint Γ1 Γ2
H0: x `in` domset Γ2
x `notin` domset Γ1
    rewrite disjoint_sym in H2.A: Type
x: atom
a: A
Γ1, Γ2: list (atom * A)
H: uniq Γ1
H1: uniq Γ2
H2: disjoint Γ2 Γ1
H0: x `in` domset Γ2
x `notin` domset Γ1
    eauto with tea_alist.
  Qed.

  (* If x is in an alist, it is either in the front half or
   the back half. *)
  Lemma in_split : forall x a Γ,
    (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2.A: Type
forall x a Γ,
(x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
  Proof.A: Type
forall x a Γ,
(x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
    introv Hin.A: Type
x: atom
a: A
Γ: list (atom * A)
Hin: (x, a) ∈ Γ
exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2 induction Γ.A: Type
x: atom
a: A
Hin: (x, a) ∈ []
exists Γ1 Γ2, [] = Γ1 ++ x ~ a ++ Γ2
A: Type
x: atom
a: A
a0: atom * A
Γ: list (atom * A)
Hin: (x, a) ∈ (a0 :: Γ)
IHΓ: (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, a0 :: Γ = Γ1 ++ x ~ a ++ Γ2
    -A: Type
x: atom
a: A
Hin: (x, a) ∈ []
exists Γ1 Γ2, [] = Γ1 ++ x ~ a ++ Γ2 now simpl_list in *.
    -A: Type
x: atom
a: A
a0: atom * A
Γ: list (atom * A)
Hin: (x, a) ∈ (a0 :: Γ)
IHΓ: (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, a0 :: Γ = Γ1 ++ x ~ a ++ Γ2 destruct a0 as [z a'].A: Type
x: atom
a: A
z: atom
a': A
Γ: list (atom * A)
Hin: (x, a) ∈ ((z, a') :: Γ)
IHΓ: (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ x ~ a ++ Γ2 simpl_list in *.A: Type
x: atom
a: A
z: atom
a': A
Γ: list (atom * A)
Hin: (x, a) = (z, a') \/ (x, a) ∈ Γ
IHΓ: (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ x ~ a ++ Γ2
      destruct Hin as [Hin|Hin].A: Type
x: atom
a: A
z: atom
a': A
Γ: list (atom * A)
Hin: (x, a) = (z, a')
IHΓ: (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ x ~ a ++ Γ2
A: Type
x: atom
a: A
z: atom
a': A
Γ: list (atom * A)
Hin: (x, a) ∈ Γ
IHΓ: (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ x ~ a ++ Γ2
      +A: Type
x: atom
a: A
z: atom
a': A
Γ: list (atom * A)
Hin: (x, a) = (z, a')
IHΓ: (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ x ~ a ++ Γ2 inverts Hin.A: Type
z: atom
a': A
Γ: list (atom * A)
IHΓ: (z, a') ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ z ~ a' ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ z ~ a' ++ Γ2 exists (@nil (atom * A)) Γ.A: Type
z: atom
a': A
Γ: list (atom * A)
IHΓ: (z, a') ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ z ~ a' ++ Γ2
(z, a') :: Γ = [] ++ z ~ a' ++ Γ reflexivity.
      +A: Type
x: atom
a: A
z: atom
a': A
Γ: list (atom * A)
Hin: (x, a) ∈ Γ
IHΓ: (x, a) ∈ Γ -> exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ x ~ a ++ Γ2 specialize (IHΓ Hin).A: Type
x: atom
a: A
z: atom
a': A
Γ: list (atom * A)
Hin: (x, a) ∈ Γ
IHΓ: exists Γ1 Γ2, Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ x ~ a ++ Γ2 destruct IHΓ as [Γ1 [Γ2 rest]].A: Type
x: atom
a: A
z: atom
a': A
Γ: list (atom * A)
Hin: (x, a) ∈ Γ
Γ1, Γ2: list (atom * A)
rest: Γ = Γ1 ++ x ~ a ++ Γ2
exists Γ1 Γ2, (z, a') :: Γ = Γ1 ++ x ~ a ++ Γ2
        subst.A: Type
x: atom
a: A
z: atom
a': A
Γ1, Γ2: list (atom * A)
Hin: (x, a) ∈ (Γ1 ++ x ~ a ++ Γ2)
exists Γ3 Γ4,
  (z, a') :: Γ1 ++ x ~ a ++ Γ2 = Γ3 ++ x ~ a ++ Γ4 exists ((z, a') :: Γ1) Γ2.A: Type
x: atom
a: A
z: atom
a': A
Γ1, Γ2: list (atom * A)
Hin: (x, a) ∈ (Γ1 ++ x ~ a ++ Γ2)
(z, a') :: Γ1 ++ x ~ a ++ Γ2 =
((z, a') :: Γ1) ++ x ~ a ++ Γ2 reflexivity.
  Qed.

End binds_theorems.

(** ** Permutation lemmas *)
(*******************************************************************************)
Section permute_lemmas.

  Context
    {A : Type}
    (l1 l2 : alist A)
    (Hperm : Permutation l1 l2).

  Lemma perm_dom : forall (x : atom),
      x ∈ dom l1 <-> x ∈ dom l2.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall x : atom, x ∈ dom l1 <-> x ∈ dom l2
  Proof.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall x : atom, x ∈ dom l1 <-> x ∈ dom l2
    setoid_rewrite in_dom_iff.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall x : atom,
(exists a : A, (x, a) ∈ l1) <->
(exists a : A, (x, a) ∈ l2)
    setoid_rewrite (List.permutation_spec Hperm).A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall x : atom,
(exists a : A, (x, a) ∈ l2) <->
(exists a : A, (x, a) ∈ l2)
    reflexivity.
  Qed.

  Lemma perm_domset :
    domset l1 [=] domset l2.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
domset l1 [=] domset l2
  Proof.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
domset l1 [=] domset l2
    unfold domset.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
atoms (dom l1) [=] atoms (dom l2)
    intro a; rewrite <- 2(in_atoms_iff).A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
a: AtomSet.elt
a ∈ dom l1 <-> a ∈ dom l2
    apply perm_dom.
  Qed.

  Lemma perm_range : forall (a : A),
      a ∈ range l1 <-> a ∈ range l2.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall a : A, a ∈ range l1 <-> a ∈ range l2
  Proof.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall a : A, a ∈ range l1 <-> a ∈ range l2
    setoid_rewrite in_range_iff.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall a : A,
(exists x : atom, (x, a) ∈ l1) <->
(exists x : atom, (x, a) ∈ l2)
    setoid_rewrite (List.permutation_spec Hperm).A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall a : A,
(exists x : atom, (x, a) ∈ l2) <->
(exists x : atom, (x, a) ∈ l2)
    reflexivity.
  Qed.

  Lemma perm_disjoint_l : forall (l3 : alist A),
      disjoint l1 l3 <-> disjoint l2 l3.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall l3 : alist A, disjoint l1 l3 <-> disjoint l2 l3
  Proof.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall l3 : alist A, disjoint l1 l3 <-> disjoint l2 l3
    intros.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
l3: alist A
disjoint l1 l3 <-> disjoint l2 l3 unfold disjoint.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
l3: alist A
domset l1 ∩ domset l3 [=] ∅ <->
domset l2 ∩ domset l3 [=] ∅ now rewrite perm_domset.
  Qed.

  Lemma perm_disjoint_r : forall (l3 : alist A),
      disjoint l3 l1 <-> disjoint l3 l2.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall l3 : alist A, disjoint l3 l1 <-> disjoint l3 l2
  Proof.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
forall l3 : alist A, disjoint l3 l1 <-> disjoint l3 l2
    intros.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
l3: alist A
disjoint l3 l1 <-> disjoint l3 l2 unfold disjoint.A: Type
l1, l2: alist A
Hperm: Permutation l1 l2
l3: alist A
domset l3 ∩ domset l1 [=] ∅ <->
domset l3 ∩ domset l2 [=] ∅ now rewrite perm_domset.
  Qed.

End permute_lemmas.

Lemma uniq_perm : forall (A : Type) (l1 l2 : alist A),
    Permutation l1 l2 ->
    uniq l1 <-> uniq l2.forall (A : Type) (l1 l2 : alist A),
Permutation l1 l2 -> uniq l1 <-> uniq l2
Proof.forall (A : Type) (l1 l2 : alist A),
Permutation l1 l2 -> uniq l1 <-> uniq l2
  introv J.A: Type
l1, l2: alist A
J: Permutation l1 l2
uniq l1 <-> uniq l2 induction J.A: Type
uniq [] <-> uniq []
A: Type
x: atom * A
l, l': list (atom * A)
J: Permutation l l'
IHJ: uniq l <-> uniq l'
uniq (x :: l) <-> uniq (x :: l')
A: Type
x, y: atom * A
l: list (atom * A)
uniq (y :: x :: l) <-> uniq (x :: y :: l)
A: Type
l, l', l'': list (atom * A)
J1: Permutation l l'
J2: Permutation l' l''
IHJ1: uniq l <-> uniq l'
IHJ2: uniq l' <-> uniq l''
uniq l <-> uniq l''
  -A: Type
uniq [] <-> uniq [] reflexivity.
  -A: Type
x: atom * A
l, l': list (atom * A)
J: Permutation l l'
IHJ: uniq l <-> uniq l'
uniq (x :: l) <-> uniq (x :: l') destruct x.A: Type
n: atom
a: A
l, l': list (atom * A)
J: Permutation l l'
IHJ: uniq l <-> uniq l'
uniq ((n, a) :: l) <-> uniq ((n, a) :: l') autorewrite with tea_rw_uniq.A: Type
n: atom
a: A
l, l': list (atom * A)
J: Permutation l l'
IHJ: uniq l <-> uniq l'
n `notin` domset l /\ uniq l <->
n `notin` domset l' /\ uniq l'
    rewrite IHJ, perm_domset; eauto.A: Type
n: atom
a: A
l, l': list (atom * A)
J: Permutation l l'
IHJ: uniq l <-> uniq l'
n `notin` domset l' /\ uniq l' <->
n `notin` domset l' /\ uniq l' tauto.
  -A: Type
x, y: atom * A
l: list (atom * A)
uniq (y :: x :: l) <-> uniq (x :: y :: l) destruct x, y.A: Type
n: atom
a: A
n0: atom
a0: A
l: list (atom * A)
uniq ((n0, a0) :: (n, a) :: l) <->
uniq ((n, a) :: (n0, a0) :: l) autorewrite with tea_rw_uniq tea_rw_dom.A: Type
n: atom
a: A
n0: atom
a0: A
l: list (atom * A)
(n0 <> n /\ n0 `notin` domset l) /\
n `notin` domset l /\ uniq l <->
(n <> n0 /\ n `notin` domset l) /\
n0 `notin` domset l /\ uniq l
    intuition.
  -A: Type
l, l', l'': list (atom * A)
J1: Permutation l l'
J2: Permutation l' l''
IHJ1: uniq l <-> uniq l'
IHJ2: uniq l' <-> uniq l''
uniq l <-> uniq l'' tauto.
Qed.

Lemma binds_perm : forall (A : Type) (l1 l2 : list (atom * A)) (x : atom) (a : A),
    Permutation l1 l2 -> (x, a) ∈ l1 <-> (x, a) ∈ l2.forall (A : Type) (l1 l2 : list (atom * A)) (x : atom)
  (a : A),
Permutation l1 l2 -> (x, a) ∈ l1 <-> (x, a) ∈ l2
Proof.forall (A : Type) (l1 l2 : list (atom * A)) (x : atom)
  (a : A),
Permutation l1 l2 -> (x, a) ∈ l1 <-> (x, a) ∈ l2
  intros.A: Type
l1, l2: list (atom * A)
x: atom
a: A
H: Permutation l1 l2
(x, a) ∈ l1 <-> (x, a) ∈ l2 now erewrite List.permutation_spec; eauto.
Qed.

Create HintDb tea_rw_perm.
#[export] Hint Rewrite @perm_dom @perm_range @perm_domset @perm_disjoint_l @perm_disjoint_r
     @uniq_perm using (auto; try symmetry; auto) : tea_rw_perm.

(** For any given finite set of atoms, we can generate an atom fresh
    for it. *)
Lemma atom_fresh : forall L : AtomSet.t, { x : atom | ~ x `in` L }.forall L : AtomSet.t, {x : atom | x `notin` L}
Proof.forall L : AtomSet.t, {x : atom | x `notin` L}
  intros L.L: AtomSet.t
{x : atom | x `notin` L}
  exists (fresh (AtomSet.elements L)).L: AtomSet.t
fresh ((elements) L) `notin` L
  rewrite in_elements_iff.L: AtomSet.t
~ fresh ((elements) L) ∈ (elements) L
  apply (Name.fresh_not_in (AtomSet.elements L)).
Qed.

(** * Tactic support for picking fresh atoms *)
(* ********************************************************************** *)

Ltac ltac_remove_dups xs :=
  let rec remove xs acc :=
    match xs with
      | List.nil => acc
      | List.cons ?x ?xs =>
        match acc with
          | context [x] => remove xs acc
          | _ => remove xs (List.cons x acc)
        end
    end
  in
  match type of xs with
    | List.list ?A =>
      let xs := eval simpl in xs in
      let xs := remove xs (@List.nil A) in
      eval simpl in (List.rev xs)
  end.

(** The auxiliary tactic [simplify_list_of_atom_sets] takes a list of
    finite sets of atoms and unions everything together, returning the
    resulting single finite set. *)
Ltac simplify_list_of_atom_sets L :=
  let L := eval simpl in L in
  let L := ltac_remove_dups L in
  let L := eval simpl in (List.fold_right AtomSet.union AtomSet.empty L) in
  match L with
    | context C [AtomSet.union ?E AtomSet.empty] => context C [ E ]
  end.

(** [gather_atoms_with F] returns the union of all the finite sets
    [F x] where [x] is a variable from the context such that [F x]
    type checks. *)

Ltac gather_atoms_with F :=
  let apply_arg x :=
    match type of F with
      | _ -> _ -> _ -> _ => constr:(@F _ _ x)
      | _ -> _ -> _ => constr:(@F _ x)
      | _ -> _ => constr:(@F x)
    end in
  let rec gather V :=
    match goal with
      | H : _ |- _ =>
        let FH := apply_arg H in
        match V with
          | context [FH] => fail 1
          | _ => gather (AtomSet.union FH V)
        end
      | _ => V
    end in
  let L := gather AtomSet.empty in eval simpl in L.

(** [beautify_fset V] assumes that [V] is built as a union of finite
    sets and returns the same set cleaned up: empty sets are removed
    and items are laid out in a nicely parenthesized way. *)

Ltac beautify_fset V :=
  let rec go Acc E :=
     match E with
     | AtomSet.union ?E1 ?E2 => let Acc2 := go Acc E2 in go Acc2 E1
     | AtomSet.empty => Acc
     | ?E1 => match Acc with
                | AtomSet.empty => E1
                | _ => constr:(AtomSet.union E1 Acc)
              end
     end
  in go AtomSet.empty V.

(** The tactic [pick fresh Y for L] takes a finite set of atoms [L]
    and a fresh name [Y], and adds to the context an atom with name
    [Y] and a proof that [~ In Y L], i.e., that [Y] is fresh for [L].
    The tactic will fail if [Y] is already declared in the context.
    The variant [pick fresh Y] is similar, except that [Y] is fresh
    for "all atoms in the context."  This version depends on the
    tactic [gather_atoms], which is responsible for returning the set
    of "all atoms in the context."  By default, it returns the empty
    set, but users are free (and expected) to redefine it. *)

Ltac gather_atoms :=
  constr:(AtomSet.empty).

Tactic Notation "pick" "fresh" ident(Y) "for" constr(L) :=
  let Fr := fresh "Hfresh" in
  let L := beautify_fset L in
  (destruct (atom_fresh L) as [Y Fr]).

Tactic Notation "pick" "fresh" ident(Y) :=
  let L := gather_atoms in
  pick fresh Y for L.

Ltac pick_fresh y :=
  pick fresh y.

(** Example: We can redefine [gather_atoms] to return all the
    "obvious" atoms in the context using the [gather_atoms_with] thus
    giving us a "useful" version of the "[pick fresh]" tactic. *)

Ltac gather_atoms ::=
  let A := gather_atoms_with (fun x : AtomSet.t => x) in
  let B := gather_atoms_with (fun x : atom => AtomSet.singleton x) in
  constr:(AtomSet.union A B).

Lemma example_pick_fresh_use : forall (x y z : atom) (L1 L2 L3 : AtomSet.t), True.atom ->
atom ->
atom -> AtomSet.t -> AtomSet.t -> AtomSet.t -> True
(* begin show *)
Proof.atom ->
atom ->
atom -> AtomSet.t -> AtomSet.t -> AtomSet.t -> True
  intros x y z L1 L2 L3.x, y, z: atom
L1, L2, L3: AtomSet.t
True
  pick fresh k.x, y, z: atom
L1, L2, L3: AtomSet.t
k: atom
Hfresh: k
`notin` (L1
         ∪ (L2
            ∪ (L3 ∪ ({{x}} ∪ ({{y}} ∪ {{z}})))))
True

  (** At this point in the proof, we have a new atom [k] and a
      hypothesis [Fr] that [k] is fresh for [x], [y], [z], [L1], [L2],
      and [L3]. *)

  trivial.
Qed.

Tactic Notation
  "pick" "fresh" ident(atom_name)
  "excluding" constr(L)
  "and" "apply" constr(H)
  :=
    first [apply (@H L) | eapply (@H L)];
      match goal with
        | |- forall _, ~ AtomSet.In _ _ -> _ =>
          let Fr := fresh "Fr" in intros atom_name Fr
        | |- forall _, ~ AtomSet.In _ _ -> _ =>
          fail 1 "because" atom_name "is already defined"
        | _ =>
          idtac
      end.

Tactic Notation
  "pick" "fresh" ident(atom_name)
  "and" "apply" constr(H)
  :=
    let L := gather_atoms in
    let L := beautify_fset L in
    pick fresh atom_name excluding L and apply H.

Ltac specialize_cof H e :=
  specialize (H e ltac:(fsetdec)).

Ltac specialize_freshly H :=
  let e := fresh "e" in
  pick fresh e;
  specialize_cof H e.

(** When the goal is a cofinite quantification, introduce a new atom
      and specialize assumption H to this variable. *)
Ltac intros_cof H :=
  match goal with
  | |- forall e, ~ AtomSet.In e _ -> _ =>
    match type of H with
    | forall e, ~ AtomSet.In _ _ -> _ =>
      let e := fresh "e" in
      let Notin := fresh "Notin" in
      intros e Notin; specialize_cof H e
    | _ => fail "Argument should be cofinitely quantified hypothesis"
    end
  end.

Ltac apply_cof H :=
  intros_cof H; apply H.

Ltac eapply_cof H :=
  intros_cof H; eapply H.

Ltac cleanup_cofinite :=
  repeat
    match goal with
    | H : forall e, ?x |- _ => specialize_freshly H
    end.

Ltac cc := cleanup_cofinite.