From 308cf30860d890eeef31748338b5d02679e74cad Mon Sep 17 00:00:00 2001 From: Malvin Gattinger Date: Tue, 26 Nov 2024 18:40:13 +0100 Subject: [PATCH] WIP winning_strategy_of_all_next_when_others_turn --- Pdl/Game.lean | 69 +++++++++++++++++++++++++++++++++------------------ 1 file changed, 45 insertions(+), 24 deletions(-) diff --git a/Pdl/Game.lean b/Pdl/Game.lean index 0180993..b3c3f5c 100644 --- a/Pdl/Game.lean +++ b/Pdl/Game.lean @@ -189,7 +189,8 @@ lemma winner_eq_of_strategy_eq_from_here {g : Game} {sI sI' : Strategy g i} apply le_of_lt apply bound_strat_lt -lemma winning_strategy_of_next_when_my_turn (g : Game) [DecidableEq g.Pos] +/-- First helper for `gamedet'`. -/ +lemma winning_strategy_of_one_next_when_my_turn (g : Game) [DecidableEq g.Pos] (p : g.Pos) (whose_turn : g.turn p = i) (nextPos : g.moves p) (s : Strategy g i) (s_wins_next : winning nextPos s) : ∃ s' : Strategy g i, winning p s' := by @@ -216,6 +217,21 @@ lemma winning_strategy_of_next_when_my_turn (g : Game) [DecidableEq g.Pos] subst whose_turn simp_all +/-- Second helper for `gamedet'`. NOTE: might not be correct yet! -/ +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) + : ∃ (s : Strategy g i), winning p s := by + -- We need to "stitch together" the strategies given by `win_all_next`. + let s' : Strategy g i := + (fun pos turn_i has_moves => if h : pos ∈ Game.moves p + then (Classical.choose (win_all_next pos h)) pos turn_i has_moves + else sorry) -- PROBLEM: how to choose later strategy without memory ??? + use s' + unfold winning winner + intro sJ + sorry + /-- Generalized version of `gamedet` for the proof by induction on `g.bound p`. -/ theorem gamedet' (g : Game) [DecidableEq g.Pos] (p : g.Pos) n (h : n = g.bound p) : (∃ s : Strategy g A, winning p s) ∨ (∃ s : Strategy g B, winning p s) := by @@ -242,30 +258,23 @@ theorem gamedet' (g : Game) [DecidableEq g.Pos] (p : g.Pos) n (h : n = g.bound p -- -- If the bound still allows moves, distinguish cases if there are any. by_cases haveMoves : (g.moves p).Nonempty - · -- By IH, at all next states one of the players must have a winning strategy: - have claim : ∀ pNext ∈ g.moves p, (∃ (s : Strategy g A), winning pNext s) - ∨ ∃ (s : Strategy g B), winning pNext s := by - intro pNext pNext_in_moves_p - let m := g.bound pNext - have : m ≤ n := by apply Nat.le_of_lt_succ; rw [h]; exact g.bound_h _ _ pNext_in_moves_p - exact IH _ this pNext rfl - -- Is there a next state where the current player has a winning strategy? + · -- There is a move. Is there a next state where the current player has a winning strategy? by_cases ∃ pNext ∈ g.moves p, ∃ (s : Strategy g (g.turn p)), winning pNext s case pos hyp => rcases hyp with ⟨pNext, pNext_in, s, s_winning⟩ -- Whose turn is it? That player has a winning strategy! cases whose_turn : g.turn p + -- GOLF: merge/shorten? case A => left - apply winning_strategy_of_next_when_my_turn g p whose_turn ⟨pNext, _⟩ (whose_turn ▸ s) + apply winning_strategy_of_one_next_when_my_turn g p whose_turn ⟨pNext, _⟩ (whose_turn ▸ s) convert s_winning · simp_all · exact eqRec_heq whose_turn s · exact pNext_in case B => right - -- Analogous to `case A`. - apply winning_strategy_of_next_when_my_turn g p whose_turn ⟨pNext, _⟩ (whose_turn ▸ s) + apply winning_strategy_of_one_next_when_my_turn g p whose_turn ⟨pNext, _⟩ (whose_turn ▸ s) convert s_winning · simp_all · exact eqRec_heq whose_turn s @@ -276,20 +285,32 @@ theorem gamedet' (g : Game) [DecidableEq g.Pos] (p : g.Pos) n (h : n = g.bound p cases whose_turn : g.turn p case A => right - rcases Classical.choice haveMoves.to_subtype with ⟨pNext, pNext_in⟩ - -- Situation: - -- it is the turn of A - specialize hyp pNext pNext_in -- all A strategies here are NOT winning - specialize claim pNext pNext_in -- in the next position someone has a winning strategy - -- TODO: - -- claim that B has a winning strategy - -- show that the move by A does not matter - -- also use `winning_strategy_of_next_when_my_turn` here? - sorry + apply winning_strategy_of_all_next_when_others_turn _ _ (by simp_all) + -- By IH and `hyp` at all next states B must have a winning strategy: + intro pNext pNext_in_moves_p + let m := g.bound pNext + have : m ≤ n := by apply Nat.le_of_lt_succ; rw [h]; exact g.bound_h _ _ pNext_in_moves_p + have Awin_or_Bwin := IH _ this pNext rfl + have := hyp pNext pNext_in_moves_p + suffices ¬ (∃ (s : Strategy g _), winning pNext s) by tauto + push_neg + intro s + rw [whose_turn] at this + exact this s case B => left - -- should be analogous to `case A`. - sorry + apply winning_strategy_of_all_next_when_others_turn _ _ (by simp_all) + -- By IH and `hyp` at all next states B must have a winning strategy: + intro pNext pNext_in_moves_p + let m := g.bound pNext + have : m ≤ n := by apply Nat.le_of_lt_succ; rw [h]; exact g.bound_h _ _ pNext_in_moves_p + have Awin_or_Bwin := IH _ this pNext rfl + have := hyp pNext pNext_in_moves_p + suffices ¬ (∃ (s : Strategy g _), winning pNext s) by tauto + push_neg + intro s + rw [whose_turn] at this + exact this s · -- No moves left, we have a winner by definition. unfold winning unfold winner