Negating a Prop without lambdas

Stream: new members

[Yakov Pechersky]

Is there a short notation for the following:

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

[Mario Carneiro]

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

[Yakov Pechersky]

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

[Chris B]

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]

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]

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]

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

[Yakov Pechersky]

But that's not exactly the same thing.

[Yakov Pechersky]

This fails:

#check (show decidable_pred not, by apply_instance)

[Reid Barton]

And there can't be such an instance

[Yakov Pechersky]

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]

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

[Reid Barton]

You'd want a reducible version of ∘.

[Yakov Pechersky]

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]

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

[Reid Barton]

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

[Mario Carneiro]

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]

Does that mean things like this should also be avoided?

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

[Yakov Pechersky]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Yakov Pechersky]

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]

what's the context of the goal?

[Reid Barton]

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]

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]

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

[Yakov Pechersky]

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]

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

[Mario Carneiro]

what is the type of v?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

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

[Mario Carneiro]

Still a bit hard to give pointed advice without a mwe

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Kevin Lacker]

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

[Kevin Lacker]

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]

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

[Yakov Pechersky]

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]

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]

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]

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

[Yakov Pechersky]

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]

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]

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

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

make lemmas about chess boards

[Kevin Lacker]

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

[Yakov Pechersky]

And it's be nice to just say:

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

and have the pieces and contents correct.

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

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]

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]

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]

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

[Julian Berman]

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]

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

[Kevin Lacker]

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

[Kevin Lacker]

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]

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]

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

[Julian Berman]

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]

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]

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]

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]

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

[Kevin Lacker]

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

[Julian Berman]

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

[Kevin Lacker]

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

[Kevin Lacker]

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

[Julian Berman]

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]

but yeah there are mathy principles for proving existence

[Julian Berman]

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]

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]

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

[Julian Berman]

nod

[Mario Carneiro]

What if you just had

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

?

[Mario Carneiro]

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

[Yakov Pechersky]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

algebraic chess notation doesn't index pieces by number

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

it makes it easy to define the knights move requirement

[Mario Carneiro]

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]

guardb is the same thing but for bools

[Mario Carneiro]

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]

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]

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

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]

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

[Kevin Lacker]

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]

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

from mathlib

[Yakov Pechersky]

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]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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]

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]

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

[Bryan Gin-ge Chen]

Yeah, that's true.

[Eric Wieser]

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]

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