'simp'lifying 'match' expressions

Stream: lean4

[Michael Stoll]

Consider

import Mathlib.Data.ZMod.Defs

def foo (a : ZMod 4) : Nat :=
  match a with
  | 0 | 2 => 37
  | 1 => 389
  | 3 => 5077

example : ∃ n : Nat, foo 2 = n := by
  simp only [foo]
  /- ⊢ ∃ n,
  (match 2 with
    | 0 => 37
    | 2 => 37
    | 1 => 389
    | 3 => 5077) =
    n
  -/
  sorry

How can I get the (match 2 with ...) simplified to 37? (They are defeq, so change ∃ n,37 = n would work, but I'd like to get this automatically.)

Note:

• Replacing foo 2 by foo 0 or foo 1 works (i.e., simp only [foo] resolves the match).
• Replacing ZMod 4 by Fin 4 in the definition of foo also works.
• dsimp does not work.

Of course, one could add simp lemmas lemma foo_two : foo 2 = 37 := rfl etc., but when 4 is a bit larger, that gets tedious...

[Michael Stoll]

Any ideas?

[Damiano Testa]

On the webserver, simp only [foo, exists_eq'] works: is this not suitable?

[Damiano Testa]

Or do you want simp to stop before closing the goal?

[Michael Stoll]

This is cheating and an artifact of the MWE :smile:
Maybe this is better:

import Mathlib.Data.ZMod.Defs

def foo (a : ZMod 4) : Nat :=
  match a with
  | 0 | 2 => 37
  | 1 => 389
  | 3 => 5077

example : foo 2 = 95 := by
  simp [foo]
  sorry

The point is that simp does not resolve the match (when the argument is at least 2).

[Damiano Testa]

example [Nat.AtLeastTwo 2] : foo 2 = 95 := by
  simp [foo]

?

EDIT: this looked correct, but it was probably due to some cached state.

[Michael Stoll]

This still doesn't resolve the match.

[Adam Topaz]

Does split split the match?

[Michael Stoll]

example : foo 2 = 95 := by
  simp [foo]
  split
  all_goals try tauto
  sorry

works, but seems a bit clumsy. ( split leaves four goals.)

[Adam Topaz]

Yeah I agree. What if you tag foo with simp?

[Damiano Testa]

split is also what aesop uses.

[Michael Stoll]

Adam Topaz said:

Yeah I agree. What if you tag foo with simp?

That does not seem to change anything (except that I don't have to give foo explicitly to simp).

[Michael Stoll]

I would say resolving match expressions may look like something a simproc could do.

In any case, I find it a bit strange that simp only [foo] does work when foo is defined as Fin 4 → Nat.

[Shreyas Srinivas]

I know why. ZMod is a def

[Shreyas Srinivas]

See this. I just redefined ZMod as it is in mathlib except it is now reducible:

import Mathlib.Data.ZMod.Defs

namespace Play
abbrev ZMod : ℕ → Type
  | 0 => ℤ
  | n + 1 => Fin (n + 1)
abbrev foo (a : ZMod 4) : Nat :=
  match a with
  | 0 | 2 => 37
  | 1 => 389
  | 3 => 5077

example : ∃ n : Nat, foo 2 = n := by
  simp only [foo]
  done
  /- ⊢ ∃ n,37 =n
  -/


end Play

[Michael Stoll]

But simp [foo, ZMod] does not work either...

[Adam Topaz]

Does it work if you use Fin instead of Zmod?

[Michael Stoll]

Yes, as already mentioned.

[Adam Topaz]

Sorry, I’m on mobile so I missed it

[Adam Topaz]

You can also use change foo (a : Fin _) = _ before the simp and it should (hopefully!) work

[Shreyas Srinivas]

simp has no occurrences of ZMod to rewrite I suppose

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

That was not the case. Once the def of foo was unfolded, even if you had changed 2's type to Fin, it gets rewritten as ZMod.

[Matthew Ballard]

Add

instance ZMod.instOfNat: ∀ n m : ℕ, OfNat (ZMod n) m
  | 0, m => inferInstanceAs (OfNat ℤ m)
  | n + 1, m => inferInstanceAs (OfNat (Fin (n + 1)) m)

to L105 of file#Data/ZMod/Defs

[Michael Stoll]

OK, let me make a PR...

[Matthew Ballard]

I didn't check the resulting diamond though

[Michael Stoll]

I'll see how it goes.

[Michael Stoll]

This runs into problems:

import Mathlib.Data.ZMod.Defs

instance ZMod.instOfNat (n m : ℕ) [Nat.AtLeastTwo m] : OfNat (ZMod n) m := inferInstance

shows that there is (of course) another OfNat instance on ZMod n, and having both makes (perhaps among other problems) ring/ring_nf stop working on ZMod n. (And of course it violates the principle that instances should be "morally unique".) But this other instance (which comes from docs#instOfNatAtLeastTwo) does not help with reducing the match.

[Eric Wieser]

Matthew Ballard said:

Add

instance ZMod.instOfNat: ∀ n m : ℕ, OfNat (ZMod n) m
  | 0, m => inferInstanceAs (OfNat ℤ m)
  | n + 1, m => inferInstanceAs (OfNat (Fin (n + 1)) m)

to L105 of file#Data/ZMod/Defs

m should not be part of the match here

[Kevin Buzzard]

0 should map to 11, right?