infinite_game.lean

import tactic.basic

/-- The states and moves of an infinite two-player game. -/
structure game :=
(angel_state devil_state : Type)
(angel_move : angel_state → set devil_state) 
(devil_move : devil_state → set angel_state) 
-- one could also define `angel_move : angel_state → Type`
-- and `next_state : Π {s}, angel_move s → devil_state`,
-- to allow the game to  distinguish moves leading to the same state.

variable {G : game}

def angel_move (s : G.angel_state) : set G.devil_state := G.angel_move s
def devil_move (s : G.devil_state) : set G.angel_state := G.devil_move s

/- We assume the rules of the game are such that Devil wins when Angel has no valid move, and Angel
wins if they can keep playing forever. -/

/-- `devil_strat s` is the type of strategies for Devil which ensure that, starting from `s`,
Angel runs out of moves in finite time. -/
inductive devil_strat : G.angel_state ⊕ G.devil_state → Type
| inl {s : G.angel_state} (f : Π t ∈ angel_move s, devil_strat (sum.inr t)) : 
  devil_strat (sum.inl s)
| inr {s : G.devil_state} {t : G.angel_state} (v : t ∈ devil_move s) 
  (strat : devil_strat (sum.inl t)) : devil_strat (sum.inr s)

/- Same as above, but proof irrelevant. -/
inductive devil_win : G.angel_state ⊕ G.devil_state → Prop
| inl {s : G.angel_state} (h : ∀ t ∈ angel_move s, devil_win (sum.inr t)) : 
  devil_win (sum.inl s)
| inr {s : G.devil_state} {t : G.angel_state} (v : t ∈ devil_move s) 
  (h : devil_win (sum.inl t)) : devil_win (sum.inr s)

/-- This relates the proof-relevant notion of winning strategy with the 'winning position' 
predicate.-/
lemma nonempty_devil_strat_iff_devil_win (s : G.angel_state ⊕ G.devil_state) : 
  nonempty (devil_strat s) ↔ devil_win s :=
begin
  split,
  { rintros ⟨h⟩,
    induction h with s f ih s t v str ih,
    { exact devil_win.inl (λ t v, ih _ v) },
    { exact devil_win.inr v ih } },
  { intro h,
    induction h with s h ih s t v h ih,
    { exact ⟨devil_strat.inl $ λ t v, classical.choice (ih t v)⟩ },
    { exact ⟨devil_strat.inr v (classical.choice ih)⟩ } }
end

/-- If it's the opponent's turn and the current position is a win for you, then any valid move for 
your opponent leads to a winning position for you. -/
lemma devil_win_inl_iff (s : G.angel_state) :
  devil_win (sum.inl s) ↔ ∀ t ∈ angel_move s, devil_win (sum.inr t) :=
⟨by { rintro ⟨⟩, assumption }, devil_win.inl⟩

/-- If it's your turn and the current position is a win, then you have a valid move leading to
another winning position for you. -/
lemma devil_win_inr_iff (s : G.devil_state) :
  devil_win (sum.inr s) ↔ ∃ t ∈ devil_move s, devil_win (sum.inl t) :=
⟨by intro h; rcases h; exact ⟨h_t, h_v, h_h⟩, by rintro ⟨t, v, h⟩; exact devil_win.inr v h⟩

/-- `angel_win s` means that Angel can play forever starting from `s`. -/
def angel_win (s : G.angel_state ⊕ G.devil_state) : Prop := ¬ devil_win s

lemma angel_win_inl_iff (s : G.angel_state) : 
  angel_win (sum.inl s) ↔ ∃ t ∈ angel_move s, angel_win (sum.inr t) :=
by { unfold angel_win, rw devil_win_inl_iff, simp only [not_forall] }

lemma angel_win_inr_iff (s : G.devil_state) : 
  angel_win (sum.inr s) ↔ ∀ t ∈ devil_move s, angel_win (sum.inl t) :=
by { unfold angel_win, rw devil_win_inr_iff, simp only [not_exists] }

/-- This expresses that `angel_win` is the largest predicate on `G.angel_state ⊕ G.devil_state`
satisfying the forward implications in `angel_win_in*_iff`. -/
lemma angel_win_coinduction {P : G.angel_state ⊕ G.devil_state → Prop}
  (h_inl : ∀ s : G.angel_state, P (sum.inl s) → ∃ t ∈ angel_move s, P (sum.inr t))
  (h_inr : ∀ s : G.devil_state, P (sum.inr s) → ∀ t ∈ devil_move s, P (sum.inl t))
  (s : G.angel_state ⊕ G.devil_state) (ps : P s) : angel_win s :=
begin
  intro hd,
  induction hd with s' f ih s' t v ht ih,
  { rcases h_inl s' ps with ⟨t, v, tp⟩, exact ih t v tp },
  { exact ih (h_inr s' ps t v) }
end

lemma determinacy (s : G.angel_state ⊕ G.devil_state) : angel_win s ∨ devil_win s := em' _

/- In gneral, strategies for an infinite game should be given by a coinductive type family:
`angel_strat : G.angel_state ⊕ G.devil_state → Type` is the 'largest' type family equipped with
projections 
`inl : angel_strat (sum.inl s) → option (Σ t ∈ angel_move, angel_strat (sum.inr t))` and
`inr : angel_strat (sum.inr s) → Π t ∈ devil_move, angel_strat (sum.inl t)`.
(The `option` in the return type of `inl` allows Angel to resign at any point. You can remove it 
if you don't want to allow this.)

We can't define this type family directly since Lean doesn't support coinduction. But as shown 
above, we can define the type family of *winning* strategies inductively when a 'win' means making
sure your opponent runs out of moves in finite time (this is what `devil_strat` does).
We can also define the `Prop`-version of the type of winning strategies for Angel
(we defined `angel_win s := ¬ devil_win s` above, but we could also have defined it as the union
of an appropriate family of subsets).

One would like to prove the Angel analogue of `nonempty_devil_strat_iff_devil_win`, and the proof
should be equally easy, except we don't yet have the coinductive type `angel_strat s`. -/