simp? giving nonsense lemmas

Stream: mathlib4

[Bhavik Mehta]

I think this has been around for a while but I haven't seen any progress on it and I can't find it in issues. What's the status of simp? giving lemmas which are entirely irrelevant? Is this something that's being actively worked on, or is it just an accepted known regression?

[Scott Morrison]

Could you make an issue with some examples?

[Scott Morrison]

(It's surely neither actively worked on, nor an accepted known regression, if it doesn't have an issue. :-)

[Bhavik Mehta]

Sure, I just wanted to check that no-one else knew about an issue first! Searching simp? seemed pretty useless :P

[David Renshaw]

At this point I've just sort of gotten accustomed to manually deleting stuff from the output of simp?.

[Bhavik Mehta]

Yeah I'm the same, but I decided today that I probably shouldn't be finding this acceptable!

[Bhavik Mehta]

Tangential question - what's the trace option to turn on to get simp to tell me which rewrites are occurring and where? edit: found it, it was trace.Meta.Tactic.simp.rewrite

[Bhavik Mehta]

Here's one example, simplified a bunch but not yet mathlib-free:

import Mathlib.Data.Int.Cast.Lemmas

lemma square_eq (x y : ℤ) : max x.natAbs y.natAbs = max |x| |y| := by
  simp?

[Bhavik Mehta]

It seems that simp is applying ge_iff_le to an expression which is an le - ge_iff_le and gt_iff_lt are the ones I experience most like this (a syntactic change that's definitionally rfl) but I'll check others too

[Kyle Miller]

I've frequently experienced those lemmas appearing in simp? too

[Eric Rodriguez]

I was just going to make an issue for this!

[Scott Morrison]

I just moved ge_iff_le to Std, so hopefully that makes it easier to make a #mwe!

[Eric Rodriguez]

Bhavik Mehta said:

It seems that simp is applying ge_iff_le to an expression which is an le - ge_iff_le and gt_iff_lt are the ones I experience most like this (a syntactic change that's definitionally rfl) but I'll check others too

My theory is that it comes from some of the metadata that's attached to exprs in lean4 - how can we see this?

[Scott Morrison]

You need to get hold of the actual Expr and print / process the raw representation.

[Scott Morrison]

import Lean
import Qq

open Lean Meta Qq

def foo := Expr.mdata .empty q(Int)

#reduce foo -- Expr.mdata { entries := [] } (Expr.const `Int [])
#eval show MetaM _ from do ppExpr foo -- Int

[Eric Rodriguez]

here's some minimisation:

import Std.Tactic.SimpTrace

-- this import is important: commenting it out fixes the issue (in this specific case)
import Mathlib.Data.Nat.Order.Basic
-- as it imports only:
import Mathlib.Algebra.Order.Ring.Canonical
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Bits

example {n : Nat} : n = 2 - (n + 1) := by
  simp?
  sorry

still working on it!

[Eric Rodriguez]

Here's a Std-only repro, as minimal as I can get it without downloading Std (which I am doing right now)

import Std.Tactic.SimpTrace
import Std.Classes.Order -- this import is minimal

universe u
-- this is important!
--variable {α : Type} [LE α] [Sub α] [OfNat α 0] {a b c d : α} -- doesn't have the issue!

variable {α : Type u} [LE α] [Sub α] [OfNat α 0] {a b c d : α}

@[simp]
theorem tsub_eq_zero_of_le : a ≤ b → a - b = 0 := by sorry

example {n : Nat} : n = 2 - (n + 1) := by
  simp? [Nat.succ_sub_succ_eq_sub]
  sorry

I'm going to keep trying to minimise, I think I'm pretty close. Note the really surprising thing is that somehow this is a universe issue!

[Eric Rodriguez]

it seems simp? is reporting on lemmas that it is trying and then giving up on, though

[Eric Rodriguez]

import Std.Tactic.SimpTrace

universe u
-- this is important! {α : Type} works as expected, as does making all these lemmas for `Nat`.
variable {α : Type u} [LE α] [Sub α] [OfNat α 0] {a b c d x y : α}

@[simp]
theorem tsub_eq_zero_of_le : a ≤ b → a - b = 0 := by sorry

@[simp]
theorem ge_iff_le : x ≥ y ↔ y ≤ x := Iff.rfl

example {n : Nat} : n = 2 - (n + 1) := by
  simp? [Nat.succ_sub_succ_eq_sub]
  sorry

it just needed ge_iff_le, d'oh. here's a minimal one @Scott Morrison :)

[Scott Morrison]

@Eric Rodriguez, here is is without Std:

universe u

-- {α : Type} works as expected, as does making this lemma for `Nat`.
@[simp]
theorem tsub_eq_zero_of_le {α : Type u} [LE α] [Sub α] [OfNat α 0] {a b : α} :
    a ≤ b → a - b = 0 := by sorry

@[simp]
theorem ge_iff_le (x y : Nat) : x ≥ y ↔ y ≤ x := Iff.rfl

set_option tactic.simp.trace true

example {n : Nat} : n = 2 - (n + 1) := by
  simp [Nat.succ_sub_succ_eq_sub] -- Try this: simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub]
  sorry

[Scott Morrison]

Turning on set_option trace.Meta.Tactic.simp true, it looks like lemmas that it is successfully rewriting by during failed discharging attempts are being recorded in the output.

[Scott Morrison]

Hopefully that's the clue. :-)

[Scott Morrison]

Oh, I bet the MonadBacktrack instance for SimpM is wrong.

[Scott Morrison]

Yay, have a fix along these lines.

[Scott Morrison]

I'm not entirely certain how much state I should be backtracking when the discharger fails.

[Scott Morrison]

So I'm not sure whether I should make the minimal fix, that just backtracks UsedSimps, or if it's okay to backtrack the whole MetaM state too.

[Scott Morrison]

We can sort that out in review.

[Scott Morrison]

@Eric Rodriguez, would you mind posting an issue with that last #mwe, and I'll clean up the fix?

[Eric Rodriguez]

In the lean4 repo, or std?

[Scott Morrison]

Lean

[Scott Morrison]

The fix is at lean4#2923

[Patrick Massot]

It would be nice to use the opportunity to work on getting simp? closer to optionally output a simp_rw.

[Scott Morrison]

I'm thinking about it... it's pretty tricky, because the lemmas returned by UsedTheorems are currently a big bag of lemmas used for rewriting, discharging, and congruence. Working out how to thread through a replayable history of what simp does is a tall order.

[Scott Morrison]

I'm still more in optimistic about the "take the big bag, and shake it into the right order using a search heuristic" approach...

[Bhavik Mehta]

Scott Morrison said:

I'm thinking about it... it's pretty tricky, because the lemmas returned by UsedTheorems are currently a big bag of lemmas used for rewriting, discharging, and congruence. Working out how to thread through a replayable history of what simp does is a tall order.

There's a good chance I'm misunderstanding the complexities of what's going on here, but it seems like the obvious solution is for UsedTheorems to return a tree, so the lemmas used to solve side goals from a rewrite A would be all contained in a subtree of A. Then if it turns out we don't want to keep A, we can throw away the whole subtree and know safely that this doesn't affect any other rewrites

[Eric Rodriguez]

I'm still befuddled as to where the universe comes into it all.