Formalizing strategy problems

Stream: new members

[klh]

image.png
I want to formalize its solution,but I can not even formalize the quesion itself.I just want to use lean to solve some strategy problems.Can someone help me illustrate this with lean4.

[klh]

image.png
The answer is easy,so I think its solution will be a good exercise for a beginner like me.The tough part is just the statement of the question itself :face_holding_back_tears:

[Eric Wieser]

It won't be smooth sailing, but maybe docs#SetTheory.PGame.State is a good tool here

[Violeta Hernández]

I don't think I'd be recommending the PGame API to any beginner. There's a lot of flaws with it in its current state...

[Violeta Hernández]

(no pun intended)

[Violeta Hernández]

That being said, I don't think we currently have any better mechanism to formalize questions like these.

[Eric Wieser]

I agree that this probably isn't very beginner friendly, but I think this would be a good exercise in finding and resolving painpoints in the PGame API, and hopefully you can get expert help from people like Violeta

[Eric Wieser]

I think this might be a correct statement?

import Mathlib

structure Garden (m n : Nat) where
  dandelions : Finset (Fin m × Fin n)
deriving DecidableEq

def Garden.mowRow (g : Garden m n) (i : Fin m) : Option (Garden m n) :=
  if i ∈ g.dandelions.image (·.1) then
    some { dandelions := g.dandelions.filter (·.1 ≠ i) }
  else
    none

abbrev Garden.univ (m n : Nat) : Garden m n where dandelions := Finset.univ

instance : SetTheory.PGame.State (Garden m n) where
  turnBound g := g.dandelions.card
  l g := (Finset.univ.image g.mowRow).filterMap id fun _ _ _ hx hy => by aesop
  r g := sorry
  left_bound := sorry
  right_bound := sorry

example : {(m, n) | SetTheory.Game.ofState (Garden.univ m n) > 0 } = _ := sorry

[David Renshaw]

For this kind of problem, I have had success with a more direct encoding via inductives. (The austere abstractions of the PGame API scare me away).
Something like this should work:

import Mathlib.Tactic

inductive Player where
| Jana : Player
| Viviane : Player
deriving DecidableEq

def Player.other : Player → Player
| .Jana => Viviane
| .Viviane => Jana

structure State (m n : Nat) where
  dandelions : Finset (Fin m × Fin n)
  turn : Player
deriving DecidableEq

inductive Move (m n : Nat) where
| DeleteRow : Fin m → Move m n
| DeleteColumn : Fin n → Move m n
deriving DecidableEq

def Move.IsValid {m n : Nat} (s : State m n) : Move m n → Prop
| DeleteRow ii => ii ∈ s.dandelions.image (·.1)
| DeleteColumn jj => jj ∈ s.dandelions.image (·.2)

def make_move {m n : Nat} (s : State m n) : Move m n → State m n
| .DeleteRow ii => ⟨s.dandelions.filter (·.1 ≠ ii), s.turn.other⟩
| .DeleteColumn jj => ⟨s.dandelions.filter (·.2 ≠ jj), s.turn.other⟩

inductive HasForcedWin (m n : ℕ) : Player → State m n → Prop where

-- If it's player p's turn and there is a valid move after which we can prove
-- `HasForcedWin p`, then `HasForcedWin p` holds on the initial state.
| Self (s : State m n) (mv : Move m n) : Move.IsValid s mv →
   HasForcedWin m n s.turn (make_move s mv) →
   HasForcedWin m n s.turn s

-- If it's player p's turn and all valid moves lead to states where
-- `HasForcedWin p.other` holds, then `HasForcedWin p.other` holds on
-- the initial state.
-- This case includes the end of game condition -- if there are no valid moves,
-- then the play whose turn it is has lost.
| Opponent (s : State m n) :
  (∀ mv, Move.IsValid s mv → HasForcedWin m n s.turn (make_move s mv)) →
   HasForcedWin m n s.turn.other s

abbrev JanaWinsSet : Set (ℕ × ℕ) := sorry

theorem problem1 (m n : ℕ) :
    (m, n) ∈ JanaWinsSet ↔
    HasForcedWin m n Player.Jana ⟨Finset.univ, Player.Jana⟩ := by
  sorry

[klh]

Eric Wieser 发言道：

I think this might be a correct statement?

import Mathlib

structure Garden (m n : Nat) where
  dandelions : Finset (Fin m × Fin n)
deriving DecidableEq

def Garden.mowRow (g : Garden m n) (i : Fin m) : Option (Garden m n) :=
  if i ∈ g.dandelions.image (·.1) then
    some { dandelions := g.dandelions.filter (·.1 ≠ i) }
  else
    none

abbrev Garden.univ (m n : Nat) : Garden m n where dandelions := Finset.univ

instance : SetTheory.PGame.State (Garden m n) where
  turnBound g := g.dandelions.card
  l g := (Finset.univ.image g.mowRow).filterMap id fun _ _ _ hx hy => by aesop
  r g := sorry
  left_bound := sorry
  right_bound := sorry

example : {(m, n) | SetTheory.Game.ofState (Garden.univ m n) > 0 } = _ := sorry

Thank you,this is a little difficult for me :face_holding_back_tears:

[klh]

David Renshaw 发言道：

For this kind of problem, I have had success with a more direct encoding via inductives. (The austere abstractions of the PGame API scare me away).
Something like this should work:

import Mathlib.Tactic

inductive Player where
| Jana : Player
| Viviane : Player
deriving DecidableEq

def Player.other : Player → Player
| .Jana => Viviane
| .Viviane => Jana

structure State (m n : Nat) where
  dandelions : Finset (Fin m × Fin n)
  turn : Player
deriving DecidableEq

inductive Move (m n : Nat) where
| DeleteRow : Fin m → Move m n
| DeleteColumn : Fin n → Move m n
deriving DecidableEq

def Move.IsValid {m n : Nat} (s : State m n) : Move m n → Prop
| DeleteRow ii => ii ∈ s.dandelions.image (·.1)
| DeleteColumn jj => jj ∈ s.dandelions.image (·.2)

def make_move {m n : Nat} (s : State m n) : Move m n → State m n
| .DeleteRow ii => ⟨s.dandelions.filter (·.1 ≠ ii), s.turn.other⟩
| .DeleteColumn jj => ⟨s.dandelions.filter (·.2 ≠ jj), s.turn.other⟩

inductive HasForcedWin (m n : ℕ) : Player → State m n → Prop where

-- If it's player p's turn and there is a valid move after which we can prove
-- `HasForcedWin p`, then `HasForcedWin p` holds on the initial state.
| Self (s : State m n) (mv : Move m n) : Move.IsValid s mv →
   HasForcedWin m n s.turn (make_move s mv) →
   HasForcedWin m n s.turn s

-- If it's player p's turn and all valid moves lead to states where
-- `HasForcedWin p.other` holds, then `HasForcedWin p.other` holds on
-- the initial state.
-- This case includes the end of game condition -- if there are no valid moves,
-- then the play whose turn it is has lost.
| Opponent (s : State m n) :
  (∀ mv, Move.IsValid s mv → HasForcedWin m n s.turn (make_move s mv)) →
   HasForcedWin m n s.turn.other s

abbrev JanaWinsSet : Set (ℕ × ℕ) := sorry

theorem problem1 (m n : ℕ) :
    (m, n) ∈ JanaWinsSet ↔
    HasForcedWin m n Player.Jana ⟨Finset.univ, Player.Jana⟩ := by
  sorry

Oh!Thank you

[klh]

David Renshaw 发言道：

For this kind of problem, I have had success with a more direct encoding via inductives. (The austere abstractions of the PGame API scare me away).
Something like this should work:

import Mathlib.Tactic

inductive Player where
| Jana : Player
| Viviane : Player
deriving DecidableEq

def Player.other : Player → Player
| .Jana => Viviane
| .Viviane => Jana

structure State (m n : Nat) where
  dandelions : Finset (Fin m × Fin n)
  turn : Player
deriving DecidableEq

inductive Move (m n : Nat) where
| DeleteRow : Fin m → Move m n
| DeleteColumn : Fin n → Move m n
deriving DecidableEq

def Move.IsValid {m n : Nat} (s : State m n) : Move m n → Prop
| DeleteRow ii => ii ∈ s.dandelions.image (·.1)
| DeleteColumn jj => jj ∈ s.dandelions.image (·.2)

def make_move {m n : Nat} (s : State m n) : Move m n → State m n
| .DeleteRow ii => ⟨s.dandelions.filter (·.1 ≠ ii), s.turn.other⟩
| .DeleteColumn jj => ⟨s.dandelions.filter (·.2 ≠ jj), s.turn.other⟩

inductive HasForcedWin (m n : ℕ) : Player → State m n → Prop where

-- If it's player p's turn and there is a valid move after which we can prove
-- `HasForcedWin p`, then `HasForcedWin p` holds on the initial state.
| Self (s : State m n) (mv : Move m n) : Move.IsValid s mv →
   HasForcedWin m n s.turn (make_move s mv) →
   HasForcedWin m n s.turn s

-- If it's player p's turn and all valid moves lead to states where
-- `HasForcedWin p.other` holds, then `HasForcedWin p.other` holds on
-- the initial state.
-- This case includes the end of game condition -- if there are no valid moves,
-- then the play whose turn it is has lost.
| Opponent (s : State m n) :
  (∀ mv, Move.IsValid s mv → HasForcedWin m n s.turn (make_move s mv)) →
   HasForcedWin m n s.turn.other s

abbrev JanaWinsSet : Set (ℕ × ℕ) := sorry

theorem problem1 (m n : ℕ) :
    (m, n) ∈ JanaWinsSet ↔
    HasForcedWin m n Player.Jana ⟨Finset.univ, Player.Jana⟩ := by
  sorry

image.pngWhat is wrong with the last line?

[David Renshaw]

is there anything farther down in the file?

[David Renshaw]

it might be failing to parse the next command and reporting the error there

[klh]

image.png
No,this is just the last line in my code.

[David Renshaw]

you might try restarting the lean server on that file

[David Renshaw]

If that doesn't work, please copy/paste your code here, rather than posting a screenshot. It's difficult to debug a screenshot.

[David Renshaw]

What Lean version are you using?