FormalConjecturesUtil/Answer.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

12 declarations, 1 contain sorry, 0 declared as axioms

The answer( ) elaborator

This file provides syntax for marking up answers in a problem statement.

Note: certain problems also providing an answer, and can be formalised using answer(sorry) as a placeholder. While providing a proof simply requires finding any way to replace := sorry, providing an answer is not just finding any way to replace answer(sorry): it requires evaluation of mathematical meaning, which is a job for human mathematicians, not Lean alone.

Imports (3)
Imported by 4 files
  1. inductive Google.AnswerSetting A type that captures the current setting for the answer() elaborator line 43 source

    Source documentation

    A type that captures the current setting for the answer() elaborator.

    no axioms what this means

    inductive AnswerSetting
  /--Default mode: `answer(sorry)` defaults to `True` when `sorry` has type `Prop`. -/
  | alwaysTrue
  /-- Default mode for `answer(foo)`: just postpones elaboration. -/
  | postpone
  /-- Elaborate `answer(foo)` by creating an auxiliary definition with value `foo`. -/
  | withAuxiliary
deriving Inhabited, ToJson, BEq

    Mentions: foo

  2. instance Google.(instance at line 52) line 52 source
  3. instance Google.(instance at line 58) line 58 source
  4. def Google.mkAnswerAnnotation line 71 source

    no axioms what this means

    Statement uses: Lean.Expr

    Proof uses: Lean.mkAnnotation, Lean.Name.mkStr1

  5. def Google.findAnswerExpr Find the first subexpression carrying the answer annotation, returning the inner (unwrapped) expression if found line 75 source

    Source documentation

    Find the first subexpression carrying the answer annotation, returning the inner (unwrapped) expression if found.

    standard axioms: propext what this means

    Statement uses: Lean.Expr, Option

    Proof uses: Option.map, Lean.Expr.mdataExpr!, Lean.Expr.find?, Bool, Lean.MData, Lean.KVMap.contains, Lean.Name.mkStr1, Bool.false

    1 instances, coercions and auxiliary constants left out.

    def findAnswerExpr (e : Expr) : Option Expr :=
…
  6. def Google.findAnswerExprs Collect all subexpressions carrying the answer annotation, returning the inner (unwrapped) expressions line 82 source

    Source documentation

    Collect all subexpressions carrying the answer annotation, returning the inner (unwrapped) expressions.

    no axioms what this means

    Statement uses: Lean.Expr, Array

    Proof uses: List.toArray, List.nil

    1 instances, coercions and auxiliary constants left out.

    partial def findAnswerExprs (e : Expr) : Array Expr :=
…
  7. def Google.elabTermAndAnnotate line 95 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, Option, Lean.Expr, optParam, Bool, Bool.false, Lean.Elab.Term.TermElabM

    Proof uses: Functor.map, Lean.Elab.Term.Context, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Google.mkAnswerAnnotation, ite, Eq, Bool.true, Bind.bind, Lean.SourceInfo, Lean.MonadRef.mkInfoFromRefPos, Lean.MacroScope, Lean.MonadQuotation.getCurrMacroScope, Lean.Name, Lean.MonadQuotation.getContext, Pure.pure, Lean.TSyntax.mk, Lean.Syntax.node2 and 6 more

    11 instances, coercions and auxiliary constants left out.

  8. def Google.mkCanonicalSorryAnnotation Construct a canonical sorryAx application with a stable, module-independent tag line 107 source

    Source documentation

    Construct a canonical sorryAx application with a stable, module-independent tag. Unlike Lean's built-in sorry macro, this does not embed the current module name via hygiene, so the resulting expression is identical regardless of whether the file is compiled as Challenge or Solution.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Lean.Expr, Lean.Elab.Term.TermElabM

    Proof uses: Bind.bind, liftM, ReaderT, Lean.Meta.Context, StateRefT', IO.RealWorld, Lean.Meta.State, Lean.Core.CoreM, Lean.Elab.Term.Context, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Meta.mkSorry, Bool.false, Pure.pure, Google.mkAnswerAnnotation

    10 instances, coercions and auxiliary constants left out.

    def mkCanonicalSorryAnnotation (expectedType : Expr) : TermElabM Expr := do
…
  9. def Google.answerElab Indicates where the answer is in a problem statement sorry line 113 source

    Source documentation

    Indicates where the answer is in a problem statement.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Lean.Elab.Term.TermElab

    Proof uses: Lean.Syntax, Option, Lean.Expr, ite, Lean.Elab.Term.TermElabM, Eq, Bool, Lean.Syntax.isOfKind, Lean.Name.mkStr2, Bool.true, Lean.Syntax.getArg, OfNat.ofNat, Nat, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, Lean.TSyntax.mk, Bind.bind and 73 more

    37 instances, coercions and auxiliary constants left out.

    def answerElab : TermElab := fun stx expectedType? => do
…
  10. structure Google.AnswerInfo An answer: a term, and the context in which it was elaborated line 157 source

    Source documentation

    An answer: a term, and the context in which it was elaborated

    standard axioms: Classical.choice, Quot.sound, propext what this means

    structure AnswerInfo where
…
  11. def Google.AnswerInfo.format Print an answer line 162 source

    Source documentation

    Print an answer

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Google.AnswerInfo, Lean.Elab.Term.TermElabM, Lean.MessageData

    Proof uses: Lean.Meta.withMCtx, Lean.Meta.MetaM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Elab.Term.Context, Lean.Meta.Context, Lean.Meta.State, Lean.Core.CoreM, Lean.Elab.CommandContextInfo.mctx, Lean.Elab.ContextInfo.toCommandContextInfo, Google.AnswerInfo.ctx, Lean.Meta.withLCtx, Lean.Elab.TermInfo.lctx, Google.AnswerInfo.term, EmptyCollection.emptyCollection, Lean.LocalInstances, Lean.LocalInstance, Bind.bind, Lean.Expr and 15 more

    28 instances, coercions and auxiliary constants left out.

    def AnswerInfo.format (a : AnswerInfo) : Elab.Term.TermElabM MessageData :=
…

    Mentions: Google.AnswerInfo

  12. def Google.getAnswers Find answers by inspecting an InfoTree line 169 source

    Source documentation

    Find answers by inspecting an InfoTree

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Monad, Lean.Elab.InfoTree, Array, Google.AnswerInfo

    Proof uses: Option.none, Lean.Elab.ContextInfo

    1 instances, coercions and auxiliary constants left out.

    partial def getAnswers {m} [Monad m] (i : InfoTree) : m (Array AnswerInfo) :=
…

    Mentions: Google.AnswerInfo