The proof_wanted command

Use proof_wanted name binders : T to mark a theorem the library should eventually contain without blocking compilation. The declaration elaborates to a private placeholder def name binders : ProofWanted T := ⟨⟩, so the wanted result is visible to downstream files and tools by type rather than by side-channel.

Inside another proof_wanted statement, ❰foo❱ references an earlier proof_wanted; for parametrised foo, write ❰foo❱ x y to apply it. The brackets desugar to fresh hypothesis binders, so the dependency appears in the recorded type.

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❱.

Equations

• x✝.Stmt = α

def proofWantedRef : Lean.ParserDescr

Internal bracket syntax ❰foo❱ for referencing an earlier proof_wanted. Only meaningful inside the statement of a proof_wanted; the term elaborator errors everywhere else.

Equations

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

def elabProofWantedRef : Lean.Elab.Term.TermElab

Elaborator that errors when ❰…❱ is used outside a proof_wanted statement.

Equations

• elabProofWantedRef x✝¹ x✝ = Lean.throwError (Lean.toMessageData "`❰…❱` may only appear inside the statement of `proof_wanted`")

def proof_wanted : Lean.Parser.Parser

This proof would be a welcome contribution to the library!

The syntax of proof_wanted declarations is just like that of theorem, but without := or the proof. Lean checks that proof_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.

Inside another proof_wanted's statement, write ❰foo❱ to assume an earlier proof_wanted named foo. The bracket may only appear inside the statement, since there is no proof body. It desugars to a fresh hypothesis 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.

Typical usage:

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

-- Referencing an earlier `proof_wanted` inside a statement (here in the `Fin`
-- bound proof, which rewrites by the wanted fact):
proof_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:
proof_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`.
proof_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

Equations

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

def elabProofWanted : Lean.Elab.Command.CommandElab

Elaborate a proof_wanted declaration into a private placeholder def of type ProofWanted, expanding any ❰…❱ references to fresh hypothesis binders.

Equations

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