## 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 ≠ ♔ :=
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 (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: May 16 2021 at 20:13 UTC