Experimenting with a new tactic - unknown tag

Stream: new members

[Michael Bucko]

I am writing a tactic build_connect_line_no_hashing_direct_construction and somehow always getting unknown attribute [build_connect_line_no_hashing_direct_construction], even though the attribute registration code goes first.

What am I doing wrong?

import Lean
import Mathlib

open Lean Meta Elab Tactic

initialize buildAttr : ParametricAttribute Unit ←
  registerParametricAttribute {
    name := `build
    descr := "Build by connecting two concepts"
    getParam := fun _ _ => pure ()
  }

elab "build_connect_line_no_hashing_direct_construction" : tactic => do
  let env ← getEnv
  let entries := buildAttr.ext.getState env
  let decls := entries.toList.map (·.1)
  let goal ← getMainGoal
  let axiomsTypes ← decls.mapM fun decl => do
    let cinfo ← liftMetaM (getConstInfo decl)
    pure cinfo.type
  if axiomsTypes.isEmpty then return
  let allAxioms ← axiomsTypes.foldlM (init := axiomsTypes.head!) fun acc newTy => do
    let accType ← liftMetaM (whnf acc)
    let newType ← liftMetaM (whnf newTy)
    liftMetaM (mkAppM ``And #[accType, newType])
  let placeholderProp := mkForall Name.anonymous BinderInfo.default (mkConst ``False) (mkConst ``False)
  liftMetaM (goal.assign (mkForall Name.anonymous BinderInfo.default allAxioms placeholderProp))
  let goals ← getGoals
  match goals with
  | [g] => do
    let (_, g1) ← liftMetaM (g.intro1)
    let (_, g2) ← liftMetaM (g1.intro1)
    let g2Type ← liftMetaM (g2.getType)
    let sorryExpr ← liftMetaM (mkSorry g2Type true)
    let newGoals ← liftMetaM (g2.apply sorryExpr)
    setGoals newGoals
  | _ => pure ()

def is_k_almost_prime (k n : Nat) : Bool :=
  n > 1 && n.factorization.sum (fun _ multiplicity => multiplicity) == k

def is_k_almost_prime_prop (k n : Nat) : Prop :=
  is_k_almost_prime k n = true

noncomputable def nth_k_almost_prime (k i : Nat) : Nat :=
  Classical.epsilon (fun n =>
    is_k_almost_prime_prop k n ∧
    (((List.range (n+1)).filter (is_k_almost_prime k)).length = i+1)
  )

noncomputable def almost_prime_table (k i : Nat) : Nat :=
  nth_k_almost_prime (k+1) i

def col_has_power (k power : Nat) : Prop :=
  ∃ i, almost_prime_table k i = power

noncomputable instance (k power : Nat) : Decidable (col_has_power k power) :=
  Classical.propDecidable _

noncomputable def find_power_index (k power : Nat) : Option Nat :=
  if h : col_has_power k power then
    some (Nat.find h)
  else
    none

noncomputable def red_diamond_sequence_column (k : Nat) : Set Nat :=
  let currentPower := 3^(k+1)
  let nextPower := 3^(k+2)
  match find_power_index (k+1) nextPower with
  | some r => { n | n ≥ currentPower ∧ ∃ i, i < r ∧ almost_prime_table k i = n }
  | none   => { n | n ≥ currentPower ∧ ∃ i, almost_prime_table k i = n }

@[build_connect_line_no_hashing_direct_construction]
axiom red_diamond_conjecture_infinite : ∀ k,
  (∀ r, find_power_index (k+1) (3^(k+2)) = some r →
    almost_prime_table (k+1) r = 3^(k+2) ∧
    (∀ i, i < r → almost_prime_table k i ∈ red_diamond_sequence_column k))

@[build_connect_line_no_hashing_direct_construction]
axiom beal_conjecture :
  ∀ x y z : ℕ, x > 2 → y > 2 → z > 2 →
  ∀ A B C : ℕ, A > 0 → B > 0 → C > 0 →
  A ^ x + B ^ y = C ^ z →
  Finset.gcd {A, B, C} id > 1

@[build_connect_line_no_hashing_direct_construction]
axiom abc_conjecture :
  ∀ (ε : ℝ) (_ : 0 < ε), ∃ (K : ℝ),
    ∀ (a b c : ℕ), a > 0 → b > 0 → c > 0 →
    a + b = c →
    gcd a b = 1 →
    (↑c : ℝ) < K * Real.rpow (↑(Nat.primeFactorsList (a * b * c)).prod) (1 + ε)

[Damiano Testa]

I have not tried to see if this is the case, but attributes can only be used in a file in which their definition is imported: the file that defines an attribute should not have access to the attribute itself.

[Michael Bucko]

(Thank you @Damiano Testa . Testing this -- but having some problems with the toolchain, so it's taking some time)

[Michael Bucko]

@Damiano Testa Divided the code into two files (below), but I am still getting the same thing (nonetheless, your point is still good, and I was not aware of that).

import Lean
import Mathlib
import build_connect_line_no_hashing_direct_construction

open Lean Meta Elab Tactic

@[build_connect_line_no_hashing_direct_construction]
axiom red_diamond_conjecture_infinite : ∀ k,
  (∀ r, find_power_index (k+1) (3^(k+2)) = some r →
    almost_prime_table (k+1) r = 3^(k+2) ∧
    (∀ i, i < r → almost_prime_table k i ∈ red_diamond_sequence_column k))

@[build_connect_line_no_hashing_direct_construction]
axiom beal_conjecture :
  ∀ x y z : ℕ, x > 2 → y > 2 → z > 2 →
  ∀ A B C : ℕ, A > 0 → B > 0 → C > 0 →
  A ^ x + B ^ y = C ^ z →
  Finset.gcd {A, B, C} id > 1

@[build_connect_line_no_hashing_direct_construction]
axiom abc_conjecture :
  ∀ (ε : ℝ) (_ : 0 < ε), ∃ (K : ℝ),
    ∀ (a b c : ℕ), a > 0 → b > 0 → c > 0 →
    a + b = c →
    gcd a b = 1 →
    (↑c : ℝ) < K * Real.rpow (↑(Nat.primeFactorsList (a * b * c)).prod) (1 + ε)

and build_connect_line_no_hashing_direct_construction.lean

import Lean
import Mathlib

open Lean Meta Elab Tactic

initialize buildAttr : ParametricAttribute Unit ←
  registerParametricAttribute {
    name := `build
    descr := "Build by connecting two concepts"
    getParam := fun _ _ => pure ()
  }

elab "build_connect_line_no_hashing_direct_construction" : tactic => do
  let env ← getEnv
  let entries := buildAttr.ext.getState env
  let decls := entries.toList.map (·.1)
  let goal ← getMainGoal
  let axiomsTypes ← decls.mapM fun decl => do
    let cinfo ← liftMetaM (getConstInfo decl)
    pure cinfo.type
  if axiomsTypes.isEmpty then return
  let allAxioms ← axiomsTypes.foldlM (init := axiomsTypes.head!) fun acc newTy => do
    let accType ← liftMetaM (whnf acc)
    let newType ← liftMetaM (whnf newTy)
    liftMetaM (mkAppM ``And #[accType, newType])
  let placeholderProp := mkForall Name.anonymous BinderInfo.default (mkConst ``False) (mkConst ``False)
  liftMetaM (goal.assign (mkForall Name.anonymous BinderInfo.default allAxioms placeholderProp))
  let goals ← getGoals
  match goals with
  | [g] => do
    let (_, g1) ← liftMetaM (g.intro1)
    let (_, g2) ← liftMetaM (g1.intro1)
    let g2Type ← liftMetaM (g2.getType)
    let sorryExpr ← liftMetaM (mkSorry g2Type true)
    let newGoals ← liftMetaM (g2.apply sorryExpr)
    setGoals newGoals
  | _ => pure ()