## Stream: new members

### Topic: Negating a Prop without lambdas

#### Yakov Pechersky (Nov 05 2020 at 03:55):

Is there a short notation for the following:

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


#### Mario Carneiro (Nov 05 2020 at 04:04):

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


#### 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),
⊢ decidable_pred not


#### 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


#### 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


#### 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


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

#### Yakov Pechersky (Nov 05 2020 at 19:28):

But that's not exactly the same thing.

#### Yakov Pechersky (Nov 05 2020 at 19:28):

This fails:

#check (show decidable_pred not, by apply_instance)


#### Reid Barton (Nov 05 2020 at 19:36):

And there can't be such an instance

#### 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!

#### 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

#### Reid Barton (Nov 05 2020 at 19:39):

You'd want a reducible version of ∘.

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

#### Yakov Pechersky (Nov 05 2020 at 19:41):

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

#### 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

#### 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

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


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


#### Reid Barton (Nov 05 2020 at 19:57):

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

#### 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

#### Reid Barton (Nov 05 2020 at 19:59):

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

#### 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

#### Mario Carneiro (Nov 05 2020 at 20:08):

what's the context of the goal?

#### 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

#### 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


#### 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.

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

#### 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.

#### Mario Carneiro (Nov 05 2020 at 20:26):

what is the type of v?

#### Mario Carneiro (Nov 05 2020 at 20:27):

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

#### 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

#### 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

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

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

#### 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.

#### 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.

#### 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

#### Mario Carneiro (Nov 05 2020 at 21:41):

Still a bit hard to give pointed advice without a mwe

#### 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

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

#### 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


#### 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  #### 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. #### Yakov Pechersky (Nov 05 2020 at 22:19): Happy to hear any suggestions and to be set on a right path. #### 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? #### 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 #### Yakov Pechersky (Nov 05 2020 at 22:33): The general context is the following project: https://github.com/Julian/lean-across-the-board #### 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. #### 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 #### 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? #### 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 #### 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? #### 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. #### 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 #### 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⟩  #### Kevin Lacker (Nov 05 2020 at 22:42): so dont try to make a bunch of lemmas like vector.filter_some_pred #### 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)] ], }  #### Kevin Lacker (Nov 05 2020 at 22:42): make lemmas about chess boards #### Kevin Lacker (Nov 05 2020 at 22:42): yeah if you read like PGN or ASCII format it'll be much nicer #### 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. #### 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)  #### Yakov Pechersky (Nov 05 2020 at 22:45): Specifically, that convert respects and satisfies the contains and injects constraints. #### 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. #### 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 #### 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*)  #### 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. #### 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 #### 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 #### 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 #### Kevin Lacker (Nov 05 2020 at 23:39): i'm saying, at least, it would be smoother to use lists there #### 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. #### 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) #### Julian Berman (Nov 05 2020 at 23:44): But unlike normal chess we do I think want/need to track "identity" of pieces globally #### 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? #### 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 #### 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? #### 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" #### Julian Berman (Nov 05 2020 at 23:48): i.e. both of them need to cover every square once (and cannot capture each other) #### Kevin Lacker (Nov 05 2020 at 23:49): is the existence just supposed to follow from the existence of a single tour #### 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 #### 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 #### Kevin Lacker (Nov 05 2020 at 23:51): or is there some mathy principle for how you'd prove the existence #### 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" #### Julian Berman (Nov 05 2020 at 23:51): but yeah there are mathy principles for proving existence #### 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 #### 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 #### 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 #### Julian Berman (Nov 05 2020 at 23:53): nod #### Mario Carneiro (Nov 06 2020 at 00:05): What if you just had def starting_position : chess.board _ _ _ _ := ![ ![♞, __, ♞], ![__, __, __], ![♘, __, ♘] ]  ? #### 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 #### Yakov Pechersky (Nov 06 2020 at 00:11): Because in a chess game, the piece behind an index can change (pawn upgrades). #### Mario Carneiro (Nov 06 2020 at 00:12): if the pieces are on the board, you just change what is stored at that position #### 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  #### 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  #### Yakov Pechersky (Nov 06 2020 at 00:18): Of course, that's not relevant if one throws indexing out of the window. #### Mario Carneiro (Nov 06 2020 at 00:18): algebraic chess notation doesn't index pieces by number #### 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  #### 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  #### 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 #### Mario Carneiro (Nov 06 2020 at 05:44): nat.dist is abs (x - y) defined on nats #### Mario Carneiro (Nov 06 2020 at 05:44): it makes it easy to define the knights move requirement #### 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 #### Mario Carneiro (Nov 06 2020 at 05:45): guardb is the same thing but for bools #### 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 #### 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 #### 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.) #### 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 #### Bryan Gin-ge Chen (Nov 06 2020 at 07:53): l : list (option colored_pieces) and a : option colored_pieces. #### 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 #### Yakov Pechersky (Nov 06 2020 at 08:03): def to_list : option α → list α | none := [] | (some a) := [a]  from mathlib #### 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  #### 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)))


#### 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.

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

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

#### 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.

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

#### Eric Wieser (Nov 06 2020 at 08:22):

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

#### Bryan Gin-ge Chen (Nov 06 2020 at 08:23):

Yeah, that's true.

#### 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

#### 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: Dec 20 2023 at 11:08 UTC