binderNameHint & simp

Stream: general

[Mirek Olšák]

In the docs, binderNameHint should be supported by simp, but it doesn't seem to me... Am I doing something wrong?

def forall_and'.{u} {α : Type u} {p q : α → Prop} :
    (∀ a : α, p a ∧ q a) ↔
    (∀ b, binderNameHint b p (p b)) ∧ (∀ c, binderNameHint c q (q c)) :=
  forall_and

example : ∀ my_favorite_name : Nat,
    2 + my_favorite_name < my_favorite_name + 10 ∧ my_favorite_name * 2 ≤ my_favorite_name * 3 := by
  -- rw [forall_and'] -- keeps the name
  simp only [forall_and'] -- changes the name to `a`

[Jovan Gerbscheid]

I think binderNameHint generally has trouble dealing with forall binder names

[Robin Arnez]

Hmm the problem seems to be that rw uses occurrence =?= pattern while simp uses pattern =?= occurrence and the name on the left-hand side seems to always take precedence so in simp, the a from the left-hand side of forall_and' takes precedence over my_favorite_name.

[Robin Arnez]

So the fix would be to swap lhs and e in here

private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
  recordTriedSimpTheorem thm.origin
  let rec go (e : Expr) : SimpM (Option Result) := do
    trace[Debug.Meta.Tactic.simp] "trying {← ppSimpTheorem thm} to rewrite{indentExpr e}"
    if (← withSimpMetaConfig <| isDefEq lhs e) then -- here

[Robin Arnez]

... except, that pattern =?= occurrence makes sense for other reasons, namely unifying meta-variables; e.g. in ?a =?= ?b, ?a has priority for being instantiated and that should then be the pattern.

[Mirek Olšák]

This other occasion when pattern =?= occurrence is more suitable does not apply for rw?

[Robin Arnez]

Really so?

example : True := by
  apply (fun (n : Nat) (h : Nat.succ n = 3) => trivial)
  rewrite [Nat.succ_eq_add_one]

creates a new metavariable although I'd argue it should just keep ?n

[Mirek Olšák]

Looks like Lean is still far from a principled solution...

[Jovan Gerbscheid]

I had observed this quirk as well. I made a PR a while ago that made this change in simp, but it did break a bunch of proofs in mathlib, so I didn't pursue it further.

[Robin Arnez]

I think a better change (that would have less impact) would be to prefer the right-hand side name in isDefEq and use pattern =?= occurrence is rw too

[Robin Arnez]

Here's a PR: lean4#12380