Simp regressions probably related to transparency

[PatrickMassot]

Prerequisites

• [C] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

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

example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
  (a : α) (b : β) : f (a, b) b = b := by
  -- simp [h] -- fails but worked in Lean 3
  rw [h] -- works

example {α β : Type} {f : α × β → β → β}
  (a : α) (b : β) (h : f (a,b) (a,b).2 = (a,b).2) : f (a, b) b = b := by
  -- simp [h] -- fails but worked in Lean 3
  rw [h] -- works

Expected behavior:

The simp call closes the goal as they did in Lean 3.

Actual behavior:

simp is not working but rw works.

Versions

Lean (version 4.2.0-rc1, commit a62d2fd, 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 and rw.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[leodemoura]

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.

[digama0]

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).

[leodemoura]

@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.

[digama0]

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.

[digama0]

@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.

[leodemoura]

@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.

[PatrickMassot]

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.