RFC: remove simpCtorEq from the default simprocs

[hrmacbeth]

Proposal

Currently simp only simplifies an equality a = b to False, if a and b are different constructors for an inductive type. This is apparently done by the Meta.Simp.simpCtorEq simproc.

Would it be possible to turn off this simproc in simp only, while still keeping it in the set of rules used by simp? Here are three arguments in favour of this change:

1. This simproc can cause unpredictable behaviour. For example,

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`

The simpCtorEq simproc is applicable to the first and last of these goals but not to the middle one.

2. This simproc can cause inefficient behaviour. For example (from @kmill):

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
-/

3. There are use cases where unambiguously this simproc is undesirable, so it's awkward to have it baked into simp only, where it is (AFAICT) impossible to turn off. For example, the simp tactic is used internally in the Mathlib ring tactic to clean up failures before they are presented to the user. This simproc actually cleans up some failures too aggressively, so that the information to the user is lost!

import Mathlib

-- simproc does not act, user gets useful error message
example (x : ℤ) : x + 1 - x = 0 := by ring
/-
error: unsolved goals
⊢ 1 = 0
-/

-- simproc acts, user does not get useful error message
example (x : ℤ) : x - 1 - x = 0 := by ring
/-
error: unsolved goals
⊢ False
-/

Community Feedback

Discussion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20only.20on.20numeric.20goals

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Kha]

Side note: ring could likely be fixed by adjusting Methods.post in the simp call