review the formalized statement of CF 1526C2

Stream: new members

[Huỳnh Trần Khanh]

so i'm trying to formalize the game described here
and this is my code:

import data.list.basic
import tactic.omega
structure game_state :=
(running_total : ℤ)
(score : ℤ)
(remaining : list ℤ)

inductive game : game_state → Prop
| empty (running_total : ℤ) : game {
  running_total := running_total,
  score := 0,
  remaining := []
}
| ignore (previous : game_state) (value : ℤ) : game previous → game {
  running_total := previous.running_total,
  score := previous.score,
  remaining := value::previous.remaining
}
| take (previous : game_state) (value : ℤ) (h : previous.running_total - value ≥ 0) : game previous → game {
  running_total := previous.running_total - value,
  score := previous.score + 1,
  remaining := value::previous.remaining
}

def make_goal (values : list ℤ) (score : ℤ) : game_state := {
  running_total := 0,
  score := score,
  remaining := values
}

open game

lemma possible : game (make_goal [1, -2, 3] 2) := begin
  rw make_goal,
  apply take { running_total := 1, score := 1, remaining := [-2, 3] } 1 begin
    omega
  end,
  apply ignore { running_total := 1, score := 1, remaining := [3] } (-2 : ℤ),
  apply take { running_total := 4, score := 0, remaining := [] } 3 begin
    omega,
  end,
  exact empty 4,
end

i have several questions:

• does the inductive definition accurately describe the game
• is there a better way to encode the game

[Huỳnh Trần Khanh]

i haven't done something like this before sorry

[Huỳnh Trần Khanh]

so... game (make_goal [a1, a2, a3, ...] score) means it's possible to drink score potions if the potion values are [a1, a2, a3, ...]

[Kevin Buzzard]

If you lint your file by typing #lint at the end, then you will discover that you have undocumented definitions.

/- The `doc_blame` linter reports: -/
/- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
#print game_state /- constant missing doc string -/
#print game /- constant missing doc string -/
#print make_goal /- def missing doc string -/

Carefully documenting your definitions makes your code much more readable, and greatly helps any human trying to understand what your API does. For example I have a look at your game_state and I have no idea what the difference is between score and running_total, and you have not explained anywhere what these fields are supposed to represent.

[Scott Morrison]

You should try for a design that doesn't require writing an explicit game_state at each step in the proof. It seems quite plausible that the proof could be apply take, apply ignore, apply take, dec_trivial if designed right.

[Scott Morrison]

That is, rather than taking game previous as an argument, and returning game XXX where XXX is some modification of previous, do it the other way around.

[Scott Morrison]

It may also be cleaner to not use a structure for game_state, and directly use an inductive type. I haven't tried doing this so I'm not sure if that helps yet.

[Eric Wieser]

I'd consider renaming game to game_state.is_possible

[Huỳnh Trần Khanh]

wait, how? names aren't supposed to have dots :joy:

[Huỳnh Trần Khanh]

is there a way to put dots inside inductive type names?

[Huỳnh Trần Khanh]

ah, i can just put dots in them :joy: silly me

[Huỳnh Trần Khanh]

til dots don't have special meaning in lean

[Huỳnh Trần Khanh]

wait @Scott Morrison I don't quite understand what you're saying at all, what do you mean by "the other way around"? take XXX, return previous? then i still need to write an explicit game state at each step of the argument

[Huỳnh Trần Khanh]

am i missing something

[Scott Morrison]

import data.list.basic

structure game_state :=
(t s : ℤ)
(r : list ℤ)

inductive game : game_state → Prop
| empty (t : ℤ) : game ⟨t, 0, []⟩
| ignore (t : ℤ) (s : ℤ) (p : ℤ) (r : list ℤ) : game ⟨t,s,r⟩ → game ⟨t,s,p::r⟩
| take (t : ℤ) (s : ℤ) (p : ℤ) (r : list ℤ) : game ⟨t-1,s-p,r⟩ → game ⟨t,s,p::r⟩

open game

lemma possible : game ⟨2, 4, [1, -2, 3]⟩ := begin
  apply take,
  apply ignore,
  apply take,
  convert empty 0,
end

[Scott Morrison]

(Apologies to Kevin for the lack of doc-strings!)