From 967570c3804c3ad772ab7b254f2e9394b09a8c75 Mon Sep 17 00:00:00 2001 From: Evan Marzion Date: Mon, 1 Jan 2024 17:30:42 -0600 Subject: [PATCH] replacing string keys with int keys (#28) * replacing string keys with int keys * finish proof --- bin/gen/ExtractRomanWheel.v | 1 + bin/gen/M.ml | 8 +- bin/gen/dune | 1 + bin/gen/gen_file.ml | 4 +- bin/gen/uint63.ml | 247 ++++++++++ bin/query/ExtractQuery.v | 73 ++- bin/query/M.ml | 8 +- bin/query/dune | 9 +- bin/query/read_file.ml | 9 +- bin/query/uint63.ml | 215 +++++++++ bin/web/index.ml | 7 +- theory/Bear/BearGame.v | 40 +- theory/Bear/RomanWheel.v | 630 ++++++++++++++++++++------ theory/Game/OCamlTB.v | 36 +- theory/Game/Player.v | 18 - theory/Game/SampleGame.v | 62 ++- theory/Game/TB.v | 118 ++--- theory/Util/IntHash.v | 25 + theory/Util/{StringMap.v => IntMap.v} | 222 ++++----- theory/Util/OMap.v | 28 +- theory/Util/Show.v | 2 +- 21 files changed, 1317 insertions(+), 446 deletions(-) create mode 100644 bin/gen/uint63.ml create mode 100644 bin/query/uint63.ml create mode 100644 theory/Util/IntHash.v rename theory/Util/{StringMap.v => IntMap.v} (54%) diff --git a/bin/gen/ExtractRomanWheel.v b/bin/gen/ExtractRomanWheel.v index dadcf17..9a73f22 100644 --- a/bin/gen/ExtractRomanWheel.v +++ b/bin/gen/ExtractRomanWheel.v @@ -6,6 +6,7 @@ Require Import Extraction. Require Import ExtrOcamlBasic. Require Import ExtrOcamlNatInt. Require Import ExtrOcamlNativeString. +Require Import ExtrOCamlInt63. Extraction Language OCaml. Require Import Games.Util.OMap. diff --git a/bin/gen/M.ml b/bin/gen/M.ml index 34e4556..9875d30 100644 --- a/bin/gen/M.ml +++ b/bin/gen/M.ml @@ -1,5 +1,5 @@ -module SM = Map.Make(String) +module SM = Map.Make(Uint63) type 'a t = 'a SM.t @@ -8,13 +8,15 @@ let insert = SM.add let lookup = SM.find_opt let size = SM.cardinal let bindings = SM.bindings - +(* let printMap m = SM.iter (fun key value -> Printf.printf "%s -> %d\n" key value) m + *) -let tr_concat xss = +(* let tr_concat xss = let rec aux acc ls = match ls with | [] -> acc | xs :: xss' -> aux (List.rev_append xs acc) xss' in aux [] xss + *) \ No newline at end of file diff --git a/bin/gen/dune b/bin/gen/dune index 9d4e58e..50beda1 100644 --- a/bin/gen/dune +++ b/bin/gen/dune @@ -8,6 +8,7 @@ (modules ;; Patch code M + Uint63 ;; Extracted code TBGen diff --git a/bin/gen/gen_file.ml b/bin/gen/gen_file.ml index 56d887a..6bdb352 100644 --- a/bin/gen/gen_file.ml +++ b/bin/gen/gen_file.ml @@ -9,11 +9,11 @@ let print_player pl = | Black -> "Black" let tup_to_json tup : string * t = - let (str, (pl, n)) = tup in + let (i, (pl, n)) = tup in let pl_t = `String (print_player pl) in let n_t = `Int n in let pair_t = `Tuple [pl_t; n_t] in - (str, pair_t) + (string_of_int i, pair_t) let tups_to_json tups = `Assoc (List.map tup_to_json tups) diff --git a/bin/gen/uint63.ml b/bin/gen/uint63.ml new file mode 100644 index 0000000..28a2a68 --- /dev/null +++ b/bin/gen/uint63.ml @@ -0,0 +1,247 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* = 0 then + begin q := !q lor 1; nh := Int64.sub !nh y; end + done; + !q, Int64.to_int !nh + +let div21 xh xl y = + let xh = to_uint64 xh in + let y = to_uint64 y in + if Int64.compare y xh <= 0 then 0, 0 else div21 xh xl y + + (* exact multiplication *) +(* TODO: check that none of these additions could be a logical or *) + + +(* size = 32 + 31 + (hx << 31 + lx) * (hy << 31 + ly) = + hxhy << 62 + (hxly + lxhy) << 31 + lxly +*) + +(* precondition : (x lsr 62 = 0 || y lsr 62 = 0) *) +let mulc_aux x y = + let lx = x land maxuint31 in + let ly = y land maxuint31 in + let hx = x lsr 31 in + let hy = y lsr 31 in + (* hx and hy are 32 bits value but at most one is 32 *) + let hxy = hx * hy in (* 63 bits *) + let hxly = hx * ly in (* 63 bits *) + let lxhy = lx * hy in (* 63 bits *) + let lxy = lx * ly in (* 62 bits *) + let l = lxy lor (hxy lsl 62) (* 63 bits *) in + let h = hxy lsr 1 in (* 62 bits *) + let hl = hxly + lxhy in (* We can have a carry *) + let h = if lt hl hxly then h + (1 lsl 31) else h in + let hl'= hl lsl 31 in + let l = l + hl' in + let h = if lt l hl' then h + 1 else h in + let h = h + (hl lsr 32) in + (h,l) + +let mulc x y = + if (x lsr 62 = 0 || y lsr 62 = 0) then mulc_aux x y + else + let yl = y lxor (1 lsl 62) in + let (h,l) = mulc_aux x yl in + (* h << 63 + l = x * yl + x * y = x * (1 << 62 + yl) = + x << 62 + x*yl = x << 62 + h << 63 + l *) + let l' = l + (x lsl 62) in + let h = if lt l' l then h + 1 else h in + (h + (x lsr 1), l') + +let equal (x : int) (y : int) = x = y +[@@ocaml.inline always] + +let compare (x:int) (y:int) = + let x = x lxor 0x4000000000000000 in + let y = y lxor 0x4000000000000000 in + Int.compare x y + +let compares (x : int) (y : int) = + Int.compare x y + + (* head tail *) + +let head0 x = + let r = ref 0 in + let x = ref x in + if !x land 0x7FFFFFFF00000000 = 0 then r := !r + 31 + else x := !x lsr 31; + if !x land 0xFFFF0000 = 0 then (x := !x lsl 16; r := !r + 16); + if !x land 0xFF000000 = 0 then (x := !x lsl 8; r := !r + 8); + if !x land 0xF0000000 = 0 then (x := !x lsl 4; r := !r + 4); + if !x land 0xC0000000 = 0 then (x := !x lsl 2; r := !r + 2); + if !x land 0x80000000 = 0 then (x := !x lsl 1; r := !r + 1); + if !x land 0x80000000 = 0 then ( r := !r + 1); + !r;; + +let tail0 x = + let r = ref 0 in + let x = ref x in + if !x land 0xFFFFFFFF = 0 then (x := !x lsr 32; r := !r + 32); + if !x land 0xFFFF = 0 then (x := !x lsr 16; r := !r + 16); + if !x land 0xFF = 0 then (x := !x lsr 8; r := !r + 8); + if !x land 0xF = 0 then (x := !x lsr 4; r := !r + 4); + if !x land 0x3 = 0 then (x := !x lsr 2; r := !r + 2); + if !x land 0x1 = 0 then ( r := !r + 1); + !r + +let is_uint63 t = + Obj.is_int t +[@@ocaml.inline always] + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +let addc x y = + let r = x + y in + if lt r x then C1 r else C0 r + +let addcarryc x y = + let r = x + y + 1 in + if le r x then C1 r else C0 r + +let subc x y = + let r = x - y in + if le y x then C0 r else C1 r + +let subcarryc x y = + let r = x - y - 1 in + if lt y x then C0 r else C1 r \ No newline at end of file diff --git a/bin/query/ExtractQuery.v b/bin/query/ExtractQuery.v index 7824595..a5e0138 100644 --- a/bin/query/ExtractQuery.v +++ b/bin/query/ExtractQuery.v @@ -7,9 +7,11 @@ Require Import Extraction. Require Import ExtrOcamlBasic. Require Import ExtrOcamlNatInt. Require Import ExtrOcamlNativeString. +Require Import ExtrOCamlInt63. Extraction Language OCaml. Require Import Games.Util.Show. +Require Import Games.Util.IntHash. Require Import Games.Util.OMap. Require Import Games.Bear.Sort. Require Import Games.Bear.BearGame. @@ -69,6 +71,72 @@ Proof. 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; + 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} (m : BG_Move s) : string. Proof. @@ -85,10 +153,6 @@ Definition RW_exec_move (s : BG_State RomanWheel) : BG_Move s -> BG_State RomanWheel := exec_move. -Definition show_RW_State (s : BG_State RomanWheel) - : string := - show s. - Definition query_RW_TB : OCamlTablebase (BearGame RomanWheel) -> BG_State RomanWheel -> option (Player.Player * nat) := @@ -106,7 +170,6 @@ Separate Extraction RW_exec_move BearGame.enum_moves print_RW_move - show_RW_State query_RW_TB p_leb rw_tb_strat diff --git a/bin/query/M.ml b/bin/query/M.ml index 34e4556..9875d30 100644 --- a/bin/query/M.ml +++ b/bin/query/M.ml @@ -1,5 +1,5 @@ -module SM = Map.Make(String) +module SM = Map.Make(Uint63) type 'a t = 'a SM.t @@ -8,13 +8,15 @@ let insert = SM.add let lookup = SM.find_opt let size = SM.cardinal let bindings = SM.bindings - +(* let printMap m = SM.iter (fun key value -> Printf.printf "%s -> %d\n" key value) m + *) -let tr_concat xss = +(* let tr_concat xss = let rec aux acc ls = match ls with | [] -> acc | xs :: xss' -> aux (List.rev_append xs acc) xss' in aux [] xss + *) \ No newline at end of file diff --git a/bin/query/dune b/bin/query/dune index 8de5394..bee358b 100644 --- a/bin/query/dune +++ b/bin/query/dune @@ -9,17 +9,19 @@ ExtractQuery Game Graph + IntHash + IntMap List0 OCamlTB OMap Player + PrimInt63 RomanWheel Show Sort Specif Strategy String0 - StringMap TB ) (theories Games)) @@ -29,6 +31,7 @@ (modules ;; Patch code M + Uint63 ;; Extracted code Ascii @@ -39,17 +42,19 @@ ExtractQuery Game Graph + IntHash + IntMap List0 OCamlTB OMap Player + PrimInt63 RomanWheel Show Sort Specif Strategy String0 - StringMap TB ;; Ocaml code diff --git a/bin/query/read_file.ml b/bin/query/read_file.ml index ebf2ef4..9009c07 100644 --- a/bin/query/read_file.ml +++ b/bin/query/read_file.ml @@ -1,11 +1,8 @@ open Yojson.Safe -open Extracted_code -open TBGen - let json_to_tup = function - | (str, `Tuple [`String "White"; `Int n]) -> (str, (White, n)) - | (str, `Tuple [`String "Black"; `Int n]) -> (str, (Black, n)) + | (i_str, `Tuple [`String "White"; `Int n]) -> (Int64.of_string i_str, (Player.White, n)) + | (i_str, `Tuple [`String "Black"; `Int n]) -> (Int64.of_string i_str, (Player.Black, n)) | _ -> failwith "Error converting json to tuple." let json_to_tups = function @@ -23,4 +20,4 @@ let make_tb = let m_b = List.fold_left (fun m (str, pr) -> M.insert str pr m) M.empty tups_b in let () = close_in inc_w in let () = close_in inc_b in - { tb_whites = m_w; tb_blacks = m_b } \ No newline at end of file + { OCamlTB.tb_whites = m_w; OCamlTB.tb_blacks = m_b } \ No newline at end of file diff --git a/bin/query/uint63.ml b/bin/query/uint63.ml new file mode 100644 index 0000000..d03f61d --- /dev/null +++ b/bin/query/uint63.ml @@ -0,0 +1,215 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* = 0 then + begin q := Int64.logor !q 1L; nh := Int64.sub !nh y; end + done; + !q, !nh + +let div21 xh xl y = + if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y + +(* exact multiplication *) +let mulc x y = + let lx = Int64.logand x maxuint31 in + let ly = Int64.logand y maxuint31 in + let hx = Int64.shift_right x 31 in + let hy = Int64.shift_right y 31 in + (* compute the median products *) + let s = Int64.add (Int64.mul lx hy) (Int64.mul hx ly) in + (* s fits on 64 bits, split it into a 33-bit high part and a 31-bit low part *) + let lr = Int64.shift_left (Int64.logand s maxuint31) 31 in + let hr = Int64.shift_right_logical s 31 in + (* add the outer products *) + let lr = Int64.add (Int64.mul lx ly) lr in + let hr = Int64.add (Int64.mul hx hy) hr in + (* hr fits on 64 bits, since the final result fits on 126 bits *) + (* now x * y = hr * 2^62 + lr and lr < 2^63 *) + let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in + let hr = Int64.shift_right_logical hr 1 in + (* now x * y = hr * 2^63 + lr, but lr might be too large *) + if Int64.logand lr Int64.min_int <> 0L + then Int64.add hr 1L, mask63 lr + else hr, lr + +let equal (x : t) y = x = y + +let compare x y = Int64.compare x y + +let compares x y = Int64.(compare (shift_left x 1) (shift_left y 1)) + +(* Number of leading zeroes *) +let head0 x = + let r = ref 0 in + let x = ref x in + if Int64.logand !x 0x7FFFFFFF00000000L = 0L then r := !r + 31 + else x := Int64.shift_right !x 31; + if Int64.logand !x 0xFFFF0000L = 0L then (x := Int64.shift_left !x 16; r := !r + 16); + if Int64.logand !x 0xFF000000L = 0L then (x := Int64.shift_left !x 8; r := !r + 8); + if Int64.logand !x 0xF0000000L = 0L then (x := Int64.shift_left !x 4; r := !r + 4); + if Int64.logand !x 0xC0000000L = 0L then (x := Int64.shift_left !x 2; r := !r + 2); + if Int64.logand !x 0x80000000L = 0L then (x := Int64.shift_left !x 1; r := !r + 1); + if Int64.logand !x 0x80000000L = 0L then (r := !r + 1); + Int64.of_int !r + +(* Number of trailing zeroes *) +let tail0 x = + let r = ref 0 in + let x = ref x in + if Int64.logand !x 0xFFFFFFFFL = 0L then (x := Int64.shift_right !x 32; r := !r + 32); + if Int64.logand !x 0xFFFFL = 0L then (x := Int64.shift_right !x 16; r := !r + 16); + if Int64.logand !x 0xFFL = 0L then (x := Int64.shift_right !x 8; r := !r + 8); + if Int64.logand !x 0xFL = 0L then (x := Int64.shift_right !x 4; r := !r + 4); + if Int64.logand !x 0x3L = 0L then (x := Int64.shift_right !x 2; r := !r + 2); + if Int64.logand !x 0x1L = 0L then (r := !r + 1); + Int64.of_int !r + +(* May an object be safely cast into an Uint63.t ? *) +let is_uint63 t = + Obj.is_block t && Int.equal (Obj.tag t) Obj.custom_tag + && le (Obj.magic t) maxuint63 + +(* Arithmetic with explicit carries *) + +(* Analog of Numbers.Abstract.Cyclic.carry *) +type 'a carry = C0 of 'a | C1 of 'a + +let addc x y = + let r = add x y in + if lt r x then C1 r else C0 r + +let addcarryc x y = + let r = addcarry x y in + if le r x then C1 r else C0 r + +let subc x y = + let r = sub x y in + if le y x then C0 r else C1 r + +let subcarryc x y = + let r = subcarry x y in + if lt y x then C0 r else C1 r diff --git a/bin/web/index.ml b/bin/web/index.ml index ed7748d..c0e69c8 100644 --- a/bin/web/index.ml +++ b/bin/web/index.ml @@ -523,6 +523,11 @@ module View = struct svg [Js_of_ocaml_tyxml.Tyxml_js.R.Svg.g sig_pieces] ) + let print_player pl = + match pl with + | Player.White -> "White" + | Player.Black -> "Black" + let pure_curr_res tb x = match x with | Model.Play { curr_state; _ } -> ( @@ -530,7 +535,7 @@ module View = struct match BearGame.atomic_res RomanWheel.coq_RomanWheel curr_state with | Some res -> ( match res with - | Game.Win pl -> Player.show_player pl ^ " wins!" + | Game.Win pl -> print_player pl ^ " wins!" | Game.Draw -> "Drawn." ) | None -> " " diff --git a/theory/Bear/BearGame.v b/theory/Bear/BearGame.v index ac3a45b..07529ad 100644 --- a/theory/Bear/BearGame.v +++ b/theory/Bear/BearGame.v @@ -10,10 +10,10 @@ Require Import Games.Bear.Graph. Require Import Games.Bear.Sort. Require Import Games.Game.TB. Require Import Games.Game.Player. -Require Import Games.Util.Show. +Require Import Games.Util.IntHash. Require Import Games.Util.Dec. Require Import Games.Util.AssocList. -Require Import Games.Util.StringMap. +Require Import Games.Util.IntMap. Definition NoDup_dec {X} `{Discrete X} (xs : list X) : { NoDup xs } + { ~ NoDup xs }. @@ -518,39 +518,6 @@ Definition strLP : string := "(". Definition strComma : string := ",". Definition strRP : string := ")". -Global Instance BearGameStateShow {G} `{sh : Show (Vert G)} - `{@CommaFree _ sh, @Nonnil _ sh, @SemicolonFree _ sh} : Show (GameState (BearGame G)). -Proof. - simpl. - refine {| - show := fun s => strLP ++ show (to_play s) ++ strComma ++ show (bear s) ++ strComma ++ show (hunters s) ++ strRP; - show_inj := _ - |}. - intros s s' pf. - assert (to_play s = to_play s') as pf1. - { destruct (to_play s), (to_play s'); - (discriminate || reflexivity). - } - assert (bear s = bear s') as pf2. - { destruct pf1. - pose proof (app_l_cancel ("(" ++ show (to_play s)) _ _ pf) - as pf'; clear pf. - pose proof (app_l_cancel "," _ _ pf') as pf. - apply show_inj. - apply (char_free_split pf); apply comma_free. - } - assert (hunters s = hunters s'). - { destruct pf1, pf2. - pose proof (app_l_cancel ("(" ++ show (to_play s)) _ _ pf) - as pf'; clear pf. - pose proof (app_l_cancel ("," ++ show (bear s)) _ _ pf') as pf; clear pf'. - pose proof (app_l_cancel "," _ _ pf) as pf'; clear pf. - apply show_inj. - exact (string_app_lemma _ _ ")" pf'). - } - now apply BG_State_ext. -Defined. - Lemma NoDup_sublists {X} : forall (xs : list X) n, NoDup xs -> forall ys, In ys (sublists n xs) -> NoDup ys. Proof. @@ -1107,6 +1074,5 @@ Defined. Require Import Games.Util.OMap. Require Import Games.Game.OCamlTB. -Definition Bear_TB (G : Graph) `{sh : Show (Vert G)} - `{@CommaFree _ sh, @Nonnil _ sh, @SemicolonFree _ sh} +Definition Bear_TB (G : Graph) `{hsh : IntHash (GameState (BearGame G))} : OCamlTablebase (BearGame G) := certified_TB. diff --git a/theory/Bear/RomanWheel.v b/theory/Bear/RomanWheel.v index 51238ea..88357c5 100644 --- a/theory/Bear/RomanWheel.v +++ b/theory/Bear/RomanWheel.v @@ -1,10 +1,12 @@ Require Import List. Import ListNotations. -Require Import String. -Open Scope string_scope. +Require Import PrimInt63. +Require Import Uint63. +Require Import ZArith. +Require Import Lia. -Require Import Games.Util.Show. +Require Import Games.Util.IntHash. Require Import Games.Bear.Graph. Require Import Games.Bear.BearGame. Require Import Games.Game.TB. @@ -39,41 +41,9 @@ Definition c_clockwise (s : Spoke) : Spoke := Definition list_spokes := [S1;S2;S3;S4;S5;S6;S7;S8]. -Definition str1 : string := "1". -Definition str2 : string := "2". -Definition str3 : string := "3". -Definition str4 : string := "4". -Definition str5 : string := "5". -Definition str6 : string := "6". -Definition str7 : string := "7". -Definition str8 : string := "8". - -Definition show_spoke (s : Spoke) : string := ( - match s with - | S1 => str1 - | S2 => str2 - | S3 => str3 - | S4 => str4 - | S5 => str5 - | S6 => str6 - | S7 => str7 - | S8 => str8 - end)%string. - Inductive SpokeLoc := Mid | L | R. -Definition strM : string := "M". -Definition strL : string := "L". -Definition strR : string := "R". - -Definition show_loc (l : SpokeLoc) : string := ( - match l with - | Mid => strM - | L => strL - | R => strR - end)%string. - Definition list_locs := [Mid;L;R]. @@ -81,118 +51,90 @@ Inductive RWVert := | Center | SpokeVert (s : Spoke) (l : SpokeLoc). -Lemma show_loc_inj : forall l l', - show_loc l = show_loc l' -> l = l'. -Proof. - intros l l'. - destruct l, l'; simpl; - (discriminate || reflexivity). -Qed. - -Lemma spoke_loc : forall s s' l l', - show_spoke s ++ show_loc l = - show_spoke s' ++ show_loc l' -> - s = s' /\ l = l'. -Proof. - intros s s' l l' pf. - destruct s, s'; try inversion pf; - (split; [reflexivity|now apply show_loc_inj]). -Qed. - -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 := +Definition hash_RWVert (v : RWVert) : int := 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 + | Center => 0 + | SpokeVert S1 L => 1 + | SpokeVert S1 Mid => 2 + | SpokeVert S1 R => 3 + | SpokeVert S2 L => 4 + | SpokeVert S2 Mid => 5 + | SpokeVert S2 R => 6 + | SpokeVert S3 L => 7 + | SpokeVert S3 Mid => 8 + | SpokeVert S3 R => 9 + | SpokeVert S4 L => 10 + | SpokeVert S4 Mid => 11 + | SpokeVert S4 R => 12 + | SpokeVert S5 L => 13 + | SpokeVert S5 Mid => 14 + | SpokeVert S5 R => 15 + | SpokeVert S6 L => 16 + | SpokeVert S6 Mid => 17 + | SpokeVert S6 R => 18 + | SpokeVert S7 L => 19 + | SpokeVert S7 Mid => 20 + | SpokeVert S7 R => 21 + | SpokeVert S8 L => 22 + | SpokeVert S8 Mid => 23 + | SpokeVert S8 R => 24 end. -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 unhash_RWVert (z : Z) : option RWVert := ( + match z with + | 0 => Some Center + | 1 => Some (SpokeVert S1 L) + | 2 => Some (SpokeVert S1 Mid) + | 3 => Some (SpokeVert S1 R) + | 4 => Some (SpokeVert S2 L) + | 5 => Some (SpokeVert S2 Mid) + | 6 => Some (SpokeVert S2 R) + | 7 => Some (SpokeVert S3 L) + | 8 => Some (SpokeVert S3 Mid) + | 9 => Some (SpokeVert S3 R) + | 10 => Some (SpokeVert S4 L) + | 11 => Some (SpokeVert S4 Mid) + | 12 => Some (SpokeVert S4 R) + | 13 => Some (SpokeVert S5 L) + | 14 => Some (SpokeVert S5 Mid) + | 15 => Some (SpokeVert S5 R) + | 16 => Some (SpokeVert S6 L) + | 17 => Some (SpokeVert S6 Mid) + | 18 => Some (SpokeVert S6 R) + | 19 => Some (SpokeVert S7 L) + | 20 => Some (SpokeVert S7 Mid) + | 21 => Some (SpokeVert S7 R) + | 22 => Some (SpokeVert S8 L) + | 23 => Some (SpokeVert S8 Mid) + | 24 => Some (SpokeVert S8 R) + | _ => None + end)%Z. -Global Instance RWVert_Nonnil : Nonnil RWVert. +Lemma unhash_hash : forall v, + unhash_RWVert (to_Z (hash_RWVert v)) = Some v. Proof. - constructor. - destruct x; simpl. - - discriminate. - - destruct s; destruct l; discriminate. + destruct v as [|[] []]; reflexivity. Qed. -Global Instance RWVert_CommaFree : CommaFree RWVert. +Lemma hash_RWVert_inj : forall v v', + hash_RWVert v = hash_RWVert v' -> v = v'. Proof. - constructor. - destruct x. - - simpl; repeat split; discriminate. - - unfold show. - unfold Show_RWVert. - destruct s, l; simpl; - repeat split; discriminate. + intros v v' pf1. + pose proof (unhash_hash v) as pf2. + rewrite pf1 in pf2. + rewrite unhash_hash in pf2. + congruence. Qed. -Global Instance RWVert_Semicolon : SemicolonFree RWVert. +Global Instance IntHash_RWVert : IntHash RWVert := {| + hash := hash_RWVert; + hash_inj := hash_RWVert_inj; + |}. + +Lemma hash_small : forall v, + (to_Z (hash v) < 2 ^ 5)%Z. Proof. - constructor. - destruct x. - - simpl; repeat split; discriminate. - - unfold show. - unfold Show_RWVert. - destruct s, l; simpl; - repeat split; discriminate. + intros [|[][ ]]; simpl; reflexivity. Qed. Lemma NoDup_list_locs : NoDup list_locs. @@ -342,7 +284,419 @@ Proof. now inversion Heq. Defined. -Global Instance Show_RWV : Show (Vert RomanWheel) := - Show_RWVert. +Global Instance IntHash_RWV : IntHash (Vert RomanWheel) := + IntHash_RWVert. + +Definition add_vert (v : Vert RomanWheel) (i : int) : int := + (hash v) lor (i << 5). + +Definition lsb (i : Z) (n : Z) : Z := + i mod (2 ^ n). + +Fixpoint pow2 n : positive := + match n with + | 0 => xH + | S m => xO (pow2 m) + end. + +Lemma pow2_correct : forall n, + 2 ^ n = Pos.to_nat (pow2 n). +Proof. + induction n. + - reflexivity. + - rewrite Nat.pow_succ_r'. + simpl pow2. + rewrite Pos2Nat.inj_xO. + lia. +Qed. + +Lemma pow_pow2 : forall p, + (2 ^ p)%positive = pow2 (Pos.to_nat p). +Proof. + intro p. + apply Pos2Nat.inj. + rewrite Pos2Nat.inj_pow. + apply pow2_correct. +Qed. + +Lemma Pos_lor_add : forall n x y, ( + x < pow2 n -> + Pos.lor x (pow2 n * y) = x + (pow2 n * y))%positive. +Proof. + induction n. + - simpl; lia. + - simpl; intros x y x_small. + destruct x; simpl in *. + + f_equal. + apply IHn. + unfold Pos.lt in x_small. + unfold Pos.compare in x_small. + simpl in x_small. + rewrite Pos.compare_cont_Gt_Lt in x_small. + assumption. + + f_equal. + apply IHn. + assumption. + + f_equal. +Qed. + +Lemma lor_add : forall n x y, ( + 0 <= n -> + 0 <= x -> + 0 <= y -> + x < 2 ^ n -> + Z.lor x (y * 2 ^ n) = x + (y * 2 ^ n))%Z. +Proof. + intros. + rewrite Z.mul_comm. + destruct x. + - rewrite Z.lor_0_l. + lia. + - destruct y; try lia. + + rewrite Z.mul_0_r. + rewrite Z.lor_0_r; lia. + + destruct n; try lia. + rewrite <- Pos2Z.inj_pow in *. + rewrite <- Pos2Z.inj_mul. + simpl; f_equal. + rewrite pow_pow2 in *. + apply Pos_lor_add; assumption. + - lia. +Qed. + +Lemma Pos_lor_small : forall n x y, ( + x < pow2 n -> + y < pow2 n -> + Pos.lor x y < pow2 n)%positive. +Proof. + induction n; intros; simpl in *. + - lia. + - unfold Pos.lt in *. + unfold Pos.compare in *. + destruct x, y; simpl in *. + + rewrite Pos.compare_cont_Gt_Lt in *. + apply IHn; assumption. + + rewrite Pos.compare_cont_Gt_Lt in *. + apply IHn; assumption. + + assumption. + + rewrite Pos.compare_cont_Gt_Lt in *. + apply IHn; assumption. + + apply IHn; assumption. + + now rewrite Pos.compare_cont_Gt_Lt. + + assumption. + + now rewrite Pos.compare_cont_Gt_Lt. + + reflexivity. +Qed. + +Lemma lor_small : forall x y d, ( + 0 <= d -> + 0 <= x -> + 0 <= y -> + x < 2 ^ d -> + y < 2 ^ d -> + Z.lor x y < 2 ^ d)%Z. +Proof. + intros x y d d_nn x_nn y_nn Hx Hy. + destruct x; try lia. + - now rewrite Z.lor_0_l. + - destruct y; try lia. + + now rewrite Z.lor_0_r. + + simpl. + destruct d; try lia. + rewrite <- Pos2Z.inj_pow in *. + apply Pos2Z.pos_lt_pos. + rewrite pow_pow2 in *. + apply Pos_lor_small; assumption. +Qed. + +Definition get_vert (i : int) : option (Vert RomanWheel * int) := + match unhash_RWVert (lsb (to_Z i) 5) with + | Some v => Some (v, i >> 5)%uint63 + | None => None + end. + +Lemma get_vert_add_vert : forall v i d, + (to_Z i < 2^d)%Z -> + (0 <= d)%Z -> + (d + 5 <= 63)%Z -> + get_vert (add_vert v i) = Some (v, i). +Proof. + intros. + unfold get_vert, add_vert. + rewrite lor_spec'. + rewrite lsl_spec. + unfold lsb. + rewrite (Z.mod_small _ wB). + - rewrite lor_add; try apply to_Z_bounded; try apply hash_small. + rewrite Z_mod_plus_full. + rewrite Z.mod_small. + + rewrite unhash_hash. + simpl Vert; do 2 f_equal. + apply to_Z_inj. + rewrite lsr_spec. + rewrite lor_spec'. + rewrite lsl_spec. + rewrite Z.mod_small. + * rewrite <- Z.shiftr_div_pow2; [|apply to_Z_bounded]. + rewrite Z.shiftr_lor. + rewrite (Z.shiftr_div_pow2 (to_Z i * _)); [|apply to_Z_bounded]. + rewrite Z.div_mul; [|vm_compute; lia]. + rewrite Z.shiftr_eq_0; try apply to_Z_bounded. + -- apply Z.lor_0_l. + -- destruct (Z.eq_dec 0 (to_Z (hash v))). + ++ simpl Vert in *; rewrite <- e; reflexivity. + ++ rewrite <- Z.log2_lt_pow2. + ** apply hash_small. + ** destruct (to_Z_bounded (hash v)). + simpl Vert in *; lia. + * split. + -- apply Z.mul_nonneg_nonneg; [|lia]. + apply to_Z_bounded. + -- unfold wB. + simpl Z.of_nat. + apply (Z.lt_le_trans _ (2^(d+5))). + ++ rewrite Z.pow_add_r; simpl; lia. + ++ apply Z.pow_le_mono_r; lia. + + split. + * apply to_Z_bounded. + * apply hash_small. + - split. + + apply Z.mul_nonneg_nonneg; [|lia]. + apply to_Z_bounded. + + unfold wB. + simpl Z.of_nat. + apply (Z.lt_le_trans _ (2^(d+5))). + * rewrite Z.pow_add_r; simpl; lia. + * apply Z.pow_le_mono_r; lia. +Qed. + +Lemma add_vert_small v i d : + (0 <= d)%Z -> + (d + 5 <= 63)%Z -> + (to_Z i < 2^d)%Z -> + (to_Z (add_vert v i) < 2^(d+5))%Z. +Proof. + intros d_nonneg d_small i_small. + unfold add_vert. + rewrite lor_spec'. + rewrite lsl_spec. + rewrite Z.mod_small. + - apply lor_small; try lia. + + apply to_Z_bounded. + + apply Z.mul_nonneg_nonneg; [|lia]. + apply to_Z_bounded. + + apply (Z.lt_le_trans _ (2^5)). + * apply hash_small. + * apply Z.pow_le_mono_r; lia. + + rewrite Z.pow_add_r; try lia. + apply Zmult_gt_0_lt_compat_r; auto; lia. + - split. + + apply Z.mul_nonneg_nonneg; [|lia]. + apply to_Z_bounded. + + apply (Z.lt_le_trans _ (2^(d+5))). + * rewrite Z.pow_add_r; try lia. + apply Zmult_gt_0_lt_compat_r; auto; lia. + * unfold wB, size. + apply Z.pow_le_mono_r; lia. +Qed. + +Definition add_verts (vs : list (Vert RomanWheel)) (i : int) : int := + fold_right add_vert i vs. + +Fixpoint get_verts n (i : int) : option (list (Vert RomanWheel)) := + match n with + | 0 => Some [] + | S m => + match get_vert i with + | Some (v, j) => + match get_verts m j with + | Some vs => Some (v :: vs) + | None => None + end + | None => None + end + end. + +Lemma add_verts_small vs i d : + (0 <= d)%Z -> + (d + 5 * Z.of_nat (length vs) <= 63)%Z -> + (to_Z i < 2^d)%Z -> + (to_Z (add_verts vs i) < 2^(d + 5 * Z.of_nat (length vs)))%Z. +Proof. + intro d_nonneg. + unfold add_verts. + induction vs. + - simpl. + rewrite Z.add_0_r. + lia. + - simpl length. + rewrite Nat2Z.inj_succ. + rewrite <- Z.add_1_r. + simpl fold_right. + intro. + assert (d + 5 * (Z.of_nat (length vs) + 1) = + (d + 5 * (Z.of_nat (length vs))) + 5)%Z as pf by lia. + simpl Vert in pf. + rewrite pf. + intro Hi. + apply add_vert_small; simpl Vert; try lia. + apply IHvs; auto. + simpl Vert; lia. +Qed. + +Lemma get_verts_add_verts : forall vs i d, + (to_Z i < 2^d)%Z -> + (0 <= d)%Z -> + (d + 5 * (Z.of_nat (length vs)) <= 63)%Z -> + get_verts (length vs) (add_verts vs i) = Some vs. +Proof. + induction vs. + - intros; reflexivity. + - intros; simpl. + erewrite get_vert_add_vert. + + erewrite IHvs. + * reflexivity. + * exact H. + * auto. + * simpl length in H1. + simpl Vert. lia. + + apply add_verts_small; eauto. + simpl length in H1. + rewrite Nat2Z.inj_succ in H1. + rewrite <- Z.add_1_r in H1. + simpl Vert; lia. + + simpl length in H1. + rewrite Nat2Z.inj_succ in H1. + rewrite <- Z.add_1_r in H1. + simpl Vert; lia. + + simpl length in H1. + rewrite Nat2Z.inj_succ in H1. + rewrite <- Z.add_1_r in H1. + simpl Vert; lia. +Qed. + +Definition add_player (p : Player.Player) (i : int) : int := + match p with + | Player.White => i << 1 + | Player.Black => 1 lor (i << 1) + end. + +Definition get_player (i : int) : Player.Player * int := + match is_even i with + | true => (Player.White, i >> 1) + | false => (Player.Black, i >> 1) + end%uint63. + +Lemma lor_1_even : forall x : Z, + (0 <= x -> Z.even x = true -> Z.lor 1 x = x + 1)%Z. +Proof. + intros x x_nonneg x_even. + unfold Z.lor. + destruct x; try lia. + rewrite Pos2Z.add_pos_pos. + destruct p; try discriminate. + reflexivity. +Qed. + +Lemma get_player_add_player : forall p i, + (to_Z i < 2^62)%Z -> + get_player (add_player p i) = (p,i). +Proof. + intros. + unfold get_player, add_player. + destruct p. + - rewrite is_even_lsl_1. + f_equal. + apply to_Z_inj. + rewrite lsr_spec. + rewrite lsl_spec. + rewrite Z.mod_small. + + simpl; unfold Z.pow_pos; simpl. + apply Z.div_mul; lia. + + split. + * apply Z.mul_nonneg_nonneg; [|lia]. + apply to_Z_bounded. + * simpl; unfold Z.pow_pos; simpl. + unfold wB; simpl Z.of_nat. + lia. + - rewrite is_even_bit. + rewrite lor_spec; simpl. + f_equal. + apply to_Z_inj. + rewrite lsr_spec. + rewrite lor_spec'. + rewrite lsl_spec. + simpl Z.pow. + unfold Z.pow_pos; simpl Pos.iter. + rewrite Z.mod_small. + + rewrite lor_1_even. + * rewrite Z.div_add_l; [|lia]. + unfold Z.div; simpl; lia. + * apply Z.mul_nonneg_nonneg; [|lia]. + apply to_Z_bounded. + * rewrite Z.even_mul. + apply Bool.orb_true_r. + + split. + * apply Z.mul_nonneg_nonneg; [|lia]. + apply to_Z_bounded. + * simpl; unfold Z.pow_pos; simpl. + unfold wB; simpl Z.of_nat. + lia. +Qed. + +Definition hash_RW_State (s : BG_State RomanWheel) : int := + match s with + | Build_BG_State _ p b hs _ _ _ _ => + add_player p (add_vert b (add_verts hs 0)) + end. + +Lemma hash_RW_State_inj : forall s s', + hash_RW_State s = hash_RW_State s' -> s = s'. +Proof. + intros s s' Hss'. + unfold hash_RW_State in Hss'. + destruct s, s'; simpl in *. + pose proof (f_equal get_player Hss') as pf1. + rewrite get_player_add_player in pf1. + rewrite get_player_add_player in pf1. + - inversion pf1. + pose proof (f_equal get_vert H1) as pf2. + rewrite (get_vert_add_vert _ _ 15) in pf2; try lia. + rewrite (get_vert_add_vert _ _ 15) in pf2; try lia. + + inversion pf2. + pose proof (f_equal (get_verts (length hunters)) H3) as pf3. + rewrite (get_verts_add_verts _ 0 0) in pf3; try (lia||reflexivity). + rewrite hunters_3 in pf3. + rewrite <- hunters_0 in pf3. + rewrite (get_verts_add_verts _ 0 0) in pf3; try (lia||reflexivity). + * apply BG_State_ext; simpl; congruence. + * simpl Vert; rewrite hunters_0; lia. + * simpl Vert; rewrite hunters_3; lia. + + pose proof (add_verts_small hunters0 0 0). + simpl Vert in *. + rewrite hunters_0 in H. + apply H; simpl; [lia|lia |reflexivity]. + + pose proof (add_verts_small hunters 0 0). + simpl Vert in *. + rewrite hunters_3 in H. + apply H; simpl; [lia|lia|reflexivity]. + - apply (Z.lt_trans _ (2^20)); [|lia]. + apply (add_vert_small _ _ 15); simpl; [lia|lia|]. + pose (add_verts_small hunters0) as pf'. + simpl Vert in *. + rewrite hunters_0 in pf'. + apply (pf' _ 0)%Z; unfold to_Z; simpl; try lia. + - apply (Z.lt_trans _ (2^20)); [|lia]. + apply (add_vert_small _ _ 15); simpl; [lia|lia|]. + pose (add_verts_small hunters) as pf'. + simpl Vert in *. + rewrite hunters_3 in pf'. + apply (pf' _ 0)%Z; unfold to_Z; simpl; try lia. +Qed. + +Global Instance IntHash_RW : IntHash (Game.GameState (BearGame RomanWheel)) := {| + hash := hash_RW_State; + hash_inj := hash_RW_State_inj; + |}. Definition RW_TB := Bear_TB RomanWheel. diff --git a/theory/Game/OCamlTB.v b/theory/Game/OCamlTB.v index 40256ac..a8a49be 100644 --- a/theory/Game/OCamlTB.v +++ b/theory/Game/OCamlTB.v @@ -5,15 +5,15 @@ Require Import Compare_dec. Require Import Games.Game.Game. Require Import Games.Game.TB. Require Import Games.Util.OMap. -Require Import Games.Util.Show. +Require Import Games.Util.IntHash. Require Import Games.Game.Player. -Require Import Games.Util.StringMap. +Require Import Games.Util.IntMap. Require Import Games.Game.Strategy. Require Import Games.Game.Win. Require Import Games.Game.Draw. Require Import Games.Util.Dec. -Record OCamlTablebase (G : Game) `{Show (GameState G)} : Type := { +Record OCamlTablebase (G : Game) `{IntHash (GameState G)} : Type := { tb_whites : OM (Player * nat)%type; tb_blacks : OM (Player * nat)%type }. @@ -21,15 +21,15 @@ Record OCamlTablebase (G : Game) `{Show (GameState G)} : Type := { Arguments tb_whites {_} {_} _. Arguments tb_blacks {_} {_} _. -Definition query_TB {G} `{Show (GameState G)} +Definition query_TB {G} `{IntHash (GameState G)} (tb : OCamlTablebase G) (s : GameState G) : option (Player * nat) := match to_play s with - | White => str_lookup s (tb_whites tb) - | Black => str_lookup s (tb_blacks tb) + | White => hash_lookup s (tb_whites tb) + | Black => hash_lookup s (tb_blacks tb) end. -Record CorrectTablebase {M} `{StringMap M} - {G} `{Show (GameState G)} (tb : OCamlTablebase G) := { +Record CorrectTablebase {M} `{IntMap M} + {G} `{IntHash (GameState G)} (tb : OCamlTablebase G) := { query_mate : forall s pl n, query_TB tb s = Some (pl, n) -> @@ -52,8 +52,8 @@ Record CorrectTablebase {M} `{StringMap M} Arguments query_mate {_} {_} {_} {_}. Arguments query_draw {_} {_} {_} {_}. -Definition certified_TB {M} `{StringMap M} - {G} `{Show (GameState G)} `{FinGame G} `{Reversible G} +Definition certified_TB {M} `{IntMap M} + {G} `{IntHash (GameState G)} `{FinGame G} `{Reversible G} `{NiceGame G} `{forall s : GameState G, Discrete (Move s)} : OCamlTablebase G := match TB_final with @@ -64,8 +64,8 @@ Definition certified_TB {M} `{StringMap M} |} end. -Lemma certified_TB_whites {M} `{StringMap M} - {G} `{Show (GameState G)} `{FinGame G} `{Reversible G} +Lemma certified_TB_whites {M} `{IntMap M} + {G} `{IntHash (GameState G)} `{FinGame G} `{Reversible G} `{NiceGame G} `{forall s : GameState G, Discrete (Move s)} : tb_whites certified_TB = white_positions TB_final. Proof. @@ -73,8 +73,8 @@ Proof. destruct TB_final; reflexivity. Qed. -Lemma certified_TB_blacks {M} `{StringMap M} - {G} `{Show (GameState G)} `{FinGame G} `{Reversible G} +Lemma certified_TB_blacks {M} `{IntMap M} + {G} `{IntHash (GameState G)} `{FinGame G} `{Reversible G} `{NiceGame G} `{forall s : GameState G, Discrete (Move s)} : tb_blacks certified_TB = black_positions TB_final. Proof. @@ -82,8 +82,8 @@ Proof. destruct TB_final; reflexivity. Qed. -Lemma certified_TB_correct {M} `{StringMap M} - {G} `{Show (GameState G)} `{FinGame G} `{Reversible G} +Lemma certified_TB_correct {M} `{IntMap M} + {G} `{IntHash (GameState G)} `{FinGame G} `{Reversible G} `{NiceGame G} `{forall s : GameState G, Discrete (Move s)} : CorrectTablebase certified_TB. Proof. @@ -152,8 +152,8 @@ Proof. Qed. CoFixpoint tb_strat {M} {G} (s : GameState G) pl - `{StringMap M} - `{Show (GameState G)} + `{IntMap M} + `{IntHash (GameState G)} (tb : OCamlTablebase G) : strategy pl s. Proof. - destruct (atomic_res s) eqn:s_res. diff --git a/theory/Game/Player.v b/theory/Game/Player.v index d2d3466..f02a0a1 100644 --- a/theory/Game/Player.v +++ b/theory/Game/Player.v @@ -1,27 +1,9 @@ -Require Import String. -Require Import Games.Util.Show. Require Import Games.Util.All. Inductive Player := | White : Player | Black : Player. -Definition show_player : Player -> string := - fun p => - match p with - | White => "White"%string - | Black => "Black"%string - end. - -Global Instance Show_Player : Show Player. -Proof. - refine ( {| - show := show_player; - show_inj := _ - |} ). - intros [] [] pf; (reflexivity || discriminate). -Defined. - #[export] Instance Player_Discrete : Discrete Player. Proof. diff --git a/theory/Game/SampleGame.v b/theory/Game/SampleGame.v index 8b26f1b..82f9a78 100644 --- a/theory/Game/SampleGame.v +++ b/theory/Game/SampleGame.v @@ -1,6 +1,7 @@ Require Import List. Import ListNotations. -Require Import String. +Require Import PrimInt63. +Require Import Uint63. Require Import Games.Game.Player. Require Import Games.Game.Game. @@ -8,9 +9,12 @@ Require Import Games.Game.Draw. Require Import Games.Game.Win. Require Import Games.Game.TB. Require Import Games.Util.AssocList. -Require Import Games.Util.Show. +Require Import Games.Util.IntHash. Require Import Games.Util.Dec. +Require Import Games.Util.OMap. +Require Import Games.Game.OCamlTB. + Inductive Pos := A | B | C | D | E | F. @@ -381,42 +385,30 @@ Proof. - intros [[] []] []; simpl; tauto. Defined. -Global Instance CF_Player : CommaFree Player. -Proof. - constructor. - intros []; - simpl; repeat split; discriminate. -Defined. - -Definition show_pos : Pos -> string := - fun p => - match p with - | A => "A" - | B => "B" - | C => "C" - | D => "D" - | E => "E" - | F => "F" - end. - -Global Instance Show_Pos : Show Pos. -Proof. - refine ( {| - show := show_pos; - show_inj := _ - |} ). - intros [] [] pf; (reflexivity || discriminate). -Defined. +Definition hash_St (st : St) : int := + match st with + | (White,A) => 0 + | (White,B) => 1 + | (White,C) => 2 + | (White,D) => 3 + | (White,E) => 4 + | (White,F) => 5 + | (Black,A) => 6 + | (Black,B) => 7 + | (Black,C) => 8 + | (Black,D) => 9 + | (Black,E) => 10 + | (Black,F) => 11 + end. -Global Instance CF_Pos : CommaFree Pos. +Global Instance foo : IntHash St. refine {| + hash := hash_St; + hash_inj := _; + |}. Proof. - constructor. - intros []; - simpl; repeat split; discriminate. + intros [[][]] [[][]]; simpl; intro pf; try reflexivity; + discriminate ((f_equal to_Z pf)). Defined. -Require Import Games.Util.OMap. -Require Import Games.Game.OCamlTB. - Definition TB_Sample : OCamlTablebase SampleGame := certified_TB. diff --git a/theory/Game/TB.v b/theory/Game/TB.v index 1387054..c9c8358 100644 --- a/theory/Game/TB.v +++ b/theory/Game/TB.v @@ -11,8 +11,8 @@ Require Import Games.Game.Win. Require Import Games.Game.Strategy. (*Require Import Games.Util.TBLoop.*) -Require Import Games.Util.StringMap. -Require Import Games.Util.Show. +Require Import Games.Util.IntMap. +Require Import Games.Util.IntHash. Require Import Games.Util.Dec. Require Import Games.Util.NewLoop. @@ -56,11 +56,11 @@ Context {G : Game}. Context `{FinGame G}. Context `{NiceGame G}. Context `{Reversible G}. -Context `{Show (GameState G)}. +Context `{IntHash (GameState G)}. Context `{forall s : GameState G, Discrete (Move s)}. Context {M : Type -> Type}. -Context `{StringMap M}. +Context `{IntMap M}. Inductive Step := | Eloise : Step @@ -93,8 +93,8 @@ Record TB : Type := { Definition tb_lookup (tb : TB) (s : GameState G) : option (Player * nat) := match to_play s with - | White => str_lookup s (white_positions tb) - | Black => str_lookup s (black_positions tb) + | White => hash_lookup s (white_positions tb) + | Black => hash_lookup s (black_positions tb) end. Definition tag (winner : Player) (n : nat) (s : GameState G) := @@ -102,7 +102,7 @@ Definition tag (winner : Player) (n : nat) (s : GameState G) := Definition add_positions (m : M (Player * nat)) (winner : Player) (n : nat) (ps : list (GameState G)) : M (Player * nat) := - str_adds (map (tag winner n) ps) m. + 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 @@ -186,8 +186,8 @@ Definition eloise_step (tb : TB) (pl : Player) : list (GameState G) := end in let candidates := concat (map enum_preds prev) in let candidates' := - filter_Nones (fun s => str_lookup s m) candidates in - nodup Show_dec candidates'. + filter_Nones (fun s => hash_lookup s m) candidates in + nodup IntHash_dec candidates'. Definition abelard_step (tb : TB) (pl : Player) : list (GameState G) := let prev := @@ -227,14 +227,14 @@ Definition abelard_step (tb : TB) (pl : Player) : list (GameState G) := end in let candidates := concat (map enum_preds prev) in let candidates' := - filter_Nones (fun s => str_lookup s m) candidates in + filter_Nones (fun s => hash_lookup s m) candidates in let candidates'' := filter (fun s => forallb (fun m => - match str_lookup (exec_move s m) m' with + match hash_lookup (exec_move s m) m' with | Some (pl',_) => player_eqb (opp pl) pl' | None => false end) (enum_moves s)) candidates' in - nodup Show_dec candidates''. + nodup IntHash_dec candidates''. Definition TB_init : TB := {| curr := 0; @@ -243,8 +243,8 @@ Definition TB_init : TB := {| white_positions := empty; black_positions := empty; - last_white_positions := nodup Show_dec (enum_wins Black); - last_black_positions := nodup Show_dec (enum_wins White); + last_white_positions := nodup IntHash_dec (enum_wins Black); + last_black_positions := nodup IntHash_dec (enum_wins White); |}. Definition TB_step (tb : TB) : TB := {| @@ -285,10 +285,10 @@ Proof. unfold num_left. intros []; simpl. unfold add_positions. - pose proof (str_size_adds_le + pose proof (hash_size_adds_le (map (tag (step_player last_step0 White) curr0) last_white_positions0) white_positions0). - pose proof (str_size_adds_le + pose proof (hash_size_adds_le (map (tag (step_player last_step0 Black) curr0) last_black_positions0) black_positions0). lia. @@ -321,11 +321,11 @@ Record TB_valid (tb : TB) : Type := { n < curr tb; tb_white : forall {s pl n}, - str_lookup s (white_positions tb) = Some (pl, n) -> + hash_lookup s (white_positions tb) = Some (pl, n) -> to_play s = White; tb_black : forall {s pl n}, - str_lookup s (black_positions tb) = Some (pl, n) -> + hash_lookup s (black_positions tb) = Some (pl, n) -> to_play s = Black; tb_None : forall {s pl} (w : win pl s), @@ -354,9 +354,9 @@ Record TB_valid (tb : TB) : Type := { lbp_NoDup : NoDup (last_black_positions tb); - lwp_disj : forall s, In s (last_white_positions tb) -> str_lookup s (white_positions tb) = None; + lwp_disj : forall s, In s (last_white_positions tb) -> hash_lookup s (white_positions tb) = None; - lbp_disj : forall s, In s (last_black_positions tb) -> str_lookup s (black_positions tb) = None; + lbp_disj : forall s, In s (last_black_positions tb) -> hash_lookup s (black_positions tb) = None; lwp_white : forall s, In s (last_white_positions tb) -> to_play s = White; @@ -422,15 +422,15 @@ Proof. - intros s pl n Htb. unfold tb_lookup, TB_init in Htb; simpl in Htb. destruct (to_play s); - now rewrite str_lookup_empty in Htb. + now rewrite hash_lookup_empty in Htb. - intros s pl n Htb. unfold tb_lookup, TB_init in Htb; simpl in Htb. destruct (to_play s); - now rewrite str_lookup_empty in Htb. + now rewrite hash_lookup_empty in Htb. - intros s pl n Htb; simpl in Htb. - now rewrite str_lookup_empty in Htb. + now rewrite hash_lookup_empty in Htb. - intros s pl n Htb; simpl in Htb. - now rewrite str_lookup_empty in Htb. + now rewrite hash_lookup_empty in Htb. - intros; simpl; lia. - intros s pl s_play [w [w_d _]]. destruct w; simpl in *; try lia. @@ -457,9 +457,9 @@ Proof. - apply NoDup_nodup. - apply NoDup_nodup. - intros. - now apply str_lookup_empty. + now apply hash_lookup_empty. - intros. - now apply str_lookup_empty. + now apply hash_lookup_empty. - intros s HIn; simpl in *. rewrite nodup_In in HIn. pose proof (enum_wins_correct1 _ _ HIn) as s_res. @@ -687,7 +687,7 @@ Proof. destruct (to_play s) eqn:s_play. * simpl. unfold add_positions. - rewrite str_lookup_adds_nIn; auto. + rewrite hash_lookup_adds_nIn; auto. rewrite map_map. unfold tag; simpl. rewrite map_id. @@ -695,7 +695,7 @@ Proof. rewrite lwp_disj in Htb; congruence. * simpl. unfold add_positions. - rewrite str_lookup_adds_nIn; auto. + rewrite hash_lookup_adds_nIn; auto. rewrite map_map. unfold tag; simpl. rewrite map_id. @@ -706,7 +706,7 @@ Proof. destruct (to_play s) eqn:s_play. * simpl. unfold add_positions. - erewrite str_lookup_adds; + erewrite hash_lookup_adds; [reflexivity| apply map_tag_functional|]. rewrite in_map_iff. exists s. @@ -717,7 +717,7 @@ Proof. now rewrite Hpl. * simpl. unfold add_positions. - erewrite str_lookup_adds; + erewrite hash_lookup_adds; [reflexivity| apply map_tag_functional|]. rewrite in_map_iff. exists s. @@ -732,7 +732,7 @@ Proof. destruct (to_play s) eqn:s_play. + simpl in Htb. unfold add_positions in Htb. - destruct (str_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. + destruct (hash_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. * destruct (in_map_sig pf) as [s' [Hs'1 Hs'2]]. unfold tag in Hs'1. epose (lwp_mate _ v Hs'2). @@ -743,7 +743,7 @@ Proof. now rewrite s_play. + simpl in Htb. unfold add_positions in Htb. - destruct (str_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. + destruct (hash_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. * destruct (in_map_sig pf) as [s' [Hs'1 Hs'2]]. unfold tag in Hs'1. epose (lbp_mate _ v Hs'2). @@ -756,14 +756,14 @@ Proof. - intros s pl n Htb. unfold tb_lookup in Htb. destruct (to_play s) eqn:s_play; simpl in *. - + destruct (str_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. + + destruct (hash_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. * rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1; lia. * cut (n < curr tb); [lia|]. eapply (tb_small _ v). unfold tb_lookup; rewrite s_play; eauto. - + destruct (str_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. + + destruct (hash_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. * rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1; lia. @@ -773,7 +773,7 @@ Proof. (* tb_white *) - intros s pl n Htb. simpl in Htb. - destruct (str_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. + destruct (hash_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. + rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1; subst. @@ -782,7 +782,7 @@ Proof. (* tb_black *) - intros s pl n Htb. simpl in Htb. - destruct (str_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. + destruct (hash_lookup_adds_invert _ _ _ _ Htb) as [pf|pf]. + rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1; subst. @@ -793,7 +793,7 @@ Proof. unfold tb_lookup in tb_s. simpl in *. destruct (to_play s) eqn:s_play. - + destruct (str_lookup_adds_None_invert tb_s) as [s_lwp tb'_s]. + + destruct (hash_lookup_adds_None_invert tb_s) as [s_lwp tb'_s]. epose proof (tb_None _ v w) as Hs. unfold tb_lookup in Hs. rewrite s_play in Hs. @@ -812,7 +812,7 @@ Proof. rewrite e. apply (tb_None _ v w'). unfold tb_lookup; now rewrite s_play. - + destruct (str_lookup_adds_None_invert tb_s) as [s_lbp tb'_s]. + + destruct (hash_lookup_adds_None_invert tb_s) as [s_lbp tb'_s]. epose proof (tb_None _ v w) as Hs. unfold tb_lookup in Hs. rewrite s_play in Hs. @@ -841,7 +841,7 @@ Proof. -- rewrite tb_step; simpl. apply not_Some_None. intros [pl' n] tb_s. - destruct (str_lookup_adds_invert _ _ _ _ tb_s) as [pf|pf]. + destruct (hash_lookup_adds_invert _ _ _ _ tb_s) as [pf|pf]. ++ rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1; subst. @@ -872,8 +872,8 @@ Proof. by now rewrite to_play_exec_move, s_play. pose proof (step_player_black _ v sm'_play smm') as Hpl. rewrite tb_step in Hpl; simpl in Hpl. - destruct str_lookup as [[pl' n']|] eqn:tb_sm. - -- destruct (str_lookup_adds_invert _ _ _ _ tb_sm) as [pf|pf]. + destruct hash_lookup as [[pl' n']|] eqn:tb_sm. + -- destruct (hash_lookup_adds_invert _ _ _ _ tb_sm) as [pf|pf]. ++ rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1. @@ -895,7 +895,7 @@ Proof. destruct (m0 _ _ pf); eauto. -- subst. rewrite tb_step in tb_sm; simpl in *. - destruct (str_lookup_adds_None_invert tb_sm). + destruct (hash_lookup_adds_None_invert tb_sm). destruct sm as [w [w_d wm]]. destruct w; [simpl in w_d; lia|congruence|]. pose (tb_None _ v (w m)). @@ -936,7 +936,7 @@ Proof. rewrite In_filter_Nones_iff; split. * apply not_Some_None. intros [pl' n] tb_s. - destruct (str_lookup_adds_invert _ _ _ _ tb_s) as [pf|pf]. + destruct (hash_lookup_adds_invert _ _ _ _ tb_s) as [pf|pf]. -- rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1; subst. @@ -992,11 +992,11 @@ Proof. assert (forall m, {w : win Black (exec_move s m) & depth w <= curr tb /\ minimal w}). { intro m'. specialize (Hforall m' (enum_all m')). - destruct (str_lookup (exec_move s m') + destruct (hash_lookup (exec_move s m') (add_positions (black_positions tb) Black (curr tb) (last_black_positions tb))) as [[[|] n]|] eqn:Hsm; try congruence. clear Hforall. - destruct (str_lookup_adds_invert _ _ _ _ Hsm) as [HIn|tb_sm]. + destruct (hash_lookup_adds_invert _ _ _ _ Hsm) as [HIn|tb_sm]. + destruct (in_map_sig HIn) as [s' [G1 G2]]; inversion G1; subst. pose (lbp_mate _ v G2) as sm. rewrite tb_step in sm; simpl in sm. @@ -1065,7 +1065,7 @@ Proof. destruct w'; simpl in *; try congruence. apply le_n_S. rewrite w_d. - destruct (str_lookup_adds_None_invert Hs1) as [tb_b lwp_b]. + destruct (hash_lookup_adds_None_invert Hs1) as [tb_b lwp_b]. pose (w'' := eloise_win s_res s_play m0 w'). epose proof (tb_None _ v w'') as Hw'. unfold tb_lookup in Hw'. @@ -1094,7 +1094,7 @@ Proof. -- rewrite tb_step; simpl. apply not_Some_None. intros [pl' n] tb_s. - destruct (str_lookup_adds_invert _ _ _ _ tb_s) as [pf|pf]. + destruct (hash_lookup_adds_invert _ _ _ _ tb_s) as [pf|pf]. ++ rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1; subst. @@ -1125,8 +1125,8 @@ Proof. by now rewrite to_play_exec_move, s_play. pose proof (step_player_white _ v sm'_play smm') as Hpl. rewrite tb_step in Hpl; simpl in Hpl. - destruct str_lookup as [[pl' n']|] eqn:tb_sm. - -- destruct (str_lookup_adds_invert _ _ _ _ tb_sm) as [pf|pf]. + destruct hash_lookup as [[pl' n']|] eqn:tb_sm. + -- destruct (hash_lookup_adds_invert _ _ _ _ tb_sm) as [pf|pf]. ++ rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1. @@ -1148,7 +1148,7 @@ Proof. destruct (m0 _ _ pf); eauto. -- subst. rewrite tb_step in tb_sm; simpl in *. - destruct (str_lookup_adds_None_invert tb_sm). + destruct (hash_lookup_adds_None_invert tb_sm). destruct sm as [w [w_d wm]]. destruct w; [simpl in w_d; lia|congruence|]. pose (tb_None _ v (w m)). @@ -1189,7 +1189,7 @@ Proof. rewrite In_filter_Nones_iff; split. * apply not_Some_None. intros [pl' n] tb_s. - destruct (str_lookup_adds_invert _ _ _ _ tb_s) as [pf|pf]. + destruct (hash_lookup_adds_invert _ _ _ _ tb_s) as [pf|pf]. -- rewrite in_map_iff in pf. destruct pf as [s' [Hs'1 Hs'2]]. inversion Hs'1; subst. @@ -1245,11 +1245,11 @@ Proof. assert (forall m, {w : win White (exec_move s m) & depth w <= curr tb /\ minimal w}). { intro m'. specialize (Hforall m' (enum_all m')). - destruct (str_lookup (exec_move s m') + destruct (hash_lookup (exec_move s m') (add_positions (white_positions tb) White (curr tb) (last_white_positions tb))) as [[[|] n]|] eqn:Hsm; try congruence. clear Hforall. - destruct (str_lookup_adds_invert _ _ _ _ Hsm) as [HIn|tb_sm]. + destruct (hash_lookup_adds_invert _ _ _ _ Hsm) as [HIn|tb_sm]. + destruct (in_map_sig HIn) as [s' [G1 G2]]; inversion G1; subst. pose (lwp_mate _ v G2) as sm. rewrite tb_step in sm; simpl in sm. @@ -1318,7 +1318,7 @@ Proof. destruct w'; simpl in *; try congruence. apply le_n_S. rewrite w_d. - destruct (str_lookup_adds_None_invert Hs1) as [tb_b lwp_b]. + destruct (hash_lookup_adds_None_invert Hs1) as [tb_b lwp_b]. pose (w'' := eloise_win s_res s_play m0 w'). epose proof (tb_None _ v w'') as Hw'. unfold tb_lookup in Hw'. @@ -1648,7 +1648,7 @@ Proof. destruct (good_to_list _ (white_good _ X0)) as [ws Hws]. destruct (good_to_list _ (black_good _ X0)) as [bs Hbs]. unfold add_positions. - repeat rewrite str_size_adds; try + repeat rewrite hash_size_adds; try (rewrite map_map; unfold tag; simpl; @@ -1843,23 +1843,23 @@ Proof. apply enum_states_correct. } destruct (to_play s) eqn:s_play. - + assert (In (s, (Black, 0)) (map (tag Black 0) (nodup Show_dec (enum_wins Black)))) as Hs. + + assert (In (s, (Black, 0)) (map (tag Black 0) (nodup IntHash_dec (enum_wins Black)))) as Hs. { rewrite in_map_iff. exists s; split; [reflexivity|]. rewrite nodup_In. erewrite atomic_win_opp in s_play; [|exact s_res]. apply enum_wins_correct2; now destruct pl. } - pose proof (str_adds_ne_pos (map (tag Black 0) (nodup Show_dec (enum_wins Black))) + pose proof (hash_adds_ne_pos (map (tag Black 0) (nodup IntHash_dec (enum_wins Black))) s (Black, 0) Hs); lia. - + assert (In (s, (White, 0)) (map (tag White 0) (nodup Show_dec (enum_wins White)))) as Hs. + + assert (In (s, (White, 0)) (map (tag White 0) (nodup IntHash_dec (enum_wins White)))) as Hs. { rewrite in_map_iff. exists s; split; [reflexivity|]. rewrite nodup_In. erewrite atomic_win_opp in s_play; [|exact s_res]. apply enum_wins_correct2; now destruct pl. } - pose proof (str_adds_ne_pos (map (tag White 0) (nodup Show_dec (enum_wins White))) + pose proof (hash_adds_ne_pos (map (tag White 0) (nodup IntHash_dec (enum_wins White))) s (White, 0) Hs); lia. - intros s pl s_res. apply mate_TB_final_lookup. diff --git a/theory/Util/IntHash.v b/theory/Util/IntHash.v new file mode 100644 index 0000000..ac5f480 --- /dev/null +++ b/theory/Util/IntHash.v @@ -0,0 +1,25 @@ +Require Import Ascii. +Open Scope char. + +Require Import PrimInt63. +Require Import Uint63. +Require Import Lia. +Require List. +Import List.ListNotations. + +Class IntHash (X : Type) : Type := { + hash : X -> int; + hash_inj : forall x x', hash x = hash x' -> x = x' + }. + +Definition IntHash_dec {X} `{IntHash X} : forall x x' : X, + {x = x'} + {x <> x'}. +Proof. + intros. + destruct (eqb (hash x) (hash x')) eqn:Heq. + - rewrite eqb_spec in Heq. + left; now apply hash_inj. + - right; intro. + rewrite eqb_false_spec in Heq. + apply Heq; congruence. +Defined. diff --git a/theory/Util/StringMap.v b/theory/Util/IntMap.v similarity index 54% rename from theory/Util/StringMap.v rename to theory/Util/IntMap.v index 1de2cce..3274fbe 100644 --- a/theory/Util/StringMap.v +++ b/theory/Util/IntMap.v @@ -1,70 +1,71 @@ Require Import Lia. Require Import List. Import ListNotations. -Require Import String. +Require Import PrimInt63. +Require Import Uint63. Require Import Games.Util.Dec. -Require Import Games.Util.Show. +Require Import Games.Util.IntHash. Require Games.Util.AssocList. Module AL := AssocList. -Class StringMap (M : Type -> Type) : Type := { +Class IntMap (M : Type -> Type) : Type := { empty {X} : M X; - add {X} : string -> X -> M X -> M X; - lookup {X} : string -> M X -> option X; + add {X} : int -> X -> M X -> M X; + lookup {X} : int -> 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; + lookup_empty {X} : forall k, lookup k (empty : M X) = None; + lookup_add {X} : forall k (x : X) m, lookup k (add k x m) = Some x; + lookup_add_neq {X} : forall k k' (x : X) m, k <> k' -> + lookup k (add k' x m) = lookup k 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 + size_add {X} : forall k (x : X) m, + size (add k x m) = + match lookup k m with | Some _ => size m | None => S (size m) end }. -Definition str_add {M} {X Y} `{StringMap M} `{Show X} : +Definition hash_add {M} {X Y} `{IntMap M} `{IntHash X} : X -> Y -> M Y -> M Y := - fun x => add (show x). + fun x => add (hash x). -Definition str_lookup {M} {X Y} `{StringMap M} `{Show X} : +Definition hash_lookup {M} {X Y} `{IntMap M} `{IntHash X} : X -> M Y -> option Y := - fun x => lookup (show x). + fun x => lookup (hash x). -Lemma str_lookup_empty {M} {X Y} `{StringMap M} `{Show X} : - forall x, str_lookup x (empty : M Y) = None. +Lemma hash_lookup_empty {M} {X Y} `{IntMap M} `{IntHash X} : + forall x, hash_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. +Lemma hash_lookup_add {M} {X Y} `{IntMap M} `{IntHash X} : + forall (x : X) (y : Y) m, hash_lookup x (hash_add x y m) = Some y. Proof. intros. apply lookup_add. Qed. -Lemma str_lookup_add_neq {M} {X Y} `{StringMap M} `{Show X} : +Lemma hash_lookup_add_neq {M} {X Y} `{IntMap M} `{IntHash X} : forall (x x' : X) (y : Y) m, x <> x' -> - str_lookup x (str_add x' y m) = str_lookup x m. + hash_lookup x (hash_add x' y m) = hash_lookup x m. Proof. intros x x' y m Hxx'. apply lookup_add_neq. - intro Hshow. + intro Hhash. apply Hxx'. - now apply show_inj. + now apply hash_inj. Qed. -Lemma str_size_add {M} {X Y} `{StringMap M} `{Show X} : +Lemma hash_size_add {M} {X Y} `{IntMap M} `{IntHash X} : forall (x : X) (y : Y) m, - size (str_add x y m) = - match str_lookup x m with + size (hash_add x y m) = + match hash_lookup x m with | Some _ => size m | None => S (size m) end. @@ -73,21 +74,21 @@ Proof. apply size_add. Qed. -Fixpoint str_adds {M} {X Y} `{StringMap M} `{Show X} +Fixpoint hash_adds {M} {X Y} `{IntMap M} `{IntHash 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) + | (x,y) :: qs => hash_adds qs (hash_add x y m) end. -Inductive good {M} {X Y} `{StringMap M} `{Show X} : M Y -> Prop := +Inductive good {M} {X Y} `{IntMap M} `{IntHash 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). + | good_a {x y m} : good m -> hash_lookup x m = None -> good (hash_add x y m). -Fixpoint good_as {M} {X Y} `{StringMap M} `{Show X} {ps : list (X * Y)} +Fixpoint good_as {M} {X Y} `{IntMap M} `{IntHash 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). + (disj : forall x y, In (x,y) ps -> hash_lookup x m = None) {struct ps} + : good (hash_adds ps m). Proof. induction ps as [|[x y] qs]. - exact pf. @@ -97,7 +98,7 @@ Proof. apply (disj x y); now left. + now inversion nd. + intros x' y' HIn. - rewrite str_lookup_add_neq. + rewrite hash_lookup_add_neq. * apply (disj x' y'); now right. * simpl in nd; inversion nd. intro Heq. @@ -107,16 +108,16 @@ Proof. exists (x', y'); split; auto. Qed. -Record map_list_equiv {M} {X Y} `{Show X} `{StringMap M} +Record map_list_equiv {M} {X Y} `{IntMap M} `{IntHash X} (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; + lookup_in {x y} : hash_lookup x m = Some y <-> In (x,y) ps; }. -Lemma str_adds_add {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_adds_add {M} {X Y} `{IntMap M} `{IntHash X} {ps : list (X * Y)} : forall x y m, - str_add x y (str_adds ps m) = str_adds (ps ++ [(x,y)]) m. + hash_add x y (hash_adds ps m) = hash_adds (ps ++ [(x,y)]) m. Proof. induction ps; intros. - reflexivity. @@ -125,9 +126,9 @@ Proof. now rewrite IHps. Qed. -Lemma str_adds_app {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_adds_app {M} {X Y} `{IntMap M} `{IntHash X} {ps : list (X * Y)} : forall qs m, - str_adds ps (str_adds qs m) = str_adds (qs ++ ps) m. + hash_adds ps (hash_adds qs m) = hash_adds (qs ++ ps) m. Proof. induction ps; intros. - simpl; now rewrite app_nil_r. @@ -137,72 +138,72 @@ Proof. { now rewrite <- app_assoc. } rewrite H1. rewrite <- IHps. - now rewrite str_adds_add. + now rewrite hash_adds_add. Qed. -Lemma str_size_add_le {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_size_add_le {M} {X Y} `{IntMap M} `{IntHash X} (x : X) (y : Y) : forall m : M Y, - size m <= size (str_add x y m). + size m <= size (hash_add x y m). Proof. intro. - rewrite str_size_add. - destruct str_lookup; lia. + rewrite hash_size_add. + destruct hash_lookup; lia. Qed. -Lemma str_size_add_lt {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_size_add_lt {M} {X Y} `{IntMap M} `{IntHash X} : forall (m : M Y) (x : X) (y : Y), - str_lookup x m = None -> - size m < size (str_add x y m). + hash_lookup x m = None -> + size m < size (hash_add x y m). Proof. - intros. - rewrite str_size_add. - rewrite H1. + intros m x y Hlookup. + rewrite hash_size_add. + rewrite Hlookup. lia. Qed. -Lemma str_size_adds_le {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_size_adds_le {M} {X Y} `{IntMap M} `{IntHash X} (ps : list (X * Y)) : forall m : M Y, - size m <= size (str_adds ps m). + size m <= size (hash_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 (PeanoNat.Nat.le_trans _ (size (hash_add x y m))). + + apply hash_size_add_le. + apply IHqs. Qed. -Lemma str_adds_ne_pos {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_adds_ne_pos {M} {X Y} `{IntMap M} `{IntHash X} (ps : list (X * Y)) : forall (x : X) (y : Y), - In (x,y) ps -> size (str_adds ps empty) > 0. + In (x,y) ps -> size (hash_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. + pose proof (hash_size_adds_le qs (hash_add x' y' empty)). + rewrite hash_size_add in H2. + rewrite hash_lookup_empty in H2. lia. Qed. -Lemma str_size_adds {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_size_adds {M} {X Y} `{IntMap M} `{IntHash 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. + (forall x, In x (map fst ps) -> hash_lookup x m = None) -> + size (hash_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 hash_size_add. rewrite Hpsm. * apply PeanoNat.Nat.add_succ_r. * left; reflexivity. + now inversion ndps. + intros. - rewrite str_lookup_add_neq. + rewrite hash_lookup_add_neq. * apply Hpsm. right; auto. * intro Hx0x. @@ -210,32 +211,41 @@ Proof. now inversion ndps. Qed. -Global Instance string_Discrete : Discrete string := {| - eq_dec := string_dec - |}. +Global Instance int_Discrete : Discrete int. +Proof. + constructor. + intros x y. + destruct (eqb x y) eqn:Heq. + - left. + rewrite eqb_spec in Heq. + exact Heq. + - right. + rewrite eqb_false_spec in Heq. + exact Heq. +Defined. -Lemma str_lookup_adds_invert {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_lookup_adds_invert {M} {X Y} `{IntMap M} `{IntHash 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}. + hash_lookup x (hash_adds ps m) = Some y -> + {In (x,y) ps} + {hash_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. + + destruct (eq_dec (hash x') (hash x)). + * assert (x' = x) as Hx'x by now apply hash_inj. rewrite Hx'x in e. - rewrite str_lookup_add in e. + rewrite hash_lookup_add in e. left; left; congruence. - * rewrite str_lookup_add_neq in e. + * rewrite hash_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} +Lemma good_to_list {M} {X Y} `{IntHash X} `{IntMap M} (m : M Y) (g : good m) : exists (ps : list (X * Y)), map_list_equiv m ps. Proof. induction g. @@ -243,12 +253,12 @@ Proof. + now rewrite size_empty. + constructor. + intros x y. - unfold str_lookup. + unfold hash_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. + + unfold hash_add. + unfold hash_lookup in H1. rewrite size_add. rewrite H1. simpl; congruence. @@ -260,28 +270,28 @@ Proof. rewrite Hx1 in Hx2. rewrite <- l_in in Hx2; congruence. + intros. - unfold str_lookup, str_add. - destruct (string_dec (show x0) (show x)). + unfold hash_lookup, hash_add. + destruct (eq_dec (hash x0) (hash x)). * rewrite e. rewrite lookup_add. split; intro. - -- pose (show_inj _ _ e). + -- pose (hash_inj _ _ e). left; congruence. -- destruct H2; [congruence|]. rewrite <- l_in in H2. - pose (show_inj _ _ e); congruence. + pose (hash_inj _ _ e); congruence. * rewrite lookup_add_neq; auto. - unfold str_lookup in l_in. + unfold hash_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} +Lemma hash_lookup_adds_None_invert {M} {X Y} `{IntMap M} `{IntHash X} {ps} : forall {m : M Y} {x : X}, - str_lookup x (str_adds ps m) = None -> + hash_lookup x (hash_adds ps m) = None -> (~ In x (List.map fst ps)) /\ - str_lookup x m = None. + hash_lookup x m = None. Proof. induction ps as [|[x y] qs]; intros m x' Hx'. - split. @@ -292,26 +302,26 @@ Proof. split. + intros [|]. * rewrite H3 in H2. - now rewrite str_lookup_add in H2. + now rewrite hash_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. + + destruct (eq_dec (hash x') (hash x)). + * rewrite (hash_inj _ _ e) in H2. + now rewrite hash_lookup_add in H2. + * rewrite hash_lookup_add_neq in H2; auto. congruence. Qed. -Lemma str_lookup_adds_nIn {M} {X Y} `{StringMap M} `{Show X} : +Lemma hash_lookup_adds_nIn {M} {X Y} `{IntMap M} `{IntHash 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. + hash_lookup x (hash_adds ps m) = hash_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. + + rewrite hash_lookup_add_neq. * reflexivity. * intro Hxx'; apply nIn. left; symmetry; exact Hxx'. @@ -337,16 +347,20 @@ Definition in_decb {X} `{Discrete X} (x : X) (xs : list X) := | right _ => false end. -Global Instance Show_disc {X} `{Show X} : Discrete X. +Global Instance Hash_disc {X} `{IntHash X} : Discrete X. Proof. constructor. - apply Show_dec. + intros x y. + destruct (eq_dec (hash x) (hash y)). + - left. + now apply hash_inj. + - right; congruence. Defined. -Lemma str_lookup_adds {M} {X Y} `{StringMap M} `{Show X} +Lemma hash_lookup_adds {M} {X Y} `{IntMap M} `{IntHash 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. + hash_lookup x (hash_adds ps m) = Some y. Proof. induction ps as [|[x y] qs]; intros m ndkeys x' y' HIn. - destruct HIn. @@ -354,7 +368,7 @@ Proof. destruct HIn. + inversion H1; subst. destruct (in_dec x' (map fst qs)). - * apply (IHqs (str_add x' y' m)); + * apply (IHqs (hash_add x' y' m)); [exact (AL.functional_tail ndkeys)|]. unfold AL.functional in ndkeys. rewrite in_map_iff in i. @@ -363,13 +377,13 @@ Proof. rewrite (ndkeys x' y' v); auto. ** now left. ** now right. - * rewrite str_lookup_adds_nIn; auto. - apply str_lookup_add. + * rewrite hash_lookup_adds_nIn; auto. + apply hash_lookup_add. + apply IHqs; auto. exact (AL.functional_tail ndkeys). Qed. -Global Instance AssocList_SM : StringMap (AL.t string) := {| +Global Instance AssocList_SM : IntMap (AL.t int) := {| empty X := AL.empty; add X := AL.add; lookup X := AL.lookup; diff --git a/theory/Util/OMap.v b/theory/Util/OMap.v index 1ab083f..b2e2c0a 100644 --- a/theory/Util/OMap.v +++ b/theory/Util/OMap.v @@ -1,11 +1,11 @@ -Require Import String. -Require Games.Util.StringMap. +Require Import PrimInt63. +Require Games.Util.IntMap. Parameter OM : Type -> Type. Parameter empty : forall {X}, OM X. -Parameter add : forall {X}, string -> X -> OM X -> OM X. -Parameter lookup : forall {X}, string -> OM X -> option X. +Parameter add : forall {X}, int -> X -> OM X -> OM X. +Parameter lookup : forall {X}, int -> OM X -> option X. Parameter size : forall {X}, OM X -> nat. Axiom lookup_empty : forall {X} str, @@ -22,16 +22,16 @@ Axiom size_add : forall {X} str (x : X) m, | None => S (size m) end. -Global Instance OMap : StringMap.StringMap OM := {| - StringMap.empty := @empty; - StringMap.add := @add; - StringMap.lookup := @lookup; - StringMap.size := @size; - StringMap.lookup_empty := @lookup_empty; - StringMap.lookup_add := @lookup_add; - StringMap.lookup_add_neq := @lookup_add_neq; - StringMap.size_empty := @size_empty; - StringMap.size_add := @size_add +Global Instance OMap : IntMap.IntMap OM := {| + IntMap.empty := @empty; + IntMap.add := @add; + IntMap.lookup := @lookup; + IntMap.size := @size; + IntMap.lookup_empty := @lookup_empty; + IntMap.lookup_add := @lookup_add; + IntMap.lookup_add_neq := @lookup_add_neq; + IntMap.size_empty := @size_empty; + IntMap.size_add := @size_add |}. Require Import Extraction. diff --git a/theory/Util/Show.v b/theory/Util/Show.v index c62f39d..5c43ba0 100644 --- a/theory/Util/Show.v +++ b/theory/Util/Show.v @@ -202,4 +202,4 @@ Proof. * apply comma_free. * destruct xs; simpl in *; rewrite char_free_app in IHxs; tauto. -Defined. +Defined. \ No newline at end of file