non-interactive `apply`

Stream: general

[Scott Morrison]

Consider the following tactic block:

def bar (a b : ℕ) (h₁ : 1 < b) (h₂ : 0 < a) :
  a < a * b :=
begin
  apply (lt_mul_iff_one_lt_right _).mpr,
  exact h₁,
  exact h₂,
end

I would like to know how to write a non-interactive tactic def foo (n : name) : tactic unit, so that when it is passed `lt_mul_iff_one_lt_right for n, it implements exactly the first apply tactic invocation, producing precisely two subgoals.

This function foo should work out how many explicit arguments mk_const n has, provide those as metavariables, check that the result is an iff, and then apply iff.mpr.

[Scott Morrison]

My attempts so far are failing

[Scott Morrison]

because when I introduce metavariables for the arguments of lt_mul_iff_one_lt_right, I can't help but produce too many, so by the time I have an expression ready to pass to tactic.apply, too many extra goals get generated (for the various implicit arguments).

[Rob Lewis]

Is this too dumb?

meta def mpr_apply (n : name) : tactic unit :=
applyc `iff.mpr >> applyc n

[Scott Morrison]

Ah... I missed a major constraint: which is that this function has to actually build an expr to pass to a single apply call!

[Scott Morrison]

I wonder if I can reverse engineer my expression by actually running your two applyc tactics, however (i.e. use the show_term trick).

[Scott Morrison]

Hmm, no, if I time-travel back before the two applyc invocations, the new metavariables created by them will get stranded. :-(

[Rob Lewis]

Uh, this might be an xy thing. I think it's safer to let apply create the mvars for you than to manually create the goals you need and build the expression for apply. But if that's really what you have to do, you could do something like this, where I haven't implemented replace_mvars_with_fresh_ones:

meta def mpr_apply (n : name) : tactic unit :=
do t ← target,
   e ← prod.snd <$> (solve_aux t $ applyc `iff.mpr >> applyc n) >>= instantiate_mvars,
   trace e,
   e ← replace_mvars_with_fresh_ones e,
   apply e $> ()

[Rob Lewis]

Using apply on an expr with handmade mvars doesn't add those mvars as goals, does it? Or am I misremembering?

[Scott Morrison]

@Rob Lewis, this is now failing in the opposite direction than my previous attempts. Here's what I have so far, filling out your solution:

import data.nat.basic

open tactic expr

namespace expr

/-- Implementation of `expr.mreplace`. -/
meta def mreplace_aux {m : Type* → Type*} [monad m] [alternative m] (R : expr → nat → m expr) :
  expr → ℕ → m expr
| (app f x) n := R (app f x) n <|>
  (do Rf ← mreplace_aux f n, Rx ← mreplace_aux x n, return $ app Rf Rx)
| (lam nm bi ty bd) n := R (lam nm bi ty bd) n <|>
  (do Rty ← mreplace_aux ty n, Rbd ← mreplace_aux bd (n+1), return $ lam nm bi Rty Rbd)
| (pi nm bi ty bd) n := R (pi nm bi ty bd) n <|>
  (do Rty ← mreplace_aux ty n, Rbd ← mreplace_aux bd (n+1), return $ pi nm bi Rty Rbd)
| (elet nm ty a b) n := R (elet nm ty a b) n <|>
  (do Rty ← mreplace_aux ty n,
    Ra ← mreplace_aux a n,
    Rb ← mreplace_aux b n,
    return $ elet nm Rty Ra Rb)
| e n := R e n <|> return e

/--
Monadic equivalent of `expr.replace`.

The function `R` visits each subexpression `e`, and is called with `R e n`, where
`n` is the number of binders above `e`.
If `R e n` returns some value, `e` is replaced with that value (and `mreplace` does not visit
its subexpressions).
If `R e n` fails, the `mreplace` continues visiting subexpressions of `e`.
-/
meta def mreplace {m : Type* → Type*} [monad m] [alternative m]
  (R : expr → nat → m expr) (e : expr) : m expr :=
mreplace_aux R e 0

/--
Replace each metavariable in an expression with a fresh metavariable of the same type.
-/
meta def refresh_mvars (e : expr) : tactic expr :=
e.mreplace (λ f n, if f.is_mvar then infer_type f >>= mk_meta_var else failed)

end expr

/--
Prepares a ``(n ___).mpr` expression that can be applied against the goal,
where `___` is however many `_`s are needed to obtain an `iff`.
-/
meta def iff_mpr_apply (n : name) : tactic expr :=
do t ← target,
   e ← prod.snd <$> (solve_aux t $ applyc `iff.mpr >> applyc n) >>= instantiate_mvars,
   e ← e.refresh_mvars,
   return e.app_fn

example (a b : ℕ) (h₁ : 1 < b) (h₂ : 0 < a) :
  a < a * b :=
begin
  apply (lt_mul_iff_one_lt_right _).mpr,
  exact h₁,
  exact h₂,
end

example (a b : ℕ) (h₁ : 1 < b) (h₂ : 0 < a) :
  a < a * b :=
begin
  iff_mpr_apply `lt_mul_iff_one_lt_right >>= trace, -- looks good: `(lt_mul_iff_one_lt_right ?m_1).mpr`
  iff_mpr_apply `lt_mul_iff_one_lt_right >>= apply,
  -- but we only get one goal :-(
  exact h₁,
end

[Scott Morrison]

It seems iff_mpr_apply is producing exactly the expression we were hoping for. I'm just not working out how to get apply to do what I want!

[Scott Morrison]

I think I'm having the opposite problem that you were worried about: I want apply to create new goals for these metavariables.

[Rob Lewis]

Scott Morrison said:

I think I'm having the opposite problem that you were worried about: I want apply to create new goals for these metavariables.

Yeah, I get that's what you want, but it's not what apply does. Which is why this feels kind of xy to me -- you're trying to duplicate some of the behavior of apply, so that you can call apply in a way it's not really designed for.

[Rob Lewis]

Instead of using refresh_mvars (and e.app_fn) you could lambda abstract the mvars in e. Then you get something you can apply.

[Rob Lewis]

FYI there's a non-docstring comment on src#tactic.i_to_expr_for_apply that might be relevant here. At least pointing out that there are subtleties in doing this correctly

[Scott Morrison]

Sorry -- to explain the #xy behind this, I am writing a tactic tactify, which eats a term mode proof and attempts to spit out a human-plausible tactic mode proof for it. (Why? Helpful for teaching what tactics do, and perhaps helpful for generating training data.)

With the notable exception of proofs which use cases, induction, or pattern matching, this is actually pretty doable. (See branch#tactify; it's extremely messy at the moment.)

I'm at the point where I want to make some proofs more human-plausible. A very common pattern at the moment is that it spits out proof scripts that look like

apply iff.mpr,
apply lt_mul_iff_one_lt_right,

which no human in their right mind would write, because the first apply is unmotivated. Instead I want:

apply (lt_mul_iff_one_lt_right _).mpr,

The general way that tactify works is that it maintains a list of solutions for the current goals, and after inspecting the current solution for the main goal, it decides on a tactic to use, then runs that tactic and uses unification to generate the corresponding new list of solutions for the new goals.

This means that I need to be able to simulate "under the hood" exactly the behaviour of the interactive mode tactic that I am going to propose in the tactic script. Hopefully this explains the xy!

(As a general point, I think it's pretty important that we can reproduce in non-interactive tactics the exact behaviour of the interactive tactics, and I'm a bit sad to be struggling here --- perhaps if one could use antiquotations inside `[...] blocks we'd be okay.)

[Scott Morrison]

I'm worried with your new suggestion (lamba abstract the mvars) I will have to generate the tactic step apply (λ x, (lt_mul_iff_one_lt_right x).mpr, which again does not look human-plausible.