Closed PatrickMassot closed 8 months ago
Yes, it is due to discriminations trees. We can disable the discrimination tree indexing for a subterm t
using no_index t
. Example:
example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p (no_index p.2) = p.2)
(a : α) (b : β) : f (a, b) b = b := by
simp [h]
example {α β : Type} {f : α × β → β → β}
(a : α) (b : β) (h : f (a,b) (no_index (a,b).2) = (a,b).2) : f (a, b) b = b := by
simp [h]
A possible workaround: global @[simp]
theorems do not usually have LHS's with reducible terms such as (a, b).2
, but this kind of term does occur in local hypotheses. One option is to instruct Lean to always use no_index
for the arguments of local hypotheses. We would recover the Lean 3 behavior for them. Drawback: performance impact on tactics such as simp_all
that may operate in big local contexts.
global @[simp] theorems do not usually have LHS's with reducible terms such as (a, b).2,
Unfortunately, these do exist in the category theory library, usually deep inside some implicit type arguments in dependencies of the main arguments (which makes manually adding no_index
quite painful in practice). Possibly this could be addressed by preprocessing the LHS of simp theorems when they are added to the tree to dsimp them away, although this is problematic when the lemma is itself about this reduction (i.e. @[simp] theorem mk_snd : (a, b).2 = b
).
@digama0 Could you please provide evidence for your claim? It is not clear to me why someone will write (a, b).2
in a theorem statement if they want to be able to match with b
.
They don't write it themselves, it is generated by elaboration up in the implicit type dependencies that users don't see. This is a half-remembered example from when I had to debug such an issue, the text (a, b).2
never appears in the source text and you only notice it appearing in the elaboration trace if you dig into the terms. I will see if I can locate the example.
EDIT: I don't think it is an exact match but https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20not.20using.20a.20simp.20lemma/near/353943416 is a similar issue.
@leodemoura Here's the issue I was recalling. As you can see from the debugging discussion, the term (W, X).fst
shows up as the inferred argument to a function with some complex dependencies, even though it was never explicitly written down.
@digama0 Could you please show me the actual Mathlib theorem statement that contains (W, X).fst
? Moreover, if it is an implicit argument, it should not matter since the discrimination tree ignores them.
I'm sorry about the confusion brought by my second example. The first failure was the one I actually encountered when porting the sphere eversion project. The second one was brought up during the Zulip discussion. I just checked that no_index
works in the example that triggered the discussion.
Prerequisites
Description
Many
simp
proofs from Lean 3 no longer work, probably because the discrimination tree that is necessary for improved performance does not allow seeing through definitional equality. I think this is worth reporting anyway.Context
The specific examples come from this Zulip discussion
Steps to Reproduce
Expected behavior:
The
simp
call closes the goal as they did in Lean 3.Actual behavior:
simp
is not working butrw
works.Versions
Lean (version 4.2.0-rc1, commit https://github.com/leanprover/lean4/commit/a62d2fd4979671b76b8ab13ccbe4fdf410ec0d9d, Release) Ubuntu 22.04
Impact
In isolation this is not a problem, but when porting project it can make a complicated simp call involving a lot of lemmas very painful to debug. And the ported output then requires alternating calls to
simp only
andrw
.Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.