Communicate between successive tactics

Stream: metaprogramming / tactics

[Anatole Dedecker]

What is the best way to transfer data between two different tactic calls? More specifically, I want to make two tactics A and B such that A creates some metavariables, and then B retrieves those metavariables and do things with them, possibly with many tactics invocation in between. I suppose I could use tags to find them back, but that seems like a hacky solution (and I'm not actually sure it even works)

[Jannis Limperg]

You could maybe store the mvars as types of hidden hypotheses in the context. What's the specific use case? (Also, Lean 3 or 4?)

[Anatole Dedecker]

It’s for Lean 4. I am thinking about making a version of filter_upwards that is more flexible in that you don’t have to provide all hypotheses you want to make (as in "we can assume this and this and that because these are all true in a neighborhood of x_0") all at once, and you can instead add them incrementally, which makes it more intuitive

[Anatole Dedecker]

And the way I want to do that is by having metavariables for the list of assumptions made, that I can partially instantiate when the user makes a new assumption, and eventually instantiate the remaining one with true when we no longer have assumptions to make

[Kyle Miller]

Maybe you could have some special kind of tactic block that keeps track of a certain list of goal metavariables? Like perhaps your filter_upwards has syntax that allows any number of tactics to follow it (along with, possibly, one last thing for finally filling in these lingering goals)

[Anatole Dedecker]

Here is an example I did "by hand" in Lean3 (so it looks very messy). Each "block" in this proof should become one tactic call, and ideally I'd use metavariables instead of goals so that this is not too frightening for the user.

import order.filter.basic

open set filter function list

variables {α β : Type*} {f : filter α} {p q r : α → Prop}

lemma test (hp : ∀ᶠ x in f, p x) (hpq : ∀ᶠ x in f, p x → q x) (hqr : ∀ᶠ x in f, q x → r x) :
  ∀ᶠ x in f, r x :=
begin
  let _U : list (set α) := _,
  have _hU : ∀ s ∈ _U, s ∈ f := _,
  have _key : foldr (∩) (univ : set α) _U ∈ f :=
    @foldr_rec_on (set α) (set α) (λ s, s ∈ f) _U (∩) (univ : set α) univ_mem
    (λ s hs t ht, inter_mem (_hU t ht) hs),
  refine mem_of_superset _key (λ x _hx, _),
  dsimp only [mem_set_of],

  work_on_goal 3 { refine (set_of (λ x, q x → r x)) :: _ },
  work_on_goal 2 { refine forall_mem_cons.mpr ⟨hqr, _⟩, },
  rw [foldr_cons] at _hx,
  rcases _hx with ⟨hqrx, _hx⟩,
  dsimp only [mem_set_of] at hqrx,

  apply hqrx,

  work_on_goal 2 { refine (set_of (λ x, p x → q x)) :: _ },
  work_on_goal 3 { refine forall_mem_cons.mpr ⟨hpq, _⟩, },
  rw [foldr_cons] at _hx,
  rcases _hx with ⟨hpqx, _hx⟩,
  dsimp only [mem_set_of] at hpqx,

  apply hpqx,

  work_on_goal 2 { refine (set_of p) :: _ },
  work_on_goal 3 { refine forall_mem_cons.mpr ⟨hp, _⟩, },
  rw [foldr_cons] at _hx,
  rcases _hx with ⟨hpx, _hx⟩,
  dsimp only [mem_set_of] at hpx,

  exact hpx,

  exact nil,
  exact forall_mem_nil _
end

[Anatole Dedecker]

Kyle Miller said:

Maybe you could have some special kind of tactic block that keeps track of a certain list of goal metavariables? Like perhaps your filter_upwards has syntax that allows any number of tactics to follow it (along with, possibly, one last thing for finally filling in these lingering goals)

Oh I didn't think about doing that as one syntax for everything, that could probably work