opaque auto.getHints.failOnParseError : Lean.Option Bool

def auto.getHints.getFailOnParseError (opts : Lean.Options) : Bool

Equations

• auto.getHints.getFailOnParseError opts = Lean.Option.get opts auto.getHints.failOnParseError

def auto.getHints.getFailOnParseErrorM : Lean.CoreM Bool

Equations

• auto.getHints.getFailOnParseErrorM = do let opts ← Lean.getOptions pure (auto.getHints.getFailOnParseError opts)

def Auto.hintelem : Lean.ParserDescr

* : LCtxHyps, * <ident> : Lemma database

Equations

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

def Auto.hints : Lean.ParserDescr

Equations

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

def Auto.unfolds : Lean.ParserDescr

Specify constants to unfold. unfolds Must not contain cyclic dependency

Equations

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

def Auto.defeqs : Lean.ParserDescr

Specify constants to collect definitional equality for

Equations

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

def Auto.uord : Lean.ParserDescr

Equations

• Auto.uord = Lean.ParserDescr.nodeWithAntiquot "uord" `Auto.uord (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.unary `atomic Auto.unfolds) Auto.defeqs)

def Auto.autoinstr : Lean.ParserDescr

Equations

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

def Auto.auto : Lean.ParserDescr

Equations

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

def Auto.mononative : Lean.ParserDescr

Equations

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

def Auto.mono : Lean.ParserDescr

Equations

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

inductive Auto.Instruction : Type

• none : Instruction
• useSorry : Instruction

def Auto.parseInstr : Lean.TSyntax `Auto.autoinstr → Lean.Elab.Tactic.TacticM Instruction

Equations

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

inductive Auto.HintElem : Type

• term : Lean.Term → HintElem
• lemdb : Lean.Name → HintElem
• lctxhyps : HintElem

instance Auto.instInhabitedHintElem : Inhabited HintElem

Equations

• Auto.instInhabitedHintElem = { default := Auto.instInhabitedHintElem.default }

def Auto.instInhabitedHintElem.default : HintElem

Equations

• Auto.instInhabitedHintElem.default = Auto.HintElem.term default

def Auto.instBEqHintElem.beq : HintElem → HintElem → Bool

Equations

• Auto.instBEqHintElem.beq (Auto.HintElem.term a) (Auto.HintElem.term b) = (a == b)
• Auto.instBEqHintElem.beq (Auto.HintElem.lemdb a) (Auto.HintElem.lemdb b) = (a == b)
• Auto.instBEqHintElem.beq Auto.HintElem.lctxhyps Auto.HintElem.lctxhyps = true
• Auto.instBEqHintElem.beq x✝¹ x✝ = false

instance Auto.instBEqHintElem : BEq HintElem

Equations

• Auto.instBEqHintElem = { beq := Auto.instBEqHintElem.beq }

def Auto.parseHintElem : Lean.TSyntax `Auto.hintelem → Lean.Elab.Tactic.TacticM HintElem

Equations

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

structure Auto.InputHints : Type

• terms : Array Lean.Term
• lemdbs : Array Lean.Name
• lctxhyps : Bool

instance Auto.instInhabitedInputHints : Inhabited InputHints

Equations

• Auto.instInhabitedInputHints = { default := Auto.instInhabitedInputHints.default }

def Auto.instInhabitedInputHints.default : InputHints

Equations

• Auto.instInhabitedInputHints.default = { terms := default, lemdbs := default, lctxhyps := default }

def Auto.instBEqInputHints.beq : InputHints → InputHints → Bool

Equations

• Auto.instBEqInputHints.beq { terms := a, lemdbs := a_1, lctxhyps := a_2 } { terms := b, lemdbs := b_1, lctxhyps := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Auto.instBEqInputHints.beq x✝¹ x✝ = false

instance Auto.instBEqInputHints : BEq InputHints

Equations

• Auto.instBEqInputHints = { beq := Auto.instBEqInputHints.beq }

def Auto.parseHints : Lean.TSyntax `Auto.hints → Lean.Elab.Tactic.TacticM InputHints

Parse hints to an array of Term, which is still syntax

Equations

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

def Auto.parseUnfolds : Lean.TSyntax `Auto.unfolds → Lean.Elab.Tactic.TacticM (Array Prep.ConstUnfoldInfo)

Equations

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

def Auto.parseDefeqs : Lean.TSyntax `Auto.defeqs → Lean.Elab.Tactic.TacticM (Array Lean.Name)

Equations

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

def Auto.parseUOrD : Lean.TSyntax `Auto.uord → Lean.Elab.Tactic.TacticM (Array Prep.ConstUnfoldInfo ⊕ Array Lean.Name)

Equations

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

def Auto.parseUOrDs (stxs : Array (Lean.TSyntax `Auto.uord)) : Lean.Elab.Tactic.TacticM (Array Prep.ConstUnfoldInfo × Array Lean.Name)

Equations

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

def Auto.collectLctxLemmas (lctxhyps : Bool) (ngoalAndBinders : Array Lean.FVarId) : Lean.MetaM (Array Lemma)

Equations

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

def Auto.collectUserLemmas (terms : Array Lean.Term) : Lean.Elab.Tactic.TacticM (Array Lemma)

Equations

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

def Auto.collectHintDBLemmas (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM (Array Lemma)

Equations

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

def Auto.collectDefeqLemmas (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM (Array Lemma)

Equations

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

def Auto.unfoldConstAndPreprocessLemma (unfolds : Array Prep.ConstUnfoldInfo) (lem : Lemma) : Lean.MetaM Lemma

Equations

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

def Auto.unfoldConstAndprepReduceDefeq (unfolds : Array Prep.ConstUnfoldInfo) (lem : Lemma) : Lean.MetaM Lemma

We assume that all defeq facts have the form ∀ (x₁ : ⋯) ⋯ (xₙ : ⋯), c ... = ... where c is a constant. To avoid whnf from reducing c, we call forallTelescope, then call prepReduceExpr on · All the arguments of c, and · The right-hand side of the equation

Equations

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

def Auto.traceLemmas (traceClass : Lean.Name) (pre : String) (lemmas : Array Lemma) : Lean.CoreM Unit

Equations

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

def Auto.checkDuplicatedFact (terms : Array Lean.Term) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def Auto.checkDuplicatedLemmaDB (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def Auto.collectAllLemmas (hintstx : Lean.TSyntax `Auto.hints) (uords : Array (Lean.TSyntax `Auto.uord)) (ngoalAndBinders : Array Lean.FVarId) : Lean.Elab.Tactic.TacticM (Array Lemma × Array Lemma)

Equations

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

def Auto.queryTPTP (exportFacts : Array Embedding.Lam.REntry) : LamReif.ReifM (Option Lean.Expr × Option (Array Embedding.Lam.REntry))

Equations

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

def Auto.commonPrefix (s t : Substring) : Substring

Returns the longest common prefix of two substrings. The returned substring will use the same underlying string as s.

Note: Code taken from Std

Equations

• Auto.commonPrefix s t = { str := s.str, startPos := s.startPos, stopPos := Auto.commonPrefix.loop s t s.startPos t.startPos }

@[irreducible]

def Auto.commonPrefix.loop (s t : Substring) (spos tpos : String.Pos) : String.Pos

Returns the ending position of the common prefix, working up from spos, tpos.

Equations

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

def Auto.dropPrefix? (s pre : Substring) : Option Substring

If pre is a prefix of s, i.e. s = pre ++ t, returns the remainder t.

Equations

• Auto.dropPrefix? s pre = if (Auto.commonPrefix s pre).bsize = pre.bsize then some { str := s.str, startPos := (Auto.commonPrefix s pre).stopPos, stopPos := s.stopPos } else none

def Auto.addTryThisTacticSeqSuggestion (ref : Lean.Syntax) (suggestion : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (origSpan? : Option Lean.Syntax := none) : Lean.MetaM Unit

Equations

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

def Auto.addTryThisTacticSeqSuggestion.dedent (s : String) : String

Equations

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

def Auto.querySMT (exportFacts : Array Embedding.Lam.REntry) (exportInds : Array Embedding.Lam.MutualIndInfo) : LamReif.ReifM (Option Lean.Expr × Option (Array Embedding.Lam.REntry))

Equations

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

@[reducible, inline]

abbrev Auto.solverHints : Type

solverHints includes:

• unsatCoreDerivLeafStrings an array of Strings that appear as leaves in any derivation for any fact in the unsat core
• selectorInfos which is an array of
  • The SMT selector name (String)
  • The constructor that the selector is for (Expr)
  • The index of the argument it is a selector for (Nat)
  • The type of the selector function (Expr)
• preprocessFacts : List Expr
• theoryLemmas : List Expr
• instantiations : List Expr
• computationLemmas : List Expr
• polynomialLemmas : List Expr
• rewriteFacts : List (List Expr)

Note 1: In all fields except selectorInfos, there may be loose bound variables. The loose bound variable #i corresponds to the selector indicated by selectorInfos[i]

Note 2: When the external solver is cvc5, all fields can be populated, but when the external solver is Zipperposition, only the first field (unsatCoreDerivLeafStrings) will be populated

Equations

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

def Auto.querySMTForHints (exportFacts : Array Embedding.Lam.REntry) (exportInds : Array Embedding.Lam.MutualIndInfo) : LamReif.ReifM (Option solverHints)

Equations

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

def Auto.callNative_checker (nonempties valids : Array Embedding.Lam.REntry) (prover : Array Lemma → Array Lemma → Lean.MetaM Lean.Expr) : LamReif.ReifM (Lean.Expr × Embedding.Lam.LamTerm × Array Nat × Array Embedding.Lam.REntry × Array Embedding.Lam.REntry)

Given · nonempties = #[s₀, s₁, ⋯, sᵤ₋₁] · valids = #[t₀, t₁, ⋯, kₖ₋₁] Invoke prover to get a proof of proof : (∀ (_ : v₀) (_ : v₁) ⋯ (_ : vᵤ₋₁), w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥).interp and returns · fun etoms => proof · ∀ etoms, ∀ (_ : v₀) (_ : v₁) ⋯ (_ : vᵤ₋₁), w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥) · etoms · [s₀, s₁, ⋯, sᵤ₋₁] · [w₀, w₁, ⋯, wₗ₋₁] Here · [v₀, v₁, ⋯, vᵤ₋₁] is a subsequence of [s₀, s₁, ⋯, sᵤ₋₁] · [w₀, w₁, ⋯, wₗ₋₁] is a subsequence of [t₀, t₁, ⋯, kₖ₋₁] · etoms are all the etoms present in w₀ → w₁ → ⋯ → wₗ₋₁ → ⊥

Note that MetaState.withTemporaryLCtx is used to isolate the prover from the current local context. This is necessary because lean-auto assumes that the prover does not use free variables introduced during monomorphization

Equations

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

def Auto.callMkMVar_checker (nonempties valids : Array Embedding.Lam.REntry) : LamReif.ReifM (Array (Embedding.Lam.REntry × DTr) × Array (Embedding.Lam.REntry × DTr) × Lean.MVarId × Lean.Expr × Embedding.Lam.LamTerm × Array Lean.Expr × Array Nat)

Equations

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

def Auto.callNative_direct (nonempties valids : Array Embedding.Lam.REntry) (prover : Array Lemma → Array Lemma → Lean.MetaM Lean.Expr) : LamReif.ReifM Lean.Expr

Similar in functionality compared to callNative_checker, but all valid entries are supposed to be reified facts (so there should be no etoms). We invoke the prover to get the same proof as callNativeChecker, but we return a proof of ⊥ by applying proof to un-reified facts.

Note that MetaState.withTemporaryLCtx is used to isolate the prover from the current local context. This is necessary because lean-auto assumes that the prover does not use free variables introduced during monomorphization

Equations

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

def Auto.queryNative (declName? : Option Lean.Name) (exportFacts exportInhs : Array Embedding.Lam.REntry) (prover? : Option (Array Lemma → Array Lemma → Lean.MetaM Lean.Expr) := none) : LamReif.ReifM Lean.Expr

If prover? is specified, use the specified one. Otherwise use the one determined by Solver.Native.queryNative

Equations

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

def Auto.rewriteIteCondDecide (lemmas : Array Lemma) : Lean.MetaM (Array Lemma)

Equations

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

def Auto.runAuto (declName? : Option Lean.Name) (lemmas inhFacts : Array Lemma) : Lean.MetaM Lean.Expr

Run auto's preprocessing and monomorphization, then send the problem to different solvers

Equations

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

def Auto.runAuto.reifMAction (declName? : Option Lean.Name) (uvalids uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal)) : LamReif.ReifM Lean.Expr

Equations

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

def Auto.evalAuto : Lean.Elab.Tactic.Tactic

Equations

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

def Auto.runAutoGetHints (lemmas inhFacts : Array Lemma) : Lean.MetaM solverHints

Runs auto's monomorphization and preprocessing, then returns solverHints determined by the external prover's output

Equations

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

def Auto.runAutoGetHints.reifMAction (uvalids uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal)) : LamReif.ReifM solverHints

Equations

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

def Auto.autoGetHints : Lean.ParserDescr

Equations

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

partial def Auto.getForallArgumentTypes (e : Lean.Expr) : List Lean.Expr

Given an expression ∀ x1 : t1, x2 : t2, ... xn : tn, b, returns [t1, t2, ..., tn]. If the given expression is not a forall expression, then getForallArgumentTypes just returns the empty list

def Auto.buildSelectorForInhabitedType (selCtor : Lean.Expr) (argIdx : Nat) : Lean.MetaM Lean.Expr

Given the constructor selCtor of some inductive datatype and an argIdx which is less than selCtor's total number of fields, buildSelectorForInhabitedType uses the datatype's recursor to build a function that takes in the datatype and outputs a value of the same type as the argument indicated by argIdx. This function has the property that if it is passed in selCtor, it returns the argIdxth argument of selCtor, and if it is passed in a different constructor, it returns the default value of the appropriate type.

Equations

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

def Auto.buildSelectorForUninhabitedType (selCtor : Lean.Expr) (argIdx : Nat) : Lean.MetaM Lean.Expr

Given the constructor selCtor of some inductive datatype and an argIdx which is less than selCtor's total number of fields, buildSelectorForUninhabitedType uses the datatype's recursor to build a function that takes in the datatype and outputs a value of the same type as the argument indicated by argIdx. This function has the property that if it is passed in selCtor, it returns the argIdxth argument of selCtor, and if it is passed in a different constructor, it returns sorry.

Equations

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

def Auto.buildSelector (selCtor : Lean.Expr) (argIdx : Nat) : Lean.MetaM Lean.Expr

Given the constructor selCtor of some inductive datatype and an argIdx which is less than selCtor's total number of fields, buildSelectorForInhabitedType uses the datatype's recursor to build a function that takes in the datatype and outputs a value of the same type as the argument indicated by argIdx. This function has the property that if it is passed in selCtor, it returns the argIdxth argument of selCtor.

Equations

• Auto.buildSelector selCtor argIdx = tryCatch (Auto.buildSelectorForInhabitedType selCtor argIdx) fun (x : Lean.Exception) => Auto.buildSelectorForUninhabitedType selCtor argIdx

def Auto.buildSelectorFact (selName : String) (selCtor selType : Lean.Expr) (argIdx : Nat) : Lean.MetaM Lean.Expr

Given the information relating to a selector of type idt → argType, returns the selector fact entailed by SMT-Lib's semantics (∃ f : idt → argType, ∀ ctor_fields, f (ctor ctor_fields) = ctor_fields[argIdx])

Equations

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

def Auto.ppOptionsSetting (o : Lean.Options) : Lean.Options

ppOptionsSetting is used to ensure that the tactics suggested by autoGetHints are pretty printed correctly

Equations

• Auto.ppOptionsSetting o = (((Lean.KVMap.set o `pp.analyze true).set `pp.proofs true).set `pp.funBinderTypes true).set `pp.piBinderTypes true

def Auto.evalAutoGetHints : Lean.Elab.Tactic.Tactic

Equations

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

def Auto.runMono (declName? : Option Lean.Name) (lemmas inhFacts : Array Lemma) : Lean.MetaM (Lean.Expr × Lean.MVarId × Array (Lean.FVarId × Lean.Expr) × Array (Lean.FVarId × DTr))

Run auto's preprocessing and monomorphization to abstract the problem into an essentially higher-order problem

Input · declName? : The name of the declaration where you're calling mono from · lemmas : An array of lemmas that you want to monomorphize. They are meant to be generated by collectAllLemmas · inhFacts : An array of inhabitation lemmas that you want to monomorphize. They are meant to be generated by collectAllLemmas

Return Value · e : Expr : An term of type False, which contains one metavariable yet to be assigned · id : MVarId : The ID of the metavariable in e yet to be assigned · atomVals : Array (FVarId × Expr) The values of the type lam-atoms and term lam-atoms · derivs : Array (FVarId × DTr) The DTrs associated with (monomorphized) lemmas and inhabitation lemmas in the context of id. Using this information you can obtain the correspondence between monomorphized lemmas and the original lemmas

Equations

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

def Auto.runMono.reifMAction (declName? : Option Lean.Name) (uvalids uinhs : Array UMonoFact) (minds : Array (Array SimpleIndVal)) : LamReif.ReifM (Lean.Expr × Lean.MVarId × Array (Lean.FVarId × Lean.Expr) × Array (Lean.FVarId × DTr))

Equations

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

def Auto.evalMono : Lean.Elab.Tactic.Tactic

Equations

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

def Auto.monoInterface (lemmas inhFacts : Array Lemma) (prover : Array Lemma → Array Lemma → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.Expr

A monomorphization interface that can be invoked by repos dependent on lean-auto.

Equations

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

def Auto.runNativeProverWithAuto (declName? : Option Lean.Name) (prover : Array Lemma → Array Lemma → Lean.MetaM Lean.Expr) (lemmas inhFacts : Array Lemma) : Lean.MetaM Lean.Expr

Run native prover with monomorphization and preprocessing of auto

Equations

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

def Auto.evalMonoNative : Lean.Elab.Tactic.Tactic

Equations

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