simp_all removing a hypothesis before it can be used

Stream: metaprogramming / tactics

[Geoffrey Irving]

Here is an example which I'd hope simp_all could resolve, but which does not work:

import Mathlib

lemma simp_all_test (f : ℕ → Bool) (t i : ℕ) (s : t < 64) : f (i + t % 64) = f (i + t) := by
  have h : t < 64 → t % 64 = t := fun h ↦ by rw [Nat.mod_eq_of_lt h]
  -- simp only [s, true_implies] at h; simp only [h]  -- Works, as the conclusion of h stays
  -- simp at h  -- Changes h to True due to Nat.mod_succ_eq_iff_lt
  simp_all  -- h disappears, so can't be used to simplify the goal
  sorry  -- I wish we didn't get here

Ideally simp_all would use s to simplify h to t % 64 = t, then use that to simplify and thus close the goal. But unfortunately there is a simp lemma Nat.mod_succ_eq_iff_lt which causes simp at h to turn h into True, rather than into a useful hypothesis.

Is there a convenient way to get around this?

(This is a minimized version of https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Forward.20chaining.20with.20.60aesop.60/near/405526750.)

[Geoffrey Irving]

Possibly everything is working fine except that Nat.mod_succ_eq_iff_lt is a weird lemma to be marked as simp?

[Eric Rodriguez]

docs#Nat.mod_succ_eq_iff_lt

[Geoffrey Irving]

attribute [-simp] Nat.mod_succ_eq_iff_lt does fix it.

[Yaël Dillies]

Why not just simp [Nat.mod_eq_of_lt, *]?

[Geoffrey Irving]

Because actually what I did originally was call aesop, and one of my useful hypotheses disappeared along the way. I'm trying to do either aesop or call split_ifs and get ~10 different branches that can each be closed with simp_all.

That is, this is a minimization of the aesop thread at https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Forward.20chaining.20with.20.60aesop.60/near/405526750.

[Yaël Dillies]

Then I would hope that your useful hypothesis was not that useful and that instead you were missing a simp lemma (or another lemma should be simp).

[Geoffrey Irving]

Well, in this case the useful hypothesis is an application of Nat.mod_eq_of_lt, as in the MWE. But as far as I know I can't mark that as simp, because it has a hypothesis. What would be the fix I should apply then?

[Yaël Dillies]

Nonono, simp does handle lemmas with preconditions!

[Geoffrey Irving]

Ah, that's useful to know! Should Nat.mod_eq_of_lt be simp?

[Yaël Dillies]

I think it's sensible, but there might surprises.

[Jannis Limperg]

Sorry, I had forgotten about this thread (or rather, the original Aesop thread). As a workaround, you can erase the simp lemma from Aesop's simp calls as well:

import Mathlib.Data.Nat.Basic
import Aesop

lemma simp_all_test (f : ℕ → Bool) (t i : ℕ) (s : t < 64) : f (i + t % 64) = f (i + t) := by
  have h : t < 64 → t % 64 = t := fun h ↦ by rw [Nat.mod_eq_of_lt h]
  aesop (erase simp Nat.mod_succ_eq_iff_lt)

[Geoffrey Irving]

In this case adding Nat.mod_eq_of_lt is better as Yael points out, and I’ll do that at file-level for now.