pruning unused stuff

bin/query/ExtractQuery.v

@@ -15,6 +15,7 @@ Require Import TBGen.Util.IntHash.
 Require Import TBGen.Util.OMap.
 Require Import TBGen.Bear.Sort.
 Require Import TBGen.Bear.BearGame.
+Require Import TBGen.Bear.RomanWheelExtras.
 Require Import TBGen.Bear.RomanWheel.
 Require Import TBGen.TB.TB.
 Require Import TBGen.TB.OCamlTB.
@@ -128,13 +129,8 @@ Definition show_RWVert (v : RWVert) : string :=
 
 Global Instance Show_RWVert : Show RWVert. refine {|
   show := show_RWVert;
-  show_inj := _;
   |}.
 Proof.
-  - intros v v'.
-    destruct v as [|[] []];
-    destruct v' as [|[] []]; try reflexivity.
-    all: discriminate.
 Defined.
 
 Definition print_RW_move {s : BG_State RomanWheel}

theory/Bear/RomanWheel.v

@@ -11,7 +11,7 @@ Require Import TBGen.Bear.Graph.
 Require Import TBGen.Bear.BearGame.
 Require Import TBGen.TB.TB.
 
-Inductive Spoke :=
+Variant Spoke :=
   S1 | S2 | S3 | S4 | S5 | S6 | S7 | S8.
 
 Definition clockwise (s : Spoke) : Spoke :=
@@ -41,13 +41,13 @@ Definition c_clockwise (s : Spoke) : Spoke :=
 Definition list_spokes :=
   [S1;S2;S3;S4;S5;S6;S7;S8].
 
-Inductive SpokeLoc :=
+Variant SpokeLoc :=
   Mid | L | R.
 
 Definition list_locs :=
   [Mid;L;R].
 
-Inductive RWVert :=
+Variant RWVert :=
   | Center
   | SpokeVert (s : Spoke) (l : SpokeLoc).
 

theory/Bear/RomanWheelExtras.v

@@ -0,0 +1,160 @@
+Require Import Lia.
+Require Import List.
+Require Import String.
+Import ListNotations.
+
+Require Import Extraction.
+Require Import ExtrOcamlBasic.
+Require Import ExtrOcamlNatInt.
+Require Import ExtrOcamlNativeString.
+Require Import ExtrOCamlInt63.
+Extraction Language OCaml.
+
+Require Import TBGen.Util.Show.
+Require Import TBGen.Util.IntHash.
+Require Import TBGen.Util.OMap.
+Require Import TBGen.Bear.Sort.
+Require Import TBGen.Bear.BearGame.
+Require Import TBGen.Bear.RomanWheel.
+Require Import TBGen.TB.TB.
+Require Import TBGen.TB.OCamlTB.
+
+Definition make_BG_State {G} (pl : Player.Player)
+  (b h1 h2 h3 : Graph.Vert G) : option (BG_State G).
+Proof.
+  destruct (NoDup_dec [b; h1; h2; h3]) as [pf|].
+  - apply Some.
+    refine {|
+      to_play := pl;
+      bear :=  b;
+      hunters := insertion_sort [h1; h2; h3];
+      hunters_sort := _;
+      hunters_3 := _;
+      hunters_distinct := _;
+      bear_not_hunter := _
+    |}.
+    + apply insertion_sort_sorts.
+    + now rewrite insertion_sort_length.
+    + apply insertion_sort_NoDup.
+      now inversion pf.
+    + rewrite insertion_sort_In.
+      now inversion pf.
+  - exact None.
+Defined.
+
+Definition make_RW_State (pl : Player.Player)
+  (b h1 h2 h3 : RWVert) : option (BG_State RomanWheel) :=
+  @make_BG_State RomanWheel pl b h1 h2 h3.
+
+Definition init_RW_State : BG_State RomanWheel.
+Proof.
+  refine {|
+    to_play := Player.White;
+    bear := Center : Graph.Vert RomanWheel;
+    hunters :=
+      [ SpokeVert S1 Mid
+      ; SpokeVert S1 L
+      ; SpokeVert S1 R];
+  |}.
+  - do 2 constructor.
+    + repeat constructor.
+    + constructor; [|constructor].
+      compute; lia.
+    + compute; lia.
+    + constructor; [|constructor].
+      compute; lia.
+  - reflexivity.
+  - repeat constructor; simpl; auto.
+    + intros [|[|]]; auto; discriminate.
+    + intros [|]; auto; discriminate.
+  - simpl.
+    intros [|[|[|]]]; auto; discriminate.
+Defined.
+
+Definition strC : string := "C".
+Definition str1L : string := "1L".
+Definition str1M : string := "1M".
+Definition str1R : string := "1R".
+Definition str2L : string := "2L".
+Definition str2M : string := "2M".
+Definition str2R : string := "2R".
+Definition str3L : string := "3L".
+Definition str3M : string := "3M".
+Definition str3R : string := "3R".
+Definition str4L : string := "4L".
+Definition str4M : string := "4M".
+Definition str4R : string := "4R".
+Definition str5L : string := "5L".
+Definition str5M : string := "5M".
+Definition str5R : string := "5R".
+Definition str6L : string := "6L".
+Definition str6M : string := "6M".
+Definition str6R : string := "6R".
+Definition str7L : string := "7L".
+Definition str7M : string := "7M".
+Definition str7R : string := "7R".
+Definition str8L : string := "8L".
+Definition str8M : string := "8M".
+Definition str8R : string := "8R".
+
+Definition show_RWVert (v : RWVert) : string :=
+  match v with
+  | Center => strC
+  | SpokeVert S1 L => str1L
+  | SpokeVert S1 Mid => str1M
+  | SpokeVert S1 R => str1R
+  | SpokeVert S2 L => str2L
+  | SpokeVert S2 Mid => str2M
+  | SpokeVert S2 R => str2R
+  | SpokeVert S3 L => str3L
+  | SpokeVert S3 Mid => str3M
+  | SpokeVert S3 R => str3R
+  | SpokeVert S4 L => str4L
+  | SpokeVert S4 Mid => str4M
+  | SpokeVert S4 R => str4R
+  | SpokeVert S5 L => str5L
+  | SpokeVert S5 Mid => str5M
+  | SpokeVert S5 R => str5R
+  | SpokeVert S6 L => str6L
+  | SpokeVert S6 Mid => str6M
+  | SpokeVert S6 R => str6R
+  | SpokeVert S7 L => str7L
+  | SpokeVert S7 Mid => str7M
+  | SpokeVert S7 R => str7R
+  | SpokeVert S8 L => str8L
+  | SpokeVert S8 Mid => str8M
+  | SpokeVert S8 R => str8R
+  end.
+
+Global Instance Show_RWVert : Show RWVert. refine {|
+  show := show_RWVert;
+  |}.
+Proof.
+Defined.
+
+Definition print_RW_move {s : BG_State RomanWheel}
+  (m : BG_Move s) : string.
+Proof.
+  destruct m.
+  - destruct b.
+    exact ("B" ++ show b_dest).
+  - destruct h.
+    exact ("H" ++ show h_orig ++ show h_dest).
+Defined.
+
+Extraction Blacklist String List.
+
+Definition RW_exec_move (s : BG_State RomanWheel)
+ : BG_Move s -> BG_State RomanWheel :=
+  exec_move.
+
+Definition query_RW_TB :
+  OCamlTablebase (BearGame RomanWheel) ->
+  BG_State RomanWheel -> option (Player.Player * nat) :=
+  query_TB.
+
+Definition rw_tb_strat (pl : Player.Player)
+  (s : Game.GameState (BearGame RomanWheel))
+  (tb : OCamlTablebase (BearGame RomanWheel))
+ : Strategy.strategy pl s :=
+  tb_strat s pl tb.

theory/TB/TB.v

@@ -56,7 +56,7 @@ Context `{forall s : GameState G, Discrete (Move s)}.
 Context {M : Type -> Type}.
 Context `{IntMap M}.
 
-Inductive Step :=
+Variant Step :=
   | Eloise : Step
   | Abelard : Step.
 
@@ -1649,23 +1649,6 @@ Proof.
   - now apply (mate_tb _ TB_final_valid).
 Qed.
 
-Lemma map_fg_lemma {X Y Z} `{Discrete Y} {f : X -> Z} {g : Y -> Z} :
-  forall {xs ys}, map f xs = map g ys -> 
-  forall y, In y ys -> {x : X & In x xs /\ f x = g y}.
-Proof.
-  induction xs as [|x xs']; intros ys pf y Hy.
-  - destruct ys; [destruct Hy|inversion pf].
-  - destruct ys; [inversion pf|].
-    destruct (eq_dec y0 y).
-    + exists x; split.
-      * now left.
-      * inversion pf; congruence.
-    + inversion pf.
-      destruct (IHxs' _ H8 y).
-      * destruct Hy; [contradiction|auto].
-      * exists x0; split; [now right| tauto].
-Defined.
-
 Lemma forallb_false {X} (p : X -> bool) (xs : list X) :
   forallb p xs = false -> {x : X & In x xs /\ p x = false}.
 Proof.
@@ -1677,17 +1660,6 @@ Proof.
     + exists x; tauto.
 Defined.
 
-Lemma forallb_true {X} (p : X -> bool) (xs : list X) :
-  forallb p xs = true -> forall x, In x xs -> p x = true.
-Proof.
-  induction xs as [|x' xs']; intros Hpxs x Hx.
-  - destruct Hx.
-  - destruct Hx; subst; simpl in *.
-    + destruct (p x); [reflexivity|discriminate].
-    + destruct (p x'); [simpl in *|discriminate].
-      now apply IHxs'.
-Qed.
-
 Definition respects_atomic_wins (tb : TB) : Prop :=
   forall s pl, atomic_res s = Some (Win pl) ->
   tb_lookup tb s = Some (pl, 0).

theory/Util/IntMap.v

@@ -128,21 +128,6 @@ Proof.
     now rewrite IHps.
 Qed.
 
-Lemma hash_adds_app {M} {X Y} `{IntMap M} `{IntHash X}
-  {ps : list (X * Y)} : forall qs m,
-  hash_adds ps (hash_adds qs m) = hash_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 hash_adds_add.
-Qed.
-
 Lemma hash_size_add_le {M} {X Y} `{IntMap M} `{IntHash X}
   (x : X) (y : Y) : forall m : M Y,
   size m <= size (hash_add x y m).
@@ -152,17 +137,6 @@ Proof.
   destruct hash_lookup; lia.
 Qed.
 
-Lemma hash_size_add_lt {M} {X Y} `{IntMap M} `{IntHash X}
-  : forall (m : M Y) (x : X) (y : Y),
-  hash_lookup x m = None ->
-  size m < size (hash_add x y m).
-Proof.
-  intros m x y Hlookup.
-  rewrite hash_size_add.
-  rewrite Hlookup.
-  lia.
-Qed.
-
 Lemma hash_size_adds_le {M} {X Y} `{IntMap M} `{IntHash X}
   (ps : list (X * Y)) : forall m : M Y,
   size m <= size (hash_adds ps m).