From 924759a303e3f684daf78e690811aafdc02434d7 Mon Sep 17 00:00:00 2001
From: emarzion <emarzion@gmail.com>
Date: Mon, 30 Sep 2024 22:11:06 -0500
Subject: [PATCH] cleanup

---
 bin/query/dune          |   2 +
 theory/Bear/BearGame.v  |   4 +-
 theory/TB/TB.v          | 136 +-------------
 theory/Util/AssocList.v |  10 --
 theory/Util/GameUtil.v  |  29 +++
 theory/Util/IntMap.v    |  32 ++--
 theory/Util/ListUtil.v  | 177 +++++++++++++++++++
 theory/Util/StringMap.v | 383 ----------------------------------------
 8 files changed, 222 insertions(+), 551 deletions(-)
 create mode 100644 theory/Util/GameUtil.v
 create mode 100644 theory/Util/ListUtil.v
 delete mode 100644 theory/Util/StringMap.v

diff --git a/bin/query/dune b/bin/query/dune
index 960b9ee..534f7f2 100644
--- a/bin/query/dune
+++ b/bin/query/dune
@@ -12,6 +12,7 @@
     IntHash
     IntMap
     List0
+    ListUtil
     OCamlTB
     OMap
     Player
@@ -45,6 +46,7 @@
     IntHash
     IntMap
     List0
+    ListUtil
     OCamlTB
     OMap
     Player
diff --git a/theory/Bear/BearGame.v b/theory/Bear/BearGame.v
index 7c545a1..5696098 100644
--- a/theory/Bear/BearGame.v
+++ b/theory/Bear/BearGame.v
@@ -349,7 +349,7 @@ Proof.
       rewrite Bool.orb_true_iff in Hv.
       destruct Hv as [Hv|Hv].
       * unfold in_decb in Hv.
-        destruct (in_dec v (hunters s)).
+        destruct (ListUtil.in_dec v (hunters s)).
         -- discriminate.
         -- contradiction.
       * unfold eqb in Hv.
@@ -369,7 +369,7 @@ Proof.
     + rewrite filter_In in HIn.
       destruct HIn as [_ HIn].
       unfold in_decb in HIn.
-      destruct (in_dec v (hunters s)).
+      destruct (ListUtil.in_dec v (hunters s)).
       * discriminate.
       * auto.
 Defined.
diff --git a/theory/TB/TB.v b/theory/TB/TB.v
index 31ab2d6..7e350fd 100644
--- a/theory/TB/TB.v
+++ b/theory/TB/TB.v
@@ -14,14 +14,7 @@ Require Import TBGen.Util.IntMap.
 Require Import TBGen.Util.IntHash.
 Require Import Games.Util.Dec.
 Require Import TBGen.Util.Loop.
-
-Global Instance List_disc {X} `{Discrete X} : Discrete (list X).
-Proof.
-  constructor.
-  unfold decision.
-  decide equality.
-  apply eq_dec.
-Defined.
+Require Import TBGen.Util.ListUtil.
 
 Class FinGame (G : Game) : Type := {
   enum_states : list (GameState G);
@@ -103,65 +96,6 @@ Definition add_positions (m : M (Player * nat)) (winner : Player) (n : nat)
   (ps : list (GameState G)) : M (Player * nat) :=
   hash_adds (map (tag winner n) ps) m.
 
-Fixpoint filter_Nones_aux {X Y} (acc : list X) (f : X -> option Y) (xs : list X) : list X :=
-  match xs with
-  | [] => acc
-  | x :: xs' =>
-    match f x with
-    | None => filter_Nones_aux (x :: acc) f xs'
-    | Some _ => filter_Nones_aux acc f xs'
-    end
-  end.
-
-Lemma In_filter_Nones_aux_correct1 {X Y} (f : X -> option Y) (xs : list X) :
-  forall acc x, In x (filter_Nones_aux acc f xs) -> (f x = None /\ In x xs) \/ In x acc.
-Proof.
-  induction xs as [|x' xs']; intros acc x HIn; simpl in *.
-  - now right.
-  - destruct (f x') eqn:fx'.
-    + destruct (IHxs' _ _ HIn).
-      * left; split; tauto.
-      * now right.
-    + destruct (IHxs' _ _ HIn) as [Heq|HIn'].
-      * left; split; tauto.
-      * destruct HIn'.
-        -- left; split; auto; congruence.
-        -- now right.
-Qed.
-
-Lemma In_filter_Nones_aux_correct2 {X Y} (f : X -> option Y) (xs : list X) :
-  forall acc x, (f x = None /\ In x xs) \/ In x acc -> In x (filter_Nones_aux acc f xs).
-Proof.
-  induction xs as [|x' xs'].
-  - intros acc x [[_ []]|]; auto.
-  - intros acc x [[fx [Heq|HIn]]|Q]; simpl.
-    + rewrite Heq, fx. simpl.
-      apply IHxs'; right; now left.
-    + destruct (f x'); apply IHxs'; left; now split.
-    + destruct (f x'); apply IHxs'.
-      -- now right.
-      -- right; now right.
-Qed.
-
-Lemma In_filter_Nones_aux_iff {X Y} (f : X -> option Y) (xs : list X) :
-  forall acc x, In x (filter_Nones_aux acc f xs) <-> (f x = None /\ In x xs) \/ In x acc.
-Proof.
-  intros; split.
-  - apply In_filter_Nones_aux_correct1.
-  - apply In_filter_Nones_aux_correct2.
-Qed.
-
-Definition filter_Nones {X Y} (f : X -> option Y) (xs : list X) : list X :=
-  filter_Nones_aux [] f xs.
-
-Lemma In_filter_Nones_iff {X Y} (f : X -> option Y) (xs : list X) :
-  forall x, In x (filter_Nones f xs) <-> f x = None /\ In x xs.
-Proof.
-  intro.
-  unfold filter_Nones.
-  rewrite In_filter_Nones_aux_iff; simpl; tauto.
-Qed.
-
 Definition eloise_step (tb : TB) (pl : Player) : list (GameState G) :=
   let prev :=
     match pl with
@@ -391,9 +325,6 @@ Proof.
   exact (unique_winner _ _ _ w w').
 Qed.
 
-Definition disj {X} (xs ys : list X) : Prop :=
-  forall x, In x xs -> ~ In x ys.
-
 Lemma NoDup_app {X} : forall (xs ys : list X),
   NoDup xs -> NoDup ys -> disj xs ys -> NoDup (xs ++ ys).
 Proof.
@@ -470,7 +401,7 @@ Proof.
 Defined.
 
 Lemma map_tag_functional : forall pl n ps,
-  AL.functional (map (tag pl n) ps).
+  functional (map (tag pl n) ps).
 Proof.
   intros pl n ps.
   intros s [q1 k] [q2 l] Hq1 Hq2.
@@ -481,61 +412,6 @@ Proof.
   congruence.
 Qed.
 
-Lemma in_map_sig {X Y} `{Discrete Y} {f : X -> Y} {xs} {y}
-  : In y (map f xs) -> {x : X & f x = y /\ In x xs}.
-Proof.
-  induction xs as [|x xs'].
-  - intros [].
-  - intro HIn.
-    destruct (eq_dec (f x) y).
-    + exists x; split; auto.
-      now left.
-    + destruct IHxs' as [x' [Hx'1 Hx'2]].
-      * destruct HIn; [contradiction|auto].
-      * exists x'; split; auto.
-        now right.
-Defined.
-
-Lemma not_Some_None {X} (o : option X) :
-  (forall x, ~ o = Some x) -> o = None.
-Proof.
-  intro nSome.
-  destruct o; [|reflexivity].
-  elim (nSome x); reflexivity.
-Qed.
-
-Lemma None_or_all_Some {X Y} (f : X -> option Y) (xs : list X) :
-  { x : X & f x = None } +
-  { ys : list Y & map f xs = map Some ys }.
-Proof.
-  induction xs as [|x xs'].
-  - right.
-    exists [].
-    reflexivity.
-  - destruct (f x) eqn:fx.
-    + destruct IHxs' as [[x' Hx']| [ys Hys]].
-      * left; now exists x'.
-      * right; exists (y :: ys); simpl; congruence.
-    + left; now exists x.
-Defined.
-
-Lemma list_max_is_max : forall xs x, In x xs -> x <= list_max xs.
-Proof.
-  intro xs.
-  rewrite <- Forall_forall.
-  rewrite <- list_max_le.
-  lia.
-Qed.
-
-Lemma not_None_in_Somes {X} (xs : list X) :
-  ~ In None (map Some xs).
-Proof.
-  induction xs.
-  - intros [].
-  - intros [|]; auto.
-    congruence.
-Qed.
-
 Lemma mate_S_lemma (tb : TB) (v : TB_valid tb) :
   forall {s : GameState G} {pl},
   mate pl s (S (curr tb)) ->
@@ -1496,14 +1372,6 @@ Proof.
       exists s; exact sm.
 Defined.
 
-Lemma In_length_pos {X} (xs : list X) : forall x, In x xs ->
-  length xs > 0.
-Proof.
-  destruct xs; intros y HIn.
-  - destruct HIn.
-  - simpl; lia.
-Qed.
-
 Definition in_decb {X} `{Discrete X}
   (x : X) (xs : list X) : bool :=
   match in_dec x xs with
diff --git a/theory/Util/AssocList.v b/theory/Util/AssocList.v
index 9ce7c5a..bd84e75 100644
--- a/theory/Util/AssocList.v
+++ b/theory/Util/AssocList.v
@@ -83,13 +83,3 @@ Proof.
     + reflexivity.
     + simpl; destruct (lookup k m'); auto.
 Qed.
-
-Definition functional {K V} (ps : list (K * V)) : Prop :=
-  forall x y y', In (x,y) ps -> In (x,y') ps -> y = y'.
-
-Lemma functional_tail {K V} {p : K * V} {qs} :
-  functional (p :: qs) -> functional qs.
-Proof.
-  intros Hfunc k v v' Hin Hin'.
-  eapply Hfunc; right; eauto.
-Qed.
diff --git a/theory/Util/GameUtil.v b/theory/Util/GameUtil.v
new file mode 100644
index 0000000..f76d531
--- /dev/null
+++ b/theory/Util/GameUtil.v
@@ -0,0 +1,29 @@
+Require Import Lia.
+Require Import List.
+
+Require Import Games.Game.Game.
+Require Import Games.Game.Player.
+Require Import Games.Game.Strategy.
+Require Import Games.Game.Win.
+
+(* stuff that should eventually be added to games *)
+
+Lemma mate_eq {G} {s : GameState G} {pl pl'} {n n'} :
+  mate pl s n ->
+  mate pl' s n' ->
+  n = n'.
+Proof.
+  intros sm sm'.
+  assert (pl = pl') as Heq.
+  { destruct sm as [w _].
+    destruct sm' as [w' _].
+    exact (unique_winner _ _ _ w w').
+  }
+  rewrite Heq in sm.
+  destruct sm as [w [w_d w_m]].
+  destruct sm' as [w' [w'_d w'_m]].
+  rewrite <- w_d, <- w'_d.
+  apply PeanoNat.Nat.le_antisymm.
+  - apply w_m.
+  - apply w'_m.
+Qed.
\ No newline at end of file
diff --git a/theory/Util/IntMap.v b/theory/Util/IntMap.v
index 43048ae..8cc9692 100644
--- a/theory/Util/IntMap.v
+++ b/theory/Util/IntMap.v
@@ -6,6 +6,8 @@ Require Import Uint63.
 
 Require Import Games.Util.Dec.
 Require Import TBGen.Util.IntHash.
+Require Import TBGen.Util.ListUtil.
+
 Require TBGen.Util.AssocList.
 
 Module AL := AssocList.
@@ -211,6 +213,7 @@ Proof.
         now inversion ndps.
 Qed.
 
+(*TODO*)
 Global Instance int_Discrete : Discrete int.
 Proof.
   constructor.
@@ -329,24 +332,6 @@ Proof.
       right; auto.
 Qed.
 
-Lemma in_dec {X} `{Discrete X} (x : X) (xs : list X) :
-  { In x xs } + { ~ In x xs }.
-Proof.
-  induction xs as [|x' xs']; simpl.
-  - now right.
-  - destruct (eq_dec x' x).
-    + left; now left.
-    + destruct IHxs'.
-      * left; now right.
-      * right; intros [|]; contradiction.
-Defined.
-
-Definition in_decb {X} `{Discrete X} (x : X) (xs : list X) :=
-  match in_dec x xs with
-  | left _ => true
-  | right _ => false
-  end.
-
 Global Instance Hash_disc {X} `{IntHash X} : Discrete X.
 Proof.
   constructor.
@@ -358,7 +343,7 @@ Proof.
 Defined.
 
 Lemma hash_lookup_adds {M} {X Y} `{IntMap M} `{IntHash X}
-  (ps : list (X * Y)) : forall m : M Y, AL.functional ps ->
+  (ps : list (X * Y)) : forall m : M Y, functional ps ->
   forall (x : X) (y : Y), In (x,y) ps ->
   hash_lookup x (hash_adds ps m) = Some y.
 Proof.
@@ -367,10 +352,13 @@ Proof.
   - simpl in *.
     destruct HIn.
     + inversion H1; subst.
+
+
+
       destruct (in_dec x' (map fst qs)).
       * apply (IHqs (hash_add x' y' m));
-          [exact (AL.functional_tail ndkeys)|].
-        unfold AL.functional in ndkeys.
+          [exact (functional_tail ndkeys)|].
+        unfold functional in ndkeys.
         rewrite in_map_iff in i.
         destruct i as [[u v] [Heq HIn]].
         simpl in Heq; subst.
@@ -380,7 +368,7 @@ Proof.
       * rewrite hash_lookup_adds_nIn; auto.
         apply hash_lookup_add.
     + apply IHqs; auto.
-      exact (AL.functional_tail ndkeys).
+      exact (functional_tail ndkeys).
 Qed.
 
 Global Instance AssocList_SM : IntMap (AL.t int) := {|
diff --git a/theory/Util/ListUtil.v b/theory/Util/ListUtil.v
new file mode 100644
index 0000000..96be3e3
--- /dev/null
+++ b/theory/Util/ListUtil.v
@@ -0,0 +1,177 @@
+Require Import List.
+Import ListNotations.
+Require Import Games.Util.Dec.
+
+Fixpoint filter_Nones_aux {X Y} (acc : list X) (f : X -> option Y) (xs : list X) : list X :=
+  match xs with
+  | [] => acc
+  | x :: xs' =>
+    match f x with
+    | None => filter_Nones_aux (x :: acc) f xs'
+    | Some _ => filter_Nones_aux acc f xs'
+    end
+  end.
+
+Lemma In_filter_Nones_aux_correct1 {X Y} (f : X -> option Y) (xs : list X) :
+  forall acc x, In x (filter_Nones_aux acc f xs) -> (f x = None /\ In x xs) \/ In x acc.
+Proof.
+  induction xs as [|x' xs']; intros acc x HIn; simpl in *.
+  - now right.
+  - destruct (f x') eqn:fx'.
+    + destruct (IHxs' _ _ HIn).
+      * left; split; tauto.
+      * now right.
+    + destruct (IHxs' _ _ HIn) as [Heq|HIn'].
+      * left; split; tauto.
+      * destruct HIn'.
+        -- left; split; auto; congruence.
+        -- now right.
+Qed.
+
+Lemma In_filter_Nones_aux_correct2 {X Y} (f : X -> option Y) (xs : list X) :
+  forall acc x, (f x = None /\ In x xs) \/ In x acc -> In x (filter_Nones_aux acc f xs).
+Proof.
+  induction xs as [|x' xs'].
+  - intros acc x [[_ []]|]; auto.
+  - intros acc x [[fx [Heq|HIn]]|Q]; simpl.
+    + rewrite Heq, fx. simpl.
+      apply IHxs'; right; now left.
+    + destruct (f x'); apply IHxs'; left; now split.
+    + destruct (f x'); apply IHxs'.
+      -- now right.
+      -- right; now right.
+Qed.
+
+Lemma In_filter_Nones_aux_iff {X Y} (f : X -> option Y) (xs : list X) :
+  forall acc x, In x (filter_Nones_aux acc f xs) <-> (f x = None /\ In x xs) \/ In x acc.
+Proof.
+  intros; split.
+  - apply In_filter_Nones_aux_correct1.
+  - apply In_filter_Nones_aux_correct2.
+Qed.
+
+Definition filter_Nones {X Y} (f : X -> option Y) (xs : list X) : list X :=
+  filter_Nones_aux [] f xs.
+
+Lemma In_filter_Nones_iff {X Y} (f : X -> option Y) (xs : list X) :
+  forall x, In x (filter_Nones f xs) <-> f x = None /\ In x xs.
+Proof.
+  intro.
+  unfold filter_Nones.
+  rewrite In_filter_Nones_aux_iff; simpl; tauto.
+Qed.
+
+Definition disj {X} (xs ys : list X) : Prop :=
+  forall x, In x xs -> ~ In x ys.
+
+Definition functional {K V} (ps : list (K * V)) : Prop :=
+  forall x y y', In (x,y) ps -> In (x,y') ps -> y = y'.
+
+Lemma functional_tail {K V} {p : K * V} {qs} :
+  functional (p :: qs) -> functional qs.
+Proof.
+  intros Hfunc k v v' Hin Hin'.
+  eapply Hfunc; right; eauto.
+Qed.
+
+Lemma in_map_sig {X Y} `{Discrete Y} {f : X -> Y} {xs} {y}
+  : In y (map f xs) -> {x : X & f x = y /\ In x xs}.
+Proof.
+  induction xs as [|x xs'].
+  - intros [].
+  - intro HIn.
+    destruct (eq_dec (f x) y).
+    + exists x; split; auto.
+      now left.
+    + destruct IHxs' as [x' [Hx'1 Hx'2]].
+      * destruct HIn; [contradiction|auto].
+      * exists x'; split; auto.
+        now right.
+Defined.
+
+Lemma not_Some_None {X} (o : option X) :
+  (forall x, ~ o = Some x) -> o = None.
+Proof.
+  intro nSome.
+  destruct o; [|reflexivity].
+  elim (nSome x); reflexivity.
+Qed.
+
+Lemma None_or_all_Some {X Y} (f : X -> option Y) (xs : list X) :
+  { x : X & f x = None } +
+  { ys : list Y & map f xs = map Some ys }.
+Proof.
+  induction xs as [|x xs'].
+  - right.
+    exists [].
+    reflexivity.
+  - destruct (f x) eqn:fx.
+    + destruct IHxs' as [[x' Hx']| [ys Hys]].
+      * left; now exists x'.
+      * right; exists (y :: ys); simpl; congruence.
+    + left; now exists x.
+Defined.
+
+Lemma list_max_is_max : forall xs x, In x xs -> x <= list_max xs.
+Proof.
+  intro xs.
+  rewrite <- Forall_forall.
+  rewrite <- list_max_le.
+  constructor.
+Qed.
+
+Lemma not_None_in_Somes {X} (xs : list X) :
+  ~ In None (map Some xs).
+Proof.
+  induction xs.
+  - intros [].
+  - intros [|]; auto.
+    congruence.
+Qed.
+
+Lemma In_length_pos {X} (xs : list X) : forall x, In x xs ->
+  length xs > 0.
+Proof.
+  destruct xs; intros y HIn.
+  - destruct HIn.
+  - simpl. apply PeanoNat.Nat.lt_0_succ.
+Qed.
+
+Global Instance List_disc {X} `{Discrete X} :
+  Discrete (list X).
+Proof.
+  constructor.
+  intro xs; induction xs as [|x xs]; intro ys.
+  - destruct ys as [|y ys].
+    + now left.
+    + now right.
+  - destruct ys as [|y ys].
+    + now right.
+    + destruct (eq_dec x y).
+      * destruct (IHxs ys).
+        -- left; congruence.
+        -- right; intro pf.
+           inversion pf; auto.
+      * right; intro pf.
+        inversion pf; auto.
+Defined.
+
+Lemma in_dec {X} `{Discrete X} (x : X) (xs : list X) :
+  { In x xs } + { ~ In x xs }.
+Proof.
+  induction xs as [|x' xs']; simpl.
+  - now right.
+  - destruct (eq_dec x' x).
+    + left; now left.
+    + destruct IHxs'.
+      * left; now right.
+      * right; intros [|]; contradiction.
+Defined.
+
+Definition in_decb {X} `{Discrete X} (x : X) (xs : list X) : bool :=
+  match in_dec x xs with
+  | left _ => true
+  | right _ => false
+  end.
+
+
diff --git a/theory/Util/StringMap.v b/theory/Util/StringMap.v
deleted file mode 100644
index 7270af5..0000000
--- a/theory/Util/StringMap.v
+++ /dev/null
@@ -1,383 +0,0 @@
-Require Import Lia.
-Require Import List.
-Import ListNotations.
-Require Import String.
-
-Require Import Games.Util.Dec.
-Require Import TBGen.Util.Show.
-Require TBGen.Util.AssocList.
-
-Module AL := AssocList.
-
-Class StringMap (M : Type -> Type) : Type := {
-  empty {X} : M X;
-  add {X} : string -> X -> M X -> M X;
-  lookup {X} : string -> M X -> option X;
-  size {X} : M X -> nat;
-
-  lookup_empty {X} : forall str, lookup str (empty : M X) = None;
-  lookup_add {X} : forall str (x : X) m, lookup str (add str x m) = Some x;
-  lookup_add_neq {X} : forall str str' (x : X) m, str <> str' ->
-    lookup str (add str' x m) = lookup str m;
-  size_empty {X} : size (empty : M X) = 0;
-  size_add {X} : forall str (x : X) m,
-    size (add str x m) =
-      match lookup str m with
-      | Some _ => size m
-      | None => S (size m)
-      end
-  }.
-
-Definition str_add {M} {X Y} `{StringMap M} `{Show X} :
-  X -> Y -> M Y -> M Y :=
-  fun x => add (show x).
-
-Definition str_lookup {M} {X Y} `{StringMap M} `{Show X} :
-  X -> M Y -> option Y :=
-  fun x => lookup (show x).
-
-Lemma str_lookup_empty {M} {X Y} `{StringMap M} `{Show X} :
-  forall x, str_lookup x (empty : M Y) = None.
-Proof.
-  intro.
-  apply lookup_empty.
-Qed.
-
-Lemma str_lookup_add {M} {X Y} `{StringMap M} `{Show X} :
-  forall (x : X) (y : Y) m, str_lookup x (str_add x y m) = Some y.
-Proof.
-  intros.
-  apply lookup_add.
-Qed.
-
-Lemma str_lookup_add_neq {M} {X Y} `{StringMap M} `{Show X} :
-  forall (x x' : X) (y : Y) m, x <> x' ->
-    str_lookup x (str_add x' y m) = str_lookup x m.
-Proof.
-  intros x x' y m Hxx'.
-  apply lookup_add_neq.
-  intro Hshow.
-  apply Hxx'.
-  now apply show_inj.
-Qed.
-
-Lemma str_size_add {M} {X Y} `{StringMap M} `{Show X} :
-  forall (x : X) (y : Y) m,
-    size (str_add x y m) =
-      match str_lookup x m with
-      | Some _ => size m
-      | None => S (size m)
-      end.
-Proof.
-  intros.
-  apply size_add.
-Qed.
-
-Fixpoint str_adds {M} {X Y} `{StringMap M} `{Show X}
-  (ps : list (X * Y)) (m : M Y) {struct ps} : M Y :=
-  match ps with
-  | [] => m
-  | (x,y) :: qs => str_adds qs (str_add x y m)
-  end.
-
-Inductive good {M} {X Y} `{StringMap M} `{Show X} : M Y -> Prop :=
-  | good_e : good empty
-  | good_a {x y m} : good m -> str_lookup x m = None -> good (str_add x y m).
-
-Fixpoint good_as {M} {X Y} `{StringMap M} `{Show X} {ps : list (X * Y)}
-  {m : M Y} (pf : good m) (nd : NoDup (map fst ps))
-  (disj : forall x y, In (x,y) ps -> str_lookup x m = None) {struct ps}
-  : good (str_adds ps m).
-Proof.
-  induction ps as [|[x y] qs].
-  - exact pf.
-  - simpl.
-    apply good_as.
-    + apply good_a; auto.
-      apply (disj x y); now left.
-    + now inversion nd.
-    + intros x' y' HIn.
-      rewrite str_lookup_add_neq.
-      * apply (disj x' y'); now right.
-      * simpl in nd; inversion nd.
-        intro Heq.
-        apply H3.
-        rewrite <- Heq.
-        rewrite in_map_iff.
-        exists (x', y'); split; auto.
-Qed.
-
-Record map_list_equiv {M} {X Y} `{Show X} `{StringMap M}
-  (m : M Y) (ps : list (X * Y)) : Prop := {
-  to_list_size : size m = List.length ps;
-  keys_unique : NoDup (map fst ps);
-  lookup_in {x y} : str_lookup x m = Some y <-> In (x,y) ps;
-  }.
-
-Lemma str_adds_add {M} {X Y} `{StringMap M} `{Show X}
-  {ps : list (X * Y)} : forall x y m,
-  str_add x y (str_adds ps m) = str_adds (ps ++ [(x,y)]) m.
-Proof.
-  induction ps; intros.
-  - reflexivity. 
-  - simpl.
-    destruct a.
-    now rewrite IHps.
-Qed.
-
-Lemma str_adds_app {M} {X Y} `{StringMap M} `{Show X}
-  {ps : list (X * Y)} : forall qs m,
-  str_adds ps (str_adds qs m) = str_adds (qs ++ ps) m.
-Proof.
-  induction ps; intros.
-  - simpl; now rewrite app_nil_r.
-  - simpl.
-    destruct a.
-    assert (qs ++ (x,y) :: ps = (qs ++ [(x,y)]) ++ ps)%list.
-    { now rewrite <- app_assoc. }
-    rewrite H1.
-    rewrite <- IHps.
-    now rewrite str_adds_add.
-Qed.
-
-Lemma str_size_add_le {M} {X Y} `{StringMap M} `{Show X}
-  (x : X) (y : Y) : forall m : M Y,
-  size m <= size (str_add x y m).
-Proof.
-  intro.
-  rewrite str_size_add.
-  destruct str_lookup; lia.
-Qed.
-
-Lemma str_size_add_lt {M} {X Y} `{StringMap M} `{Show X}
-  : forall (m : M Y) (x : X) (y : Y),
-  str_lookup x m = None ->
-  size m < size (str_add x y m).
-Proof.
-  intros.
-  rewrite str_size_add.
-  rewrite H1.
-  lia.
-Qed.
-
-Lemma str_size_adds_le {M} {X Y} `{StringMap M} `{Show X}
-  (ps : list (X * Y)) : forall m : M Y,
-  size m <= size (str_adds ps m).
-Proof.
-  induction ps as [|[x y] qs].
-  - intro; simpl. lia.
-  - intros; simpl.
-    simpl.
-    apply (PeanoNat.Nat.le_trans _ (size (str_add x y m))).
-    + apply str_size_add_le.
-    + apply IHqs.
-Qed.
-
-Lemma str_adds_ne_pos {M} {X Y} `{StringMap M} `{Show X}
-  (ps : list (X * Y)) : forall (x : X) (y : Y),
-  In (x,y) ps -> size (str_adds ps empty) > 0.
-Proof.
-  destruct ps as [|[x' y'] qs]; intros.
-  - destruct H1.
-  - simpl.
-    pose proof (str_size_adds_le qs (str_add x' y' empty)).
-    rewrite str_size_add in H2.
-    rewrite str_lookup_empty in H2.
-    lia.
-Qed.
-
-Lemma str_size_adds {M} {X Y} `{StringMap M} `{Show X}
-  (ps : list (X * Y)) : forall m : M Y,
-  NoDup (map fst ps) ->
-  (forall x, In x (map fst ps) -> str_lookup x m = None) ->
-  size (str_adds ps m) = List.length ps + size m.
-Proof.
-  induction ps as [|[x y] qs]; intros m ndps Hpsm.
-  - reflexivity.
-  - simpl.
-    rewrite IHqs.
-    + rewrite str_size_add.
-      rewrite Hpsm.
-      * apply PeanoNat.Nat.add_succ_r.
-      * left; reflexivity.
-    + now inversion ndps.
-    + intros.
-      rewrite str_lookup_add_neq.
-      * apply Hpsm.
-        right; auto.
-      * intro Hx0x.
-        rewrite Hx0x in H1.
-        now inversion ndps.
-Qed.
-
-Global Instance string_Discrete : Discrete string := {|
-  eq_dec := string_dec
-  |}.
-
-Lemma str_lookup_adds_invert {M} {X Y} `{StringMap M} `{Show X}
-  (ps : list (X * Y)) : forall (m : M Y) (x : X) (y : Y),
-  str_lookup x (str_adds ps m) = Some y ->
-  {In (x,y) ps} + {str_lookup x m = Some y}.
-Proof.
-  induction ps as [|[x y] qs]; intros m x' y' Hx'.
-  - right. exact Hx'.
-  - simpl in Hx'.
-    destruct (IHqs _ _ _ Hx').
-    + left; now right.
-    + destruct (eq_dec (show x') (show x)).
-      * assert (x' = x) as Hx'x by now apply show_inj.
-        rewrite Hx'x in e.
-        rewrite str_lookup_add in e.
-        left; left; congruence.
-      * rewrite str_lookup_add_neq in e.
-        ** now right.
-        ** intro Hx'x.
-           now rewrite Hx'x in n.
-Defined.
-
-Lemma good_to_list {M} {X Y} `{Show X} `{StringMap M}
-  (m : M Y) (g : good m) : exists (ps : list (X * Y)), map_list_equiv m ps.
-Proof.
-  induction g.
-  - exists nil; constructor.
-    + now rewrite size_empty.
-    + constructor.
-    + intros x y.
-      unfold str_lookup.
-      now rewrite lookup_empty.
-  - destruct IHg as [ps [tl_sz key_un l_in]].
-    exists ((x,y) :: ps); constructor.
-    + unfold str_add.
-      unfold str_lookup in H1.
-      rewrite size_add.
-      rewrite H1.
-      simpl; congruence.
-    + simpl; constructor; auto.
-      intro HIn.
-      rewrite in_map_iff in HIn.
-      destruct HIn as [[str x'] [Hx1 Hx2]].
-      simpl in *.
-      rewrite Hx1 in Hx2.
-      rewrite <- l_in in Hx2; congruence.
-    + intros.
-      unfold str_lookup, str_add.
-      destruct (string_dec (show x0) (show x)).
-      * rewrite e.
-        rewrite lookup_add.
-        split; intro.
-        -- pose (show_inj _ _ e).
-           left; congruence.
-        -- destruct H2; [congruence|].
-           rewrite <- l_in in H2.
-           pose (show_inj _ _ e); congruence.
-      * rewrite lookup_add_neq; auto.
-        unfold str_lookup in l_in.
-        rewrite l_in.
-        split; intro; [now right|].
-        destruct H2; [congruence|auto].
-Qed.
-
-Lemma str_lookup_adds_None_invert {M} {X Y} `{StringMap M} `{Show X}
-  {ps} : forall {m : M Y} {x : X},
-  str_lookup x (str_adds ps m) = None ->
-  (~ In x (List.map fst ps)) /\
-  str_lookup x m = None.
-Proof.
-  induction ps as [|[x y] qs]; intros m x' Hx'.
-  - split.
-    + intros [].
-    + exact Hx'.
-  - simpl in *.
-    destruct (IHqs _ _ Hx').
-    split.
-    + intros [|].
-      * rewrite H3 in H2.
-        now rewrite str_lookup_add in H2.
-      * contradiction.
-    + destruct (eq_dec (show x') (show x)).
-      * rewrite (show_inj _ _ e) in H2.
-        now rewrite str_lookup_add in H2.
-      * rewrite str_lookup_add_neq in H2; auto.
-        congruence.
-Qed.
-
-Lemma str_lookup_adds_nIn {M} {X Y} `{StringMap M} `{Show X} :
-  forall (ps : list (X * Y)) (x : X) m,
-    ~ In x (List.map fst ps) ->
-    str_lookup x (str_adds ps m) = str_lookup x m.
-Proof.
-  intro ps.
-  induction ps as [|[x y] qs]; intros x' m nIn.
-  - reflexivity.
-  - simpl.
-    rewrite IHqs.
-    + rewrite str_lookup_add_neq.
-      * reflexivity.
-      * intro Hxx'; apply nIn.
-        left; symmetry; exact Hxx'.
-    + intro HIn; apply nIn.
-      right; auto.
-Qed.
-
-Lemma in_dec {X} `{Discrete X} (x : X) (xs : list X) :
-  { In x xs } + { ~ In x xs }.
-Proof.
-  induction xs as [|x' xs']; simpl.
-  - now right.
-  - destruct (eq_dec x' x).
-    + left; now left.
-    + destruct IHxs'.
-      * left; now right.
-      * right; intros [|]; contradiction.
-Defined.
-
-Definition in_decb {X} `{Discrete X} (x : X) (xs : list X) :=
-  match in_dec x xs with
-  | left _ => true
-  | right _ => false
-  end.
-
-Global Instance Show_disc {X} `{Show X} : Discrete X.
-Proof.
-  constructor.
-  apply Show_dec.
-Defined.
-
-Lemma str_lookup_adds {M} {X Y} `{StringMap M} `{Show X}
-  (ps : list (X * Y)) : forall m : M Y, AL.functional ps ->
-  forall (x : X) (y : Y), In (x,y) ps ->
-  str_lookup x (str_adds ps m) = Some y.
-Proof.
-  induction ps as [|[x y] qs]; intros m ndkeys x' y' HIn.
-  - destruct HIn.
-  - simpl in *.
-    destruct HIn.
-    + inversion H1; subst.
-      destruct (in_dec x' (map fst qs)).
-      * apply (IHqs (str_add x' y' m));
-          [exact (AL.functional_tail ndkeys)|].
-        unfold AL.functional in ndkeys.
-        rewrite in_map_iff in i.
-        destruct i as [[u v] [Heq HIn]].
-        simpl in Heq; subst.
-        rewrite (ndkeys x' y' v); auto.
-        ** now left.
-        ** now right.
-      * rewrite str_lookup_adds_nIn; auto.
-        apply str_lookup_add.
-    + apply IHqs; auto.
-      exact (AL.functional_tail ndkeys).
-Qed.
-
-Global Instance AssocList_SM : StringMap (AL.t string) := {|
-  empty X := AL.empty;
-  add X := AL.add;
-  lookup X := AL.lookup;
-  size X := AL.size;
-
-  lookup_empty X := AL.lookup_empty;
-  lookup_add X := AL.lookup_add;
-  lookup_add_neq X := AL.lookup_add_neq;
-  size_empty X := AL.size_empty;
-  size_add X := AL.size_add;
-  |}.