more expr munging

Stream: general

[Scott Morrison]

Say I have an expr representing an iterated pi type, which is finally an equation, something like Π (a : ℕ) (b : ℕ), f a b = g (a + b). From that, I want to produce f ?m_1 ?m_2, where ?m_1 and ?m_2 are newly created metavariables of the appropriate types.

[Scott Morrison]

Any suggestions?

[Reid Barton]

Are you guaranteed that the left hand side will be literally <something> a b, where a and b are the variables introduced by the Pis in order? Or could it be some arbitrary expression involving a and b?

[Simon Hudon]

meta def get_lhs : expr -> tactic expr
| (expr.pi n bi d b) :=
do v <- mk_local' n bi d,
      b' <- whnf $ b.instantiate_var v
      get_lhs b'
| `(%%a = %%b) := pure a
| _ := failed

[Reid Barton]

Yes this strategy is what I was about to suggest. Peel off one outer Pi at a type, leaving a formula with a free variable, and then substitute a fresh metavariable or whatever else you want for that free variable

[Simon Hudon]

Actually, we can be more direct:

meta def get_lhs : expr -> tactic expr
| (expr.pi n bi d b) :=
do v <- mk_meta_var d,
   b' <- whnf $ b.instantiate_var v
   get_lhs b'
| `(%%a = %%b) := pure a
| _ := failed

[Scott Morrison]

(I'm doubly impressed, Simon, that your code often doesn't quite compile: there's a comma missing in that first one. :-)

[Simon Hudon]

Where would be the fun if you didn't have to fix my mistakes?

[Scott Morrison]

So I'm trying to do something a bit fancier here, and while get_lhs work as requested, really I want something more. :-)

[Simon Hudon]

I'm listening (sort of)

[Scott Morrison]

I had written:

meta def substitutions' : expr → bool → list expr →
  tactic (tactic (expr × expr × list expr))
| (expr.pi n bi d b) symm types :=
  do substitutions' b symm (d :: types)
| `(%%lhs = %%rhs) symm types :=
  do let (lhs, rhs) := if symm then (rhs, lhs) else (lhs, rhs),
     let tac := (do mvars ← types.mmap mk_meta_var,
        let pattern := lhs.instantiate_vars mvars,
        ty ← infer_type pattern,
        return (pattern, ty, mvars)),
     return tac
| _ _ _ := failed

[Scott Morrison]

The idea being to return a tactic, which could be invoked multiple times, each time producing the pattern with "fresh" mvars.

[Scott Morrison]

However it's ... still somewhat mysteriously ... not working in all cases. (Sorry this is far from a MWE.)

[Reid Barton]

Is this supposed to be more efficient than just invoking something like get_lhs repeatedly?

[Scott Morrison]

Yeah, I guess so.

[Scott Morrison]

But maybe I am needlessly complicating things. :-(

[Simon Hudon]

I think you need to reverse mvars

[Reid Barton]

It's probably about equally or less efficient because the representation of that tactic object in the VM is going to be basically the same as or a more complicated structure than the outer Pis of the original type.

[Scott Morrison]

Hmm. I had tried (on a purely voodoo basis) reversing mvars, without apparent success. Let me go away on de-complicate for a bit. :-)

[Scott Morrison]

Thanks for the help!

[Simon Hudon]

After squinting at it for a while, I agree with @Reid Barton

[Reid Barton]

(Or at least, that would be true in the GHC runtime system, which is probably a terrible mental model for the Lean VM but the best one I have available.)

[Simon Hudon]

My reasoning is that, for each bound variable, the expensive thing is instantiate_var, the number of which does not decrease in this approach

[Reid Barton]

Right, you only save the decomposition of the Pis.

[Reid Barton]

Which is cheap anyways, but to make things worse, you replace it by having to do an equal number of applications-of-variable-functions (the inner tacticwhich you build up).

[Reid Barton]

Oh wait, you implemented it in a way so that there is only one closure being built (tac), but still each invocation of tac has to process the list types, which has the same information as the outer Pis of the original expression.

[Scott Morrison]

and, happily it all seems to work now!

[Scott Morrison]

(or at least the "all" that I hoped to have done tonight!)