Zulip Chat Archive

Stream: new members

Topic: Simplifying inductive type inequalities

Yakov Pechersky (Dec 23 2020 at 00:30):

What is missing in my lemmas or simp set such that this inequality in an inductive type is not simplifying to false?

import tactic.derive_fintype

@[derive [decidable_eq, fintype]]
inductive color
| white
| black

@[derive [decidable_eq, fintype]]
inductive piece
| king
| queen

@[derive [decidable_eq, fintype]]
structure colored_piece :=
(piece : piece)
(color : color)

instance : has_coe colored_piece piece := colored_piece.piece

@[simp] protected lemma piece.coe {p : colored_piece} : (p : piece) = p.piece := rfl

@[pattern] def white_king : colored_piece := piece.king, color.white

open piece

notation `  ` := white_king

example : queen   :=
  intro h,
  simp at h, -- doesn't simp to false
  have : ♔.piece = king := rfl,
  simp [this] at h, -- now it works
  exact h

Yakov Pechersky (Dec 23 2020 at 00:32):

I can't tag colored_piece with simps either, it complains that it is not a structure?

Eric Wieser (Dec 23 2020 at 00:33):

Does tagging the structure with ext help?

Eric Wieser (Dec 23 2020 at 00:34):

pattern does nothing in that example.

Eric Wieser (Dec 23 2020 at 00:35):

Using reducible in its place might

Yakov Pechersky (Dec 23 2020 at 00:36):

The pattern is to make something else work, namely something like:

def piece_repr : colored_piece  string
|  := "♔"
| _ := "just an example"

Yakov Pechersky (Dec 23 2020 at 00:38):

Tagging with ext won't help because any lemmas will be about the equality of colored_piece, but here my hypothesis is an equality of pieces.

Alex J. Best (Dec 23 2020 at 00:39):

example : queen  ♔.

works :smile:, see https://leanprover.zulipchat.com/#narrow/stream/240192-Berkeley-Lean.20Seminar/topic/Periods.20at.20the.20end.20of.20statements/near/202467782 and other topics about empty pattern match proofs

Mario Carneiro (Dec 23 2020 at 00:40):

simp [white_king] at h, works

Mario Carneiro (Dec 23 2020 at 00:41):

you can tag white_king as simp but that will unfold it everywhere so probably not what you want

Yakov Pechersky (Dec 23 2020 at 00:41):

Thanks! I have such an equality in the middle of a big proposition term, so simplifying it would make the whole thing false -- couldn't rely on just empty pattern matches

Mario Carneiro (Dec 23 2020 at 00:42):

tagging white_king as simps also works and makes a bit more sense

Yakov Pechersky (Dec 23 2020 at 00:43):

That works too. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC