Tactic that survives the goal it's called on

Stream: metaprogramming / tactics

[Robert Maxton]

Is there a way to write a tactic that closes the goal it's pointed at and keeps going? In particular, I'm trying to write a capture x conv tactic that assigns the currently-focused goal to a metavariable ?x, closes the most recent conv context with rfl, and then runs set x := ?x; the current implementation gets as far as rfl and then says "no goals left to be solved". Fair enough, but is there a workaround?

[Aaron Liu]

You have to match the contexts though

[Robert Maxton]

how so?

[Aaron Liu]

example (h : ∀ (x : Nat), x = x) : True := by
  conv at h =>
    intro x
    capture hx
  -- what is `hx` here?
  trivial

[Robert Maxton]

Ah, I see. In that case the answer is "whatever is most suitable for rewriting/wrapping and generalizing later", so in this case hx := fun x => x = x

[Robert Maxton]

Which yes, isn't particularly useful in this specific case, but if you imagine some more complicated sequence like

example (h : ∀ (a b c : Nat), ((a + b) + c) = (a + (b + c))) : True := by
  conv at h =>
    enter [a, b, c, 1, 1]
    capture ab
  sorry

Now you can generate a function that represents a + b for any a, b from your conv target. In general it gets more useful the more complicated your target is -- it was conceived because I got tired of writing long change or convert lines >.>;

[Kyle Miller]

If there were some term elaborator that could refer to a metavariable in an incompatible context and close the incompatible free variables, you could get this to work:

example (h : ∀ (a b c : Nat), ((a + b) + c) = (a + (b + c))) : True := by
  conv at h =>
    enter [a, b, c, 1, 1]
    change ?ab
  let ab := ?ab
  /-
  synthetic hole has already been defined and assigned to value incompatible with the current context
    a + b
  -/

[Robert Maxton]

In simpler cases (i.e. ones without funext), that already works when you write it out like that; I just don't see a way to turn it into a single tactic that exits conv mode for you and does one last thing in the 'outside' context before it terminates.

[Kyle Miller]

Maybe it would be helpful to have some realistic examples with what you'd want to see happen (before/after goal states)

[Robert Maxton]

With the funext, things are somewhat harder, but I think it should basically be a matter of looking at the captured local context of the saved metavariable, comparing it to the "new" context (context outside the original conv environment), and then using one of the mkLambdaFVars series to create an appropriate new definition

[Robert Maxton]

Kyle Miller said:

Maybe it would be helpful to have some realistic examples with what you'd want to see happen (before/after goal states)

Unfortunately, kinda by definition all the realistic examples involve a whole bunch of leadup/complexity ^.^; I'll try and come up with something, though.

[Aaron Liu]

I think this would be useful! There have been many times I have wanted to traverse into an expression and "capture" a long complicated form.

[Robert Maxton]

But mostly, the short answer is that what I want is pretty much exactly what you have up there, modulo whatever is necessary to make it work inside binders, so that I can abstract away some annoying complicated expression that also repeats many times.

Oh, I know. Functor application. One sec.

[Robert Maxton]

... Okay, this doesn't quite work, but it's at least very similar to an example I've actually run into:

import Mathlib.CategoryTheory.Equivalence

open CategoryTheory
universe v₂ v₁ u₂ u₁

variable {C D} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D]
         (ε : C ≌ D)


example {X Y : C} : True := by
  let ffffff (f : X ⟶ Y) := ε.functor.map <| ε.inverse.map <| ε.functor.map <| ε.inverse.map <| ε.functor.map f
  conv at ffffff =>
    enter [f]
    lhs
    change ?X'
  set X' := ?X'

[Robert Maxton]

In practice the long chain of applications on both objects of the hom isn't quite so easily removed as repeated functor-inverse pairs, and I'd really like to be able to just eat them into an ε f for some ε : (X ⟶ Y) -> ...

[Robert Maxton]

Not least because in that form, it tends to be a lot easier to rewrite or operate on ε and ε f; much less dependent typing to get in the way

[Robert Maxton]

(I have no idea why conv is complaining here when we try to enter the body of ffffff)

[Aaron Liu]

Robert Maxton said:

(I have no idea why conv is complaining here when we try to enter the body of ffffff)

That's a bug in conv! conv assumes that all dependent functions are "forall" statements, and tries to apply docs#forall_congr, which only works for Prop-valued motives.

[Robert Maxton]

Ahh, instead of trying to use hfunext?
Okay, good to know.