iApply tactic implemented

Stream: iris-lean

[Oliver Soeser]

The iapply tactic has been implemented! (PR #80)

Like most iris-lean tactics, it does not yet have the same flexibility as its Rocq equivalent, however I'm confident that the tactic is sufficiently useful in its current form.

Next steps for iapply would include the ability to apply hypotheses from the lean context directly and the use of advanced specialization patterns. I could add these to the current PR though it might be worth splitting them into separate issues/PRs, let me know what you think.

If anyone could try iapply out for their proofs and give me some feedback that would be very helpful :)

[Markus de Medeiros]

Sweet! I'll merge that into my personal branch and play around with it today :)

[Markus de Medeiros]

I'll just post my feedback here as I have it: having iapply work with functions from the Lean context is definitely an important feature

[Markus de Medeiros]

The workaround I've found atm is to first put the theorem into the Iris context with transitivity and then specialize/apply it from there

[Markus de Medeiros]

(which has the major PITA that you need to spell out all of your implicits instead of getting them by unification with your goal)

[Oliver Soeser]

Yea that's definitely a major deficit, I'll make sure to add it to the current PR

[Markus de Medeiros]

Minor regression, I don't think it's that important but just be aware of it. Before in the context

∗Hσ : state_interp sl sr
∗H : ∀ sl sr, state_interp sl sr -∗ ...

I was able to do ispecialize H Hσ, but now it complains that it can't synthesize IntoWand. ispecialize H sl sr Hσ works though so it's nbd

[Markus de Medeiros]

Ah, this might be related to something in iApply. I'm struggling to minimize the example since it seems to go away when the types are simpler, but I'll put it here for posterity anyways

Example

theorem wp_gen_loc (R : Locals DataT → Locals DataT → Prop) :
  ⊢ (∀ locₗ locᵣ, ⌜R locₗ locᵣ⌝ -∗ wp (DataT := DataT) K (.run <| ⟨sₗ, locₗ⟩ :: pₗ) (.run <| ⟨sᵣ, locᵣ⟩ :: pᵣ) Φ) -∗
    ⌜R llₗ llᵣ⌝ -∗
    wp (DataT := DataT) K (.run <| ⟨sₗ, llₗ⟩ :: pₗ) (.run <| ⟨sᵣ, llᵣ⟩ :: pᵣ) Φ := by
  iintro H HR
  -- Breaks without this ispecialize
  ispecialize H _ _ HR
  iapply H

Error

failed to synthesize
  ProofMode.FromAssumption false
    iprop(∀ locₗ locᵣ,
        ⌜R locₗ locᵣ⌝ -∗
          wp K (ExecState.run ({ stmt := sₗ, env := locₗ } :: pₗ)) (ExecState.run ({ stmt := sᵣ, env := locᵣ } :: pᵣ))
            Φ)
    (wp K (ExecState.run ({ stmt := sₗ, env := llₗ } :: pₗ)) (ExecState.run ({ stmt := sᵣ, env := llᵣ } :: pᵣ)) Φ)

[Markus de Medeiros]

iApply is super nice to have even in this form!

[Markus de Medeiros]

It would be great to automatically use Affine lemmas in the case of applying wands like P -∗ (Q ∗ emp), and automatically eliminate trivial goals when applying (True ∗ P) -∗ Q, this stuff comes up when going in and out of the proofmode, which we need to do for the near future (and IMO is a super nice feature of of the proofmode!)

[Markus de Medeiros]

Also, I'm wondering if there's a way to name goals coming from iApply? I'm actually not sure if there's a way to do after the fact this in regular Lean but sometimes we might want to solve the generated goals in a different order.

[Markus de Medeiros]

Oh yeah related to the first point, an intro pattern to clear unwanted lemmas would be nice (like _ in Rocq, since _ behaves like ? in Lean)

[Oliver Soeser]

Markus de Medeiros said:

Oh yeah related to the first point, an intro pattern to clear unwanted lemmas would be nice (like _ in Rocq, since _ behaves like ? in Lean)

iintro supports using - to clear lemmas, is that what you're looking for?

[Markus de Medeiros]

TIL, thanks!

[Markus de Medeiros]

(deleted)

[Oliver Soeser]

iapply should work with lemmas from the lean context now!

[Oliver Soeser]

At the moment it is prone to adding trivial goals, so I'll try to get their automatic elimination working next

[Markus de Medeiros]

Oliver Soeser said:

iapply should work with lemmas from the lean context now!

Sweeeet!

[Oliver Soeser]

I've also put in some automatic goal elimination, though that still needs improving

[Markus de Medeiros]

How hard would it be to allow iapply to be given a proof term, or to apply a lemma that has implicits? Here's a representative example:

section Example
open Iris
variable {PROP : Type _} [BI PROP]
variable (P : Nat -> PROP) (L : ∀ {n : Nat}, P (n - 1) ⊢ P n)

-- Works when you specialize everything yourself
example : P 3 ⊢ P 4 := by
  have L' := @L 4
  iintro H
  iapply L' with [H]

theorem Lalt {n : Nat} : P (n - 1) ⊢ P n := by sorry

-- But can I apply L without providing all the implicits?
example : P 3 ⊢ P 4 := by
  iintro H
  -- iapply L with [H] -- iapply: L is not an entailment
  -- iapply Lalt       -- unexpected term '@Lalt'; expected single reference to variable
  sorry

end Example

[Markus de Medeiros]

It's not so bad in this example but when your start having more implicits, specializing them all becomes big problem
Screenshot 2025-08-06 at 10.36.42 AM.png

[Markus de Medeiros]

For example in the screenshot above I would love to be able to do iapply (wp_gen_loc (fun _ _ => True) since everything else matches with the proof goal exactly by unification

[Markus de Medeiros]

It seems that there are two issues:

• Feeding iapply a Lean term for an entailment (wp_gen_loc (fun _ _ => True)) instead of the name of a Lean term for an entailment Z
• iapplying a term with implicits

[Oliver Soeser]

For lemmas with implicits: that's gonna need some procedure to automatically fill them, which shouldn't be too difficult I hope

[Oliver Soeser]

For feeding proof terms, I'm gonna look into how I can adjust the parser to allow that

[Markus de Medeiros]

Nice. The latter might even solve the former.

[Shreyas Srinivas]

for the parser, you might be able to borrow the syntax spec of the apply tactic

[Shreyas Srinivas]

It shouldn't really affect how the proof is elaborated anyway

[Oliver Soeser]

At the moment my procedure for passing lean lemmas just very bluntly pattern matches for an entailment, so that would need to be reworked

[Oliver Soeser]

Markus de Medeiros said:

Nice. The latter might even solve the former.

That's true!

[Markus de Medeiros]

Right, I think even if you have to do iapply (@wp_gen_loc _ _ _ _ _ _ _ (fun _ _ => True)) it solves 99% of the problem! As it stands right now every time I want to apply I lemma I need to explicitly copy out the entire remaining program text to specialize it haha

[Oliver Soeser]

Markus de Medeiros said:

Also, I'm wondering if there's a way to name goals coming from iApply? I'm actually not sure if there's a way to do after the fact this in regular Lean but sometimes we might want to solve the generated goals in a different order.

I've now made it so that you can put a string at the end of a spec pat to name the corresponding subgoal, hope that resolves the issue

[Markus de Medeiros]

Ah, I realize now that I can actually get away with not writing out all my implicits by using the form
P ∗ (Q -∗ wp e') ⊢ wp e instead of ⊢ P -∗ (Q -∗ wp e') -∗ wp e so that the entire right-hand side of the turnstyle matches the entire Iris goal. I still need to manually use refine Entails.trans ?_ (@myLemma ..) for this instead of iapply due to the first issue above but at least there's a workaround for the second issue!

[Markus de Medeiros]

Kudos again for the work so far btw, iapply has definitely saved me some grief!

[Oliver Soeser]

(deleted)

[Markus de Medeiros]

⊢
  ∗IH : emp -∗ ∀ p1 p2, P ∗ wp k p1 p2 Φ -∗ wp k p1 p2 fun x1 x2 => iprop(Φ x1 x2 ∗ P)
  ∗HP : P
  ∗Hwp : wp k cl'.fst cr'.fst Φ
  ∗Hemp : emp
  ⊢ wp k cl'.fst cr'.fst fun x1 x2 => iprop(Φ x1 x2 ∗ P)

Minor thing: iapply IH doesn't work in this case yet. The two things I think are missing are specialization for empty hypotheses, and instantiation of foralls.

[Markus de Medeiros]

It would also be nice if ispecialize could specialize emp hypotheses, since atm I think you need to manually exit the proofmode and apply refine .trans sep_emp.mpr ?_ to specialize it.

[suhr]

Can this PR be merged? I believe the implementation is already quite useful. Subsequent improvements could be made in a new PR.

[Alex Bai]

What is currently status of iapply? Seems like it's one "TODO" comment for syntax away?

[Oliver Soeser]

In my view iapply is finished, the syntax is mostly the same as it is in the Rocq implementation. It is admittedly a bit clunky to use, but I don't think it's a major issue. If people feel strongly about this and have suggestions for alternative syntax I'd be happy to implement them

[Markus de Medeiros]

If you want to use iApply right now I'd suggest using the unstable branch

[Markus de Medeiros]

It is completely usable, just in the backlog of things for Mario to review