Implementing `apply ... at ...` tactic

Stream: lean4

[Vladimir Gladstein]

Hey! I was trying to implement something like apply ... at ... tactic and got stuck a bit.

Suppose we have a term t of type forall n m, n = m -> m = n, and a hypothesis h : 5 = 4 in our proof context. apply t at h should change the type of h to 4 = 5. In general, it should instantiate with h the first argument of t with a matching type. And then instantiate all arguments of t which h depends on.
If I understand it correctly, the first step here would be to find an argument of t, that matches a type of h. I have managed to do that. But I have no idea what to do next.
Could someone please help me with it?

[Ruben Van de Velde]

I'm not sure what you're asking. Does this not work for you, or are you asking about the implementation of apply?

import Mathlib

example (h1 : ∀ m n : Nat, m = n → n = m) (h2 : 5 = 4) : True := by
  apply h1 at h2
  guard_hyp h2 : 4 = 5
  trivial

[Vladimir Gladstein]

Thank you! I didn't try to find one in mathlib

[Vladimir Gladstein]

Actually, that is not exactly what I want. This tactic creates a new metavariable for each uninstantiated hypothesis. But I want is to leave those hypothesise as preconditions of h
Like if we apply forall n m, n > 0 -> n = m -> n = m at h, the type of h : 5 = 6 should be 6 > 0 -> 6 = 5

[Jannis Limperg]

One possible algorithm is this:

• Use withNewMCtxDepth to make sure that the following only assigns metavariables created by you. (Presumably, this is what you want.)
• Use forallMetaTelescope on the type of t to create metavariables ?n : Nat, ?m : Nat, ?h : ?n = ?m.
• For each such metavariable ?x, run isDefEq ?x T, where T is the type of your hypothesis (here 4 = 5).
• If any of these calls succeeds, say ?h unifies with the type of h, create the proof t ?n ?m h. (What if multiple calls succeed?)
• Instantiate metavariables in this proof to obtain t n m h.
• Your spec doesn't mention this, but you probably want to support typeclass arguments. If so, go through the metavariables and try to synthInstance those that represent typeclass arguments.
• In case the proof still contains metavariables, use abstractMVars to turn them into lambdas.
• assert the resulting proof as a new hypothesis.

This code implements this procedure, though it also does a bunch of other things so it's maybe a bit opaque.

[Vladimir Gladstein]

Thank you! abstractMVars was a missing piece for me.

[Jireh Loreaux]

This sounds exactly like apply ... at except you also match on the body of the telescoped hypothesis.

[Vladimir Gladstein]

Jireh Loreaux said:

This sounds exactly like apply ... at except you also match on the body of the telescoped hypothesis.

I am not entirely sure what do you mean. But the algorithm by @Jannis Limperg exactly does what I wanted.

[Yaël Dillies]

I think this is a strictly better version than the current apply at, if you want to PR it.

[Adam Topaz]

Note that the usual apply adds missing hypotheses as additional goals. This was the idea behind the current behavior of apply ... at ....

[Adam Topaz]

If you do change this behavior, then I would check with @Kevin Buzzard who is using this tactic in the natural number game.

[Vladimir Gladstein]

Actually, I didn't intend to change the behaviour of the current version of apply at. The reason I need it, is that I am porting Coq ssreflect tactic language to Lean, and there is something similar there

[Vladimir Gladstein]

But I can make a PR is you think it is a better version

[Mario Carneiro]

I think it is unconventional in lean for anything to put subgoals as implications in the goal except the revert tactic which is specifically for doing that. This is significantly different from ssreflect where most subgoals end up as implications in the goal

[Jireh Loreaux]

Vladimir Gladstein said:

I am not entirely sure what do you mean. But the algorithm by Jannis Limperg exactly does what I wanted.

Sorry, I misunderstood because I failed to read this message carefully.
Vladimir Gladstein said:

Actually, that is not exactly what I want. This tactic creates a new metavariable for each uninstantiated hypothesis. But I want is to leave those hypothesise as preconditions of h
Like if we apply forall n m, n > 0 -> n = m -> n = m at h, the type of h : 5 = 6 should be 6 > 0 -> 6 = 5