Advice on Definitions

Stream: new members

[Julian Berman]

Hi. I'm sure a very basic type class definition question given I'm jumping in on the deep end on something I may not be too capable of yet. I'm trying to define a structure -- M by N chessboards, and to prove some theorems about them. I defined an inductive type called pieces with just placeholders for each of the pieces, and then I was trying to define a board as a map from m -> n -> pieces (and then I was going to define moves as particular maps from boards to boards that satisfy "one thing moved, etc."). Does that sound like a reasonable approach, and if so, to express finiteness of m and n it seems like I want fintype? At least that seems like something I should read a tiny bit on looking at how mathlib defines matrices, though it doesn't look like they're defined via class. Any advice definitely welcome (including "go back to tutorials you won't be able to do that yet").

[Yakov Pechersky]

Yeah, matrices will give you what you want. You might want to look at https://leanprover-community.github.io/mathlib_docs/data/matrix/notation.html

[Yakov Pechersky]

Which are matrices indexed by fin n, the finite set of n elements. Or you can just use the matrix definition.

[Julian Berman]

Ah awesome! Thanks, I was reading the notation.lean file itself but definitely easier to read that.

[Yakov Pechersky]

There are some clumsy things about jumping between different fin n and fin m, especially when n \ne m. But if something comes up, do say something. I've been trying to make fin _ smoother. And with lean 3.19, working with fin _ might get better. If you don't care about the ordering within the "N" or "M", working directly with a fintypemight be easier.

[Yakov Pechersky]

But with a chessboard and moves, there is often "move-math" that happens, which then uses some knowledge of equality or ordering of the board.

[Yakov Pechersky]

And I don't know if you care about "computability" or not.

[Yakov Pechersky]

In any case, something like function.update might be useful to indicate moves.

[Julian Berman]

(Thanks making notes of all these to review :)

The first "theorems" I want to prove are simply given two positions exhibiting existence of a sequence of moves (with no captures for simplicity) that move the board from one to the final position

[Yakov Pechersky]

And then statements that certain sequences moves are equivalent under different ordering (of the moves, not the board arrangement), etc could rely on equality checks of the fact that the "positions" are the same.

[Yakov Pechersky]

Ah, I was just typing about sequences of moves as you posted that.

[Yakov Pechersky]

You might have to postulate first, if you disallow captures, that a valid move retains the total number of pieces on a board.

[Yakov Pechersky]

And that no two pieces can occupy the same spot.

[Julian Berman]

yeah exactly. cool -- that's I think what I was assuming I'd need to do -- and then when I did do captures, I postualte there's exactly 1 fewer piece on the board, that it's of the opposite color, and that the moved piece went to that square, and then I redefine moves to be "capture or noncapture", yeah?

[Yakov Pechersky]

Just writing up a quick example.

[Julian Berman]

Ah awesome. Much appreciated! (Don't ruin too much :D but definitely could use one next nudge yeah)

[Yakov Pechersky]

import data.matrix.notation

variables (m' n' : Type) [fintype n'] [decidable_eq n'] [fintype m'] [decidable_eq m']
variables (ι : Type) [fintype ι] [decidable_eq ι]

variables (K : Type*)

structure occupied_board :=
(pieces : ι → K)
(board : matrix m' n' (option ι))
(no_superposition : ∀ (x x' : m'), ∀ (y y' : n'), x ≠ x' → y ≠ y' →
  (board x y).is_some → (board x' y').is_some → board x y ≠ board x' y')
(constant_pieces : ∀ ix : ι, ∃ x : m', ∃ y : n', board x y = ix)

[Yakov Pechersky]

So the occupied board is a structure with some data and some axioms about how that data is structured.

[Yakov Pechersky]

You have an indexed set of pieces, so that you can tell them apart.

[Yakov Pechersky]

And a board, where at each square you have either no piece, or some piece, which you refer to by an index

[Yakov Pechersky]

For any two distinct positions, if both are occupied, they must be occupied by different pieces (they're different because their indices are different. So two identical pawns can be different because they have an index written on their bottom when checked.

[Yakov Pechersky]

There's probably a cleaner way to state that axiom, or in a way that makes proving various things easier.

[Yakov Pechersky]

The last axiom is that every index can be found in the board.

[Julian Berman]

Thanks! That is super helpful (I had some pieces of that written down and was struggling with getting it to compile, especially around the fintype declarations where I was somehow getting the syntax wrong)

[Julian Berman]

Maybe one "design" question I guess -- is the reason to use matrix simply because it's got the notation and finite domain pieces which are convenient to use?

[Julian Berman]

I obviously don't expect I'd need to use the ring operations on it right? So it's just a fancy 2d array

[Yakov Pechersky]

There are some APIs about updating it that exist. With lemmas about how transpose commutes with certain ops, etc

[Julian Berman]

a ha, got it

[Yakov Pechersky]

But a matrix is defeq to a m -> n -> alpha

[Yakov Pechersky]

It just has certain constraints on what can be m or n

[Yakov Pechersky]

You might run into some clumsiness stating things about the constant_pieces if you're actually removing pieces form the board. You could take an approach of generating a new index type with the removed pieces removed, or keeping track of a "graveyard", or something else.

[Yakov Pechersky]

Jeremy Avigad has an explanation about a Lean proof of how to place 8 (or 6) queens on a board.

[Julian Berman]

Makes sense.

[Yakov Pechersky]

Which was instrumental for me to understand how Lean works.

[Julian Berman]

ha yeah domination theorems will be next after I get this one done.

[Julian Berman]

I don't know if that's a good thing for me to read it may spoil the ending.

[Julian Berman]

(Maybe I should keep it on the side to cheat from when I get stuck?)

[Yakov Pechersky]

I can't find it at the moment. @Jeremy Avigad , do you have a link on the n-queens problem? Thanks!

[Yakov Pechersky]

I might be misremembering. I've found a mutilated chessboard experiment with Isabelle: https://github.com/avigad/arwm/blob/master/isabelle_experiments/mutilated_notes.md

[Julian Berman]

ah cool yeah the corner removal one -- I was expecting it'd be difficult to express the usual "board color parity" proof so definitely will read that

[Yakov Pechersky]

One might say, just make the indexing of the board use a Cartesian product of two fintypes

[Yakov Pechersky]

Which is also a fintype

[Yakov Pechersky]

But then statements about columns or rows get clunkier

[Yakov Pechersky]

You have to choose what definition works best for what you're trying to prove. That's one of the hardest parts!

[Yakov Pechersky]

Because a good definition leads to more smooth lemma statements and proofs

[Yakov Pechersky]

For example, I could have stated the no superposition lemma using (x, y) ne (x', y'). Which is somewhat more concise. But generating a proof of that hypothesis will be clunkier than the separate hypotheses about x and about y separately. In fact, the proof of that Cartesian pair hypothesis would likely use the separate inequality proofs anyway.

[Yakov Pechersky]

Once you've started to try to prove lemmas, and found something is clunky, there's nothing wrong with going back and reworking the definition, instead of trying to get the lemma to conform.

[Yakov Pechersky]

It might be nicer for you to define the piece as inherently indexed, for example

[Julian Berman]

hm, as in order the set of pieces arbitrarily?

[Yakov Pechersky]

So def piece := io -> K. Maybe a statement about some surjectivity of the indexing at the beginning of the game, that all the possible piece types are present initally.

[Julian Berman]

ah got it. OK going to take your examples and play around a bit and see where I run into trouble. Much appreciated again I'm sure you'll see me again :)

[Julian Berman]

Hello again. Getting back to this after a few days doing other things. Haven't made a ton of progress other than putting what was suggested here in a repo and combining it with the simple notation things I already had (https://github.com/Julian/lean-across-the-board/blob/main/src/chess/board.lean) -- I'm trying to take the board definition that was suggested and just learn how to instantiate that board now. I have:

#check {
  chess.board .
  pieces := ![♞],
  contents := ![![(0 : fin 1)], ![none], ![none]],
  contains_pieces := begin
  end,
  no_superimposed_pieces := sorry,
}

and am now I guess tasked with proving that containment. Assuming that's already on the right track, is there a tactic that's "brute force" there? What it looks like I need to prove is ∀ (ix : fin 1), ∃ (x : fin 1.succ.succ) (y : fin 1), ![![↑0], ![none], ![none]] x y = ↑ix so basically it's a finite list of things, is there a tactic that says "loop over each one and check the thing on the right side, it's there"? Or regardless, if I have fintype 1 which has one element, and I do intro h, which now hypothesizes I have an element of fin 1, how do I say "there's only one of those so give me (0 : fin 1)"?

[Julian Berman]

(If I can do the second part, extract 0: fin 1 then I can use use twice right?)

[Julian Berman]

I think I need an emoji reaction meaning decoder dictionary :D

[Reid Barton]

For the last question I think you can use fin_cases h

[Reid Barton]

but, you might get away with proving the whole ∀ (ix : fin 1), ∃ ... statement using dec_trivial

[Julian Berman]

A ha! Thank you! I tried cases but it didn't make me progress, it just told me now I have \N...

[Julian Berman]

Yeah fin_cases h, use 0, use 0, refl indeed seems to work, and dec_trivial indeed seems to be my "brute force" or whatever, and closes it itself.

[Julian Berman]

Not sure if this is a reasonable question to ask as well, but since library_search and simp didn't close the goal, which were the two things I'd previously heard of, is there some other "higher level" fancy tactic which loops over all tactics with the type of the proposition to prove and gives me one that immediately closes the goal if it does so in 1 step? (i.e. something that would have told me of the existence of dec_trivial?)

[Yakov Pechersky]

Zulip is that fancy tactic.

[Yakov Pechersky]

"there's only one of those so give me (0 : fin 1)": how about exact 0?

[Yakov Pechersky]

There's also subsingleton.elim x y which will give you x = y for x y : fin 1 or any other subsingleton type.

[Julian Berman]

Yakov Pechersky said:

"there's only one of those so give me (0 : fin 1)": how about exact 0?

if I try that I get

[lean] [E] invalid pre-numeral, universe level must be > 0
state:
h : fin 1
⊢ ∃ (y : fin 1), ![![↑0], ![none], ![none]] 0 y = ↑h

[Julian Berman]

(trying the subsingleton thing now too)

[Yakov Pechersky]

Ah, I didn't know you had an exists goal. Then yes, 0 works. You can combine use steps like so: use [0, 0].

[Yakov Pechersky]

#check {
  chess.board .
  pieces := ![♞],
  contents := ![![(0 : fin 1)], ![none], ![none]],
  contains_pieces := begin
    intro ix,
    use 0,
    simp
  end,
  no_superimposed_pieces := sorry,
}

[Julian Berman]

Nice, thanks. How can I interpret what that error message means just so I know? I didn't really take the time to understand universes yet, though I assume it has something to do with maybe russel-paradoxy-set-theory stuff? But what is that error message saying, is it telling me I needed to define that some types are at a higher universe level than I did?

[Reid Barton]

This is just an error message where Lean is completely confused about what you wanted

[Julian Berman]

A ha. OK.

[Reid Barton]

I think it happens when you try to use 0 as a type

[Reid Barton]

or more likely, accidentally use 0 as a type

[Julian Berman]

Syntactically is there a way to avoid needing the underscores when trying to write out an example of my structure: https://github.com/Julian/lean-across-the-board/blob/57ae80d7714f20299d2abab6d8a3e3ac5c477f6c/test/board.lean#L4 -- if I don't and just write example : chess.board :=, I seem to get type,mismatch as structure instance [...] but is expected to have type ⁇ : Sort ?

[Julian Berman]

(And secondly can I within a namespace make all the literals be elements of fintype so I don't have to individually annotate all the numbers I write?)

[Julian Berman]

actually I guess that fintype would change from example to example, so never mind that

[Scott Morrison]

It's possible that hint would have revealed here that dec_trivial would work.

[Julian Berman]

Scott Morrison said:

It's possible that hint would have revealed here that dec_trivial would work.

hm I must be using that wrong -- I found/followed https://leanprover-community.github.io/mathlib_docs/tactics.html#hint and added import tactic.hint but I still seem to get unknown identifier 'hint' -- did I miss a step somehow?

[Julian Berman]

oh does that mean I should add both of those imports? /me tries...

[Julian Berman]

Ah interesting ok I figured it out (that I need by hint not just hint there)

[Julian Berman]

and yes it does suggest dec_trivial, thanks!

[Scott Morrison]

Sorry, yes -- you worked it out: hint is a tactic so only does anything inside a begin ... end or by ... block.

[Scott Morrison]

Don't get in the habit of relying on hint too much. It is really dumb, and will suggest terrible ideas.

[Julian Berman]

All good -- and understood :)

[Julian Berman]

I guess I'm getting syntax fairly fundamentally wrong, but what's wrong with def width (b : board m n ι K) : ℕ := m.card? I get an error of error| [lean] invalid field notation, type is not of the form (C ...) where C is a constant [E]

[Julian Berman]

Or I guess alternatively how do I get the dimension of a side of a matrix instance, probably that's clearer anyhow... that maybe I can look up

[Anne Baanen]

It will probably work if you use fintype.card m instead of m.card.

I'm assuming you have declared m like above:

variables (m : Type) [fintype m] [decidable_eq m]

Abbreviations for the dot-notation like m.card work as follows: we infer the type of m. If it is of the form some_constant x1 x2 ..., then m.card gets expanded to some_constant.card m. So if m : finset α, we get finset.card m, but if m is just any arbitrary type there is no constant whose name we can use. Instead you have to write out the full name of fintype.card.

[Julian Berman]

Aha, ok thanks. It does indeed compile at least if I use fintype.card explicitly, though I still get another error that I've seen before when I try to use it

[Julian Berman]

(fuller example incoming...)

[Julian Berman]

def width (b : board m n ι K) : ℕ := fintype.card m

def b₁ : board _ _ _ _ :=
  { board .
    pieces := ![♞],
    contents := ![![(0 : fin 1)], ![__], ![__]],
    contains_pieces := dec_trivial,
    no_superimposed_pieces := dec_trivial, }

#check width b₁

The check produces:

type mismatch at application
  width b₁
term
  b₁
has type
  board (fin 1.succ.succ) (fin 1) (fin 1) colored_pieces : Type
but is expected to have type
  Type : Type 1

[Anne Baanen]

I suspect you need to declare some variables as implicit. What is the output of #check width?

[Julian Berman]

width :
  Π (m n : Type) [_inst_1 : fintype n] [_inst_2 : decidable_eq n] [_inst_3 : fintype m] [_inst_4 : decidable_eq m]
  (ι : Type) [_inst_5 : fintype ι] [_inst_6 : decidable_eq ι] (K : Type u_2), board m n ι K → ℕ

[Julian Berman]

do I basically put all the types there in that product-y notation as square bracketed variables in the call to width?

[Julian Berman]

er sorry definition of width

[Kenny Lau]

it's width m n ι K b₁ as dictated by the arguments with (round brackets)

[Julian Berman]

as in the signature of width is saying now I should provide all those parameters?

[Reid Barton]

You should provide the ones in () and not the ones in [] or {}.

[Anne Baanen]

Indeed, so for usage of width it's better to make some arguments implicit. Try writing

variables {m n ι K}

above def width, and now #check width b₁ should work.

[Reid Barton]

Or more likely you should arrange to not have so many ones in (), and make them {} instead.

[Julian Berman]

aha! ok {} not [] awesome, that works perfectly

[Julian Berman]

how should I understand that syntax for variables?

[Julian Berman]

more specifically -- why is that something you specify in the whole "scope" or namespace or whatever?

[Julian Berman]

and not in the function declaration?

[Johan Commelin]

to avoid repetition

[Julian Berman]

ok -- but now every function from that point till the bottom of the namespace implicitly takes that variable as an arg right?

[Johan Commelin]

Only if it needs it

[Julian Berman]

aha ok

[Anne Baanen]

Julian Berman said:

aha! ok {} not [] awesome, that works perfectly

The difference between {} and [] is that {m : Type} indicates m can be inferred from its usage later on in the type, #check width will now give something like board ?m ?n ?ι ?K → ℕ. Since b₁ : board m n ι K, and Lean is expecting this argument to be something of the form board ?m ?n ?ι ?K, it concludes the argument ?m has to be m. If you wrote [m : Type] then you're asking the typeclass inference system to produce an element of Type. #check width will give an error in that case, because there is no typeclass instance defined for Type.

[Julian Berman]

so what I tried previously was more like adding [fintype m] to the definition of width

[Julian Berman]

which I thought would say there was a fintype that should be being implicitly referred to in my function

[Julian Berman]

but that obviously didn't work either

[Julian Berman]

(thanks by the way, that explanation I think definitely helped)

[Reid Barton]

Do you mean implicitly referred to when you wrote m.card? that syntax is resolved using type information of m, and adding [fintype m] doesn't affect the type of m.

[Julian Berman]

so originally I wrote something like (without the variables statement suggested): def width (b: board m n i K) [fintype m] := fintype.card m

[Julian Berman]

which I thought would mean m was implicitly an argument

[Julian Berman]

but I guess what I should learn is that that [...] syntax is more like refining an argument that's already declared

[Julian Berman]

so I'd need both that and {m : Type} to say that m was implicit and also by the way a fintype?

[Reid Barton]

Technically a [...] argument is just another argument

[Reid Barton]

If you don't give it a name, it will be assigned one like _inst. And when the function is used, the argument will be synthesized using the type class system.

[Johan Commelin]

[fintype m] should be read as [some_variable_name_that_nobody_should_ever_mention : fintype m]

[Julian Berman]

aha... ok

[Reid Barton]

So, the end result is more or less as you describe.

[Julian Berman]

why doesn't just def width (b : board m _ _ _) : ℕ := fintype.card n work, which also confused me

[Julian Berman]

doesn't the type system know based on how I declared board what types the other 3 need to be?

[Kenny Lau]

no, they can be any fintype

[Kenny Lau]

variables (m n ι K : Type)
def board : Type := sorry
def width (b : board m n ι K) : ℕ := sorry

is equivalent to

def board (m n ι K : Type) : Type := sorry
def width (m n ι K : Type) (b : board m n ι K) : ℕ := sorry

[Kenny Lau]

so Lean doesn't know that it should use m

[Julian Berman]

not sure I understood the point yet (I'm sure that's just me being a bit dense though)

[Kenny Lau]

I might as well have written:

def width (m n ι K : Type) (b : board n n n n) : ℕ := sorry

[Julian Berman]

as in the type system doesn't know whether I meant that?

[Kenny Lau]

yes

[Julian Berman]

(sorry, maybe this is still just a poor questions but) I would assume the type system should think I mean "take the most general type from the board definition that's allowed for each field" no?

[Julian Berman]

i.e. "apply no further restrictions", so not n n n n

[Julian Berman]

(at some point feel free to just tell me "that's just not how it works" obviously :)

[Kenny Lau]

that's too much to ask for the type system to retrospectively declare variables

[Kenny Lau]

_ is reserved for situations when the type system can infer the term

[Julian Berman]

and there's no deferred mechanism there too right?

[Julian Berman]

because really the type I want is "I'm going to pass you an instance later, the type of that parameter is the type of that field on the instance I'll give you later"

[Kenny Lau]

I don't understand what you mean

[Kenny Lau]

if you want to say that Lean should use the definition to infer the underscores

[Kenny Lau]

then it is possible, but not from fintype.card n

[Julian Berman]

will maybe mull on this a bit as I learn some more (I'm sure my dynamically typed daytime programming is showing through a bit too much)

[Julian Berman]

thanks for indulging the question

[Julian Berman]

This doesn't work, in part because I don't yet understand how to easily deal with the option type, but am I on the right track syntactically with using match to define this:

/-- A move is an initial chess board along with the start and end squares
    containing the piece which is moved. -/
structure move :=
(board: board m n ι colored_pieces)
(start_square : m × n)
(end_square : m × n)
(occupied_start:
    (board.contents start_square.1 start_square.2).is_some
    . tactic.exact_dec_trivial)
(valid_for_piece: pieces → Prop :=
 match (board.pieces (board.contents start_square.1 start_square.2)) with
  | pieces.knight := (
    (abs (end_square.1 - start_square.1) = 2
        ∧ abs (end_square.2 - start_square.2) = 1) ∨
    (abs (end_square.2 - start_square.2) = 2
        ∧ abs (end_square.1 - start_square.1) = 1))
 | _ := tt
 end)

[Julian Berman]

It's valid_for_piece that I'm trying to add/define (and I don't see how to tell the match that I already know the square is occupied from occupied_start, so probably I'm doing that part wrong as well and they should somehow combine)

[Julian Berman]

I know there's likely a few things wrong with that, just trying to make progress I guess. tt is not a Prop, if that even is the right type I want there -- what's the trivial proposition?

[Kevin Buzzard]

true

[Julian Berman]

Ah of course.

[Yakov Pechersky]

I would define a separate def that takes a piece and a pair of positions and says whether it is a valid move

[Yakov Pechersky]

Whether or not the end pos is occupied

[Yakov Pechersky]

And doesn't care about board dimensions etc

[Julian Berman]

and then that def would match on the piece?

[Yakov Pechersky]

Exactly. Even more verbose would be separate defns for each move type. Then the match statement is just properly connecting to the defns you made.

[Julian Berman]

makes sense

[Yakov Pechersky]

Which you'd have to do anyway because of en passant or castling, etc.

[Julian Berman]

yeah I'm not even going to bother doing anything but knights to start, and no captures, and no other fun

[Julian Berman]

keepin it quite simple for now, I'm trying to "prove" / "represent" https://github.com/Julian/lean-across-the-board/blob/main/src/guarini.lean

[Julian Berman]

will give that a shot.

[Julian Berman]

Oh also how do I convert between m × n and m \to n? I assume there's some nicer way than the explicit unpacking I did there

[Johan Commelin]

function.curry and function.uncurry

[Julian Berman]

aha, thanks!

[Julian Berman]

I guess that I should indeed first look for things named like the operation I'm doing... :)

[Johan Commelin]

Seriously, that is an extremely important strategy.

[Johan Commelin]

It's the reason why zmod.pow_card is called like that, instead of fermats_little_theorem

[Johan Commelin]

Or look up Cayley Hamilton, or any other theorem that carries the name of a famous mathematician that you learned in 1st or 2nd year...
The mathematician might be named in the docstring, but the theorem will have some crazy name that says what it is doing.
Exception: function.curry

[Yakov Pechersky]

How do you plan on using move? As it is now, every time you try to create a move, you'll have to prove something about a complex board state.

[Yakov Pechersky]

I'm picturing a move as a pair of positions, and possibly tupled with the piece being moved. That is in turn passed to a "is_valid" which takes a board state and that move, and tells you if it's valid.

[Johan Commelin]

Maybe dec_trivial can prove that?

[Julian Berman]

I was hoping dec_trivial would do magic again yeah

[Julian Berman]

Johan Commelin said:

Or look up Cayley Hamilton, or any other theorem that carries the name of a famous mathematician that you learned in 1st or 2nd year...
The mathematician might be named in the docstring, but the theorem will have some crazy name that says what it is doing.
Exception: function.curry

yeah I've noticed a few examples of that already (from just browsing around random theorems) -- it's definitely super helpful

[Julian Berman]

Yakov Pechersky said:

How do you plan on using move? As it is now, every time you try to create a move, you'll have to prove something about a complex board state.

clearly I don't know too much about what I'm doing yet, but other than hoping that dec_trivial would just prove this for me each time I made one, I also assumed at some point I'll want to define ways to "reify" moves onto boards and be able to convert between sequences of moves and sequences of boards -- because ultimately I think the theorem I'm going for is like "this sequence of moves is valid and takes this starting board to this ending board"

[Julian Berman]

I guess "your way" you instead just have sequences of boards, and then you assert that the moves between them are all valid

[Yakov Pechersky]

Totally. Monadic moves while satisfying the valid constraint. Then the whole thing is a 'sequence' in Haskell lingo.

[Julian Berman]

Yes somehow I am getting the distinct sense that I'd be further along in Lean if I knew more Haskell :)

[Julian Berman]

Or more math.

[Julian Berman]

or both, oy.

[Scott Morrison]

@Julian Berman, I haven't looked in any detail at what you're doing, but have you looked at the existing examples of combinatorial games? They will be of a different flavour than what you're doing, but may be useful reading to see how similar things have been done previously. From memory we only have domineering and nim (there is an abandoned dots-and-boxes branch, but I think it didn't have much).

[Kevin Buzzard]

There's an abandoned dots and boxes branch??

[Julian Berman]

I saw the file actually a week or so ago when grepping around. It definitely looked interesting yeah

[Julian Berman]

I didn't read it carefully then but made a note to read it. Maybe now's indeed the time

[Scott Morrison]

The branch#dots_and_boxes seems to have irremediably diverged from master; attempting to merge gave lots of conflicts. The actual dots_and_boxes.lean file is at https://gist.github.com/semorrison/b14fac4a1cb65a117f0fab08a6afabf8, although I have no idea if there are supporting lemmas in other files that got lost. As you can see its far from complete.

[Scott Morrison]

(If I remember right, while most of that file is reasonable, at the end I tried to force dots-and-boxes to "be" a Conway combinatorial game, which it isn't, by doing something awkward like including "alternately counting claimed boxes" as moves after the end of the usual game. This is probably dumb in some way that I hadn't thought of.)

[Kevin Buzzard]

I don't think you can do it like that

[Kevin Buzzard]

I think that dots and boxes is not a combinatorial game and can't be made into one in any natural way. The combinatorial game is called nimdots.

[Kevin Buzzard]

I remember thinking hard about this a decade or so ago

[Kevin Buzzard]

nimdots is just like dots and boxes except last player to complete a legal move wins.

[Scott Morrison]

Yes, I had a bad feeling about this as I was going. In any case I hope the top 80% of that file is still sensible, and one should just lop it off at the first place pgame is mentioned.

[Kevin Buzzard]

in Winning Ways they argue that the two games are very similar, and this is true to a certain extent; I once wrote a paper explaining where the two theories started to differ.

[Scott Morrison]

In any case, I think the most important thing to salvage from that branch is the following doc-string:

/-- All games of dots and boxes are short, because it's hard to beat Kevin. -/
instance short_dots_and_boxes (b : dots_and_boxes.board) : short (dots_and_boxes b) :=

[Julian Berman]

@Yakov Pechersky some very superficial questions I'm sure as I try to understand your commits (thanks again! glad I tempted you :)

[Julian Berman]

I guess first -- rfl is to by refl what like dec_trivial is to tactic.exact_dec_trivial or so?

[Julian Berman]

it's like a tactic that just calls a specific (lemma?/callable?something? what's the terminology for what those are)

[Julian Berman]

Hm does go to definition take me to rfl's definition...

[Julian Berman]

it does, cool, so scratch the above

[Julian Berman]

ok, next, what's the point of simp only?

[Julian Berman]

I can see what it does, but is it just a performance optimization?

[Bryan Gin-ge Chen]

Yes, though it's also sometimes useful if simp simplifies an expression too much. We have a tutorial page on simp which discusses this: https://leanprover-community.github.io/extras/simp.html

[Julian Berman]

Ah, cool, thanks!

[Julian Berman]

I like that that page uses language like "Lean seems to [...] (apparently unfold just asks simp to do its dirty work for it". Makes me feel better about feeling fuzzy about lean's behavior.

[Kevin Buzzard]

The tactic refl is slightly more general than the term rfl, because the tactic will close any goal of the form R x y if R is tagged with an attribute saying it's reflexive (the attribute might also be called refl, I can't remember). On the other hand rfl is just reflexivity of equality; for example if you wanted to prove X <-> X in term mode, you'd use iff.rfl.

[Yakov Pechersky]

Writing lemma FLT : lemma_statement := rfl also flags FLT as a [refl] lemma.

[Julian Berman]

(From that simp page too) -- I guess existsi is probably similar to use? Is there a reason to use existsi instead of use or vice versa?

[Julian Berman]

Ah, use's docstring says things...

[Julian Berman]

OK I don't know the practical implications of Unlike existsi, x is elaborated with respect to the expected type. but I guess I can learn "always use use from that" probably?