Zulip Chat Archive

Stream: new members

Topic: Negating a Prop without lambdas


view this post on Zulip Yakov Pechersky (Nov 05 2020 at 03:55):

Is there a short notation for the following:

example {α : Type*} (p : α  Prop) : α  Prop := λ x, ¬ p x

view this post on Zulip Mario Carneiro (Nov 05 2020 at 04:04):

example {α : Type*} : (α  Prop)  α  Prop := () not

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 05:12):

Cool. But not ∘ p when p is decidable_pred is not decidable_pred?

failed to synthesize type class instance for
α : Type u_1,
p : α  Prop,
_inst_1 : decidable_pred p,
n : ,
hn :  (v : vector α n), ( (i : fin n), ¬p (v.nth i))  v.filter_count (not  p) = n,
v : vector α n.succ,
h :  (i : fin n.succ), ¬p (v.nth i),
this : ¬p v.head
 decidable_pred not

view this post on Zulip Chris B (Nov 05 2020 at 19:14):

I think there's just a missing instance in mathlib maybe? Something like:

instance decidable_not_of_decidable_pred {A : Sort*} (p : A -> Prop) [inst1: decidable_pred p] : decidable_pred (λ x, not (p x))
| x := if h1 : p x then is_false (absurd h1) else is_true h1

view this post on Zulip Chris B (Nov 05 2020 at 19:21):

Actually the composition one is a little nicer to look at.

instance decidable_not_of_decidable_pred
  {A : Sort*} (p : A -> Prop) [inst1: decidable_pred p] : decidable_pred (not  p)
| x := if h1 : p x then is_false (absurd h1) else is_true h1

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 19:23):

I think my not finding it was due to a congr that went too deep. Because this is in core:

  instance [decidable p] : decidable (¬p) :=
  if hp : p then is_false (absurd hp) else is_true hp

view this post on Zulip Reid Barton (Nov 05 2020 at 19:23):

Judging from docs#list.partition_eq_filter_filter it seems like such an instance must already exist, no?

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 19:28):

But that's not exactly the same thing.

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 19:28):

This fails:

#check (show decidable_pred not, by apply_instance)

view this post on Zulip Reid Barton (Nov 05 2020 at 19:36):

And there can't be such an instance

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 19:37):

Right. So again, congr'd too deep. This is all in the context of trying to define partition like things on vectors. Thanks for the pointer to that list partition lemma!

view this post on Zulip Reid Barton (Nov 05 2020 at 19:38):

Lean tends to not really like you writing not ∘ p for λ x, ¬ p x because of reasons like this

view this post on Zulip Reid Barton (Nov 05 2020 at 19:39):

You'd want a reducible version of .

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 19:40):

Relatedly, is there a partition-like sum type that splits a type into a sum of two subtypes, each predicated on the two cases of a proposition?

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 19:41):

Yeah, the friction of Lean with some pointfree style gets in the way sometimes

view this post on Zulip Reid Barton (Nov 05 2020 at 19:46):

It's better to not stir up trouble and stick to the simple λ x, ¬ p x, IMO

view this post on Zulip Mario Carneiro (Nov 05 2020 at 19:47):

Yeah, sorry for misleading with the first response. I don't recommend using pointfree style in lean because it doesn't work well with higher order type classes

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 19:56):

Does that mean things like this should also be avoided?

prod.map ((+) 1) id  (prod.map prod.fst id)

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 19:56):

In the context of

prod.map prod.fst (@id α)  (prod.map ((+) (1, 0)) id) = prod.map ((+) 1) id  (prod.map prod.fst id)

view this post on Zulip Reid Barton (Nov 05 2020 at 19:57):

This is \lam p, (1 + p.1.1, p.2)?

view this post on Zulip Reid Barton (Nov 05 2020 at 19:58):

I'd say there is certainly no advantage to the pointfree version... even ignoring it being unnecessarily higher-order

view this post on Zulip Reid Barton (Nov 05 2020 at 19:59):

Hopefully, it took me just three tries to understand what it meant

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 20:01):

I'm trying to show that one can rearrange these operations on a vector of pairs -- I guess I should probably simplify my definitions

view this post on Zulip Mario Carneiro (Nov 05 2020 at 20:08):

what's the context of the goal?

view this post on Zulip Reid Barton (Nov 05 2020 at 20:10):

I was assuming you wrote that expression... if it arose in a proof then it's not necessarily bad, but these prod.map and must have come from somewhere

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 20:10):

At this point, I've probably fixed the code enough that I don't remember where this was coming up. But I am proving (not putting in all of the auxiliary definitions):

lemma map_filter_enum_prop_eq_enum_from_filter' {m : } (h : v.filter_count p = m) :
  ((v.enum_prop' p).filter (λ xpair, p xpair.snd)
    (by rw [filter_count_of_map_snd_enum_prop', h])).map (prod.map prod.fst id) =
  (v.filter p h).enum_from' 1 := sorry

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 20:12):

The broader goal is to provide an enumerate definition for vectors, which enumerates the p x and not (p x) separately.

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 20:13):

And at the end of the day, indexes them not by nat but by fin m where m is the total number of p x in the vector (of size n).

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 20:14):

Sorry for confusion -- the explanations about pointfree or not was helpful! I think I'm good to go.

view this post on Zulip Mario Carneiro (Nov 05 2020 at 20:26):

what is the type of v?

view this post on Zulip Mario Carneiro (Nov 05 2020 at 20:27):

that rw in the middle of the statement doesn't look great

view this post on Zulip Mario Carneiro (Nov 05 2020 at 20:29):

It sounds like what you are doing could be most easily accomplished by converting the vector to a list and then using list.filter or perhaps list.partition

view this post on Zulip Mario Carneiro (Nov 05 2020 at 20:32):

to get that final indexing, you can use list.nth_le on the resulting list, after a propositional proof that the length of the list is whatever your target value is

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 20:42):

So perform all the manipulations on the list level, while carrying around proofs that the length isn't changed? Isn't that exactly what the vector type represents? I think you're saying that, yes, that is what vector represents, but it is not worth it to "avoid the underlying list". While I have been trying to try to remain in the vector API (as I build it up). Did I understand correctly?

view this post on Zulip Kevin Lacker (Nov 05 2020 at 20:56):

I don't even understand how that statement is valid Lean code... you can use a by rw inside the statement of a lemma that you're trying to prove?

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 21:14):

Why not? by is a way to enter tactic mode when in term mode. It creates a weird eq.rec term, but that shouldn't matter, because proof irrelevance means a proof that has eq.rec on it is still equal to one that doesn't. I had to use by rw in that instance because my current definitions have implicit variables where I probably should not have them. So, a simple filter_count_of_map_snd_enum_prop' ▸ h or whatever it would be doesn't work because of uninferred metavariables. But rw is able to discharge them.

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 21:17):

The reason I have that propositional term here anyway is that my definition of vector.filter requires a hypothesis that proves that the number of items that match the condition that you're filtering on is m: (h : v.filter_count p = m). This makes it easier to make proofs by operations on that m. I guess I could encode it implicitly, then have to do something like a

set m : \N := v.filter_count p with h,
...

inside all my proofs.

view this post on Zulip Mario Carneiro (Nov 05 2020 at 21:40):

while carrying around proofs that the length isn't changed?

Not carrying around the proof, inserting the proof once at the end

view this post on Zulip Mario Carneiro (Nov 05 2020 at 21:41):

Still a bit hard to give pointed advice without a mwe

view this post on Zulip Mario Carneiro (Nov 05 2020 at 21:43):

I think that vector.filter, if it is to exist at all, is forced to have essentially the type you have said, but I would want to #xy the problem a bit more and look at the reason you want this function

view this post on Zulip Mario Carneiro (Nov 05 2020 at 21:46):

However, the fact that you need a special function just to describe the length of the resulting filter, and assert equality to m, suggests that you aren't really gaining anything over a plain list.filter (which you can always force into a vector A m using the constructor, which takes a hypothesis (list.filter v p).length = m)

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:16):

The goal is to make this sorry free and legible:

example : collect_pieces
       ![![, __, ],
         ![__, __, __],
         ![, __, ]] (by sorry) = ![, , , ] := sorry

example : @number_pieces 3 3 4
       ![![, __, ],
         ![__, __, __],
         ![, __, ]] (by sorry) =
       ![![0, __, 1],
         ![__, __, __],
         ![2, __, 3]] := sorry

example {k : } (b : matrix (fin n) (fin m) (option colored_pieces)) (h : b.count_some = k) :
  (number_pieces b h).map (option.map (collect_pieces b h)) = b := sorry

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:16):

Here's a stub file with a lot of missing definitions and lemmas:

import data.matrix.notation

@[derive decidable_eq]
inductive color
| white
| black

@[derive decidable_eq]
inductive pieces
| knight

@[derive decidable_eq]
structure colored_pieces :=
(piece : pieces)
(color : color)

@[pattern] def white_knight : colored_pieces := pieces.knight, color.white
@[pattern] def black_knight : colored_pieces := pieces.knight, color.black

notation `  ` := white_knight
notation `  ` := black_knight
notation `__` := none

variables {α : Type*} {n m : }

def matrix.ravel (M : matrix (fin n) (fin m) α) : fin (n * m)  α := sorry

variables (p : α  Prop) [decidable_pred p]

def vector.filter_count (v : vector α n) := (v.to_list.filter p).length

def vector.filter (v : vector α n) (h : v.filter_count p = m) : vector α m :=
v.to_list.filter p, h

def vector.count_some (v : vector (option α) n) :  := v.filter_count (λ x, option.is_some x)

def vector.filter_some (v : vector (option α) n) (hm : v.count_some = m) : vector (option α) m :=
v.filter (λ x, option.is_some x) hm

lemma vector.filter_valid (v : vector α n) (hm : v.filter_count p = m) :  i, p ((v.filter p hm).nth i) :=
sorry

lemma vector.filter_some_pred (v : vector (option α) n) (hm : v.count_some = m) :
   i, ((v.filter_some hm).nth i).is_some :=
vector.filter_valid _ _ hm

def vector.reduce_some (v : vector (option α) n) (hm : v.count_some = m) : vector α m :=
vector.of_fn (λ i, option.get ((v.filter_some_pred hm) i))

def matrix.count_some (M : matrix (fin n) (fin m) (option α)) :  :=
vector.count_some (vector.of_fn M.ravel)

def collect_pieces {k : } (b : matrix (fin n) (fin m) (option colored_pieces))
  (h : b.count_some = k) : fin k  colored_pieces :=
vector.nth (vector.reduce_some (vector.of_fn b.ravel) h)

def number_pieces {k : } (b : matrix (fin n) (fin m) (option colored_pieces))
  (h : b.count_some = k) : matrix (fin n) (fin m) (option (fin k)) :=
sorry

instance : has_zero (option (fin (n + 1))) := some 0
instance : has_one (option (fin (n + 2))) := some 1
instance : has_add (option (fin n)) := λ x y, (+) <$> x <*> y

example : collect_pieces
       ![![, __, ],
         ![__, __, __],
         ![, __, ]] (by sorry) = ![, , , ] := sorry

example : @number_pieces 3 3 4
       ![![, __, ],
         ![__, __, __],
         ![, __, ]] (by sorry) =
       ![![0, __, 1],
         ![__, __, __],
         ![2, __, 3]] := sorry

example {k : } (b : matrix (fin n) (fin m) (option colored_pieces)) (h : b.count_some = k) :
  (number_pieces b h).map (option.map (collect_pieces b h)) = b := sorry

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:18):

For this exact problem, I could have just written all the filter stuff specialized to option, like list.reduce_option already is. But at some point, I'll need to filter on other predicates, like what piece it is, so that I can number pieces of different types.

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:19):

Happy to hear any suggestions and to be set on a right path.

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:32):

can you describe what is the overall problem you are trying to solve, like why do you want to number pieces?

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:33):

for this specific problem it seems like having a matrix is pretty inconvenient, maybe you could just turn it into a list and prove things there

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:33):

The general context is the following project: https://github.com/Julian/lean-across-the-board

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:34):

The pieces have to be numbered because one moves around pieces based on the piece identity, but tracks their positions based on index.

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:35):

does one do that? typically in chess you specify moves like Ng1-f3, you dont store an identity for a single knight across the whole game

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:35):

For example, if you wanted to model castling, would you assign the two different rooks different piece types? How would you keep track of which was the king's-side and which was the queen's-side rook to keep track of whether it has moved before castling?

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:36):

you just keep track of two boolean values, is k-side castling and q-side castling still allowed

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:39):

I think it's a matter of notation. If I started from a board with

![, , , ] @
![![0 , __, 1 ],
  ![__, __, __],
  ![2 , __, 3 ]]

and said that I made a move to end at

![, , , ] @
![![__, __, 1 ],
  ![__, __, __],
  ![3 , 0 , 2 ]]

should that be counted at legal?

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:40):

basically I recommend having some meta structure chess_board sort of class, and sticking a bunch of variables in there whenever it helps you. you probably want to keep the whole game history around in the data structure. then you can implement lots of lemmas on top of it.

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:40):

you don't really want to have to do things like extend the vector class to do different sorts of filtering

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:40):

Which we've done so far, without meta:

def starting_position : chess.board _ _ _ _ := {
  pieces := ![, , , ],
  contents := PF ![
    ![(0 : fin 4), __, (1 : fin 4)],
    ![    __,      __,       __   ],
    ![(2 : fin 4), __, (3 : fin 4)]
  ],
}


def ending_position : chess.board _ _ _ _ := {
  starting_position with
  pieces := ![, , , ],
}

-- Direct solution

def guarini_seq : chess.move.sequence.legal :=
{ start_board := starting_position,
  elements := ![
  ((2, 0), (0, 1)),
  ((2, 2), (1, 0)),
  ((0, 1), (2, 2)),
  ((0, 2), (2, 1)),
  ((0, 0), (1, 2)),
  ((1, 2), (2, 0)),
  ((2, 0), (0, 1)),
  ((2, 1), (0, 0)),
  ((0, 0), (1, 2)),
  ((1, 0), (0, 2)),
  ((0, 2), (2, 1)),
  ((2, 2), (1, 0)),
  ((1, 0), (0, 2)),
  ((0, 1), (2, 2)),
  ((2, 1), (0, 0)),
  ((1, 2), (2, 0))] }

def first_move : chess.move starting_position :=
let pair := guarini_seq.elements 0 in pair.fst, pair.snd, dec_trivial, dec_trivial

example : guarini_seq.to_sequence.boards 0  guarini_seq.start_board := dec_trivial

example : guarini_seq.to_sequence.boards 1  first_move.perform_move := dec_trivial

example :  ix, (guarini_seq.elements ix).fst  (guarini_seq.elements ix).snd := dec_trivial

lemma guarini : starting_position.has_sequence_to ending_position :=
_, guarini_seq.to_sequence, dec_trivial

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:42):

so dont try to make a bunch of lemmas like vector.filter_some_pred

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:42):

And that compiles currently without sorries. However, it's annoying to have to say:

def starting_position : chess.board _ _ _ _ := {
  pieces := ![, , , ],
  contents := PF ![
    ![(0 : fin 4), __, (1 : fin 4)],
    ![    __,      __,       __   ],
    ![(2 : fin 4), __, (3 : fin 4)]
  ],
}

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:42):

make lemmas about chess boards

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:42):

yeah if you read like PGN or ASCII format it'll be much nicer

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:43):

And it's be nice to just say:

def starting_position : chess.board _ _ _ _ := convert ![
    ![, __, ],
    ![__, __, __],
    ![, __, ]
  ]

and have the pieces and contents correct.

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:45):

But then there'll need to be lemmas making sure that convert always generates a pieces and contents that matches the defition of the board structure:

structure board :=
-- The pieces the board holds, provided as an indexed vector
(pieces : ι  K)
-- The playfield on which the pieces are placed
(contents : playfield m n ι)
-- All the pieces in `pieces` are on the `contents`
-- See "Implementation details" for info about `dec_trivial`
(contains : function.surjective contents.index_at . tactic.exact_dec_trivial)
-- Different positions hold different indices
(injects : contents.some_injective . tactic.exact_dec_trivial)

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:45):

Specifically, that convert respects and satisfies the contains and injects constraints.

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:45):

And so I ended up (over?)generalizing the vector filtering operations, instead of just working on the specific case of the chess board.

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:46):

ok. I guess overall I would just try using lists instead of vectors. you might want to make the size of the chess board part of the top level structure - it seems pretty important

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 22:46):

Sorry, I didn't include:

-- The dimensions of the board, finite and decidably equal
variables (m n : Type*) [fintype n] [decidable_eq n] [fintype m] [decidable_eq m]
-- The index associated to pieces on a playfield
variables (ι : Type*) [fintype ι] [decidable_eq ι]
-- The piece type
variables (K : Type*)

view this post on Zulip Kevin Lacker (Nov 05 2020 at 22:47):

i just mean lists for helper functions like "list all the knights on the board". if you don't know the length of the output, just make it a list rather than a vector. then i think you will avoid a lot of this painful typing.

view this post on Zulip Julian Berman (Nov 05 2020 at 23:37):

I think we're a step before that really. Like Yakov said, we're trying to make constructing boards simpler

view this post on Zulip Julian Berman (Nov 05 2020 at 23:38):

Parsing ASCII boards was my original idea, but I think that'd be fairly painful in Lean, from what I saw there's not very many implemented string manipulation methods

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:39):

i mean, this sample code is building 10 or so helper functions over vectors in order to construct a chessboard

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:39):

i'm saying, at least, it would be smoother to use lists there

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:41):

how I would represent chess positions for input is as a string like:

rnbqkbnr
pppppppp
........
........
........
........
PPPPPPPP
RNBQKBNR

you should be able to do that without any string functions except converting to a list of chars.

view this post on Zulip Julian Berman (Nov 05 2020 at 23:43):

I have to think more personally. But it's not obvious to me that that makes the "collect the knights" problem easier, it sounds like you're saying it is (and I admit I'm not fully following the conversation about vectors other than "there's a bunch more stuff implemented on list that isn't implemented on vectors", so it could just be I don't understand enough to have an opinion)

view this post on Zulip Julian Berman (Nov 05 2020 at 23:44):

But unlike normal chess we do I think want/need to track "identity" of pieces globally

view this post on Zulip Julian Berman (Nov 05 2020 at 23:44):

Because if I want to prove like 2 knights making simultaneous knights tours on a board it seems likely it's easier to do that if you remember which knight it was the whole time?

view this post on Zulip Julian Berman (Nov 05 2020 at 23:45):

But maybe my intuition is wrong there too and you'll say you can do it just as easy with just the sequences of moving numbers I don't know too hard to think before dinner

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:47):

what are you proving about two simultaneous knights tours on a board? you're giving it a tour and you want to prove that it's a tour? or you want it to automatically find one?

view this post on Zulip Julian Berman (Nov 05 2020 at 23:48):

sorry I left out words, but I meant "given a board and two knights on it, the existence (or non-existence) of a tour of both knights on it"

view this post on Zulip Julian Berman (Nov 05 2020 at 23:48):

i.e. both of them need to cover every square once (and cannot capture each other)

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:49):

is the existence just supposed to follow from the existence of a single tour

view this post on Zulip Julian Berman (Nov 05 2020 at 23:49):

no because in the general case (some number of pieces, some configuration) you can fill up squares you need to make progress

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:50):

do you want lean to like, analyze a specific position to see if there's a tour, via some search algorithm

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:51):

or is there some mathy principle for how you'd prove the existence

view this post on Zulip Julian Berman (Nov 05 2020 at 23:51):

so firstly all of this is purely for fun :) so I don't know what I personally want to do other than "prove stuff that's fun"

view this post on Zulip Julian Berman (Nov 05 2020 at 23:51):

but yeah there are mathy principles for proving existence

view this post on Zulip Julian Berman (Nov 05 2020 at 23:51):

you do coloring proofs (parity proofs) in simple cases where you show nonexistence because squares of various colors would be visited an impossible number of times

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:52):

ok. well, i dont really understand what sort of thing you're trying to do, but I am fairly sure that you don't want to be implementing vector.filter_some as part of a plan to read in chess boards from an ascii representation as part of it

view this post on Zulip Kevin Lacker (Nov 05 2020 at 23:53):

use a list when a function is returning things that might be of different lengths, it'll be easier

view this post on Zulip Julian Berman (Nov 05 2020 at 23:53):

nod

view this post on Zulip Mario Carneiro (Nov 06 2020 at 00:05):

What if you just had

def starting_position : chess.board _ _ _ _ := ![
    ![, __, ],
    ![__, __, __],
    ![, __, ]
  ]

?

view this post on Zulip Mario Carneiro (Nov 06 2020 at 00:06):

Which is to say, why bother with the pieces if you are already storing all the info in the contents

view this post on Zulip Yakov Pechersky (Nov 06 2020 at 00:11):

Because in a chess game, the piece behind an index can change (pawn upgrades).

view this post on Zulip Mario Carneiro (Nov 06 2020 at 00:12):

if the pieces are on the board, you just change what is stored at that position

view this post on Zulip Mario Carneiro (Nov 06 2020 at 00:13):

evidence that this is easier with lists:

def collect_pieces (b : list (list (option colored_pieces))) :
  list colored_pieces :=
do l  b, a  l, a.to_list

example : collect_pieces
        [[, __, ],
         [__, __, __],
         [, __, ]] = [, , , ] := rfl

view this post on Zulip Yakov Pechersky (Nov 06 2020 at 00:18):

Yeah, I have a working collect_pieces that I didn't upload above. I think I started down this path because I foresaw proving (or even expressing) that accessing by number into the collected pieces is the same as what you started with.

example {k : } (b : matrix (fin n) (fin m) (option colored_pieces)) (h : b.count_some = k) :
  (number_pieces b h).map (option.map (collect_pieces b h)) = b := sorry

view this post on Zulip Yakov Pechersky (Nov 06 2020 at 00:18):

Of course, that's not relevant if one throws indexing out of the window.

view this post on Zulip Mario Carneiro (Nov 06 2020 at 00:18):

algebraic chess notation doesn't index pieces by number

view this post on Zulip Mario Carneiro (Nov 06 2020 at 00:33):

inductive move
| knight (a b :  × )

def position := list (list (option colored_pieces))

def position.get :  ×   position  option colored_pieces
| (x, y) p := do l  p.nth y, b  l.nth x, b
def position.set :  ×   option colored_pieces  position  position
| (x, y) c p := p.modify_nth (λ l, l.update_nth x c) y

def move.eval : color  move  position  position
| c (move.knight a b) p :=
  (p.set a none).set b (some pieces.knight, c⟩)

def move.valid : color  move  position  bool
| c (move.knight (x₁, y₁) (x₂, y₂)) p :=
  (let a := x₁.dist x₂, b := y₁.dist y₂ in
   a = 1  b = 2  a = 2  b = 1) 
  p.get (x₁, y₁) = some pieces.knight, c

def move.apply (c : color) (m : move) (p : position) : option position :=
guardb (m.valid c p) >> some (m.eval c p)

example : (move.knight (0,0) (1,2)).apply color.black
        [[, __, ],
         [__, __, __],
         [, __, ]] =
   some [[__, __, ],
         [__, __, __],
         [, , ]] := rfl

view this post on Zulip Mario Carneiro (Nov 06 2020 at 01:13):

Here's an implementation of the guarini knight exchange problem:

import data.nat.dist

@[derive decidable_eq]
inductive color
| white
| black

@[derive decidable_eq]
inductive pieces
| knight

@[derive decidable_eq]
structure colored_pieces :=
(piece : pieces)
(color : color)

@[pattern] def white_knight : colored_pieces := pieces.knight, color.white
@[pattern] def black_knight : colored_pieces := pieces.knight, color.black

notation `  ` := white_knight
notation `  ` := black_knight
notation `__` := none

def colored_pieces.to_string : colored_pieces  string
| pieces.knight, color.white := "♘"
| pieces.knight, color.black := "♞"

instance : has_to_string colored_pieces := colored_pieces.to_string

def position := list (list (option colored_pieces))

def position.get :  ×   position  option (option colored_pieces)
| (x, y) p := do l  p.nth y, l.nth x
def position.set :  ×   option colored_pieces  position  position
| (x, y) c p := p.modify_nth (λ l, l.update_nth x c) y

def is_knight_move :  ×    ×   bool
| (x₁, y₁) (x₂, y₂) :=
  let a := x₁.dist x₂, b := y₁.dist y₂ in
  a = 1  b = 2  a = 2  b = 1

instance : has_repr position := λ c, c.to_string

def position.apply : ( × ) × ( × )  position  option position
| (a, b) p := do
  guardb (is_knight_move a b),
  pieces.knight, c  mjoin (p.get a),
  guard (p.get b = some none),
  some ((p.set a none).set b (some pieces.knight, c⟩))

def position.apply_seq (l : list (( × ) × ( × )))
  (p : position) : option position := l.mfoldl (λ p l, p.apply l) p

def starting_position : position :=
[[, __, ],
 [__, __, __],
 [, __, ]]

def ending_position : position :=
[[, __, ],
 [__, __, __],
 [, __, ]]

-- Direct solution

def guarini_seq := [
  ((2, 0), (0, 1)),
  ((2, 2), (1, 0)),
  ((0, 1), (2, 2)),
  ((0, 2), (2, 1)),
  ((0, 0), (1, 2)),
  ((1, 2), (2, 0)),
  ((2, 0), (0, 1)),
  ((2, 1), (0, 0)),
  ((0, 0), (1, 2)),
  ((1, 0), (0, 2)),
  ((0, 2), (2, 1)),
  ((2, 2), (1, 0)),
  ((1, 0), (0, 2)),
  ((0, 1), (2, 2)),
  ((2, 1), (0, 0)),
  ((1, 2), (2, 0))]

lemma guarini :
  position.apply_seq guarini_seq starting_position =
  some ending_position := rfl

view this post on Zulip Julian Berman (Nov 06 2020 at 02:48):

Wow, thanks, that looks way way simpler than what I ended up with. I don't know what dist or the guards do but will do some reading and then see if I can poke a bit more. Thanks this is great

view this post on Zulip Mario Carneiro (Nov 06 2020 at 05:44):

nat.dist is abs (x - y) defined on nats

view this post on Zulip Mario Carneiro (Nov 06 2020 at 05:44):

it makes it easy to define the knights move requirement

view this post on Zulip Mario Carneiro (Nov 06 2020 at 05:45):

guard is a function defined on option by guard p = if p then some () else none, which is useful to assert predicates inside the option monad

view this post on Zulip Mario Carneiro (Nov 06 2020 at 05:45):

guardb is the same thing but for bools

view this post on Zulip Mario Carneiro (Nov 06 2020 at 05:46):

By writing the function this way it is easy for lean to compute with, and you can still prove properties about the function if you want a more abstract representation

view this post on Zulip Mario Carneiro (Nov 06 2020 at 05:48):

for instance, you could prove that position.apply always returns a n × n board if the input is n × n, and similarly for other structural properties like the number of knights of each color on the board

view this post on Zulip Mario Carneiro (Nov 06 2020 at 05:51):

(By the way, when I implemented this at first I had a turn counter, that would track the current color to play, and enforced that you only move a piece of your color. I dropped this because the guarini sequence does not respect turn order, and I don't know if it's part of the original problem statement.)

view this post on Zulip Kevin Lacker (Nov 06 2020 at 07:33):

starting to get off topic, but this code confused me:

def collect_pieces (b : list (list (option colored_pieces))) :
  list colored_pieces :=
do l  b, a  l, a.to_list

So those left-arrows are de-monadizing the list and option monads? or both list monads? I don't get how that works. like what type are a and l

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 07:53):

l : list (option colored_pieces) and a : option colored_pieces.

view this post on Zulip Kevin Lacker (Nov 06 2020 at 07:58):

and then a.to_list converts an option colored_pieces to a list colored_pieces? is there some implicit monadic cast sort of thing going on here

view this post on Zulip Yakov Pechersky (Nov 06 2020 at 08:03):

def to_list : option α  list α
| none     := []
| (some a) := [a]

from mathlib

view this post on Zulip Yakov Pechersky (Nov 06 2020 at 08:12):

Compare to

def collect_pieces' (b : list (list (option colored_pieces))) :
  list (list colored_pieces) :=
b.map (λ l, do a  l, a.to_list)

example : collect_pieces'
        [[, __, ],
         [__, __, __],
         [, __, ]] =
        [[, ],
         [],
         [, ]] := rfl

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 08:13):

The do notation desugars to the following, (recalling that bind l f in the list monad is list.join (l.map f):

def collect_pieces_desugared (b : list (list (option colored_pieces))) :
  list colored_pieces :=
list.join (b.map (λ l, list.join (l.map $ λ a, a.to_list)))

view this post on Zulip Yakov Pechersky (Nov 06 2020 at 08:14):

Right, that's why my example looks like that, it's the map but without the join.

view this post on Zulip Yakov Pechersky (Nov 06 2020 at 08:15):

Are there portions of mathlib that make definitions and state/prove lemmas using do notation on the term level?

view this post on Zulip Yakov Pechersky (Nov 06 2020 at 08:16):

I understand that the tactic sequence is operating in the tactic "monad", but I mean some mathematical statements phrased in do or other monadic bind chains?

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 08:20):

The only thing that comes to mind at the moment is some list definitions stated with do notation in data.list.defs.

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 08:22):

Oh, there's also presumably a bunch of stuff in control, but just like list, I don't know whether these count as "mathematical".

view this post on Zulip Eric Wieser (Nov 06 2020 at 08:22):

Even those list defs seem to be the lemmas about other monads

view this post on Zulip Bryan Gin-ge Chen (Nov 06 2020 at 08:23):

Yeah, that's true.

view this post on Zulip Eric Wieser (Nov 06 2020 at 09:16):

My guess is that lemmas aren't stated that way because a proof about list.bind is easier to apply than a proof about @has_bind.bind list

view this post on Zulip Mario Carneiro (Nov 06 2020 at 15:27):

The turing machine stuff has a lot of proofs about things in the roption monad written in do notation


Last updated: May 15 2021 at 02:11 UTC