simp only on numeric goals

Stream: lean4

[Heather Macbeth]

Is the following discrepancy in the behaviour of simp only known?

example : (1:Nat) = 0 := by
  simp only -- goal `False`

example : (1:Int) = 0 := by
  simp only -- "simp made no progress"

example : (-1:Int) = 0 := by
  simp only -- goal `False`

I'm curious about why. (Is this a similar issue to lean4#1994?)

Personally I think the "simp made no progress" is better, because this preserves consistency with the behaviour on non-special-cased types, such as

import Mathlib

example : (1:ℝ) = 0 := by
  simp only -- "simp made no progress"

[Eric Wieser]

I think the pattern here is that it works when the outer constructors are different

[Eric Wieser]

example : (2:Nat) = 1 := by
  simp only

fails too

[Eric Wieser]

In your examples, the constructors are respectively succ,zero (ok), ofNat,ofNat (fail), and negSucc,ofNat (ok)

[Heather Macbeth]

That seems plausible, indeed:

inductive foo
  | left (b : Bool) : foo
  | right (b : Bool) : foo

export foo (left right)

example : left true = right true := by
  simp only -- goal `False`

example : left true = left false := by
  simp only -- "simp made no progress"

[Heather Macbeth]

Would someone on the FRO comment on whether they would consider getting rid of this feature? Perhaps it could be made a simp-proc, rather than baked into simp only.

[Kyle Miller]

I just found where it's defined: docs#Lean.Meta.Simp.simpCtorEq (it does exactly what Eric inferred, which is "replace equalities between different constructors with False")

[Heather Macbeth]

The issue I see with the current behaviour is that various flavours of simp occur all over the place inside other tactics, so if there's no way to avoid this behaviour, it makes those tactics unpredictable too. Here's the example where I noticed this, from simp occurring as a cleanup after failure in Mathlib's ring:

import Mathlib

example (x : ℤ) : x + 1 - x = 0 := by ring
/-
error: unsolved goals
⊢ 1 = 0
-/

example (x : ℤ) : x - 1 - x = 0 := by ring
/-
error: unsolved goals
⊢ False
-/

[Heather Macbeth]

The first case is actually much more informative -- simp has done less cleanup, so the user gets better information back from the tactic about what went wrong in ring.

[Kyle Miller]

I don't think I can comment at the moment on whether or not to include this feature — maybe it's worth creating a Lean issue explaining why this leads to unpredictability? and why it affects teaching goals?

[Heather Macbeth]

Sure, although I don't think it's a teaching issue so much as a general user issue.

[Heather Macbeth]

Is the above explanation sufficient or is there something else I should address?

[Kyle Miller]

It seems reasonable making it be a user simproc, but there might be a reason it is where it is.

I'm also wondering whether this builtin simproc should be upgraded to be stronger than it is (in particular, be able to reason about injectivity of constructors completely, so for example be able to reduce left x = left y to x = y automatically), though it might lead to some bad behavior with Nat...

[Kyle Miller]

Heather Macbeth said:

Is the above explanation sufficient or is there something else I should address?

This isn't a part of Lean that I work on, so I'm not sure what we would want to see, but I think it would be good creating an issue just to log that it's surprising that simp sees natural number literals as being constructor expressions in this context. The impact on automation like ring can help with the story too.

[Heather Macbeth]

Thanks!

[Kyle Miller]

Something suspect about this simproc is that when it figures out the constructors, it puts both sides of the expression into WHNF. For example, this triggers an error in the WHNF algorithm, despite simp being configured to do essentially nothing:

example : 2^10000 = 2^9999 := by
  simp (config := Lean.Meta.Simp.neutralConfig) only
/-
exponent 10000 exceeds the threshold 256, exponentiation operation was not evaluated,
use `set_option exponentiation.threshold <num>` to set a new threshold
-/

[Heather Macbeth]

Sorry, I don't follow -- what is Lean.Meta.Simp.neutralConfig? Is it the default, or if not then what does it turn off?

[Kyle Miller]

neutralConfig sets every simp config option that's got to do with some sort of simplification to false

[Heather Macbeth]

The behaviour you noted still occurs when you just write

example : 2^10000 = 2^9999 := by
  simp only

so I assume you were just including Lean.Meta.Simp.neutralConfig to be careful?

[Kyle Miller]

Yeah, I wanted to be sure none of the standard reductions did it

[Heather Macbeth]

@Kyle Miller The simproc simpCtorEq turns up twice in
https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/Rewrite.lean
1) in docs#Lean.Meta.Simp.postSEval and 2) in docs#Lean.Meta.Simp.postDefault. Do you know which of these two lists of simprocs is the one which controls what simp only does?

[Kyle Miller]

postDefault is for simp only and postSEval is for simp (config := { ground := true }) only (this is a special mode for symbolically evaluating ground terms)

[Heather Macbeth]

RFC at lean4#5046