Simplify match-with

Stream: new members

[Bjørn Kjos-Hanssen]

What's a good tactic for resolving a match-with expression like

(match (motive := Fin 4 → ℕ) 1 with
  | { val := 0, isLt := (_ : 0 % 4 < 4) } => 4
  | { val := 1, isLt := (_ : 1 % 4 < 4) } => 7
  | { val := 2, isLt := (_ : 2 % 4 < 4) } => 3
  | { val := 3, isLt := (_ : 3 % 4 < 4) } => 2)

?
I know I can state separately that:

have  : (match (motive := Fin 4 → ℕ) 1 with
  | { val := 0, isLt := (_ : 0 % 4 < 4) } => 4
  | { val := 1, isLt := (_ : 1 % 4 < 4) } => 7
  | { val := 2, isLt := (_ : 2 % 4 < 4) } => 3
  | { val := 3, isLt := (_ : 3 % 4 < 4) } => 2)
    = 7 := rfl

and then do rw [this].
But if the match-with appears as a part of a larger statement (as it always does) I am not sure what to do that is not tedious.

[Kyle Miller]

I'd expect dsimp only to be able to reduce it

[Bjørn Kjos-Hanssen]

Specifically, in this example:

example (a b : ℕ)  : (match (motive := Fin 4 → ℕ) 1 with
  | { val := 0, isLt := (_ : 0 % 4 < 4) } => 4
  | { val := 1, isLt := (_ : 1 % 4 < 4) } => a
  | { val := 2, isLt := (_ : 2 % 4 < 4) } => b
  | { val := 3, isLt := (_ : 3 % 4 < 4) } => 2)
    ≠
    (match (motive := Fin 4 → ℕ) 2 with
  | { val := 0, isLt := (_ : 0 % 4 < 4) } => 4
  | { val := 1, isLt := (_ : 1 % 4 < 4) } => a
  | { val := 2, isLt := (_ : 2 % 4 < 4) } => b
  | { val := 3, isLt := (_ : 3 % 4 < 4) } => 2) :=
sorry

is there a tactic that reduces the problem to a ≠ b?

[Kyle Miller]

dsimp only seems to work

[Bjørn Kjos-Hanssen]

I get dsimp made no progress.

[Kyle Miller]

I'm not sure if something changed in Lean. Here's my version:

#eval Lean.versionString
-- "4.6.0-rc1"

[Bjørn Kjos-Hanssen]

Here's an online version, with the same Lean version as you.

[Johan Commelin]

show a \ne b works, but that's not ideal in general

[Bjørn Kjos-Hanssen]

Thanks, the show idea helps a lot. But yeah, in general don't want to spend time figuring out what it is you want to show.

[Damiano Testa]

I was not able to the the No progress output, but I did find different outputs, with Mathlib's being sub-optimal:

import Mathlib

-- replaced `ℕ` with `Nat` to get it to work with no imports
example (a b : Nat)  : (match (motive := Fin 4 → Nat) 1 with
  | { val := 0, isLt := (_ : 0 % 4 < 4) } => 4
  | { val := 1, isLt := (_ : 1 % 4 < 4) } => a
  | { val := 2, isLt := (_ : 2 % 4 < 4) } => b
  | { val := 3, isLt := (_ : 3 % 4 < 4) } => 2)
    ≠
    (match (motive := Fin 4 → Nat) 2 with
  | { val := 0, isLt := (_ : 0 % 4 < 4) } => 4
  | { val := 1, isLt := (_ : 1 % 4 < 4) } => a
  | { val := 2, isLt := (_ : 2 % 4 < 4) } => b
  | { val := 3, isLt := (_ : 3 % 4 < 4) } => 2) := by
  dsimp
-- with no imports
-- ⊢ ¬a = b

-- with `import Mathlib`
-- ⊢ ¬(match 1 with
--     | { val := 0, isLt := isLt } => 4
--     | { val := 1, isLt := isLt } => a
--     | { val := 2, isLt := isLt } => b
--     | { val := 3, isLt := isLt } => 2) =
--     match 2 with
--     | { val := 0, isLt := isLt } => 4
--     | { val := 1, isLt := isLt } => a
--     | { val := 2, isLt := isLt } => b
--     | { val := 3, isLt := isLt } => 2

[Arthur Adjedj]

You could "manually" reduce the two sides of the equality using conv and whnf as such:

example (a b : ℕ)  : (match (motive := Fin 4 → ℕ) 1 with
  | { val := 0, isLt := (_ : 0 % 4 < 4) } => 4
  | { val := 1, isLt := (_ : 1 % 4 < 4) } => a
  | { val := 2, isLt := (_ : 2 % 4 < 4) } => b
  | { val := 3, isLt := (_ : 3 % 4 < 4) } => 2)
    ≠
    (match (motive := Fin 4 → ℕ) 2 with
  | { val := 0, isLt := (_ : 0 % 4 < 4) } => 4
  | { val := 1, isLt := (_ : 1 % 4 < 4) } => a
  | { val := 2, isLt := (_ : 2 % 4 < 4) } => b
  | { val := 3, isLt := (_ : 3 % 4 < 4) } => 2) :=
  by
    conv => lhs
            whnf
    conv => rhs
            whnf
 -- ⊢ a ≠ b

[Kyle Miller]

It appears to be import Mathlib.Data.Fin.Basic that provides an instance that can't be reduced.

[Kyle Miller]

It must be from that module, since if you only import that module's imports, then dsimp only works again.

Here are its imports:

import Mathlib.Algebra.NeZero
import Mathlib.Init.Data.Fin.Basic
import Mathlib.Order.RelIso.Basic
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Order.Hom.Set
import Std.Data.Fin.Basic

[Kyle Miller]

attribute [-instance] Fin.instOfNatFin causes it to elaborate in a reducible way. In my earlier tests I was on a slightly older mathlib with the same toolchain, so something somewhere seems to have changed in the meantime. This particular instance doesn't seem to have changed in awhile though, so I'm not sure.