From Tealeaves Require Import
  Backends.LN.LN
  Backends.Common.Names
  Backends.DB.DB
  Functors.List
  Functors.Option
  Classes.Categorical.ContainerFunctor
  Classes.Kleisli.DecoratedContainerFunctor
  Misc.PartialBijection.

From Coq Require Import Logic.Decidable.

Open Scope nat_scope.

Import
  List.ListNotations
  ContainerFunctor.Notations.

Generalizable All Variables.

(** * Miscellaneous lemmas *)
(******************************************************************************)
Lemma nin_list_cons:
  forall {A : Type} (a1 a2 : A) (xs : list A),
    ~ a1 ∈ (a2 :: xs) <-> a1 <> a2 /\ ~ a1 ∈ xs.
forall (A : Type) (a1 a2 : A) (xs : list A),
~ a1 ∈ (a2 :: xs) <-> a1 <> a2 /\ ~ a1 ∈ xs
Proof.
forall (A : Type) (a1 a2 : A) (xs : list A),
~ a1 ∈ (a2 :: xs) <-> a1 <> a2 /\ ~ a1 ∈ xs
  intros.
A: Type
a1, a2: A
xs: list A
~ a1 ∈ (a2 :: xs) <-> a1 <> a2 /\ ~ a1 ∈ xs rewrite element_of_list_cons.
A: Type
a1, a2: A
xs: list A
~ (a1 = a2 \/ a1 ∈ xs) <-> a1 <> a2 /\ ~ a1 ∈ xs
  intuition.
Qed.

Lemma map_Some_inv: forall `(f: A -> B) (x: option A)  y,
    (forall a a', f a = f a' -> a = a') ->
    map f x = Some (f y) ->
    x = Some y.
forall (A B : Type) (f : A -> B) (x : option A)
  (y : A),
(forall a a' : A, f a = f a' -> a = a') ->
map f x = Some (f y) -> x = Some y
Proof.
forall (A B : Type) (f : A -> B) (x : option A)
  (y : A),
(forall a a' : A, f a = f a' -> a = a') ->
map f x = Some (f y) -> x = Some y
  introv Hinj Heq.
A, B: Type
f: A -> B
x: option A
y: A
Hinj: forall a a' : A, f a = f a' -> a = a'
Heq: map f x = Some (f y)
x = Some y destruct x.
A, B: Type
f: A -> B
a, y: A
Hinj: forall a a' : A, f a = f a' -> a = a'
Heq: map f (Some a) = Some (f y)
Some a = Some y
A, B: Type
f: A -> B
y: A
Hinj: forall a a' : A, f a = f a' -> a = a'
Heq: map f None = Some (f y)
None = Some y
  -
A, B: Type
f: A -> B
a, y: A
Hinj: forall a a' : A, f a = f a' -> a = a'
Heq: map f (Some a) = Some (f y)
Some a = Some y inversion Heq.
A, B: Type
f: A -> B
a, y: A
Hinj: forall a a' : A, f a = f a' -> a = a'
Heq: map f (Some a) = Some (f y)
H0: f a = f y
Some a = Some y fequal.
A, B: Type
f: A -> B
a, y: A
Hinj: forall a a' : A, f a = f a' -> a = a'
Heq: map f (Some a) = Some (f y)
H0: f a = f y
a = y
    apply Hinj.
A, B: Type
f: A -> B
a, y: A
Hinj: forall a a' : A, f a = f a' -> a = a'
Heq: map f (Some a) = Some (f y)
H0: f a = f y
f a = f y assumption.
  -
A, B: Type
f: A -> B
y: A
Hinj: forall a a' : A, f a = f a' -> a = a'
Heq: map f None = Some (f y)
None = Some y inversion Heq.
Qed.

Ltac compare_atoms :=
    match goal with
    | H: context[?a == ?a'] |- _ =>
        destruct_eq_args a a'
    | |- context[?a == ?a'] =>
        destruct_eq_args a a'
    end.

#[global] Tactic Notation "compare" "atoms" := compare_atoms.

(** * Definition of <<key>> and main operations *)
(******************************************************************************)
Definition key :=
  list atom.

(** ** Insertion and lookup *)
(******************************************************************************)
Fixpoint key_insert_atom (k: key) (a: atom): key :=
  match k with
  | nil => [a]
  | cons x rest =>
      if a == x then k else
        x :: key_insert_atom rest a
  end.

Fixpoint getIndex (k: key) (a: atom): option nat :=
  match k with
  | [] => None
  | x :: rest =>
      if a == x
      then Some 0
      else map S (getIndex rest a)
  end.

Fixpoint getName (k: key) (ix: nat): option atom :=
  match k, ix with
  | nil, _ => None
  | cons a rest, 0 => Some a
  | cons a rest, S ix => getName rest ix
  end.

Fixpoint getIndex_rec (k: key) (acc: nat) (a: atom): option nat :=
  match k with
  | nil => None
  | cons x rest =>
      if a == x then Some acc else getIndex_rec rest (S acc) a
  end.

Definition getIndex_alt: key -> atom -> option nat :=
  fun k => getIndex_rec k 0.

(** ** Well-formedness predicates *)
(******************************************************************************)
Fixpoint unique (l: list atom): Prop :=
  match l with
  | nil => True
  | cons a rest =>
      ~ (a ∈ rest) /\ unique rest
  end.

Definition wf_LN
  `{ToSubset T} (t: T LN) (k: key): Prop :=
  unique k /\ forall (x: atom), Fr x ∈ t -> x ∈ k.

Definition resolves_gap (gap: nat) (k: key): Prop :=
  gap <= length k.

Definition contains_ix_upto (n: nat) (k: key): Prop :=
  n < length k.

Lemma resolves_gap_spec: forall (gap: nat) (k: key),
    resolves_gap gap k <-> contains_ix_upto (gap - 1) k \/ gap = 0.
forall (gap : nat) (k : key),
resolves_gap gap k <->
contains_ix_upto (gap - 1) k \/ gap = 0
Proof.
forall (gap : nat) (k : key),
resolves_gap gap k <->
contains_ix_upto (gap - 1) k \/ gap = 0
  intros.
gap: nat
k: key
resolves_gap gap k <->
contains_ix_upto (gap - 1) k \/ gap = 0
  unfold resolves_gap, contains_ix_upto.
gap: nat
k: key
gap <= length k <-> gap - 1 < length k \/ gap = 0
  split.
gap: nat
k: key
gap <= length k -> gap - 1 < length k \/ gap = 0
gap: nat
k: key
gap - 1 < length k \/ gap = 0 -> gap <= length k
  -
gap: nat
k: key
gap <= length k -> gap - 1 < length k \/ gap = 0 lia.
  -
gap: nat
k: key
gap - 1 < length k \/ gap = 0 -> gap <= length k lia.
Qed.

Lemma elt_decidable: forall (a: atom) (l: list atom),
    decidable (a ∈ l).
forall (a : atom) (l : list atom), decidable (a ∈ l)
Proof.
forall (a : atom) (l : list atom), decidable (a ∈ l)
  intros.
a: atom
l: list atom
decidable (a ∈ l)
  induction l.
a: atom
decidable (a ∈ [])
a, a0: atom
l: list atom
IHl: decidable (a ∈ l)
decidable (a ∈ (a0 :: l))
  -
a: atom
decidable (a ∈ []) right.
a: atom
~ a ∈ []
    rewrite element_of_list_nil.
a: atom
~ False
    easy.
  -
a, a0: atom
l: list atom
IHl: decidable (a ∈ l)
decidable (a ∈ (a0 :: l)) destruct IHl as [Huniq | Hnuniq].
a, a0: atom
l: list atom
Huniq: a ∈ l
decidable (a ∈ (a0 :: l))
a, a0: atom
l: list atom
Hnuniq: ~ a ∈ l
decidable (a ∈ (a0 :: l))
    +
a, a0: atom
l: list atom
Huniq: a ∈ l
decidable (a ∈ (a0 :: l)) left.
a, a0: atom
l: list atom
Huniq: a ∈ l
a ∈ (a0 :: l) simpl_list.
a, a0: atom
l: list atom
Huniq: a ∈ l
a = a0 \/ a ∈ l tauto.
    +
a, a0: atom
l: list atom
Hnuniq: ~ a ∈ l
decidable (a ∈ (a0 :: l)) destruct (a == a0).
a, a0: atom
l: list atom
Hnuniq: ~ a ∈ l
e: a = a0
decidable (a ∈ (a0 :: l))
a, a0: atom
l: list atom
Hnuniq: ~ a ∈ l
n: a <> a0
decidable (a ∈ (a0 :: l))
      *
a, a0: atom
l: list atom
Hnuniq: ~ a ∈ l
e: a = a0
decidable (a ∈ (a0 :: l)) subst.
a0: atom
l: list atom
Hnuniq: ~ a0 ∈ l
decidable (a0 ∈ (a0 :: l)) left.
a0: atom
l: list atom
Hnuniq: ~ a0 ∈ l
a0 ∈ (a0 :: l)
        simpl_list.
a0: atom
l: list atom
Hnuniq: ~ a0 ∈ l
a0 = a0 \/ a0 ∈ l now left.
      *
a, a0: atom
l: list atom
Hnuniq: ~ a ∈ l
n: a <> a0
decidable (a ∈ (a0 :: l)) right.
a, a0: atom
l: list atom
Hnuniq: ~ a ∈ l
n: a <> a0
~ a ∈ (a0 :: l)
        simpl_list.
a, a0: atom
l: list atom
Hnuniq: ~ a ∈ l
n: a <> a0
~ (a = a0 \/ a ∈ l)
        tauto.
Qed.

Lemma unique_decidable: forall (l: list atom),
    decidable (unique l).
forall l : list atom, decidable (unique l)
Proof.
forall l : list atom, decidable (unique l)
  intros.
l: list atom
decidable (unique l)
  induction l.
decidable (unique [])
a: atom
l: list atom
IHl: decidable (unique l)
decidable (unique (a :: l))
  -
decidable (unique []) left.
unique [] cbn.
True easy.
  -
a: atom
l: list atom
IHl: decidable (unique l)
decidable (unique (a :: l)) destruct IHl as [Huniq | Hnuniq].
a: atom
l: list atom
Huniq: unique l
decidable (unique (a :: l))
a: atom
l: list atom
Hnuniq: ~ unique l
decidable (unique (a :: l))
    +
a: atom
l: list atom
Huniq: unique l
decidable (unique (a :: l)) cbn.
a: atom
l: list atom
Huniq: unique l
decidable (~ a ∈ l /\ unique l) destruct (elt_decidable a l).
a: atom
l: list atom
Huniq: unique l
H: a ∈ l
decidable (~ a ∈ l /\ unique l)
a: atom
l: list atom
Huniq: unique l
H: ~ a ∈ l
decidable (~ a ∈ l /\ unique l)
      *
a: atom
l: list atom
Huniq: unique l
H: a ∈ l
decidable (~ a ∈ l /\ unique l) right.
a: atom
l: list atom
Huniq: unique l
H: a ∈ l
~ (~ a ∈ l /\ unique l) tauto.
      *
a: atom
l: list atom
Huniq: unique l
H: ~ a ∈ l
decidable (~ a ∈ l /\ unique l) left.
a: atom
l: list atom
Huniq: unique l
H: ~ a ∈ l
~ a ∈ l /\ unique l tauto.
    +
a: atom
l: list atom
Hnuniq: ~ unique l
decidable (unique (a :: l)) right.
a: atom
l: list atom
Hnuniq: ~ unique l
~ unique (a :: l) cbn.
a: atom
l: list atom
Hnuniq: ~ unique l
~ (~ a ∈ l /\ unique l)
      tauto.
Qed.

(*
Definition wf_DB `{ToCtxset nat T} (t: T nat) (k: key): Prop :=
  unique k /\ exists (gap: nat), cl_at gap t /\ resolves_gap gap k.
*)

(** * Misc *)
(******************************************************************************)
Definition key_is_atom_in (k: key) (a: atom):
  {a ∈ k} + {~ a ∈ k}.
k: key
a: atom
{a ∈ k} + {~ a ∈ k}
Proof.
k: key
a: atom
{a ∈ k} + {~ a ∈ k}
  induction k.
a: atom
{a ∈ []} + {~ a ∈ []}
a0: atom
k: list atom
a: atom
IHk: {a ∈ k} + {~ a ∈ k}
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)}
  -
a: atom
{a ∈ []} + {~ a ∈ []} right.
a: atom
~ a ∈ [] inversion 1.
  -
a0: atom
k: list atom
a: atom
IHk: {a ∈ k} + {~ a ∈ k}
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)} pose (element_of_list_cons a a0 k).
a0: atom
k: list atom
a: atom
IHk: {a ∈ k} + {~ a ∈ k}
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)}
    destruct (a == a0).
a0: atom
k: list atom
a: atom
IHk: {a ∈ k} + {~ a ∈ k}
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
e: a = a0
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)}
a0: atom
k: list atom
a: atom
IHk: {a ∈ k} + {~ a ∈ k}
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
n: a <> a0
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)}
    +
a0: atom
k: list atom
a: atom
IHk: {a ∈ k} + {~ a ∈ k}
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
e: a = a0
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)} now (left; left).
    +
a0: atom
k: list atom
a: atom
IHk: {a ∈ k} + {~ a ∈ k}
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
n: a <> a0
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)} destruct IHk.
a0: atom
k: list atom
a: atom
e: a ∈ k
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
n: a <> a0
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)}
a0: atom
k: list atom
a: atom
n0: ~ a ∈ k
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
n: a <> a0
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)}
      *
a0: atom
k: list atom
a: atom
e: a ∈ k
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
n: a <> a0
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)} now (left; right).
      *
a0: atom
k: list atom
a: atom
n0: ~ a ∈ k
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
n: a <> a0
{a ∈ (a0 :: k)} + {~ a ∈ (a0 :: k)} right.
a0: atom
k: list atom
a: atom
n0: ~ a ∈ k
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
n: a <> a0
~ a ∈ (a0 :: k) rewrite i.
a0: atom
k: list atom
a: atom
n0: ~ a ∈ k
i:= element_of_list_cons a a0 k: a ∈ (a0 :: k) <-> a = a0 \/ a ∈ k
n: a <> a0
~ (a = a0 \/ a ∈ k)
        intros [contra|contra];
          contradiction.
Defined.

Definition key_is_ix_in (k: key) (ix: nat):
  {contains_ix_upto ix k} + {~ contains_ix_upto ix k}.
k: key
ix: nat
{contains_ix_upto ix k} + {~ contains_ix_upto ix k}
Proof.
k: key
ix: nat
{contains_ix_upto ix k} + {~ contains_ix_upto ix k}
  unfold contains_ix_upto.
k: key
ix: nat
{ix < length k} + {~ ix < length k}
  generalize ix.
k: key
ix: nat
forall ix : nat, {ix < length k} + {~ ix < length k}
  generalize (length k).
k: key
ix: nat
forall n ix : nat, {ix < n} + {~ ix < n}
  intros a b.
k: key
ix, a, b: nat
{b < a} + {~ b < a}
  apply Compare_dec.le_dec.
Defined.

(** * Lemmas about <<key_insert_atom>> *)
(******************************************************************************)

(** ** Rewriting *)
(******************************************************************************)
Lemma insert_cons_eq: forall a k x,
    a = x ->
    key_insert_atom (a :: k) x = a :: k.
forall (a : atom) (k : list atom) (x : atom),
a = x -> key_insert_atom (a :: k) x = a :: k
Proof.
forall (a : atom) (k : list atom) (x : atom),
a = x -> key_insert_atom (a :: k) x = a :: k
  intros.
a: atom
k: list atom
x: atom
H: a = x
key_insert_atom (a :: k) x = a :: k cbn.
a: atom
k: list atom
x: atom
H: a = x
(if x == a then a :: k else a :: key_insert_atom k x) =
a :: k
  destruct_eq_args x a.
Qed.

Lemma insert_cons_neq: forall a k x,
    a <> x ->
    key_insert_atom (a :: k) x = a :: key_insert_atom k x.
forall (a : atom) (k : list atom) (x : atom),
a <> x ->
key_insert_atom (a :: k) x = a :: key_insert_atom k x
Proof.
forall (a : atom) (k : list atom) (x : atom),
a <> x ->
key_insert_atom (a :: k) x = a :: key_insert_atom k x
  intros.
a: atom
k: list atom
x: atom
H: a <> x
key_insert_atom (a :: k) x = a :: key_insert_atom k x cbn.
a: atom
k: list atom
x: atom
H: a <> x
(if x == a then a :: k else a :: key_insert_atom k x) =
a :: key_insert_atom k x
  destruct_eq_args x a.
Qed.

(** ** Alternative spec *)
(******************************************************************************)
Lemma getIndex_rec_spec (k: key) (a: atom) (n: nat):
  getIndex_rec k n a = map (fun m => m + n) (getIndex k a).
k: key
a: atom
n: nat
getIndex_rec k n a =
map (fun m : nat => m + n) (getIndex k a)
Proof.
k: key
a: atom
n: nat
getIndex_rec k n a =
map (fun m : nat => m + n) (getIndex k a)
  generalize dependent n.
k: key
a: atom
forall n : nat,
getIndex_rec k n a =
map (fun m : nat => m + n) (getIndex k a)
  induction k; intro n.
a: atom
n: nat
getIndex_rec [] n a =
map (fun m : nat => m + n) (getIndex [] a)
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
getIndex_rec (a0 :: k) n a =
map (fun m : nat => m + n) (getIndex (a0 :: k) a)
  -
a: atom
n: nat
getIndex_rec [] n a =
map (fun m : nat => m + n) (getIndex [] a) reflexivity.
  -
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
getIndex_rec (a0 :: k) n a =
map (fun m : nat => m + n) (getIndex (a0 :: k) a) cbn.
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
(if a == a0 then Some n else getIndex_rec k (S n) a) =
map (fun m : nat => m + n)
  (if a == a0 then Some 0 else map S (getIndex k a)) destruct (a == a0).
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
e: a = a0
Some n = map (fun m : nat => m + n) (Some 0)
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
n0: a <> a0
getIndex_rec k (S n) a =
map (fun m : nat => m + n) (map S (getIndex k a))
    +
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
e: a = a0
Some n = map (fun m : nat => m + n) (Some 0) reflexivity.
    +
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
n0: a <> a0
getIndex_rec k (S n) a =
map (fun m : nat => m + n) (map S (getIndex k a)) rewrite (IHk (S n)).
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
n0: a <> a0
map (fun m : nat => m + S n) (getIndex k a) =
map (fun m : nat => m + n) (map S (getIndex k a))
      compose near (getIndex k a) on right.
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
n0: a <> a0
map (fun m : nat => m + S n) (getIndex k a) =
(map (fun m : nat => m + n) ∘ map S) (getIndex k a)
      rewrite (fun_map_map).
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
n0: a <> a0
map (fun m : nat => m + S n) (getIndex k a) =
map ((fun m : nat => m + n) ∘ S) (getIndex k a)
      fequal.
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
n0: a <> a0
(fun m : nat => m + S n) = (fun m : nat => m + n) ∘ S ext m.
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
n0: a <> a0
m: nat
m + S n = ((fun m : nat => m + n) ∘ S) m cbn.
a0: atom
k: list atom
a: atom
IHk: forall n : nat,
getIndex_rec k n a = map (fun m : nat => m + n) (getIndex k a)
n: nat
n0: a <> a0
m: nat
m + S n = S (m + n) lia.
Qed.

Corollary getIndex_spec (k: key) (a: atom):
  getIndex_alt k a = getIndex k a.
k: key
a: atom
getIndex_alt k a = getIndex k a
Proof.
k: key
a: atom
getIndex_alt k a = getIndex k a
  unfold getIndex_alt.
k: key
a: atom
getIndex_rec k 0 a = getIndex k a
  rewrite getIndex_rec_spec.
k: key
a: atom
map (fun m : nat => m + 0) (getIndex k a) =
getIndex k a
  replace (fun m => m + 0) with (@id nat).
k: key
a: atom
map id (getIndex k a) = getIndex k a
k: key
a: atom
id = (fun m : nat => m + 0)
  now rewrite fun_map_id.
k: key
a: atom
id = (fun m : nat => m + 0)
  ext m.
k: key
a: atom
m: nat
id m = m + 0 unfold id.
k: key
a: atom
m: nat
m = m + 0 lia.
Qed.

(** ** Insertion and <<unique>> *)
(******************************************************************************)
Lemma key_nin_insert: forall k a a',
    a <> a' ->
    ~ a ∈ k ->
    ~ a ∈ key_insert_atom k a'.
forall (k : list atom) (a a' : atom),
a <> a' -> ~ a ∈ k -> ~ a ∈ key_insert_atom k a'
Proof.
forall (k : list atom) (a a' : atom),
a <> a' -> ~ a ∈ k -> ~ a ∈ key_insert_atom k a'
  introv Hneq Hnin.
k: list atom
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ k
~ a ∈ key_insert_atom k a' induction k.
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ []
~ a ∈ key_insert_atom [] a'
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ (a0 :: k)
IHk: ~ a ∈ k -> ~ a ∈ key_insert_atom k a'
~ a ∈ key_insert_atom (a0 :: k) a'
  -
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ []
~ a ∈ key_insert_atom [] a' cbn.
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ []
~ (a' = a \/ False) intros [H1|H2].
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ []
H1: a' = a
False
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ []
H2: False
False
    +
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ []
H1: a' = a
False now subst.
    +
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ []
H2: False
False assumption.
  -
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
Hnin: ~ a ∈ (a0 :: k)
IHk: ~ a ∈ k -> ~ a ∈ key_insert_atom k a'
~ a ∈ key_insert_atom (a0 :: k) a' rewrite nin_list_cons in Hnin.
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
Hnin: a <> a0 /\ ~ a ∈ k
IHk: ~ a ∈ k -> ~ a ∈ key_insert_atom k a'
~ a ∈ key_insert_atom (a0 :: k) a'
    destruct Hnin as [? Hnin].
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ k -> ~ a ∈ key_insert_atom k a'
~ a ∈ key_insert_atom (a0 :: k) a'
    specialize (IHk Hnin).
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a'
~ a ∈ key_insert_atom (a0 :: k) a'
    cbn.
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a'
~
List.In a
  (if a' == a0
   then a0 :: k
   else a0 :: key_insert_atom k a') compare atoms.
a0: atom
k: list atom
a: atom
Hneq, H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a0
DESTR_EQs: a0 = a0
~ List.In a (a0 :: k)
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a'
DESTR_NEQ: a' <> a0
DESTR_NEQs: a0 <> a'
~ List.In a (a0 :: key_insert_atom k a')
    +
a0: atom
k: list atom
a: atom
Hneq, H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a0
DESTR_EQs: a0 = a0
~ List.In a (a0 :: k) intros [contra|contra].
a0: atom
k: list atom
a: atom
Hneq, H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a0
DESTR_EQs: a0 = a0
contra: a0 = a
False
a0: atom
k: list atom
a: atom
Hneq, H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a0
DESTR_EQs: a0 = a0
contra: List.In a k
False
      now subst.
a0: atom
k: list atom
a: atom
Hneq, H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a0
DESTR_EQs: a0 = a0
contra: List.In a k
False contradiction.
    +
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a'
DESTR_NEQ: a' <> a0
DESTR_NEQs: a0 <> a'
~ List.In a (a0 :: key_insert_atom k a') intros [contra|contra].
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a'
DESTR_NEQ: a' <> a0
DESTR_NEQs: a0 <> a'
contra: a0 = a
False
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a'
DESTR_NEQ: a' <> a0
DESTR_NEQs: a0 <> a'
contra: List.In a (key_insert_atom k a')
False
      now subst.
a0: atom
k: list atom
a, a': atom
Hneq: a <> a'
H: a <> a0
Hnin: ~ a ∈ k
IHk: ~ a ∈ key_insert_atom k a'
DESTR_NEQ: a' <> a0
DESTR_NEQs: a0 <> a'
contra: List.In a (key_insert_atom k a')
False contradiction.
Qed.

Theorem key_insert_unique (k: key) (a: atom):
  unique k ->
  unique (key_insert_atom k a).
k: key
a: atom
unique k -> unique (key_insert_atom k a)
Proof.
k: key
a: atom
unique k -> unique (key_insert_atom k a)
  intros.
k: key
a: atom
H: unique k
unique (key_insert_atom k a)
  induction k.
a: atom
H: unique []
unique (key_insert_atom [] a)
a0: atom
k: list atom
a: atom
H: unique (a0 :: k)
IHk: unique k -> unique (key_insert_atom k a)
unique (key_insert_atom (a0 :: k) a)
  -
a: atom
H: unique []
unique (key_insert_atom [] a) cbn.
a: atom
H: unique []
~ False /\ True easy.
  -
a0: atom
k: list atom
a: atom
H: unique (a0 :: k)
IHk: unique k -> unique (key_insert_atom k a)
unique (key_insert_atom (a0 :: k) a) destruct H as [H1 H2].
a0: atom
k: list atom
a: atom
H1: ~ a0 ∈ k
H2: unique k
IHk: unique k -> unique (key_insert_atom k a)
unique (key_insert_atom (a0 :: k) a)
    specialize (IHk H2).
a0: atom
k: list atom
a: atom
H1: ~ a0 ∈ k
H2: unique k
IHk: unique (key_insert_atom k a)
unique (key_insert_atom (a0 :: k) a)
    cbn.
a0: atom
k: list atom
a: atom
H1: ~ a0 ∈ k
H2: unique k
IHk: unique (key_insert_atom k a)
unique
  (if a == a0
   then a0 :: k
   else a0 :: key_insert_atom k a) compare atoms.
a0: atom
k: list atom
a: atom
H1: ~ a0 ∈ k
H2: unique k
IHk: unique (key_insert_atom k a)
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
unique (a0 :: key_insert_atom k a)
    cbn.
a0: atom
k: list atom
a: atom
H1: ~ a0 ∈ k
H2: unique k
IHk: unique (key_insert_atom k a)
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
~ a0 ∈ key_insert_atom k a /\
unique (key_insert_atom k a) split; auto.
a0: atom
k: list atom
a: atom
H1: ~ a0 ∈ k
H2: unique k
IHk: unique (key_insert_atom k a)
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
~ a0 ∈ key_insert_atom k a
    apply key_nin_insert; auto.
Qed.

(** ** Insertion and <<getIndex>> *)
(******************************************************************************)
Lemma getIndex_not_in1:
  forall (k:  key) (a: atom),
    ~ a ∈ k -> getIndex k a = None.
forall (k : key) (a : atom),
~ a ∈ k -> getIndex k a = None
Proof.
forall (k : key) (a : atom),
~ a ∈ k -> getIndex k a = None
  intros.
k: key
a: atom
H: ~ a ∈ k
getIndex k a = None induction k.
a: atom
H: ~ a ∈ []
getIndex [] a = None
a0: atom
k: list atom
a: atom
H: ~ a ∈ (a0 :: k)
IHk: ~ a ∈ k -> getIndex k a = None
getIndex (a0 :: k) a = None
  -
a: atom
H: ~ a ∈ []
getIndex [] a = None reflexivity.
  -
a0: atom
k: list atom
a: atom
H: ~ a ∈ (a0 :: k)
IHk: ~ a ∈ k -> getIndex k a = None
getIndex (a0 :: k) a = None cbn.
a0: atom
k: list atom
a: atom
H: ~ a ∈ (a0 :: k)
IHk: ~ a ∈ k -> getIndex k a = None
(if a == a0 then Some 0 else map S (getIndex k a)) =
None
    rewrite nin_list_cons in H.
a0: atom
k: list atom
a: atom
H: a <> a0 /\ ~ a ∈ k
IHk: ~ a ∈ k -> getIndex k a = None
(if a == a0 then Some 0 else map S (getIndex k a)) =
None
    compare atoms.
a0: atom
k: list atom
a: atom
H: a <> a0 /\ ~ a ∈ k
IHk: ~ a ∈ k -> getIndex k a = None
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
map S (getIndex k a) = None
    rewrite IHk.
a0: atom
k: list atom
a: atom
H: a <> a0 /\ ~ a ∈ k
IHk: ~ a ∈ k -> getIndex k a = None
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
map S None = None
a0: atom
k: list atom
a: atom
H: a <> a0 /\ ~ a ∈ k
IHk: ~ a ∈ k -> getIndex k a = None
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
~ a ∈ k
    +
a0: atom
k: list atom
a: atom
H: a <> a0 /\ ~ a ∈ k
IHk: ~ a ∈ k -> getIndex k a = None
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
map S None = None reflexivity.
    +
a0: atom
k: list atom
a: atom
H: a <> a0 /\ ~ a ∈ k
IHk: ~ a ∈ k -> getIndex k a = None
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
~ a ∈ k intuition.
Qed.

Lemma getIndex_not_in2:
  forall (k:  key) (a: atom),
    getIndex k a = None -> ~ a ∈ k.
forall (k : key) (a : atom),
getIndex k a = None -> ~ a ∈ k
Proof.
forall (k : key) (a : atom),
getIndex k a = None -> ~ a ∈ k
  intros k a hyp.
k: key
a: atom
hyp: getIndex k a = None
~ a ∈ k
  induction k.
a: atom
hyp: getIndex [] a = None
~ a ∈ []
a0: atom
k: list atom
a: atom
hyp: getIndex (a0 :: k) a = None
IHk: getIndex k a = None -> ~ a ∈ k
~ a ∈ (a0 :: k)
  -
a: atom
hyp: getIndex [] a = None
~ a ∈ [] cbv.
a: atom
hyp: getIndex [] a = None
False -> False easy.
  -
a0: atom
k: list atom
a: atom
hyp: getIndex (a0 :: k) a = None
IHk: getIndex k a = None -> ~ a ∈ k
~ a ∈ (a0 :: k) rewrite nin_list_cons.
a0: atom
k: list atom
a: atom
hyp: getIndex (a0 :: k) a = None
IHk: getIndex k a = None -> ~ a ∈ k
a <> a0 /\ ~ a ∈ k
    cbn in hyp.
a0: atom
k: list atom
a: atom
hyp: (if a == a0 then Some 0 else map S (getIndex k a)) = None
IHk: getIndex k a = None -> ~ a ∈ k
a <> a0 /\ ~ a ∈ k
    compare atoms.
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
hyp: map S (getIndex k a) = None
IHk: getIndex k a = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
a <> a0 /\ ~ a ∈ k
    split.
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
hyp: map S (getIndex k a) = None
IHk: getIndex k a = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
a <> a0
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
hyp: map S (getIndex k a) = None
IHk: getIndex k a = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
~ a ∈ k
    +
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
hyp: map S (getIndex k a) = None
IHk: getIndex k a = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
a <> a0 assumption.
    +
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
hyp: map S (getIndex k a) = None
IHk: getIndex k a = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
~ a ∈ k apply IHk.
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
hyp: map S (getIndex k a) = None
IHk: getIndex k a = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
getIndex k a = None
      destruct (getIndex k a).
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
n: nat
hyp: map S (Some n) = None
IHk: Some n = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
Some n = None
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
hyp: map S None = None
IHk: None = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
None = None
      *
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
n: nat
hyp: map S (Some n) = None
IHk: Some n = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
Some n = None inversion hyp.
      *
a0: atom
k: list atom
a: atom
DESTR_NEQ: a <> a0
hyp: map S None = None
IHk: None = None -> ~ a ∈ k
DESTR_NEQs: a0 <> a
None = None reflexivity.
Qed.

Theorem getIndex_not_in_iff:
  forall (k:  key) (a: atom),
    ~ a ∈ k <-> getIndex k a = None.
forall (k : key) (a : atom),
~ a ∈ k <-> getIndex k a = None
Proof.
forall (k : key) (a : atom),
~ a ∈ k <-> getIndex k a = None
  intros.
k: key
a: atom
~ a ∈ k <-> getIndex k a = None split.
k: key
a: atom
~ a ∈ k -> getIndex k a = None
k: key
a: atom
getIndex k a = None -> ~ a ∈ k
  -
k: key
a: atom
~ a ∈ k -> getIndex k a = None apply getIndex_not_in1.
  -
k: key
a: atom
getIndex k a = None -> ~ a ∈ k apply getIndex_not_in2.
Qed.

Lemma getIndex_in1:
  forall (k:  key) (a: atom),
    a ∈ k -> {n: nat | getIndex k a = Some n}.
forall (k : key) (a : atom),
a ∈ k -> {n : nat | getIndex k a = Some n}
Proof.
forall (k : key) (a : atom),
a ∈ k -> {n : nat | getIndex k a = Some n}
  introv Hin.
k: key
a: atom
Hin: a ∈ k
{n : nat | getIndex k a = Some n} induction k.
a: atom
Hin: a ∈ []
{n : nat | getIndex [] a = Some n}
a0: atom
k: list atom
a: atom
Hin: a ∈ (a0 :: k)
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
{n : nat | getIndex (a0 :: k) a = Some n}
  -
a: atom
Hin: a ∈ []
{n : nat | getIndex [] a = Some n} inversion Hin.
  -
a0: atom
k: list atom
a: atom
Hin: a ∈ (a0 :: k)
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
{n : nat | getIndex (a0 :: k) a = Some n} rewrite element_of_list_cons in Hin.
a0: atom
k: list atom
a: atom
Hin: a = a0 \/ a ∈ k
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
{n : nat | getIndex (a0 :: k) a = Some n}
    cbn.
a0: atom
k: list atom
a: atom
Hin: a = a0 \/ a ∈ k
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
{n : nat
| (if a == a0 then Some 0 else map S (getIndex k a)) =
  Some n} compare atoms.
a0: atom
k: list atom
IHk: a0 ∈ k -> {n : nat | getIndex k a0 = Some n}
Hin: a0 = a0 \/ a0 ∈ k
DESTR_EQs: a0 = a0
{n : nat | Some 0 = Some n}
a0: atom
k: list atom
a: atom
Hin: a = a0 \/ a ∈ k
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
{n : nat | map S (getIndex k a) = Some n}
    +
a0: atom
k: list atom
IHk: a0 ∈ k -> {n : nat | getIndex k a0 = Some n}
Hin: a0 = a0 \/ a0 ∈ k
DESTR_EQs: a0 = a0
{n : nat | Some 0 = Some n} now (exists 0).
    +
a0: atom
k: list atom
a: atom
Hin: a = a0 \/ a ∈ k
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
{n : nat | map S (getIndex k a) = Some n} assert (Hink: a ∈ k) by now inversion Hin.
a0: atom
k: list atom
a: atom
Hin: a = a0 \/ a ∈ k
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
Hink: a ∈ k
{n : nat | map S (getIndex k a) = Some n}
      destruct (IHk Hink) as [m Hm].
a0: atom
k: list atom
a: atom
Hin: a = a0 \/ a ∈ k
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
Hink: a ∈ k
m: nat
Hm: getIndex k a = Some m
{n : nat | map S (getIndex k a) = Some n}
      rewrite Hm.
a0: atom
k: list atom
a: atom
Hin: a = a0 \/ a ∈ k
IHk: a ∈ k -> {n : nat | getIndex k a = Some n}
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
Hink: a ∈ k
m: nat
Hm: getIndex k a = Some m
{n : nat | map S (Some m) = Some n}
      now (exists (S m)).
Qed.

Lemma getIndex_in2:
  forall (k:  key) (a: atom) (n: nat),
    getIndex k a = Some n -> a ∈ k.
forall (k : key) (a : atom) (n : nat),
getIndex k a = Some n -> a ∈ k
Proof.
forall (k : key) (a : atom) (n : nat),
getIndex k a = Some n -> a ∈ k
  intros k a.
k: key
a: atom
forall n : nat, getIndex k a = Some n -> a ∈ k
  induction k; intros n Heq.
a: atom
n: nat
Heq: getIndex [] a = Some n
a ∈ []
a0: atom
k: list atom
a: atom
IHk: forall n : nat, getIndex k a = Some n -> a ∈ k
n: nat
Heq: getIndex (a0 :: k) a = Some n
a ∈ (a0 :: k)
  -
a: atom
n: nat
Heq: getIndex [] a = Some n
a ∈ [] inversion Heq.
  -
a0: atom
k: list atom
a: atom
IHk: forall n : nat, getIndex k a = Some n -> a ∈ k
n: nat
Heq: getIndex (a0 :: k) a = Some n
a ∈ (a0 :: k) rewrite element_of_list_cons.
a0: atom
k: list atom
a: atom
IHk: forall n : nat, getIndex k a = Some n -> a ∈ k
n: nat
Heq: getIndex (a0 :: k) a = Some n
a = a0 \/ a ∈ k
    cbn in Heq.
a0: atom
k: list atom
a: atom
IHk: forall n : nat, getIndex k a = Some n -> a ∈ k
n: nat
Heq: (if a == a0 then Some 0 else map S (getIndex k a)) = Some n
a = a0 \/ a ∈ k
    compare atoms.
a0: atom
k: list atom
IHk: forall n : nat, getIndex k a0 = Some n -> a0 ∈ k
n: nat
Heq: Some 0 = Some n
DESTR_EQs: a0 = a0
a0 = a0 \/ a0 ∈ k
a0: atom
k: list atom
a: atom
IHk: forall n : nat, getIndex k a = Some n -> a ∈ k
n: nat
DESTR_NEQ: a <> a0
Heq: map S (getIndex k a) = Some n
DESTR_NEQs: a0 <> a
a = a0 \/ a ∈ k
    +
a0: atom
k: list atom
IHk: forall n : nat, getIndex k a0 = Some n -> a0 ∈ k
n: nat
Heq: Some 0 = Some n
DESTR_EQs: a0 = a0
a0 = a0 \/ a0 ∈ k now left.
    +
a0: atom
k: list atom
a: atom
IHk: forall n : nat, getIndex k a = Some n -> a ∈ k
n: nat
DESTR_NEQ: a <> a0
Heq: map S (getIndex k a) = Some n
DESTR_NEQs: a0 <> a
a = a0 \/ a ∈ k right.
a0: atom
k: list atom
a: atom
IHk: forall n : nat, getIndex k a = Some n -> a ∈ k
n: nat
DESTR_NEQ: a <> a0
Heq: map S (getIndex k a) = Some n
DESTR_NEQs: a0 <> a
a ∈ k
      destruct (getIndex k a);
        inversion Heq.
a0: atom
k: list atom
a: atom
n0: nat
IHk: forall n : nat, Some n0 = Some n -> a ∈ k
n: nat
DESTR_NEQ: a <> a0
Heq: map S (Some n0) = Some n
DESTR_NEQs: a0 <> a
H0: S n0 = n
a ∈ k
      now eapply IHk.
Qed.

Theorem key_lookup_in_atom_iff: forall k a,
    (exists n, getIndex k a = Some n) <-> a ∈ k.
forall (k : key) (a : atom),
(exists n : nat, getIndex k a = Some n) <-> a ∈ k
Proof.
forall (k : key) (a : atom),
(exists n : nat, getIndex k a = Some n) <-> a ∈ k
  intros.
k: key
a: atom
(exists n : nat, getIndex k a = Some n) <-> a ∈ k split.
k: key
a: atom
(exists n : nat, getIndex k a = Some n) -> a ∈ k
k: key
a: atom
a ∈ k -> exists n : nat, getIndex k a = Some n
  -
k: key
a: atom
(exists n : nat, getIndex k a = Some n) -> a ∈ k intros [n H].
k: key
a: atom
n: nat
H: getIndex k a = Some n
a ∈ k eauto using getIndex_in2.
  -
k: key
a: atom
a ∈ k -> exists n : nat, getIndex k a = Some n intro Hin.
k: key
a: atom
Hin: a ∈ k
exists n : nat, getIndex k a = Some n apply getIndex_in1 in Hin.
k: key
a: atom
Hin: {n : nat | getIndex k a = Some n}
exists n : nat, getIndex k a = Some n
    firstorder.
Qed.

Theorem getIndex_decide:
  forall (k: key) (a: atom),
    ((a ∈ k) * {n: nat | getIndex k a = Some n}) +
      {~ a ∈ k /\ getIndex k a = None}.
forall (k : key) (a : atom),
(a ∈ k) * {n : nat | getIndex k a = Some n} +
{~ a ∈ k /\ getIndex k a = None}
Proof.
forall (k : key) (a : atom),
(a ∈ k) * {n : nat | getIndex k a = Some n} +
{~ a ∈ k /\ getIndex k a = None}
  intros.
k: key
a: atom
(a ∈ k) * {n : nat | getIndex k a = Some n} +
{~ a ∈ k /\ getIndex k a = None}
  destruct (key_is_atom_in k a); [left|right].
k: key
a: atom
e: a ∈ k
((a ∈ k) * {n : nat | getIndex k a = Some n})%type
k: key
a: atom
n: ~ a ∈ k
~ a ∈ k /\ getIndex k a = None
  -
k: key
a: atom
e: a ∈ k
((a ∈ k) * {n : nat | getIndex k a = Some n})%type split.
k: key
a: atom
e: a ∈ k
a ∈ k
k: key
a: atom
e: a ∈ k
{n : nat | getIndex k a = Some n}
    +
k: key
a: atom
e: a ∈ k
a ∈ k assumption.
    +
k: key
a: atom
e: a ∈ k
{n : nat | getIndex k a = Some n} auto using getIndex_in1.
  -
k: key
a: atom
n: ~ a ∈ k
~ a ∈ k /\ getIndex k a = None split.
k: key
a: atom
n: ~ a ∈ k
~ a ∈ k
k: key
a: atom
n: ~ a ∈ k
getIndex k a = None
    +
k: key
a: atom
n: ~ a ∈ k
~ a ∈ k assumption.
    +
k: key
a: atom
n: ~ a ∈ k
getIndex k a = None auto using getIndex_not_in1.
Defined.

Ltac lookup_atom_in_key k a :=
  let n := fresh "n" in
  let Hin := fresh "H_in" in
  let Hnin := fresh "H_not_in" in
  destruct (getIndex_decide k a) as
    [[Hin [n H_key_lookup]] | [Hnin H_key_lookup]];
  try contradiction.

Tactic Notation "lookup" "atom" constr(a) "in" "key" constr(k) :=
  lookup_atom_in_key k a.

Goal forall (k: key) (a: atom), a ∈ k \/ ~ a ∈ k.
forall (k : key) (a : atom), a ∈ k \/ ~ a ∈ k
Proof.
forall (k : key) (a : atom), a ∈ k \/ ~ a ∈ k
  intros.
k: key
a: atom
a ∈ k \/ ~ a ∈ k
  lookup atom a in key k.
k: key
a: atom
H_in: a ∈ k
n: nat
H_key_lookup: getIndex k a = Some n
a ∈ k \/ ~ a ∈ k
k: key
a: atom
H_not_in: ~ a ∈ k
H_key_lookup: getIndex k a = None
a ∈ k \/ ~ a ∈ k
  -
k: key
a: atom
H_in: a ∈ k
n: nat
H_key_lookup: getIndex k a = Some n
a ∈ k \/ ~ a ∈ k left.
k: key
a: atom
H_in: a ∈ k
n: nat
H_key_lookup: getIndex k a = Some n
a ∈ k intuition.
  -
k: key
a: atom
H_not_in: ~ a ∈ k
H_key_lookup: getIndex k a = None
a ∈ k \/ ~ a ∈ k now right.
Qed.

Lemma getIndex_cons_0: forall a a' k,
    getIndex (a :: k) a' = Some 0 ->
    a = a'.
forall (a a' : atom) (k : list atom),
getIndex (a :: k) a' = Some 0 -> a = a'
Proof.
forall (a a' : atom) (k : list atom),
getIndex (a :: k) a' = Some 0 -> a = a'
  introv Hlookup; cbn in *.
a, a': atom
k: list atom
Hlookup: (if a' == a
 then Some 0
 else map S (getIndex k a')) = 
Some 0
a = a'
  compare atoms.
a, a': atom
k: list atom
DESTR_NEQ: a' <> a
Hlookup: map S (getIndex k a') = Some 0
DESTR_NEQs: a <> a'
a = a'
  lookup atom a' in key k;
    rewrite H_key_lookup in Hlookup;
    now inversion Hlookup.
Qed.

Lemma getIndex_cons_S: forall a x k ix,
    getIndex (x :: k) a = Some (S ix) ->
    a <> x /\ getIndex k a = Some ix.
forall (a x : atom) (k : list atom) (ix : nat),
getIndex (x :: k) a = Some (S ix) ->
a <> x /\ getIndex k a = Some ix
Proof.
forall (a x : atom) (k : list atom) (ix : nat),
getIndex (x :: k) a = Some (S ix) ->
a <> x /\ getIndex k a = Some ix
  introv HH.
a, x: atom
k: list atom
ix: nat
HH: getIndex (x :: k) a = Some (S ix)
a <> x /\ getIndex k a = Some ix
  cbn in HH.
a, x: atom
k: list atom
ix: nat
HH: (if a == x then Some 0 else map S (getIndex k a)) =
Some (S ix)
a <> x /\ getIndex k a = Some ix
  destruct_eq_args a x.
a, x: atom
k: list atom
ix: nat
DESTR_NEQ: a <> x
HH: map S (getIndex k a) = Some (S ix)
DESTR_NEQs: x <> a
a <> x /\ getIndex k a = Some ix
  split.
a, x: atom
k: list atom
ix: nat
DESTR_NEQ: a <> x
HH: map S (getIndex k a) = Some (S ix)
DESTR_NEQs: x <> a
a <> x
a, x: atom
k: list atom
ix: nat
DESTR_NEQ: a <> x
HH: map S (getIndex k a) = Some (S ix)
DESTR_NEQs: x <> a
getIndex k a = Some ix assumption.
a, x: atom
k: list atom
ix: nat
DESTR_NEQ: a <> x
HH: map S (getIndex k a) = Some (S ix)
DESTR_NEQs: x <> a
getIndex k a = Some ix
  eauto using (map_Some_inv S).
Qed.

Theorem getIndex_cons: forall a k a' ix,
    getIndex (a :: k) a' = Some ix ->
    (a' = a /\ ix = 0) \/
      (a' <> a /\ exists ix', ix = S ix' /\ getIndex k a' = Some ix').
forall (a : atom) (k : list atom) (a' : atom)
  (ix : nat),
getIndex (a :: k) a' = Some ix ->
a' = a /\ ix = 0 \/
a' <> a /\
(exists ix' : nat,
   ix = S ix' /\ getIndex k a' = Some ix')
Proof.
forall (a : atom) (k : list atom) (a' : atom)
  (ix : nat),
getIndex (a :: k) a' = Some ix ->
a' = a /\ ix = 0 \/
a' <> a /\
(exists ix' : nat,
   ix = S ix' /\ getIndex k a' = Some ix')
  introv Hyp.
a: atom
k: list atom
a': atom
ix: nat
Hyp: getIndex (a :: k) a' = Some ix
a' = a /\ ix = 0 \/
a' <> a /\
(exists ix' : nat,
   ix = S ix' /\ getIndex k a' = Some ix') destruct ix; [left|right].
a: atom
k: list atom
a': atom
Hyp: getIndex (a :: k) a' = Some 0
a' = a /\ 0 = 0
a: atom
k: list atom
a': atom
ix: nat
Hyp: getIndex (a :: k) a' = Some (S ix)
a' <> a /\
(exists ix' : nat,
   S ix = S ix' /\ getIndex k a' = Some ix')
  -
a: atom
k: list atom
a': atom
Hyp: getIndex (a :: k) a' = Some 0
a' = a /\ 0 = 0 apply getIndex_cons_0 in Hyp.
a: atom
k: list atom
a': atom
Hyp: a = a'
a' = a /\ 0 = 0
    intuition.
  -
a: atom
k: list atom
a': atom
ix: nat
Hyp: getIndex (a :: k) a' = Some (S ix)
a' <> a /\
(exists ix' : nat,
   S ix = S ix' /\ getIndex k a' = Some ix') apply getIndex_cons_S in Hyp.
a: atom
k: list atom
a': atom
ix: nat
Hyp: a' <> a /\ getIndex k a' = Some ix
a' <> a /\
(exists ix' : nat,
   S ix = S ix' /\ getIndex k a' = Some ix')
    intuition eauto.
Qed.

(** ** Insertion and <<key_lookup_ix>> *)
(******************************************************************************)
Lemma key_lookup_ix_in:
  forall (k:  key) (ix: nat) (a: atom),
    getName k ix = Some a -> a ∈ k.
forall (k : key) (ix : nat) (a : atom),
getName k ix = Some a -> a ∈ k
Proof.
forall (k : key) (ix : nat) (a : atom),
getName k ix = Some a -> a ∈ k
  introv Hin.
k: key
ix: nat
a: atom
Hin: getName k ix = Some a
a ∈ k
  generalize dependent ix.
k: key
a: atom
forall ix : nat, getName k ix = Some a -> a ∈ k
  induction k; intros ix Hin.
a: atom
ix: nat
Hin: getName [] ix = Some a
a ∈ []
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
ix: nat
Hin: getName (a0 :: k) ix = Some a
a ∈ (a0 :: k)
  -
a: atom
ix: nat
Hin: getName [] ix = Some a
a ∈ [] inversion Hin.
  -
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
ix: nat
Hin: getName (a0 :: k) ix = Some a
a ∈ (a0 :: k) destruct ix.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
Hin: getName (a0 :: k) 0 = Some a
a ∈ (a0 :: k)
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
ix: nat
Hin: getName (a0 :: k) (S ix) = Some a
a ∈ (a0 :: k)
    +
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
Hin: getName (a0 :: k) 0 = Some a
a ∈ (a0 :: k) cbn in *.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
Hin: Some a0 = Some a
a0 = a \/ List.In a k inversion Hin.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
Hin: Some a0 = Some a
H0: a0 = a
a = a \/ List.In a k now left.
    +
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
ix: nat
Hin: getName (a0 :: k) (S ix) = Some a
a ∈ (a0 :: k) cbn in Hin.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
ix: nat
Hin: getName k ix = Some a
a ∈ (a0 :: k)
      rewrite element_of_list_cons.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
ix: nat
Hin: getName k ix = Some a
a = a0 \/ a ∈ k
      right.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> a ∈ k
ix: nat
Hin: getName k ix = Some a
a ∈ k eauto.
Qed.

Lemma key_lookup_ix_Some1:
  forall (k:  key) (ix: nat) (a: atom),
    getName k ix = Some a -> contains_ix_upto ix k.
forall (k : key) (ix : nat) (a : atom),
getName k ix = Some a -> contains_ix_upto ix k
Proof.
forall (k : key) (ix : nat) (a : atom),
getName k ix = Some a -> contains_ix_upto ix k
  introv Hin.
k: key
ix: nat
a: atom
Hin: getName k ix = Some a
contains_ix_upto ix k
  unfold contains_ix_upto.
k: key
ix: nat
a: atom
Hin: getName k ix = Some a
ix < length k
  generalize dependent ix.
k: key
a: atom
forall ix : nat,
getName k ix = Some a -> ix < length k
  induction k; intros ix Hin.
a: atom
ix: nat
Hin: getName [] ix = Some a
ix < length []
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
ix: nat
Hin: getName (a0 :: k) ix = Some a
ix < length (a0 :: k)
  -
a: atom
ix: nat
Hin: getName [] ix = Some a
ix < length [] false.
  -
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
ix: nat
Hin: getName (a0 :: k) ix = Some a
ix < length (a0 :: k) destruct ix.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
Hin: getName (a0 :: k) 0 = Some a
0 < length (a0 :: k)
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
ix: nat
Hin: getName (a0 :: k) (S ix) = Some a
S ix < length (a0 :: k)
    +
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
Hin: getName (a0 :: k) 0 = Some a
0 < length (a0 :: k) cbn.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
Hin: getName (a0 :: k) 0 = Some a
0 < S (length k) lia.
    +
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
ix: nat
Hin: getName (a0 :: k) (S ix) = Some a
S ix < length (a0 :: k) cbn.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
ix: nat
Hin: getName (a0 :: k) (S ix) = Some a
S ix < S (length k) cbn in Hin.
a0: atom
k: list atom
a: atom
IHk: forall ix : nat, getName k ix = Some a -> ix < length k
ix: nat
Hin: getName k ix = Some a
S ix < S (length k)
      specialize (IHk ix Hin).
a0: atom
k: list atom
a: atom
ix: nat
IHk: ix < length k
Hin: getName k ix = Some a
S ix < S (length k)
      lia.
Qed.

Lemma key_lookup_ix_Some2:
  forall (k:  key) (ix: nat),
    contains_ix_upto ix k ->
    {a:atom | getName k ix = Some a}.
forall (k : key) (ix : nat),
contains_ix_upto ix k ->
{a : atom | getName k ix = Some a}
Proof.
forall (k : key) (ix : nat),
contains_ix_upto ix k ->
{a : atom | getName k ix = Some a}
  unfold contains_ix_upto.
forall (k : key) (ix : nat),
ix < length k -> {a : atom | getName k ix = Some a}
  intros.
k: key
ix: nat
H: ix < length k
{a : atom | getName k ix = Some a}
  generalize dependent k.
ix: nat
forall k : key,
ix < length k -> {a : atom | getName k ix = Some a}
  induction ix; intros k Hlt.
k: key
Hlt: 0 < length k
{a : atom | getName k 0 = Some a}
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
k: key
Hlt: S ix < length k
{a : atom | getName k (S ix) = Some a}
  -
k: key
Hlt: 0 < length k
{a : atom | getName k 0 = Some a} destruct k.
Hlt: 0 < length []
{a : atom | getName [] 0 = Some a}
n: atom
k: list atom
Hlt: 0 < length (n :: k)
{a : atom | getName (n :: k) 0 = Some a}
    +
Hlt: 0 < length []
{a : atom | getName [] 0 = Some a} cbn in Hlt.
Hlt: 0 < 0
{a : atom | getName [] 0 = Some a} lia.
    +
n: atom
k: list atom
Hlt: 0 < length (n :: k)
{a : atom | getName (n :: k) 0 = Some a} cbn.
n: atom
k: list atom
Hlt: 0 < length (n :: k)
{a : atom | Some n = Some a} eauto.
  -
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
k: key
Hlt: S ix < length k
{a : atom | getName k (S ix) = Some a} destruct k.
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
Hlt: S ix < length []
{a : atom | getName [] (S ix) = Some a}
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
n: atom
k: list atom
Hlt: S ix < length (n :: k)
{a : atom | getName (n :: k) (S ix) = Some a}
    +
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
Hlt: S ix < length []
{a : atom | getName [] (S ix) = Some a} false.
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
Hlt: S ix < length []
False cbn in Hlt.
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
Hlt: S ix < 0
False lia.
    +
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
n: atom
k: list atom
Hlt: S ix < length (n :: k)
{a : atom | getName (n :: k) (S ix) = Some a} cbn in Hlt.
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
n: atom
k: list atom
Hlt: S ix < S (length k)
{a : atom | getName (n :: k) (S ix) = Some a}
      cbn.
ix: nat
IHix: forall k : key,
ix < length k ->
{a : atom | getName k ix = Some a}
n: atom
k: list atom
Hlt: S ix < S (length k)
{a : atom | getName k ix = Some a}
      specialize (IHix k ltac:(lia)).
ix: nat
k: list atom
IHix: {a : atom | getName k ix = Some a}
n: atom
Hlt: S ix < S (length k)
{a : atom | getName k ix = Some a}
      assumption.
Qed.

Lemma key_lookup_ix_Some_iff:
  forall (k:  key) (ix: nat),
    contains_ix_upto ix k <->
      exists a, getName k ix = Some a.
forall (k : key) (ix : nat),
contains_ix_upto ix k <->
(exists a : atom, getName k ix = Some a)
Proof.
forall (k : key) (ix : nat),
contains_ix_upto ix k <->
(exists a : atom, getName k ix = Some a)
  intros.
k: key
ix: nat
contains_ix_upto ix k <->
(exists a : atom, getName k ix = Some a) split.
k: key
ix: nat
contains_ix_upto ix k ->
exists a : atom, getName k ix = Some a
k: key
ix: nat
(exists a : atom, getName k ix = Some a) ->
contains_ix_upto ix k
  -
k: key
ix: nat
contains_ix_upto ix k ->
exists a : atom, getName k ix = Some a intro H; apply key_lookup_ix_Some2 in H.
k: key
ix: nat
H: {a : atom | getName k ix = Some a}
exists a : atom, getName k ix = Some a firstorder.
  -
k: key
ix: nat
(exists a : atom, getName k ix = Some a) ->
contains_ix_upto ix k intros [a H].
k: key
ix: nat
a: atom
H: getName k ix = Some a
contains_ix_upto ix k eapply key_lookup_ix_Some1.
k: key
ix: nat
a: atom
H: getName k ix = Some a
getName k ix = Some ?a eauto.
Qed.

Lemma key_lookup_ix_None1:
  forall (k:  key) (ix: nat),
    getName k ix = None -> ~ (contains_ix_upto ix k).
forall (k : key) (ix : nat),
getName k ix = None -> ~ contains_ix_upto ix k
Proof.
forall (k : key) (ix : nat),
getName k ix = None -> ~ contains_ix_upto ix k
  introv Hin.
k: key
ix: nat
Hin: getName k ix = None
~ contains_ix_upto ix k
  unfold contains_ix_upto.
k: key
ix: nat
Hin: getName k ix = None
~ ix < length k
  generalize dependent ix.
k: key
forall ix : nat,
getName k ix = None -> ~ ix < length k
  induction k; intros ix Hin.
ix: nat
Hin: getName [] ix = None
~ ix < length []
a: atom
k: list atom
IHk: forall ix : nat, getName k ix = None -> ~ ix < length k
ix: nat
Hin: getName (a :: k) ix = None
~ ix < length (a :: k)
  -
ix: nat
Hin: getName [] ix = None
~ ix < length [] cbn.
ix: nat
Hin: getName [] ix = None
~ ix < 0 lia.
  -
a: atom
k: list atom
IHk: forall ix : nat, getName k ix = None -> ~ ix < length k
ix: nat
Hin: getName (a :: k) ix = None
~ ix < length (a :: k) destruct ix.
a: atom
k: list atom
IHk: forall ix : nat, getName k ix = None -> ~ ix < length k
Hin: getName (a :: k) 0 = None
~ 0 < length (a :: k)
a: atom
k: list atom
IHk: forall ix : nat, getName k ix = None -> ~ ix < length k
ix: nat
Hin: getName (a :: k) (S ix) = None
~ S ix < length (a :: k)
    +
a: atom
k: list atom
IHk: forall ix : nat, getName k ix = None -> ~ ix < length k
Hin: getName (a :: k) 0 = None
~ 0 < length (a :: k) false.
    +
a: atom
k: list atom
IHk: forall ix : nat, getName k ix = None -> ~ ix < length k
ix: nat
Hin: getName (a :: k) (S ix) = None
~ S ix < length (a :: k) cbn.
a: atom
k: list atom
IHk: forall ix : nat, getName k ix = None -> ~ ix < length k
ix: nat
Hin: getName (a :: k) (S ix) = None
~ S ix < S (length k) cbn in Hin.
a: atom
k: list atom
IHk: forall ix : nat, getName k ix = None -> ~ ix < length k
ix: nat
Hin: getName k ix = None
~ S ix < S (length k)
      specialize (IHk ix Hin).
a: atom
k: list atom
ix: nat
IHk: ~ ix < length k
Hin: getName k ix = None
~ S ix < S (length k)
      apply PeanoNat.Nat.le_ngt.
a: atom
k: list atom
ix: nat
IHk: ~ ix < length k
Hin: getName k ix = None
S (length k) <= S ix
      lia.
Qed.

Lemma key_lookup_ix_None2:
  forall (k:  key) (ix: nat),
    ~ (contains_ix_upto ix k) ->
    getName k ix = None.
forall (k : key) (ix : nat),
~ contains_ix_upto ix k -> getName k ix = None
Proof.
forall (k : key) (ix : nat),
~ contains_ix_upto ix k -> getName k ix = None
  introv Hin.
k: key
ix: nat
Hin: ~ contains_ix_upto ix k
getName k ix = None
  unfold contains_ix_upto in *.
k: key
ix: nat
Hin: ~ ix < length k
getName k ix = None
  generalize dependent ix.
k: key
forall ix : nat,
~ ix < length k -> getName k ix = None
  induction k; intros ix Hin.
ix: nat
Hin: ~ ix < length []
getName [] ix = None
a: atom
k: list atom
IHk: forall ix : nat, ~ ix < length k -> getName k ix = None
ix: nat
Hin: ~ ix < length (a :: k)
getName (a :: k) ix = None
  -
ix: nat
Hin: ~ ix < length []
getName [] ix = None reflexivity.
  -
a: atom
k: list atom
IHk: forall ix : nat, ~ ix < length k -> getName k ix = None
ix: nat
Hin: ~ ix < length (a :: k)
getName (a :: k) ix = None cbn in *.
a: atom
k: list atom
IHk: forall ix : nat, ~ ix < length k -> getName k ix = None
ix: nat
Hin: ~ ix < S (length k)
match ix with
| 0 => Some a
| S ix => getName k ix
end = None destruct ix.
a: atom
k: list atom
IHk: forall ix : nat, ~ ix < length k -> getName k ix = None
Hin: ~ 0 < S (length k)
Some a = None
a: atom
k: list atom
IHk: forall ix : nat, ~ ix < length k -> getName k ix = None
ix: nat
Hin: ~ S ix < S (length k)
getName k ix = None
    +
a: atom
k: list atom
IHk: forall ix : nat, ~ ix < length k -> getName k ix = None
Hin: ~ 0 < S (length k)
Some a = None contradict Hin.
a: atom
k: list atom
IHk: forall ix : nat, ~ ix < length k -> getName k ix = None
0 < S (length k) lia.
    +
a: atom
k: list atom
IHk: forall ix : nat, ~ ix < length k -> getName k ix = None
ix: nat
Hin: ~ S ix < S (length k)
getName k ix = None specialize (IHk ix ltac:(lia)).
a: atom
k: list atom
ix: nat
IHk: getName k ix = None
Hin: ~ S ix < S (length k)
getName k ix = None
      assumption.
Qed.

Lemma key_lookup_ix_None_iff:
  forall (k:  key) (ix: nat),
    ~ (contains_ix_upto ix k) <->
    getName k ix = None.
forall (k : key) (ix : nat),
~ contains_ix_upto ix k <-> getName k ix = None
Proof.
forall (k : key) (ix : nat),
~ contains_ix_upto ix k <-> getName k ix = None
  intros; split;
    auto using key_lookup_ix_None1, key_lookup_ix_None2.
Qed.

Theorem key_lookup_ix_decide:
  forall (k: key) (n: nat),
    ((contains_ix_upto n k) * {a: atom | getName k n = Some a}) +
      {~ contains_ix_upto n k /\ getName k n = None}.
forall (k : key) (n : nat),
contains_ix_upto n k *
{a : atom | getName k n = Some a} +
{~ contains_ix_upto n k /\ getName k n = None}
Proof.
forall (k : key) (n : nat),
contains_ix_upto n k *
{a : atom | getName k n = Some a} +
{~ contains_ix_upto n k /\ getName k n = None}
  intros.
k: key
n: nat
contains_ix_upto n k *
{a : atom | getName k n = Some a} +
{~ contains_ix_upto n k /\ getName k n = None}
  destruct (key_is_ix_in k n); [left|right].
k: key
n: nat
c: contains_ix_upto n k
(contains_ix_upto n k *
 {a : atom | getName k n = Some a})%type
k: key
n: nat
n0: ~ contains_ix_upto n k
~ contains_ix_upto n k /\ getName k n = None
  -
k: key
n: nat
c: contains_ix_upto n k
(contains_ix_upto n k *
 {a : atom | getName k n = Some a})%type split.
k: key
n: nat
c: contains_ix_upto n k
contains_ix_upto n k
k: key
n: nat
c: contains_ix_upto n k
{a : atom | getName k n = Some a}
    +
k: key
n: nat
c: contains_ix_upto n k
contains_ix_upto n k assumption.
    +
k: key
n: nat
c: contains_ix_upto n k
{a : atom | getName k n = Some a} auto using key_lookup_ix_Some2.
  -
k: key
n: nat
n0: ~ contains_ix_upto n k
~ contains_ix_upto n k /\ getName k n = None split.
k: key
n: nat
n0: ~ contains_ix_upto n k
~ contains_ix_upto n k
k: key
n: nat
n0: ~ contains_ix_upto n k
getName k n = None
    +
k: key
n: nat
n0: ~ contains_ix_upto n k
~ contains_ix_upto n k assumption.
    +
k: key
n: nat
n0: ~ contains_ix_upto n k
getName k n = None auto using key_lookup_ix_None2.
Defined.

Ltac lookup_ix_in_key k n :=
  let a := fresh "a" in
  let Hcont := fresh "Hcont" in
  let H_key_lookup := fresh "H_key_lookup" in
  destruct (key_lookup_ix_decide k n) as
    [[Hcont [a H_key_lookup]] | [Hcont H_key_lookup]];
  try contradiction.

Tactic Notation "lookup" "index" constr(ix) "in" "key" constr(k) :=
  lookup_ix_in_key k ix.

Goal forall k (ix: nat), contains_ix_upto ix k \/ ~ contains_ix_upto ix k.
forall (k : key) (ix : nat),
contains_ix_upto ix k \/ ~ contains_ix_upto ix k
Proof.
forall (k : key) (ix : nat),
contains_ix_upto ix k \/ ~ contains_ix_upto ix k
  intros.
k: key
ix: nat
contains_ix_upto ix k \/ ~ contains_ix_upto ix k
  lookup index ix in key k.
k: key
ix: nat
Hcont: contains_ix_upto ix k
a: atom
H_key_lookup: getName k ix = Some a
contains_ix_upto ix k \/ ~ contains_ix_upto ix k
k: key
ix: nat
Hcont: ~ contains_ix_upto ix k
H_key_lookup: getName k ix = None
contains_ix_upto ix k \/ ~ contains_ix_upto ix k
  -
k: key
ix: nat
Hcont: contains_ix_upto ix k
a: atom
H_key_lookup: getName k ix = Some a
contains_ix_upto ix k \/ ~ contains_ix_upto ix k left.
k: key
ix: nat
Hcont: contains_ix_upto ix k
a: atom
H_key_lookup: getName k ix = Some a
contains_ix_upto ix k intuition.
  -
k: key
ix: nat
Hcont: ~ contains_ix_upto ix k
H_key_lookup: getName k ix = None
contains_ix_upto ix k \/ ~ contains_ix_upto ix k now right.
Qed.

(** ** Properties of <<getName>> *)
(******************************************************************************)
Lemma key_lookup_zero: forall a k ix,
    ix = 0 ->
    getName (a :: k) ix = Some a.
forall (a : atom) (k : list atom) (ix : nat),
ix = 0 -> getName (a :: k) ix = Some a
Proof.
forall (a : atom) (k : list atom) (ix : nat),
ix = 0 -> getName (a :: k) ix = Some a
  intros.
a: atom
k: list atom
ix: nat
H: ix = 0
getName (a :: k) ix = Some a subst.
a: atom
k: list atom
getName (a :: k) 0 = Some a
  reflexivity.
Qed.

Lemma getName_S: forall k ix a,
    getName k ix = Some a ->
    forall a', getName (a' :: k) (S ix) = Some a.
forall (k : key) (ix : nat) (a : atom),
getName k ix = Some a ->
forall a' : atom, getName (a' :: k) (S ix) = Some a
Proof.
forall (k : key) (ix : nat) (a : atom),
getName k ix = Some a ->
forall a' : atom, getName (a' :: k) (S ix) = Some a
  intros.
k: key
ix: nat
a: atom
H: getName k ix = Some a
a': atom
getName (a' :: k) (S ix) = Some a
  assumption.
Qed.

Lemma getName_cons: forall a' a k ix,
    getName (a' :: k) ix = Some a ->
    ix = 0 /\ a = a' \/
      exists ix', ix = S ix' /\ getName k ix' = Some a.
forall (a' a : atom) (k : list atom) (ix : nat),
getName (a' :: k) ix = Some a ->
ix = 0 /\ a = a' \/
(exists ix' : nat,
   ix = S ix' /\ getName k ix' = Some a)
Proof.
forall (a' a : atom) (k : list atom) (ix : nat),
getName (a' :: k) ix = Some a ->
ix = 0 /\ a = a' \/
(exists ix' : nat,
   ix = S ix' /\ getName k ix' = Some a)
  introv Hin.
a', a: atom
k: list atom
ix: nat
Hin: getName (a' :: k) ix = Some a
ix = 0 /\ a = a' \/
(exists ix' : nat,
   ix = S ix' /\ getName k ix' = Some a) destruct ix.
a', a: atom
k: list atom
Hin: getName (a' :: k) 0 = Some a
0 = 0 /\ a = a' \/
(exists ix' : nat, 0 = S ix' /\ getName k ix' = Some a)
a', a: atom
k: list atom
ix: nat
Hin: getName (a' :: k) (S ix) = Some a
S ix = 0 /\ a = a' \/
(exists ix' : nat,
   S ix = S ix' /\ getName k ix' = Some a)
  -
a', a: atom
k: list atom
Hin: getName (a' :: k) 0 = Some a
0 = 0 /\ a = a' \/
(exists ix' : nat, 0 = S ix' /\ getName k ix' = Some a) cbn in Hin.
a', a: atom
k: list atom
Hin: Some a' = Some a
0 = 0 /\ a = a' \/
(exists ix' : nat, 0 = S ix' /\ getName k ix' = Some a) inversion Hin.
a', a: atom
k: list atom
Hin: Some a' = Some a
H0: a' = a
0 = 0 /\ a = a \/
(exists ix' : nat, 0 = S ix' /\ getName k ix' = Some a)
    left.
a', a: atom
k: list atom
Hin: Some a' = Some a
H0: a' = a
0 = 0 /\ a = a now split.
  -
a', a: atom
k: list atom
ix: nat
Hin: getName (a' :: k) (S ix) = Some a
S ix = 0 /\ a = a' \/
(exists ix' : nat,
   S ix = S ix' /\ getName k ix' = Some a) cbn in Hin.
a', a: atom
k: list atom
ix: nat
Hin: getName k ix = Some a
S ix = 0 /\ a = a' \/
(exists ix' : nat,
   S ix = S ix' /\ getName k ix' = Some a) right.
a', a: atom
k: list atom
ix: nat
Hin: getName k ix = Some a
exists ix' : nat,
  S ix = S ix' /\ getName k ix' = Some a
    exists ix.
a', a: atom
k: list atom
ix: nat
Hin: getName k ix = Some a
S ix = S ix /\ getName k ix = Some a split; auto.
Qed.

Lemma key_bijection1: forall a k ix,
    getIndex k a = Some ix ->
    getName k ix = Some a.
forall (a : atom) (k : key) (ix : nat),
getIndex k a = Some ix -> getName k ix = Some a
Proof.
forall (a : atom) (k : key) (ix : nat),
getIndex k a = Some ix -> getName k ix = Some a
  intros.
a: atom
k: key
ix: nat
H: getIndex k a = Some ix
getName k ix = Some a
  generalize dependent ix.
a: atom
k: key
forall ix : nat,
getIndex k a = Some ix -> getName k ix = Some a
  induction k; intros ix Hix.
a: atom
ix: nat
Hix: getIndex [] a = Some ix
getName [] ix = Some a
a, a0: atom
k: list atom
IHk: forall ix : nat, getIndex k a = Some ix -> getName k ix = Some a
ix: nat
Hix: getIndex (a0 :: k) a = Some ix
getName (a0 :: k) ix = Some a
  -
a: atom
ix: nat
Hix: getIndex [] a = Some ix
getName [] ix = Some a cbn in *.
a: atom
ix: nat
Hix: None = Some ix
None = Some a inversion Hix.
  -
a, a0: atom
k: list atom
IHk: forall ix : nat, getIndex k a = Some ix -> getName k ix = Some a
ix: nat
Hix: getIndex (a0 :: k) a = Some ix
getName (a0 :: k) ix = Some a apply getIndex_cons in Hix.
a, a0: atom
k: list atom
IHk: forall ix : nat, getIndex k a = Some ix -> getName k ix = Some a
ix: nat
Hix: a = a0 /\ ix = 0 \/
a <> a0 /\ (exists ix' : nat, ix = S ix' /\ getIndex k a = Some ix')
getName (a0 :: k) ix = Some a
    destruct Hix as
      [ [Heq Hix0] | [Hneq [Hix [Heq Hlookup]]] ]; subst.
a0: atom
k: list atom
IHk: forall ix : nat, getIndex k a0 = Some ix -> getName k ix = Some a0
getName (a0 :: k) 0 = Some a0
a, a0: atom
k: list atom
IHk: forall ix : nat, getIndex k a = Some ix -> getName k ix = Some a
Hneq: a <> a0
Hix: nat
Hlookup: getIndex k a = Some Hix
getName (a0 :: k) (S Hix) = Some a
    +
a0: atom
k: list atom
IHk: forall ix : nat,
getIndex k a0 = Some ix ->
getName k ix = Some a0
getName (a0 :: k) 0 = Some a0 reflexivity.
    +
a, a0: atom
k: list atom
IHk: forall ix : nat,
getIndex k a = Some ix -> getName k ix = Some a
Hneq: a <> a0
Hix: nat
Hlookup: getIndex k a = Some Hix
getName (a0 :: k) (S Hix) = Some a cbn.
a, a0: atom
k: list atom
IHk: forall ix : nat,
getIndex k a = Some ix -> getName k ix = Some a
Hneq: a <> a0
Hix: nat
Hlookup: getIndex k a = Some Hix
getName k Hix = Some a auto.
Qed.

Lemma key_bijection2: forall a k ix,
    unique k ->
    getName k ix = Some a ->
    getIndex k a = Some ix.
forall (a : atom) (k : list atom) (ix : nat),
unique k ->
getName k ix = Some a -> getIndex k a = Some ix
Proof.
forall (a : atom) (k : list atom) (ix : nat),
unique k ->
getName k ix = Some a -> getIndex k a = Some ix
  introv Huniq Hix.
a: atom
k: list atom
ix: nat
Huniq: unique k
Hix: getName k ix = Some a
getIndex k a = Some ix
  generalize dependent ix.
a: atom
k: list atom
Huniq: unique k
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
  induction k; intros ix Hix.
a: atom
Huniq: unique []
ix: nat
Hix: getName [] ix = Some a
getIndex [] a = Some ix
a, a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix: nat
Hix: getName (a0 :: k) ix = Some a
getIndex (a0 :: k) a = Some ix
  -
a: atom
Huniq: unique []
ix: nat
Hix: getName [] ix = Some a
getIndex [] a = Some ix cbn in Hix.
a: atom
Huniq: unique []
ix: nat
Hix: None = Some a
getIndex [] a = Some ix inversion Hix.
  -
a, a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix: nat
Hix: getName (a0 :: k) ix = Some a
getIndex (a0 :: k) a = Some ix cbn.
a, a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix: nat
Hix: getName (a0 :: k) ix = Some a
(if a == a0 then Some 0 else map S (getIndex k a)) =
Some ix
    apply getName_cons in Hix.
a, a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix: nat
Hix: ix = 0 /\ a = a0 \/
(exists ix' : nat,
   ix = S ix' /\ getName k ix' = Some a)
(if a == a0 then Some 0 else map S (getIndex k a)) =
Some ix
    destruct Hix as [[Hix_zero Heq] | [ix' [Heq Hrest]]].
a, a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix: nat
Hix_zero: ix = 0
Heq: a = a0
(if a == a0 then Some 0 else map S (getIndex k a)) =
Some ix
a, a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix, ix': nat
Heq: ix = S ix'
Hrest: getName k ix' = Some a
(if a == a0 then Some 0 else map S (getIndex k a)) =
Some ix
    +
a, a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix: nat
Hix_zero: ix = 0
Heq: a = a0
(if a == a0 then Some 0 else map S (getIndex k a)) =
Some ix subst.
a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a0 ->
getIndex k a0 = Some ix
(if a0 == a0 then Some 0 else map S (getIndex k a0)) =
Some 0 compare atoms.
    +
a, a0: atom
k: list atom
Huniq: unique (a0 :: k)
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix, ix': nat
Heq: ix = S ix'
Hrest: getName k ix' = Some a
(if a == a0 then Some 0 else map S (getIndex k a)) =
Some ix destruct Huniq as [Hnin Huniq].
a, a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: unique k ->
forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix, ix': nat
Heq: ix = S ix'
Hrest: getName k ix' = Some a
(if a == a0 then Some 0 else map S (getIndex k a)) =
Some ix
      specialize (IHk Huniq).
a, a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix, ix': nat
Heq: ix = S ix'
Hrest: getName k ix' = Some a
(if a == a0 then Some 0 else map S (getIndex k a)) =
Some ix
      compare atoms.
a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: forall ix : nat,
getName k ix = Some a0 ->
getIndex k a0 = Some ix
ix': nat
Hrest: getName k ix' = Some a0
DESTR_EQs: a0 = a0
Some 0 = Some (S ix')
a, a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix': nat
Hrest: getName k ix' = Some a
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
map S (getIndex k a) = Some (S ix')
      *
a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: forall ix : nat,
getName k ix = Some a0 ->
getIndex k a0 = Some ix
ix': nat
Hrest: getName k ix' = Some a0
DESTR_EQs: a0 = a0
Some 0 = Some (S ix') false.
a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: forall ix : nat,
getName k ix = Some a0 ->
getIndex k a0 = Some ix
ix': nat
Hrest: getName k ix' = Some a0
DESTR_EQs: a0 = a0
False
        apply key_lookup_ix_in in Hrest.
a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: forall ix : nat,
getName k ix = Some a0 ->
getIndex k a0 = Some ix
ix': nat
Hrest: a0 ∈ k
DESTR_EQs: a0 = a0
False
        contradiction.
      *
a, a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix': nat
Hrest: getName k ix' = Some a
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
map S (getIndex k a) = Some (S ix') rewrite (IHk ix' Hrest).
a, a0: atom
k: list atom
Hnin: ~ a0 ∈ k
Huniq: unique k
IHk: forall ix : nat,
getName k ix = Some a -> getIndex k a = Some ix
ix': nat
Hrest: getName k ix' = Some a
DESTR_NEQ: a <> a0
DESTR_NEQs: a0 <> a
map S (Some ix') = Some (S ix')
        reflexivity.
Qed.

Lemma key_bijection: forall a k ix,
    unique k ->
    getName k ix = Some a <->
      getIndex k a = Some ix.
forall (a : atom) (k : list atom) (ix : nat),
unique k ->
getName k ix = Some a <-> getIndex k a = Some ix
Proof.
forall (a : atom) (k : list atom) (ix : nat),
unique k ->
getName k ix = Some a <-> getIndex k a = Some ix
  intros.
a: atom
k: list atom
ix: nat
H: unique k
getName k ix = Some a <-> getIndex k a = Some ix
  split; auto using key_bijection1, key_bijection2.
Qed.