Zulip Chat Archive

Stream: new members

Topic: Advice on Definitions


view this post on Zulip Julian Berman (Aug 28 2020 at 19:26):

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").

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:35):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:36):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 19:37):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:38):

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.

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:39):

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.

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:39):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:40):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 19:41):

(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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:42):

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.

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:42):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:43):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:43):

And that no two pieces can occupy the same spot.

view this post on Zulip Julian Berman (Aug 28 2020 at 19:46):

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?

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:53):

Just writing up a quick example.

view this post on Zulip Julian Berman (Aug 28 2020 at 19:54):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 19:59):

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)

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:00):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:00):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:01):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:03):

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.

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:04):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:04):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 20:05):

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)

view this post on Zulip Julian Berman (Aug 28 2020 at 20:07):

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?

view this post on Zulip Julian Berman (Aug 28 2020 at 20:07):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:10):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 20:10):

a ha, got it

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:10):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:10):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:12):

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.

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:13):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 20:13):

Makes sense.

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:13):

Which was instrumental for me to understand how Lean works.

view this post on Zulip Julian Berman (Aug 28 2020 at 20:13):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 20:13):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 20:14):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:16):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:17):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 20:18):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:29):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:29):

Which is also a fintype

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:29):

But then statements about columns or rows get clunkier

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:30):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:30):

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

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:33):

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.

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:34):

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.

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:34):

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

view this post on Zulip Julian Berman (Aug 28 2020 at 20:37):

hm, as in order the set of pieces arbitrarily?

view this post on Zulip Yakov Pechersky (Aug 28 2020 at 20:42):

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.

view this post on Zulip Julian Berman (Aug 28 2020 at 21:00):

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 :)

view this post on Zulip Julian Berman (Sep 03 2020 at 12:52):

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)"?

view this post on Zulip Julian Berman (Sep 03 2020 at 12:56):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 13:21):

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

view this post on Zulip Reid Barton (Sep 03 2020 at 13:31):

For the last question I think you can use fin_cases h

view this post on Zulip Reid Barton (Sep 03 2020 at 13:31):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 13:53):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 13:58):

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.

view this post on Zulip Julian Berman (Sep 03 2020 at 14:02):

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?)

view this post on Zulip Yakov Pechersky (Sep 03 2020 at 14:34):

Zulip is that fancy tactic.

view this post on Zulip Yakov Pechersky (Sep 03 2020 at 14:34):

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

view this post on Zulip Yakov Pechersky (Sep 03 2020 at 14:35):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 14:53):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 14:54):

(trying the subsingleton thing now too)

view this post on Zulip Yakov Pechersky (Sep 03 2020 at 14:57):

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

view this post on Zulip Yakov Pechersky (Sep 03 2020 at 15:08):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 15:35):

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?

view this post on Zulip Reid Barton (Sep 03 2020 at 15:36):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 15:37):

A ha. OK.

view this post on Zulip Reid Barton (Sep 03 2020 at 15:40):

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

view this post on Zulip Reid Barton (Sep 03 2020 at 15:40):

or more likely, accidentally use 0 as a type

view this post on Zulip Julian Berman (Sep 03 2020 at 22:18):

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 ?

view this post on Zulip Julian Berman (Sep 03 2020 at 22:19):

(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?)

view this post on Zulip Julian Berman (Sep 03 2020 at 22:20):

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

view this post on Zulip Scott Morrison (Sep 03 2020 at 22:24):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 22:31):

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?

view this post on Zulip Julian Berman (Sep 03 2020 at 22:33):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 22:52):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 22:52):

and yes it does suggest dec_trivial, thanks!

view this post on Zulip Scott Morrison (Sep 03 2020 at 22:58):

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

view this post on Zulip Scott Morrison (Sep 03 2020 at 22:58):

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

view this post on Zulip Julian Berman (Sep 03 2020 at 23:00):

All good -- and understood :)

view this post on Zulip Julian Berman (Sep 08 2020 at 13:13):

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]

view this post on Zulip Julian Berman (Sep 08 2020 at 13:14):

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

view this post on Zulip Anne Baanen (Sep 08 2020 at 13:25):

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.

view this post on Zulip Julian Berman (Sep 08 2020 at 13:34):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:34):

(fuller example incoming...)

view this post on Zulip Julian Berman (Sep 08 2020 at 13:37):

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

view this post on Zulip Anne Baanen (Sep 08 2020 at 13:42):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:43):

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  

view this post on Zulip Julian Berman (Sep 08 2020 at 13:45):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:45):

er sorry definition of width

view this post on Zulip Kenny Lau (Sep 08 2020 at 13:46):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:47):

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

view this post on Zulip Reid Barton (Sep 08 2020 at 13:48):

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

view this post on Zulip Anne Baanen (Sep 08 2020 at 13:48):

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.

view this post on Zulip Reid Barton (Sep 08 2020 at 13:48):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:49):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:51):

how should I understand that syntax for variables?

view this post on Zulip Julian Berman (Sep 08 2020 at 13:51):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:51):

and not in the function declaration?

view this post on Zulip Johan Commelin (Sep 08 2020 at 13:52):

to avoid repetition

view this post on Zulip Julian Berman (Sep 08 2020 at 13:53):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 13:53):

Only if it needs it

view this post on Zulip Julian Berman (Sep 08 2020 at 13:53):

aha ok

view this post on Zulip Anne Baanen (Sep 08 2020 at 13:55):

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.

view this post on Zulip Julian Berman (Sep 08 2020 at 13:57):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:58):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 13:58):

but that obviously didn't work either

view this post on Zulip Julian Berman (Sep 08 2020 at 14:01):

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

view this post on Zulip Reid Barton (Sep 08 2020 at 14:04):

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.

view this post on Zulip Julian Berman (Sep 08 2020 at 14:05):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:05):

which I thought would mean m was implicitly an argument

view this post on Zulip Julian Berman (Sep 08 2020 at 14:05):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:06):

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

view this post on Zulip Reid Barton (Sep 08 2020 at 14:07):

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

view this post on Zulip Reid Barton (Sep 08 2020 at 14:07):

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.

view this post on Zulip Johan Commelin (Sep 08 2020 at 14:08):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:08):

aha... ok

view this post on Zulip Reid Barton (Sep 08 2020 at 14:08):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:09):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:09):

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

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:13):

no, they can be any fintype

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:15):

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

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:15):

so Lean doesn't know that it should use m

view this post on Zulip Julian Berman (Sep 08 2020 at 14:29):

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

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:29):

I might as well have written:

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:30):

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

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:30):

yes

view this post on Zulip Julian Berman (Sep 08 2020 at 14:31):

(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?

view this post on Zulip Julian Berman (Sep 08 2020 at 14:32):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:32):

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

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:32):

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

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:33):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:33):

and there's no deferred mechanism there too right?

view this post on Zulip Julian Berman (Sep 08 2020 at 14:33):

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"

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:35):

I don't understand what you mean

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:36):

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

view this post on Zulip Kenny Lau (Sep 08 2020 at 14:36):

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

view this post on Zulip Julian Berman (Sep 08 2020 at 14:37):

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)

view this post on Zulip Julian Berman (Sep 08 2020 at 14:37):

thanks for indulging the question

view this post on Zulip Julian Berman (Sep 14 2020 at 17:01):

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)

view this post on Zulip Julian Berman (Sep 14 2020 at 17:02):

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)

view this post on Zulip Julian Berman (Sep 14 2020 at 17:07):

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?

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 17:07):

true

view this post on Zulip Julian Berman (Sep 14 2020 at 17:08):

Ah of course.

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 17:11):

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

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 17:11):

Whether or not the end pos is occupied

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 17:11):

And doesn't care about board dimensions etc

view this post on Zulip Julian Berman (Sep 14 2020 at 17:11):

and then that def would match on the piece?

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 17:12):

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.

view this post on Zulip Julian Berman (Sep 14 2020 at 17:13):

makes sense

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 17:13):

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

view this post on Zulip Julian Berman (Sep 14 2020 at 17:13):

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

view this post on Zulip Julian Berman (Sep 14 2020 at 17:14):

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

view this post on Zulip Julian Berman (Sep 14 2020 at 17:14):

will give that a shot.

view this post on Zulip Julian Berman (Sep 14 2020 at 17:16):

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

view this post on Zulip Johan Commelin (Sep 14 2020 at 17:17):

function.curry and function.uncurry

view this post on Zulip Julian Berman (Sep 14 2020 at 17:17):

aha, thanks!

view this post on Zulip Julian Berman (Sep 14 2020 at 17:17):

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

view this post on Zulip Johan Commelin (Sep 14 2020 at 17:18):

Seriously, that is an extremely important strategy.

view this post on Zulip Johan Commelin (Sep 14 2020 at 17:19):

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

view this post on Zulip Johan Commelin (Sep 14 2020 at 17:20):

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

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 17:21):

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.

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 17:22):

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.

view this post on Zulip Johan Commelin (Sep 14 2020 at 17:22):

Maybe dec_trivial can prove that?

view this post on Zulip Julian Berman (Sep 14 2020 at 17:23):

I was hoping dec_trivial would do magic again yeah

view this post on Zulip Julian Berman (Sep 14 2020 at 17:24):

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

view this post on Zulip Julian Berman (Sep 14 2020 at 17:26):

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"

view this post on Zulip Julian Berman (Sep 14 2020 at 17:29):

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

view this post on Zulip Yakov Pechersky (Sep 14 2020 at 17:53):

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

view this post on Zulip Julian Berman (Sep 14 2020 at 18:00):

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

view this post on Zulip Julian Berman (Sep 14 2020 at 18:02):

Or more math.

view this post on Zulip Julian Berman (Sep 14 2020 at 18:02):

or both, oy.

view this post on Zulip Scott Morrison (Sep 14 2020 at 22:14):

@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).

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 22:23):

There's an abandoned dots and boxes branch??

view this post on Zulip Julian Berman (Sep 14 2020 at 22:32):

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

view this post on Zulip Julian Berman (Sep 14 2020 at 22:33):

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

view this post on Zulip Scott Morrison (Sep 14 2020 at 22:38):

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.

view this post on Zulip Scott Morrison (Sep 14 2020 at 22:40):

(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.)

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 22:41):

I don't think you can do it like that

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 22:41):

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.

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 22:42):

I remember thinking hard about this a decade or so ago

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 22:42):

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

view this post on Zulip Scott Morrison (Sep 14 2020 at 22:42):

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.

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 22:43):

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.

view this post on Zulip Scott Morrison (Sep 14 2020 at 22:43):

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) :=

view this post on Zulip Julian Berman (Sep 15 2020 at 16:53):

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

view this post on Zulip Julian Berman (Sep 15 2020 at 16:54):

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

view this post on Zulip Julian Berman (Sep 15 2020 at 16:55):

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

view this post on Zulip Julian Berman (Sep 15 2020 at 16:55):

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

view this post on Zulip Julian Berman (Sep 15 2020 at 16:56):

it does, cool, so scratch the above

view this post on Zulip Julian Berman (Sep 15 2020 at 16:59):

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

view this post on Zulip Julian Berman (Sep 15 2020 at 16:59):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 15 2020 at 17:00):

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

view this post on Zulip Julian Berman (Sep 15 2020 at 17:01):

Ah, cool, thanks!

view this post on Zulip Julian Berman (Sep 15 2020 at 17:19):

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.

view this post on Zulip Kevin Buzzard (Sep 15 2020 at 17:40):

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.

view this post on Zulip Yakov Pechersky (Sep 15 2020 at 17:44):

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

view this post on Zulip Julian Berman (Sep 15 2020 at 17:49):

(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?

view this post on Zulip Julian Berman (Sep 15 2020 at 17:50):

Ah, use's docstring says things...

view this post on Zulip Julian Berman (Sep 15 2020 at 17:51):

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?


Last updated: May 08 2021 at 10:12 UTC