Proved determinacy (Zermelo's Theorem) positionally using incremental…

…ly (backwards) defined strategies

Pdl/Game.lean

@@ -41,6 +41,9 @@ theorem other_B_eq_A : other B = A := by simp [other]
 @[simp]
 theorem Player.not_eq_i_eq_other : (¬ p = i) ↔ p = other i := by cases p <;> cases i <;> simp
 
+@[simp]
+theorem Player.not_eq_other_eq_i : (¬ p = other i) ↔ p = i := by cases p <;> cases i <;> simp
+
 @[simp]
 theorem Player.not_i_eq_other : ¬ i = other i := by cases i <;> simp
 
@@ -62,7 +65,7 @@ class Game where
   turn : Pos → Player -- whose turn is it?
   moves : Pos → Finset Pos -- what are the available moves?
   bound : Pos → Nat
-  bound_h : ∀ p next : Pos, next ∈ moves p → bound next < bound p
+  bound_h : ∀ (p next : Pos), next ∈ moves p → bound next < bound p
 
 /-- Allow notation `p.moves` for `g.moves p`. -/
 abbrev Game.Pos.moves {g : Game} : g.Pos → Finset g.Pos := Game.moves
@@ -88,25 +91,21 @@ theorem Game.Pos.inductionOnLT {g : Game} (p : g.Pos) {motive : g.Pos → Prop}
     apply IH (g.bound q) (by aesop) _ rfl
 
 /-- A strategy in `g` for `i`, whenever it is `i`'s turn, chooses a move, if there are any. -/
-def Strategy (g : Game) (i : Player) : Type := ∀ p : g.Pos, g.turn p = i → g.moves p ≠ ∅ → g.moves p
+def Strategy (g : Game) (i : Player) : Type := ∀ p : g.Pos, g.turn p = i → p.moves.Nonempty → p.moves
+
+noncomputable def choose_move {g : Game} {p : g.Pos} : p.moves.Nonempty → p.moves := Classical.choice ∘ Set.Nonempty.to_subtype
 
 /-- There is always some strategy. -/
-instance Strategy.instNonempty : Nonempty (Strategy g i) := by
-  constructor
-  intro p _ moves_ne_empty
-  simp at moves_ne_empty
-  rw [@Finset.eq_empty_iff_forall_not_mem] at moves_ne_empty
-  apply Classical.choice
-  aesop
+instance Strategy.instNonempty : Nonempty (Strategy g i) := ⟨fun _ _ => choose_move⟩
 
 /-- Winner of a game, if the given strategies are used.
 A player loses iff it is their turn and there are no moves.
 A player wins if the opponent loses. -/
 def winner {g : Game} (sI : Strategy g i) (sJ : Strategy g (other i)) (p : g.Pos) : Player :=
   if h1 : (g.moves p).Nonempty
     then if h2 : g.turn p = i --
-      then winner sI sJ (sI p (by cases i <;> simp_all) (Finset.nonempty_iff_ne_empty.mp h1))
-      else winner sI sJ (sJ p (by cases i <;> simp_all) (Finset.nonempty_iff_ne_empty.mp h1))
+      then winner sI sJ (sI p h2 h1)
+      else winner sI sJ (sJ p (by cases i <;> simp_all) h1)
     else other (g.turn p) -- no more moves, the other player wins
 termination_by
   g.bound p
@@ -344,12 +343,10 @@ inductive inCone {g : Game} (p : g.Pos) : g.Pos → Prop
 | nil : inCone p p
 | step : inCone p q → r ∈ g.moves q → inCone p r
 
--- FIXME everywhere: change `≠ ∅` to `.Nonempty` if the latter is preferred by `simp`?
-
 /-- The cone of all positions reachable from `p` assuming that `i` plays `sI`. -/
 inductive inMyCone {g : Game} (sI : Strategy g i) (p : g.Pos) : g.Pos → Prop
 | nil : inMyCone sI p p
-| myStep : inMyCone sI p q → (has_moves : g.moves q ≠ ∅) → (h : g.turn q = i) → inMyCone sI p (sI q h has_moves)
+| myStep : inMyCone sI p q → (has_moves : q.moves.Nonempty) → (h : g.turn q = i) → inMyCone sI p (sI q h has_moves)
 | oStep : inMyCone sI p q → g.turn q = other i → r ∈ g.moves q → inMyCone sI p r
 
 -- USED !
@@ -362,7 +359,6 @@ lemma winning_here_then_winning_inMyCone {g : Game} [DecidableEq g.Pos] (sI : St
     intro sJ
     specialize IH sJ
     unfold winner at IH
-    have := Finset.nonempty_iff_ne_empty.mpr has_moves
     simp_all
   case oStep q r _ turn_other_i r_in IH =>
     -- Suppose sI is not winning at r.
@@ -386,7 +382,7 @@ def subset_from_here {g : Game} [DecidableEq g.Pos]
     (sI : Strategy g i) (sIset : Finset (Strategy g i)) (p : g.Pos) :=
   ∀ (q : g.Pos), inMyCone sI p q
     → (i_turn : Game.turn q = i)
-    → (has_moves : Game.moves q ≠ ∅)
+    → (has_moves : q.moves.Nonempty)
     → sI q i_turn has_moves ∈ sIset.image (fun sI' => sI' q i_turn has_moves)
 
 -- Need something like a multi-strategy version of `winning_here_then_winning_inMyCone`?
@@ -458,9 +454,8 @@ lemma winning_if_imitating_some_winning {g : Game} (p : g.Pos) (s : Strategy g i
       specialize s'_winning sJ
       simp_all [winner]
 
-noncomputable def Exists.subtype {p : α → Prop} (h : ∃ x, p x) : { x // p x } := by
-  use (Classical.choose h)
-  apply Exists.choose_spec
+noncomputable def Exists.subtype {p : α → Prop} (h : ∃ x, p x) : { x // p x } :=
+  ⟨h.choose, h.choose_spec⟩
 
 noncomputable def Exists.subtype_pair {motive : α → Prop} {p : (x : α) → motive x → Prop}
     (h : ∃ x, ∃ mx : motive x, p x mx) : { xmx : { x // motive x } // p xmx.1 xmx.2 } := by
@@ -537,7 +532,7 @@ theorem winning_strategy_of_all_next_when_others_turnCOPY (g : Game) [DecidableE
 /-- Second helper for `gamedet'`. -/
 theorem winning_strategy_of_all_next_when_others_turn (g : Game) [DecidableEq g.Pos]
     (p : g.Pos) (whose_turn : g.turn p = other i)
-    (win_all_next : ∀ pNext : Game.moves p, ∃ (s : Strategy g i), winning pNext s)
+    (win_all_next : ∀ pNext : p.moves, ∃ (s : Strategy g i), winning pNext s)
     : ∃ (s : Strategy g i), winning p s := by
   wlog has_moves : (Game.moves p).Nonempty
   · unfold winning winner
@@ -550,9 +545,10 @@ theorem winning_strategy_of_all_next_when_others_turn (g : Game) [DecidableEq g.
   --   Exists.subtype (win_all_next pNext.val pNext.prop)
   let s : Strategy g i :=
     (fun pos turn_i has_moves =>
-      if is_relevant : ∃ pNext : g.moves p, inMyCone (stratFor pNext) pNext pos
+      if is_relevant : ∃ pNext : p.moves, inMyCone (stratFor pNext) pNext pos
       then
-        let ⟨pNext, pos_inCone⟩ := Exists.subtype is_relevant
+        let pNext := WellFounded.min WellOrderingRel.isWellOrder.wf _ is_relevant
+        -- let ⟨pNext, pos_inCone⟩ := Exists.subtype is_relevant
         (stratFor pNext) pos turn_i has_moves
       else
         Classical.choice Strategy.instNonempty pos turn_i has_moves -- should never be used
@@ -587,7 +583,7 @@ theorem winning_strategy_of_all_next_when_others_turn (g : Game) [DecidableEq g.
         exact g.bound_h q nextQ.val nextQ.prop
       · simp
       · -- Use `myStep` because it is the turn of `i`.
-        have := inMyCone.myStep q_inMyCone (Finset.nonempty_iff_ne_empty.mp has_moves) turn_i
+        have := inMyCone.myStep q_inMyCone (has_moves) turn_i
         unfold nextQ
         convert this using 1
         -- PROBLEM
@@ -710,3 +706,159 @@ https://en.wikipedia.org/wiki/Zermelo%27s_theorem_(game_theory)
 -/
 theorem gamedet (g : Game) [DecidableEq g.Pos] (p : g.Pos) :
     (∃ s : Strategy g A, winning p s) ∨ (∃ s : Strategy g B, winning p s) := gamedet' g p _ rfl
+
+
+-- Strategy for specific height
+def NStrategy (g : Game) (n : ℕ) (i : Player) : Type := ∀ p, g.bound p = n → g.turn p = i → p.moves.Nonempty → p.moves
+
+-- -- Interpret Strategy as NStrategy
+-- instance Strategy_as_NStrategy : Coe (Strategy g i) (NStrategy g n i) := ⟨fun s p _ => s p⟩
+
+-- -- Winner of a game guided by the given n-strategies, starting from a position with bound <= n
+-- def Nwinner (sI : NStrategy g n i) (sJ : NStrategy g n (other i)) (p : g.Pos) (h : g.bound p <= n) : Player :=
+--   if h1 : (g.moves p).Nonempty
+--     then if h2 : g.turn p = i
+--       then Nwinner sI sJ (sI p h h2 h1) <| (le_of_lt <| g.bound_h _ _ (sI _ _ _ _).prop).trans h
+--       else Nwinner sI sJ (sJ p h _  h1) <| (le_of_lt <| g.bound_h _ _ (sJ _ _ (by cases i <;> simp_all) _).prop).trans h
+--     else other (g.turn p)
+-- termination_by
+--   g.bound p
+-- decreasing_by
+--   all_goals
+--     apply g.bound_h; simp
+
+-- -- Auxiliary theorem with n as variable for induction
+-- theorem Nwinner_eq_winner_aux {g : Game} (sI : Strategy g i) (sJ : Strategy g (other i)) (p : g.Pos)
+--     (h : g.bound p <= n) :
+--     @Nwinner _ _ i sI sJ p h = winner sI sJ p := by
+--   unfold Nwinner winner dite
+--   cases Finset.decidableNonempty with
+--   | isTrue h1 => cases instDecidableEqPlayer (g.turn p) i with
+--     | isTrue h2 => simp only [Nwinner_eq_winner_aux _ _ ((Strategy_as_NStrategy.coe sI) p ..)]
+--     | isFalse h2 => simp only [Nwinner_eq_winner_aux _ _ ((Strategy_as_NStrategy.coe sJ) p ..)]
+--   | isFalse h1 => rfl
+-- termination_by
+--   g.bound p
+-- decreasing_by
+--   all_goals
+--     apply g.bound_h; simp
+
+-- theorem Nwinner_eq_winner (sI : Strategy g i) (sJ : Strategy g (other i)) (p : g.Pos) :
+--     @Nwinner g (g.bound p) i sI sJ p rfl.le = winner sI sJ p :=
+--   Nwinner_eq_winner_aux ..
+
+-- /-- An n-strategy is winning at `p` (of height <= n) if it wins against all strategies of the other player. -/
+-- def Nwinning (sI : NStrategy g n i) (p : g.Pos) (h : g.bound p <= n) : Prop :=
+--   ∀ sJ : Strategy g (other i), Nwinner sI sJ p h = i
+
+-- noncomputable def bound_winning_strategies n i :
+--     ((p : g.Pos) → g.bound p = n → Prop) × NStrategy g n i :=
+--   Nat.strongRecOn n (fun _ ind =>
+--     let has_win p h : Prop := ∃ q h', (ind _ (lt_of_lt_of_eq (g.bound_h p _ h') h)).fst q rfl
+--     let other_lose p h : Prop := @has_win
+--     ⟨fun p h => (g.turn p = i ∧ has_win p h) ∨ (g.turn p = (other i) ∧ other_lose p h),
+--     have := Classical.dec
+--     fun p h _ nempty => if W : has_win p h
+--       then ⟨W.choose, W.choose_spec.choose⟩
+--       else choose_move nempty
+--     ⟩
+--   )
+
+noncomputable def good {g : Game} (i : Player) (p : g.Pos) : Prop :=
+  (g.turn p = i ∧ ∃ (q : g.Pos) (_ : q ∈ p.moves), good i q) ∨ (g.turn p = other i ∧ ∀ q (_ : q ∈ p.moves), good i q)
+termination_by g.bound p
+decreasing_by all_goals apply g.bound_h _ _; assumption
+
+theorem good_or_other {g : Game} (p : g.Pos) : good (g.turn p) p ∨ good (other (g.turn p)) p :=
+  Nat.strongRecMeasure (g.bound) (fun p ind =>
+    (exists_or_forall_not (fun q => ∃ (h : q ∈ p.moves), good _ q)).elim
+    (fun E => .inl <| by unfold good; apply Or.inl; exact ⟨rfl, E⟩)
+    (fun A => .inr <| by
+      unfold good; apply Or.inr; apply And.intro
+      . exact other_other.symm
+      . intro q h
+        have det := ind q (g.bound_h _ _ h)
+        have := A q
+        by_cases g.turn p = g.turn q <;> simp_all
+    )
+  ) p
+
+theorem good_A_or_B {g : Game} (p : g.Pos) : good A p ∨ good B p := by
+  have det := good_or_other p
+  cases i : g.turn p <;> cases det <;> simp_all
+
+noncomputable def good_strat (i : Player): Strategy g i := fun p turn nempty =>
+  have := Classical.dec
+  if W : good i p
+    then by
+      unfold good at W
+      have E := And.right <| W.resolve_right (not_and_of_not_left _ <| not_eq_other_eq_i.mpr turn)
+      exact ⟨E.choose, E.choose_spec.choose⟩
+    else choose_move nempty
+
+theorem sub_lt_sub_left' : ∀ {a b c : Nat}, b < c → c <= a → a - c < a - b := fun h₁ h₂ =>
+  Nat.sub_lt_sub_left (trans h₁ h₂) h₁
+
+theorem bound_le_in_cone {s : Strategy g i} : inMyCone s p q → g.bound q <= g.bound p := fun h =>
+  by induction h with
+  | nil => rfl
+  | myStep _ _ _ ih => exact le_of_lt (lt_of_lt_of_le (g.bound_h _ _ <| Subtype.mem _) ih)
+  | oStep _ _ h ih => exact le_of_lt (lt_of_lt_of_le (g.bound_h _ _ h) ih)
+
+theorem good_cone {g : Game} {p r : g.Pos} (W : good i p) (h : inMyCone (good_strat i) p r) : good i r := by
+  induction h with
+  | nil => exact W
+  | oStep _ turn h ih =>
+    unfold good at ih
+    exact (ih.resolve_left (not_and_of_not_left _ <| not_eq_i_eq_other.mpr turn)).right _ h
+  | @myStep q a nempty turn ih =>
+    unfold good_strat
+    if good i q
+      then
+        let E := good_strat.proof_1 i q turn ih
+        simp only [ih, ↓reduceDIte]
+        exact (good_strat.proof_1 i q turn (of_eq_true (eq_true ih))).choose_spec.choose_spec
+      else contradiction
+
+-- this is buggy for some reason:
+-- . unfold good at ih; exact (Exists.choose_spec (And.right <| Or.resolve_right _ (not_and_of_not_left _ <| not_eq_other_eq_i.mpr turn))).choose_spec
+-- . contradiction
+
+theorem good_is_surviving {g : Game} {p : g.Pos} : good i p → g.turn p = i → p.moves.Nonempty := by
+  intro W turn
+  unfold good at W
+  apply (Or.resolve_right . (not_and_of_not_left _ <| not_eq_other_eq_i.mpr turn)) at W
+  match W with | ⟨_, ⟨q, ⟨h, _⟩⟩⟩ => exact ⟨q,h⟩
+
+set_option pp.proofs true
+
+theorem cone_trans {p q r : g.Pos} {s : Strategy g i} : inMyCone s p q → inMyCone s q r → inMyCone s p r :=
+  fun a b => by induction b with
+  | nil => assumption
+  | myStep _ _ _ ih => exact .myStep ih ..
+  | oStep a turn h ih => exact .oStep ih turn h
+
+theorem surviving_is_winning {sI : Strategy g i} (surv : ∀ q, inMyCone sI p q → g.turn q = i → q.moves.Nonempty)
+    : winning p sI :=
+  fun sJ => by
+    unfold winner
+    split
+    case isFalse empty =>
+      by_contra turn
+      apply (not_eq_other_eq_i.mp ∘ Ne.symm) at turn
+      exact empty (surv _ .nil turn.symm)
+    split
+    . exact surviving_is_winning (surv . ∘ cone_trans (.myStep .nil _ _)) _
+    next _ turn =>
+      exact surviving_is_winning (surv . ∘ cone_trans (.oStep .nil (not_eq_i_eq_other.mp turn) <| Subtype.mem _)) _
+termination_by g.bound p
+decreasing_by all_goals apply g.bound_h; exact Subtype.mem _
+
+theorem good_strat_winning (W : good i p) : winning p (good_strat i) :=
+  surviving_is_winning fun _ => good_is_surviving ∘ (good_cone W)
+
+theorem gamedetCOPY (g : Game) [DecidableEq g.Pos] (p : g.Pos) :
+    (∃ s : Strategy g A, winning p s) ∨ (∃ s : Strategy g B, winning p s) := Or.imp
+    (⟨good_strat A, good_strat_winning .⟩)
+    (⟨good_strat B, good_strat_winning .⟩)
+    <| good_A_or_B p