Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Help on metaprogramming


Andrew Yang (Oct 09 2022 at 06:05):

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 (Oct 09 2022 at 06:27):

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 (Oct 09 2022 at 06:29):

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 (Oct 10 2022 at 02:08):

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

Notification Bot (Oct 10 2022 at 02:10):

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


Last updated: Dec 20 2023 at 11:08 UTC