attribute DIY

Stream: lean4

[Asei Inoue]

I created a custom tactic (for curiosity) inspired by gcongr in Mathlib as follows:

syntax "compatible" : tactic

macro_rules
  | `(tactic| compatible) => `(tactic| apply Nat.add_le_add_left <;> assumption)

macro_rules
  | `(tactic| compatible) => `(tactic| apply Nat.add_le_add_right <;> assumption)

macro_rules
  | `(tactic| compatible) => `(tactic| apply Nat.add_le_add <;> assumption)

example {m n : Nat} (h : n ≤ m) (l : Nat) : l + n ≤ l + m := by
  compatible

example {m n : Nat} (h : m ≤ n) (l : Nat) : m + l ≤ n + l := by
  compatible

example {m n a b : Nat} (h1 : m ≤ n) (h2 : a ≤ b) : m + a ≤ n + b := by
  compatible

This works fine for now. However, it is inconvenient to use the macro_rules command every time I need to register a rule.
Would it be possible to create a [compatible] attribute to simplify the registration of lemmas?

[Aaron Liu]

Yes

[Asei Inoue]

Sorry my bad question.... How can I create such an attribute?

[Aaron Liu]

You can use the ext tactic as an example, it is defined in Init.Ext, Lean.Meta.Tactic.Ext, and Lean.Elab.Tactic.Ext.

[Adam Topaz]

It's a bit different from most other things you do in lean. You need to do something like the following in one file:

import Lean

open Lean
initialize compatibleAttr : TagAttribute ←
  registerTagAttribute `compatible "Description goes here"

bit you can't use the attribute in the same file.

[Adam Topaz]

You can then use docs#Lean.TagAttribute.hasTag to check if a declaration has the attribute.

[Adam Topaz]

If you need more complicated elaboration for the attribute itself, then you can start to dig in registerTagAttribute to see how to do in the most general way possible.

[Asei Inoue]

@Adam Topaz

what initialize command does?

[Asei Inoue]

Step1.lean

import Lean

open Lean

initialize compatibleAttr : TagAttribute ←
  registerTagAttribute `compatible "compatible attribute"

[Asei Inoue]

Step2.lean

import Step1


open Lean Meta

structure CompatibleTheorem where
  declName : Name
  deriving Inhabited

structure CompatibleTheorems where
  tree : DiscrTree CompatibleTheorem := {}
  erased   : PHashSet Name := {}
  deriving Inhabited

initialize compatibleExtension :
    SimpleScopedEnvExtension CompatibleTheorem CompatibleTheorems ←
  registerSimpleScopedEnvExtension {
    addEntry := sorry
    initial := {}
  }

def getCompatibleTheorems (ty : Expr) : MetaM (Array Name) := do
  let compatibleTheorems := compatibleExtension.getState (← getEnv)
  let arr := compatibleTheorems.tree.getMatch ty
  sorry

[Asei Inoue]

how to implement addEntry function?

[Asei Inoue]

what data structure should I use in addEntry...?