Dependent version of `apply`

Stream: lean4

[Freddie Nash]

Is there a version of/syntax for the apply tactic which allows you to give a name to early parameters? E.g. if I want to prove p /\ q, having a proof of p around may be handy when proving q (obviously I can just bind a name to my proof of p with have, but could save a fair bit of ceremony in some situations).

I can get close (for two params) with

def dapp (f:p -> q -> r) : (p ∧ (p -> q)) -> r := by
  intro ⟨hp, hpq⟩
  exact f hp (hpq hp)

macro "dapply" f: term : tactic => `(tactic|
  (apply dapp $f; constructor)
)

but struggling with idents in tactics (e.g. syntax like dapply And.intro as lhs, performing intro lhs on the second goal), and it feels like something that someone else must have done better, and I'm just not using the right keywords to find it.

[Edward van de Meent]

i did have something similar, once... although i called it have_goal

[Edward van de Meent]

find the code here (it's one of those, but i can't remember precisely what the differences are)

[Edward van de Meent]

i guess it would be called unidiomatic by current standards since it only works when there are multiple goals available

[Edward van de Meent]

it doesn't look it but it comes with big warning signs of don't use unless you really really really have to

[Freddie Nash]

Topmost elaboration seems to work, and is rather more general than what I was going for

[Freddie Nash]

If it's not too complicated a topic, why would use of such a tactic be problematic? From my side, I'd rather name things up front, and not have issues like "now I need to close the goal with have_goal rather than throwing tactic of my choice at it" (though presumably it would be easy to adapt to use an arbitrary tactic rather than a term), but those would both be matters of style and convenience, which I expect is not what you're getting at.

[Edward van de Meent]

to be clear, i was talking about have_goal being unidiomatic, since it acts on multiple goals at once, while not necessarily working on all goals. In particular, it fails when used in combination with a focussing dot.

[Edward van de Meent]

mathlib lints against this kind of tactic, because (i think?) it makes the structure of the proof unclear?

[Freddie Nash]

I see: yes, failing with a dot did throw me initially (code examples for comparison)

theorem have_goal_test (p q r:Prop) (f:p -> q -> r) (hp:p) (hpq:p -> q) : r := by
  apply f
  have_goal lhs := hp
  exact hpq lhs

theorem dapply_test (p q r:Prop) (f:p -> q -> r) (hp:p) (hpq:p -> q) : r := by
  dapply f
  . exact hp
  . intro lhs
    exact hpq lhs

-- (not got this working)
theorem dapply_ideal (p q r:Prop) (f:p -> q -> r) (hp:p) (hpq:p -> q) : r := by
  dapply f as lhs -- ideally want to give a list of identifiers
  . exact hp
  . exact hpq lhs

(obviously with the idea that the proof of the lhs would not be trivial, and that the type of the proposition is probably long and painful to read, so you don't really want to be binding it manually)

[Kyle Miller]

You can use refine and named placeholders:

theorem dapply_ideal (p q r:Prop) (f:p -> q -> r) (hp:p) (hpq:p -> q) : r := by
  refine f ?as ?lhs
  . exact hp
  . exact hpq ?as

[Freddie Nash]

Is that a recent addition? Not seeing any bindings with 4.14-rc2 (I probably ought to bump that)

[Freddie Nash]

(nor with 4.18)

[Freddie Nash]

Ah! I missed the ? in the usage: that's exciting, and works with apply also (I presume this allows you to talk about any filled hole)

[Ruben Van de Velde]

Oh wow, I didn't realize that worked

[Kyle Miller]

Freddie Nash said:

Is that a recent addition?

It's been there since before the first public release of Lean 4.

[Freddie Nash]

Yep, I'd missed the ? in the exact hpq ?lhs bit, and assumed it wasn't working because the holes don't appear in the list of hypotheses

[Robin Arnez]

My experience with named meta-variables is that they can really be inconsistent:

theorem dapply_ideal (p q r:Prop) (f : ¬¬p -> q -> r) (hp : p) (hpq : ¬¬p -> q) : r := by
  refine f ?as ?lhs
  · rw [Classical.not_not]
    exact hp
  · exact hpq ?as -- fails because ?as : p (=> takes meta-variable at the state of `exact hp`)