apply? and the "symm" attribute

Stream: lean4

[Michael Stoll]

I'm moving this discussion from this thread in the "new members" stream here to give it more visibility.

Since a while ago (but I can't really tell precisely since when) I'm noticing that apply? behaves badly in a certain way. I managed to trace this back to an interaction between certain lemmas marked symm and apply? (my suspicion is that this may be related to discrimination trees, but I have zero experience with metaprogramming in Lean 4, so I have no idea how to check this hunch). Consider the following #mwe.

-- set up a binary relation
axiom r : Nat → Nat → Prop

-- that is symmetric
theorem r.symm {a b : Nat} : r a b → r b a := sorry

-- and has some other property
theorem r.trans {a b c : Nat} : r a b → r b c → r a c := sorry

-- now try `apply?`
example (a b c : Nat) (h₁ : r b a) (h₂ : r b c) : r c a := by
  apply?
/-
Try this: refine r.trans ?_ ?_
Remaining subgoals:
⊢ Nat
⊢ r c ?b
⊢ r ?b a

Try this: refine r.symm ?_
Remaining subgoals:
⊢ r a c

which looks fine.
-/

-- now attach the `symm` attribute to `r.symm`
attribute [symm] r.symm

-- and repeat
example (a b c : Nat) (h₁ : r b a) (h₂ : r b c) : r c a := by
  -- `exact?` → `exact?` could not close the goal.
  apply?
/-
Try this: refine r.trans (?_ (id (r.symm h₁))) (?_ (id (r.symm h₁)))
Remaining subgoals:
⊢ r a b → Nat
⊢ r a b → r c (?m.239 ⋯)
⊢ r a b → r (?m.239 ⋯) a
⊢ r c b → Nat
⊢ Nat
⊢ r c b → r c (?m.239 ⋯)
⊢ r c (?m.239 ⋯)
⊢ r c b → r (?m.239 ⋯) a
⊢ r (?m.239 ⋯) a

Try this: refine r.symm (r.trans (?_ (id (r.symm h₁))) (?_ (id (r.symm h₁))))
Remaining subgoals:
⊢ r a b → Nat
⊢ r a b → r a (?m.331 ⋯)
⊢ r a b → r (?m.331 ⋯) c
⊢ r c b → Nat
⊢ Nat
⊢ r c b → r a (?m.331 ⋯)
⊢ r a (?m.331 ⋯)
⊢ r c b → r (?m.331 ⋯) c
⊢ r (?m.331 ⋯) c

Try this: refine r.symm (?_ (id (r.symm h₁)))
Remaining subgoals:
⊢ r a b → r a c
⊢ r c b → r a c
⊢ r a c

Try this: refine r.symm (r.symm (?_ (id (r.symm h₁))))
Remaining subgoals:
⊢ r a b → r c a
⊢ r c b → r c a

... and clicking on any of these results in an error of the kind
  function expected at
    ?m.5099
  term has type
    ?m.5098

Also, I think that attaching `symm` *should* enable `apply?` to come up with
  `exact r.trans h₂.symm h₁`
-/

Since Mathlib marks a number of declarations with symm:

• Eq.symm in file#Init/Core and in file#Init/Logic
• Ne.symm, HEq.symmand Iff.symm in file#Init/Logic

and a few more specialized ones, this affects apply? whenever there are equalities (or negated equalities) in the context, which is very common.

A side effect is that the suggestions produced by apply? get very long, so that there is a lot of text in the infoview, which results in, e.g., scrolling to react very slowly. And, of course, a more immediate pain point is that the suggestions that are produced result in errors and have to be edited manually to make sense.

I feel very strongly that something needs to be done here, and I am wondering how other people put up with this. If you agree with the first part of the preceding sentence, please add a :+1: to this message.

[Michael Stoll]

It would be nice if one of the developers could either

• confirm that they consider this a problem and give an indication what they are planning to do, or else
• explain why they think it is not a problem.

I can make an issue, if that helps.

[Kevin Buzzard]

I only didn't add a thumbs up because my experience with apply? was always so bad that I just stopped using it completely

[Michael Stoll]

That would be a good reason to add several :+1:s if that were possible!

[Floris van Doorn]

I completely agree with this issue. I have regularly received suggestions from apply? that were correct, except that some metavariables were applied to arguments, which I had to remove manually. It's good to see a very small example where this already happens.

[Michael Stoll]

I hope the #mwe above will make it fairly easy to figure out what the problem is.

[Michael Stoll]

/poll How do you rate apply?
It works well for my use cases
I'd like to use it, but am unhappy with it
I have no intention to use it, no matter what

[Michael Stoll]

Maybe the poll above gives a clearer picture...

[Michael Stoll]

lean4#3922 is the issue.
@Ruben Van de Velde @Asei Inoue @Richard Osborn @Johan Commelin @Damiano Testa @Scott Carnahan @Sébastien Gouëzel @Floris van Doorn please :+1: it if you want it to have an impact.

[Kim Morrison]

The poll seems a bit of a broad question, when the thread is really about a particular bad behaviour interacting with symm... :-)

[Kim Morrison]

Proposed fixes very welcome, otherwise I'll try to investigate once my plate is a bit emptier.

[Michael Stoll]

Well, this specific bad behavior is so pervasive that it has broad implications...

Kim Morrison said:

Proposed fixes very welcome, otherwise I'll try to investigate once my plate is a bit emptier.

I was hoping that reducing the problem to the interaction with the symm attribute would be sufficient for somebody with metaprogramming skills to take over and get to the bottom of this. But the main thing is that something is done about it eventually (and in the not-too-distant future).

[Jovan Gerbscheid]

I'd like to make a version of apply? using my own discrimination tree, once my library rewrite tactic rw?? lands in Mathlib. The issue discussed here seems orthogonal to the benefits that the new discrimination tree brings, but my guess would be that reimplementing the tactic would eliminate this bug.

[Kyle Miller]

my guess would be that reimplementing the tactic would eliminate this bug

That's certainly a guess, especially if there's no theory yet about where this bug is coming from.

My current understanding is that it's an interaction with docs#Lean.MVarId.symmSaturate, which exact?/apply? use via docs#Lean.Meta.LibrarySearch.solveByElim . This is consistent with the way you get ?_ (id (r.symm h)) terms, since that's how docs#Lean.Expr.applySymm with docs#Lean.MVarId.note pass r.symm h into the newly created goal.

[Kyle Miller]

This is a tricky one... Symmetrizing hypotheses is a feature people have wanted before so it shouldn't just be removed. The symmSaturate function seems like it shouldn't be used though — my thought is that instead there should be a cache of facts that aren't attached to the local context, and this cache should be saturated. Then, only the facts that are actually used end up in the term.

[Kyle Miller]

lean4#3962 has an attempt at fixing lean4#3922

[Michael Stoll]

Thanks!

[Kyle Miller]

Merged!