The theorem_wanted, def_wanted, and instance_wanted commands

Use theorem_wanted name binders : T to mark a theorem the library should eventually contain without blocking compilation; def_wanted name binders : T does the same for any Sort, not just Prop. Each elaborates to a private placeholder def name binders : ProofWanted T := ⟨⟩ (resp. DefWanted T), so the wanted result is visible to downstream files and tools by type rather than by side-channel. proof_wanted is a synonym for theorem_wanted.

Inside any of these commands, ❰foo❱ references an earlier wanted declaration; for parametrised foo, write ❰foo❱ x y to apply it. The brackets desugar to fresh parameter binders, so the dependency appears in the recorded type. When the referenced wanted's payload is a typeclass, the generated parameter is an instance binder, so Lean's instance synth can pick it up at use sites (including via Π-instance synth when chained through another wanted).

instance_wanted name : ClassT is a variant of def_wanted whose payload must be a typeclass and whose declared name is registered file-locally: every later wanted automatically picks up an […] instance binder for it, without an explicit ❰…❱ reference.

A body may be supplied with ... := body; it must reference at least one ❰…❱ (in the statement or the body). A complete proof, construction, or instance should be a theorem, def, or instance instead, and the error includes a Try this: suggestion to that effect.

The ❰ and ❱ characters (U+2770, U+2771) are entered as \h< and \h> with the standard Lean input method.

structure ProofWanted (α : Sort u) : Type

Wrapper recording that a proof_wanted of statement α has been declared.

@[reducible]

def ProofWanted.Stmt {α : Sort u} : ProofWanted α → Sort u

Reducible accessor so a binder of type ProofWanted.Stmt foo reduces to foo's statement. Used by the desugaring of ❰foo❱ when foo is a proof_wanted.

Equations

• x✝.Stmt = α

structure DefWanted (α : Sort u) : Type

Wrapper recording that a def_wanted of type α has been declared.

@[reducible]

def DefWanted.Val {α : Sort u} : DefWanted α → Sort u

Reducible accessor so a binder of type DefWanted.Val foo reduces to foo's type. Used by the desugaring of ❰foo❱ when foo is a def_wanted.

Equations

• x✝.Val = α

def wantedRef : Lean.ParserDescr

Internal bracket syntax ❰foo❱ for referencing an earlier theorem_wanted or def_wanted. Only meaningful inside the statement or body of one of those commands; the term elaborator errors everywhere else.

Equations

• One or more equations did not get rendered due to their size.

def elabWantedRef : Lean.Elab.Term.TermElab

Elaborator that errors when ❰…❱ is used outside a wanted-declaration command.

Equations

• elabWantedRef x✝¹ x✝ = Lean.throwError (Lean.toMessageData "`❰…❱` may only appear inside the statement or body of `theorem_wanted`, `proof_wanted`, `def_wanted`, or `instance_wanted`")

def theorem_wanted : Lean.Parser.Parser

This proof would be a welcome contribution to the library!

The syntax of theorem_wanted declarations is just like that of theorem. Without := and a proof body it records a wanted theorem; with one it records a partial proof that still depends on other wanted lemmas. Lean checks that theorem_wanted declarations are well-formed (e.g. it ensures that all the mentioned names are in scope, and that the theorem statement is a valid proposition), and records a private placeholder declaration of type ... → ProofWanted statement.

Modifiers (such as @[simp]) are accepted for syntactic compatibility with theorem but are currently ignored.

proof_wanted is a synonym for theorem_wanted.

Inside another theorem_wanted or def_wanted, write ❰foo❱ to reference an earlier theorem_wanted or def_wanted named foo. The bracket may appear in the statement or the body, and each distinct reference becomes a fresh parameter binder of the matching type. For parametrised foo : ∀ args, ProofWanted _, the binder type is itself Π-quantified, so ❰foo❱ x y applies the parameter to x y. ❰foo❱ only resolves names within the current file, since the placeholders are private.

A body must reference at least one ❰…❱ (in the statement or the body); otherwise the body is a complete proof and the declaration should be a theorem.

Typical usage:

-- A parameterless wanted fact:
theorem_wanted size_of_two_pushes_onto_empty :
    ((#[] : Array Nat).push 1 |>.push 2).size = 2

-- Referencing an earlier `theorem_wanted` inside a statement (here in the `Fin`
-- bound proof, which rewrites by the wanted fact):
theorem_wanted first_index_after_two_pushes :
    (⟨0, by rw [❰size_of_two_pushes_onto_empty❱]; decide⟩
      : Fin ((#[] : Array Nat).push 1 |>.push 2).size).val = 0

-- A parametrised wanted fact:
theorem_wanted size_after_two_pushes {α : Type _} (a : Array α) (x y : α) :
    ((a.push x).push y).size = a.size + 2

-- Referencing the parametrised wanted with arguments: `❰foo❱ a x y`.
theorem_wanted index_after_two_pushes {α : Type _} (a : Array α) (x y : α) :
    (⟨a.size, by rw [❰size_after_two_pushes❱ a x y]; omega⟩
      : Fin ((a.push x).push y).size).val = a.size

-- A partial proof may be supplied with `:= body`, deferring the harder step via `❰…❱`:
theorem_wanted size_after_three_pushes {α : Type _} (a : Array α) (x y z : α) :
    (((a.push x).push y).push z).size = a.size + 3 := by
  rw [Array.size_push, ❰size_after_two_pushes❱ a x y]

Equations

• One or more equations did not get rendered due to their size.

def proof_wanted : Lean.Parser.Parser

proof_wanted is a synonym for theorem_wanted; see its documentation. (It is expected to be deprecated in favour of theorem_wanted eventually.)

Equations

• One or more equations did not get rendered due to their size.

def def_wanted : Lean.Parser.Parser

This construction would be a welcome contribution to the library!

The syntax mirrors theorem_wanted but admits any Sort (not just Prop). It records a placeholder declaration of type ... → DefWanted type and accepts the same ❰…❱ bracket syntax for cross-referencing earlier theorem_wanted or def_wanted declarations, including parametrised ones — ❰foo❱ x y applies foo's parameters. A partial body may be supplied with ... := body; as with theorem_wanted, a body without any ❰…❱ reference is rejected with an actionable "Try this:" suggesting def.

Modifiers (such as @[simp]) are accepted for syntactic compatibility with def but are currently ignored.

Typical usage:

def_wanted decision_procedure (n : Nat) : Decidable (Nat.Prime n)

def_wanted prime_dec_3 : Decidable (Nat.Prime 3) := ❰decision_procedure❱ 3

Equations

• One or more equations did not get rendered due to their size.

def elabTheoremWanted : Lean.Elab.Command.CommandElab

Parses the surface syntax of theorem_wanted and forwards to the shared elabWanted.

Equations

• One or more equations did not get rendered due to their size.

def elabProofWanted : Lean.Elab.Command.CommandElab

Parses the surface syntax of proof_wanted (a synonym for theorem_wanted) and forwards to the shared elabWanted.

Equations

• One or more equations did not get rendered due to their size.

def elabDefWanted : Lean.Elab.Command.CommandElab

Parses the surface syntax of def_wanted and forwards to the shared elabWanted.

Equations

• One or more equations did not get rendered due to their size.

def instance_wanted : Lean.Parser.Parser

This typeclass instance would be a welcome contribution to the library!

The syntax mirrors instance (the name is optional, auto-generated from the class head if absent) and the payload must be a typeclass. The placeholder is recorded as DefWanted (TheClass …) like def_wanted, but additionally the declared name is registered so every subsequent theorem_wanted / def_wanted / instance_wanted automatically picks up a [d_…] instance binder for it. Lean's typeclass synth then resolves uses of the class without an explicit ❰…❱ reference — matching the auto-availability of regular instance declarations.

The registration is module-scoped and order-sensitive: every instance_wanted declared earlier in the current file is auto-included as a binder on every later wanted declaration (without any class-name filtering — opting in via instance_wanted is taken as a request for the instance to be ambient). Registrations persist across section / namespace boundaries within the file and are dropped at module boundaries (the placeholder defs are private, so nothing propagates to importers).

Typical usage:

def_wanted Jacobian (C : Over (Spec (.of k))) [IsProper C.hom] : Over (Spec (.of k))

instance_wanted : GrpObj (❰Jacobian❱ C)

theorem_wanted comp_ofCurve … : … = η[❰Jacobian❱ C]
  -- automatically picks up the GrpObj instance, no haveI needed

Equations

• One or more equations did not get rendered due to their size.

def elabInstanceWanted : Lean.Elab.Command.CommandElab

Parses the surface syntax of instance_wanted, generates a name if absent, forwards to the shared elabWanted, validates the payload is a typeclass, and registers the declared name in wantedInstancesExt so subsequent wanted declarations auto-include it.

Equations

• One or more equations did not get rendered due to their size.