apply weaker than exact

Stream: lean4

[Jeremy Tan]

Based on my PR lean4#5359 @Joachim Breitner filed an apparent bug lean4#5366 claiming that the fact that apply is in some cases weaker than exact is surprising ("apply should always succeed when exactdoes").

But is the current behaviour meant to be that way?

[Jeremy Tan]

Specifically that exact automatically introduces implicit variables and apply does not

[Damiano Testa]

I would expect there to be situations where apply and exact work/do not work in all combinations.

My experience is that, unless a tactic is designed to first try another and then, possibly do more stuff, you should expect them to behave completely independently on appropriate goals.

[Damiano Testa]

Having said this, it is a good mental model to think that apply will work where exact will, and, by observing the situations where it doesn't, you can get a more refined point of view.

[Jeremy Tan]

So you're saying that lean4#5366 is not a bug at all and that lean4#5359 can go ahead as it is now? (I have the same views)

[Jeremy Tan]

apply and exact serve two different purposes. exact is a finishing tactic, apply is more like refine to replace a hypothesis with another

[Damiano Testa]

I'm on mobile, so I had not completely digested the issue. I'm somewhat agnostic about "implicit lambda feature", though apply rfl looks a little strange! :smile:

[Jeremy Tan]

And now @Joachim Breitner comes back and says that lean4#5359 is bad. Sure, I can revert it if you want to

[Joachim Breitner]

Sorry for the furstration this causes – it’s always painful to clean up technical dept, else it wouldn’t have accumulated.

No rush until there is an agreement and a decision, and it’s not (necessarily) your obligation to follow through with this. Likely whatever the conclusion will be will come with lean4#3714.