inductive Auto.DTr : Type

Proof Tree

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

def Auto.instInhabitedDTr.default : DTr

Equations

• Auto.instInhabitedDTr.default = Auto.DTr.node default default

instance Auto.instInhabitedDTr : Inhabited DTr

Equations

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

instance Auto.instHashableDTr : Hashable DTr

Equations

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

partial def Auto.instHashableDTr.hash : DTr → UInt64

instance Auto.instBEqDTr : BEq DTr

Equations

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

partial def Auto.instBEqDTr.beq : DTr → DTr → Bool

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

def Auto.instInhabitedUMonoFact.default : UMonoFact

Equations

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

instance Auto.instInhabitedUMonoFact : Inhabited UMonoFact

Equations

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

def Auto.instHashableUMonoFact.hash : UMonoFact → UInt64

Equations

• Auto.instHashableUMonoFact.hash { proof := a, type := a_1, deriv := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance Auto.instHashableUMonoFact : Hashable UMonoFact

Equations

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

def Auto.instBEqUMonoFact.beq : UMonoFact → UMonoFact → Bool

Equations

• Auto.instBEqUMonoFact.beq { proof := a, type := a_1, deriv := a_2 } { proof := b, type := b_1, deriv := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Auto.instBEqUMonoFact.beq x✝¹ x✝ = false

instance Auto.instBEqUMonoFact : BEq UMonoFact

Equations

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

structure Auto.Lemmaextends Auto.UMonoFact : Type

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

def Auto.instInhabitedLemma.default : Lemma

Equations

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

instance Auto.instInhabitedLemma : Inhabited Lemma

Equations

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

def Auto.instHashableLemma.hash : Lemma → UInt64

Equations

• Auto.instHashableLemma.hash { toUMonoFact := a, params := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance Auto.instHashableLemma : Hashable Lemma

Equations

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

def Auto.instBEqLemma.beq : Lemma → Lemma → Bool

Equations

• Auto.instBEqLemma.beq { toUMonoFact := a, params := a_1 } { toUMonoFact := b, params := b_1 } = (a == b && a_1 == b_1)
• Auto.instBEqLemma.beq x✝¹ x✝ = false

instance Auto.instBEqLemma : BEq Lemma

Equations

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

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) (nonDep : Bool) : 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.checkNonRecEquality (e : Lean.Expr) : Lean.MetaM Unit

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.

def Auto.Lemma.rewriteUPolyRigidNonDep (lem : Lemma) (rws : Array Lemma) : Lean.MetaM Lemma

Exhaustively rewrite using an array of universe-polymorphic rigid equalities · Only lhss occurring in non-dependent positions will be replaced by rhs · 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

def Auto.instInhabitedLemmaInst.default : LemmaInst

Equations

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

instance Auto.instInhabitedLemmaInst : Inhabited LemmaInst

Equations

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

def Auto.instHashableLemmaInst.hash : LemmaInst → UInt64

Equations

• Auto.instHashableLemmaInst.hash { toLemma := a, nbinders := a_1, nargs := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance Auto.instHashableLemmaInst : Hashable LemmaInst

Equations

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

instance Auto.instBEqLemmaInst : BEq LemmaInst

Equations

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

def Auto.instBEqLemmaInst.beq : LemmaInst → LemmaInst → Bool

Equations

• Auto.instBEqLemmaInst.beq { toLemma := a, nbinders := a_1, nargs := a_2 } { toLemma := b, nbinders := b_1, nargs := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Auto.instBEqLemmaInst.beq x✝¹ x✝ = false

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 := Auto.instInhabitedMLemmaInst.default }

def Auto.instInhabitedMLemmaInst.default : MLemmaInst

Equations

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

instance Auto.instHashableMLemmaInst : Hashable MLemmaInst

Equations

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

def Auto.instHashableMLemmaInst.hash : MLemmaInst → UInt64

Equations

• Auto.instHashableMLemmaInst.hash { origProof := a, args := a_1, type := a_2, deriv := a_3 } = mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)

def Auto.instBEqMLemmaInst.beq : MLemmaInst → MLemmaInst → Bool

Equations

• One or more equations did not get rendered due to their size.
• Auto.instBEqMLemmaInst.beq x✝¹ x✝ = false

instance Auto.instBEqMLemmaInst : BEq MLemmaInst

Equations

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

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.