Simplifying inductive type inequalities

Stream: new members

[Yakov Pechersky]

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 ≠ ♔ :=
begin
  intro h,
  simp at h, -- doesn't simp to false
  have : ♔.piece = king := rfl,
  simp [this] at h, -- now it works
  exact h
end

[Yakov Pechersky]

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

[Eric Wieser]

Does tagging the structure with ext help?

[Eric Wieser]

pattern does nothing in that example.

[Eric Wieser]

Using reducible in its place might

[Yakov Pechersky]

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

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

[Yakov Pechersky]

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]

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]

simp [white_king] at h, works

[Mario Carneiro]

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

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

That works too. Thanks!