cleanup (#36)

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

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.

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

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.

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.

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) := {|