inductive Auto.DTr : Type

Proof Tree

• node : String → Array DTr → DTr
• leaf : String → DTr

instance Auto.instInhabitedDTr : Inhabited DTr

Equations

• Auto.instInhabitedDTr = { default := Auto.DTr.node default default }

instance Auto.instHashableDTr : Hashable DTr

Equations

• Auto.instHashableDTr = { hash := Auto.hashDTr✝ }

instance Auto.instBEqDTr : BEq DTr

Equations

• Auto.instBEqDTr = { beq := Auto.beqDTr✝ }

partial def Auto.DTr.toString : DTr → String

instance Auto.instToStringDTr : ToString DTr

Equations

• Auto.instToStringDTr = { toString := Auto.DTr.toString }

partial def Auto.DTr.collectLeafStrings : DTr → Array String

structure Auto.UMonoFact : Type

Universe monomprphic facts User-supplied facts should have their universe level parameters instantiated before being put into Reif.State.facts

• proof : Lean.Expr
• type : Lean.Expr
• deriv : DTr

instance Auto.instInhabitedUMonoFact : Inhabited UMonoFact

Equations

• Auto.instInhabitedUMonoFact = { default := { proof := default, type := default, deriv := default } }

instance Auto.instHashableUMonoFact : Hashable UMonoFact

Equations

• Auto.instHashableUMonoFact = { hash := Auto.hashUMonoFact✝ }

instance Auto.instBEqUMonoFact : BEq UMonoFact

Equations

• Auto.instBEqUMonoFact = { beq := Auto.beqUMonoFact✝ }

structure Auto.Lemmaextends Auto.UMonoFact : Type

• proof : Lean.Expr
• type : Lean.Expr
• deriv : DTr
• params : Array Lean.Name

instance Auto.instInhabitedLemma : Inhabited Lemma

Equations

• Auto.instInhabitedLemma = { default := { toUMonoFact := default, params := default } }

instance Auto.instHashableLemma : Hashable Lemma

Equations

• Auto.instHashableLemma = { hash := Auto.hashLemma✝ }

instance Auto.instBEqLemma : BEq Lemma

Equations

• Auto.instBEqLemma = { beq := Auto.beqLemma✝ }

instance Auto.instToMessageDataLemma : Lean.ToMessageData Lemma

Equations

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

def Auto.Lemma.ofUMonoFact (fact : UMonoFact) : Lemma

Equations

• Auto.Lemma.ofUMonoFact fact = { toUMonoFact := fact, params := #[] }

def Auto.Lemma.toUMonoFact? (lem : Lemma) : Option UMonoFact

Equations

• lem.toUMonoFact? = match lem.params with | { toList := [] } => some lem.toUMonoFact | { toList := head :: tail } => none

def Auto.Lemma.instantiateLevelParamsArray (lem : Lemma) (lvls : Array Lean.Level) : Lemma

Equations

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

def Auto.Lemma.instantiateLevelParams (lem : Lemma) (lvls : List Lean.Level) : Lemma

Equations

• lem.instantiateLevelParams lvls = lem.instantiateLevelParamsArray { toList := lvls }

def Auto.Lemma.instantiateMVars (lem : Lemma) : Lean.MetaM Lemma

Equations

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

def Auto.Lemma.betaReduceType (lem : Lemma) : Lean.CoreM Lemma

Equations

• { proof := proof, type := type, deriv := deriv, params := params }.betaReduceType = do let type ← Lean.Core.betaReduce type pure { proof := proof, type := type, deriv := deriv, params := params }

def Auto.Lemma.ofConst (name : Lean.Name) (deriv : DTr) : Lean.CoreM Lemma

Create a Lemma out of a constant, given the name of the constant

Equations

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

def Auto.Lemma.subsumeQuick (lem₁ lem₂ : Lemma) : Lean.MetaM Bool

Check whether lem₁ subsumes lem₂

Equations

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

def Auto.Lemma.equivQuick (lem₁ lem₂ : Lemma) : Lean.MetaM Bool

Equations

• lem₁.equivQuick lem₂ = do let s₁₂ ← lem₁.subsumeQuick lem₂ let s₂₁ ← lem₂.subsumeQuick lem₁ pure (s₁₂ && s₂₁)

def Auto.Lemma.rewriteUMonoRigid? (lem : Lemma) (rw : UMonoFact) : Lean.MetaM (Option Lemma)

Rewrite using a universe-monomorphic rigid equality rw.snd should have the form lhs = rhs, where both sides are rigid · If lhs occurs in lem.type, perform rewrite and return result · If lhs does not occur in lem.type, return .none

Equations

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

def Auto.Lemma.rewriteUPolyRigid (lem rw : Lemma) : Lean.MetaM Lemma

Exhaustively rewrite using a universe-polymorphic rigid equality · If there are multiple instances of lhs with different universe level instantiations, all of these instances will be replaced with rhs · rw.snd should have the form lhs = rhs, where both sides are rigid and rhs should not contain lhs

Equations

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

structure Auto.LemmaInstextends Auto.Lemma : Type

• proof : Lean.Expr
• type : Lean.Expr
• deriv : DTr
• params : Array Lean.Name
• nbinders : Nat
• nargs : Nat

instance Auto.instInhabitedLemmaInst : Inhabited LemmaInst

Equations

• Auto.instInhabitedLemmaInst = { default := { toLemma := default, nbinders := default, nargs := default } }

instance Auto.instHashableLemmaInst : Hashable LemmaInst

Equations

• Auto.instHashableLemmaInst = { hash := Auto.hashLemmaInst✝ }

instance Auto.instBEqLemmaInst : BEq LemmaInst

Equations

• Auto.instBEqLemmaInst = { beq := Auto.beqLemmaInst✝ }

def Auto.LemmaInst.ofLemma (lem : Lemma) : Lean.MetaM LemmaInst

Equations

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

def Auto.LemmaInst.ofLemmaHOL (lem : Lemma) : Lean.MetaM LemmaInst

Only introduce leading non-prop binders But, if a prop-binder is an instance binder, we still introduce it

Equations

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

def Auto.LemmaInst.ofLemmaLeadingDepOnly (lem : Lemma) : Lean.MetaM LemmaInst

Equations

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

def Auto.LemmaInst.getProofOfLemma (li : LemmaInst) : Option Lean.Expr

Get the proof of the lemma that li is an instance of

Equations

• li.getProofOfLemma = (Auto.Expr.stripLambdaN li.nbinders li.proof).bind (Auto.Expr.getAppFnN li.nargs)

instance Auto.instToMessageDataLemmaInst : Lean.ToMessageData LemmaInst

Equations

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

def Auto.LemmaInst.subsumeQuick (li₁ li₂ : LemmaInst) : Lean.MetaM Bool

Equations

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

def Auto.LemmaInst.equivQuick (li₁ li₂ : LemmaInst) : Lean.MetaM Bool

Equations

• li₁.equivQuick li₂ = do let s₁₂ ← li₁.subsumeQuick li₂ let s₂₁ ← li₂.subsumeQuick li₁ pure (s₁₂ && s₂₁)

@[reducible, inline]

abbrev Auto.LemmaInsts : Type

Equations

• Auto.LemmaInsts = Array Auto.LemmaInst

def Auto.LemmaInsts.newInst? (lis : LemmaInsts) (li : LemmaInst) : Lean.MetaM Bool

Equations

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

structure Auto.MLemmaInst : Type

A LemmaInst, but after lambdaMetaTelescope on the proof

• origProof : Lean.Expr
• args : Array Lean.Expr
• type : Lean.Expr
• deriv : DTr

instance Auto.instInhabitedMLemmaInst : Inhabited MLemmaInst

Equations

• Auto.instInhabitedMLemmaInst = { default := { origProof := default, args := default, type := default, deriv := default } }

instance Auto.instHashableMLemmaInst : Hashable MLemmaInst

Equations

• Auto.instHashableMLemmaInst = { hash := Auto.hashMLemmaInst✝ }

instance Auto.instBEqMLemmaInst : BEq MLemmaInst

Equations

• Auto.instBEqMLemmaInst = { beq := Auto.beqMLemmaInst✝ }

instance Auto.instToMessageDataMLemmaInst : Lean.ToMessageData MLemmaInst

Equations

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

def Auto.MLemmaInst.ofLemmaInst (li : LemmaInst) : Lean.MetaM (Array Lean.Level × Array Lean.Expr × MLemmaInst)

Equations

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

def Auto.LemmaInst.ofMLemmaInst (mi : MLemmaInst) : Lean.MetaM LemmaInst

Equations

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

partial def Auto.collectUniverseLevels : Lean.Expr → Lean.MetaM (Std.HashSet Lean.Level)

def Auto.computeMaxLevel (facts : Array UMonoFact) : Lean.MetaM Lean.Level

Equations

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