Help on metaprogramming

Stream: metaprogramming / tactics

[Andrew Yang]

To introduce better notation for restriction of sheaves, I need a tactic that can discharge a goal of type U ≤ V. I would like to do this via approximating the transitive closure of the lemmas in the local context and also some tagged lemmas. This is what I have now

import topology.sheaves.presheaf

@[user_attribute]
meta def restrict_attr : user_attribute (tactic unit → tactic unit) unit :=
{ name      := `sheaf_restrict,
  descr     := "tag lemmas to use in `presheaf.restrict_tac`",
  cache_cfg :=
  { mk_cache := λ ns, pure $ λ t, do
    { ctx <- tactic.local_context,
      ctx.any_of (tactic.focus1 ∘ (tactic.apply >=> (λ _, tactic.done)) >=> (λ _, t)) <|>
      ns.any_of (tactic.focus1 ∘ (tactic.resolve_name >=> tactic.to_expr >=> tactic.apply >=>
        (λ _, tactic.done)) >=> (λ _, t)) },
    dependencies := [] } }

meta def restrict_tac : Π (n : ℕ), tactic unit
| 0 := tactic.fail "`restrict_tac` failed"
| (n + 1) := monad.join (restrict_attr.get_cache <*> pure tactic.done) <|>
    `[tactic.transitivity, mjoin (restrict_attr.get_cache <*> pure (restrict_tac n))]

attribute [sheaf_restrict] bot_le le_top le_refl inf_le_left inf_le_right le_sup_left le_sup_right

example {α} [complete_lattice α] {v w x y z : α} (h₀ : v ≤ x) (h₁ : x ≤ z ⊓ w) (h₂ : x ≤ y ⊓ z) :
  v ≤ y := by restrict_tac 5

Since this is my first time doing metaprogramming in lean, I have some questions:
Does this do what I think it does? Is there a better way to achieve this? Does the exponential behavior make it unusable in the long run?
And also I would expect the orelse to shortcut when the first argument succeeds, so it shouldn't matter a lot what large number I put, but it seems like that's not the case. What am I missing?

[Andrew Yang]

Update: It breaks when the example is changed to

example {X : Top} {v w x y z : opens X} (h₀ : v ≤ x) (h₁ : x ≤ z ⊓ w) (h₂ : x ≤ y ⊓ z) :
  v ≤ y := by restrict_tac 5

But I'm not sure why. I changed apply to apply' and the error persists.

[Andrew Yang]

Ah it seems like

example {X : Top} {v w x y z : opens X} (h₀ : v ≤ x) (h₁ : x ≤ z ⊓ w) (h₂ : x ≤ y ⊓ z) :
  v ≤ y := by { transitivity, }

breaks already and it is not my fault.

[Eric Wieser]

(note there is a #metaprogramming / tactics stream; do you want a Zulip moderator to move this topic there?)

[Notification Bot]

This topic was moved here from #general > Help on metaprogramming by Mario Carneiro.