inductive Auto.Embedding.Lam.REntry : Type

An entry of RTable

• wf : List LamSort → LamSort → LamTerm → REntry
• valid : List LamSort → LamTerm → REntry
• nonempty : LamSort → REntry

instance Auto.Embedding.Lam.instInhabitedREntry : Inhabited REntry

Equations

• Auto.Embedding.Lam.instInhabitedREntry = { default := Auto.Embedding.Lam.REntry.wf default default default }

instance Auto.Embedding.Lam.instHashableREntry : Hashable REntry

Equations

• Auto.Embedding.Lam.instHashableREntry = { hash := Auto.Embedding.Lam.hashREntry✝ }

instance Auto.Embedding.Lam.instBEqREntry : BEq REntry

Equations

• Auto.Embedding.Lam.instBEqREntry = { beq := Auto.Embedding.Lam.beqREntry✝ }

instance Auto.Embedding.Lam.instToExprREntry : Lean.ToExpr REntry

Equations

• Auto.Embedding.Lam.instToExprREntry = { toExpr := Auto.Embedding.Lam.toExprREntry✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.REntry [] }

def Auto.Embedding.Lam.REntry.repr : REntry → String

Equations

• One or more equations did not get rendered due to their size.
• (Auto.Embedding.Lam.REntry.valid a a_1).repr = toString "Auto.Embedding.Lam.REntry.valid " ++ toString (reprPrec a 1) ++ toString " " ++ toString (reprPrec a_1 1) ++ toString ""
• (Auto.Embedding.Lam.REntry.nonempty a).repr = toString "Audo.Embedding.Lam.REntry.nonempty " ++ toString (reprPrec a 1) ++ toString ""

instance Auto.Embedding.Lam.instReprREntry : Repr REntry

Equations

• Auto.Embedding.Lam.instReprREntry = { reprPrec := fun (re : Auto.Embedding.Lam.REntry) (x : Nat) => Std.Format.text re.repr }

def Auto.Embedding.Lam.REntry.toString : REntry → String

Equations

• (Auto.Embedding.Lam.REntry.wf a a_1 a_2).toString = toString "wf " ++ toString a ++ toString " " ++ toString a_1 ++ toString " " ++ toString a_2 ++ toString ""
• (Auto.Embedding.Lam.REntry.valid a a_1).toString = toString "valid " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.REntry.nonempty a).toString = toString "nonempty " ++ toString a ++ toString ""

instance Auto.Embedding.Lam.instToStringREntry : ToString REntry

Equations

• Auto.Embedding.Lam.instToStringREntry = { toString := Auto.Embedding.Lam.REntry.toString }

def Auto.Embedding.Lam.REntry.beq : REntry → REntry → Bool

Equations

• (Auto.Embedding.Lam.REntry.wf a a_1 a_2).beq (Auto.Embedding.Lam.REntry.wf b b_1 b_2) = (a == b && a_1 == b_1 && a_2 == b_2)
• (Auto.Embedding.Lam.REntry.valid a a_1).beq (Auto.Embedding.Lam.REntry.valid b b_1) = (a == b && a_1 == b_1)
• (Auto.Embedding.Lam.REntry.nonempty a).beq (Auto.Embedding.Lam.REntry.nonempty b) = (a == b)
• x✝¹.beq x✝ = false

instance Auto.Embedding.Lam.instBEqREntry_1 : BEq REntry

Equations

• Auto.Embedding.Lam.instBEqREntry_1 = { beq := Auto.Embedding.Lam.REntry.beq }

theorem Auto.Embedding.Lam.REntry.beq_def {l r : REntry} : (l == r) = l.beq r

theorem Auto.Embedding.Lam.REntry.beq_refl {r : REntry} : (r == r) = true

theorem Auto.Embedding.Lam.REntry.eq_of_beq_eq_true {l r : REntry} (H : (l == r) = true) : l = r

instance Auto.Embedding.Lam.instLawfulBEqREntry : LawfulBEq REntry

def Auto.Embedding.Lam.REntry.containsSort (re : REntry) (s : LamSort) : Bool

Equations

• (Auto.Embedding.Lam.REntry.wf a a_1 a_2).containsSort s = ((a.any fun (s' : Auto.Embedding.Lam.LamSort) => s'.contains s) || a_1.contains s || a_2.containsSort s)
• (Auto.Embedding.Lam.REntry.valid a a_1).containsSort s = ((a.any fun (s' : Auto.Embedding.Lam.LamSort) => s'.contains s) || a_1.containsSort s)
• (Auto.Embedding.Lam.REntry.nonempty a).containsSort s = a.contains s

def Auto.Embedding.Lam.REntry.allLamTerms (re : REntry) : List LamTerm

Equations

• (Auto.Embedding.Lam.REntry.wf a a_1 a_2).allLamTerms = [a_2]
• (Auto.Embedding.Lam.REntry.valid a a_1).allLamTerms = [a_1]
• (Auto.Embedding.Lam.REntry.nonempty a).allLamTerms = []

structure Auto.Embedding.Lam.RTable : Type

Table of valid propositions and well-formed formulas Note that Auto.BinTree α is equivalent to Nat → Option α, which means that .some entries may be interspersed with .none entries

• entries : BinTree REntry
• maxEVarSucc : Nat
• lamEVarTy : BinTree LamSort

def Auto.Embedding.Lam.RTable.beq : RTable → RTable → Bool

Equations

• { entries := le, maxEVarSucc := lmax, lamEVarTy := llam }.beq { entries := re, maxEVarSucc := rmax, lamEVarTy := rlam } = (le == re && lmax == rmax && llam == rlam)

instance Auto.Embedding.Lam.instBEqRTable : BEq RTable

Equations

• Auto.Embedding.Lam.instBEqRTable = { beq := Auto.Embedding.Lam.RTable.beq }

theorem Auto.Embedding.Lam.RTable.beq_def {l r : RTable} : (l == r) = l.beq r

theorem Auto.Embedding.Lam.RTable.beq_refl {r : RTable} : (r == r) = true

theorem Auto.Embedding.Lam.RTable.eq_of_beq_eq_true {l r : RTable} (H : (l == r) = true) : l = r

instance Auto.Embedding.Lam.instLawfulBEqRTable : LawfulBEq RTable

def Auto.Embedding.Lam.RTable.get? (r : RTable) (n : Nat) : Option REntry

Equations

• r.get? = r.entries.get?

def Auto.Embedding.Lam.RTable.addEntry (r : RTable) (e : REntry) (n : Nat) : RTable

Equations

• r.addEntry e n = { entries := r.entries.insert n e, maxEVarSucc := r.maxEVarSucc, lamEVarTy := r.lamEVarTy }

def Auto.Embedding.Lam.RTable.toLamEVarTy (r : RTable) (n : Nat) : LamSort

Equations

• r.toLamEVarTy n = (r.lamEVarTy.get? n).getD (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop)

structure Auto.Embedding.Lam.CPVal : Type (u + 1)

Checker Partial Valuation (Valuation without lamEVarTy and eVarVal)

• tyVal : Nat → Type u
• var : BinTree ((s : LamSort) × LamSort.interp self.tyVal s)
• il : BinTree ((s : LamSort) × ILLift (LamSort.interp self.tyVal s))

structure Auto.Embedding.Lam.CVal (lamEVarTy : BinTree LamSort) extends Auto.Embedding.Lam.CPVal : Type (u_1 + 1)

Checker Valuation

• tyVal : Nat → Type u_1
• var : BinTree ((s : LamSort) × LamSort.interp self.tyVal s)
• il : BinTree ((s : LamSort) × ILLift (LamSort.interp self.tyVal s))
• eVarVal (n : Nat) : LamSort.interp self.tyVal ((lamEVarTy.get? n).getD (LamSort.base LamBaseSort.prop))

@[reducible, inline]

abbrev Auto.Embedding.Lam.eVarTy (tyVal : Nat → Type u) (lamEVarTy : BinTree LamSort) : Type u

Equations

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

@[reducible, inline]

abbrev Auto.Embedding.Lam.varSigmaMk (tyVal : Nat → Type u) (fst : LamSort) (snd : LamSort.interp tyVal fst) : Sigma (LamSort.interp tyVal)

Used in checker metacode to construct var

Equations

• Auto.Embedding.Lam.varSigmaMk tyVal = Sigma.mk

@[reducible, inline]

abbrev Auto.Embedding.Lam.ilβ (tyVal : Nat → Type u) (s : LamSort) : Type u

Used in checker metacode to construct il

Equations

• Auto.Embedding.Lam.ilβ tyVal s = Auto.Embedding.Lam.ILLift (Auto.Embedding.Lam.LamSort.interp tyVal s)

@[reducible, inline]

abbrev Auto.Embedding.Lam.ilSigmaMk (tyVal : Nat → Type u) (fst : LamSort) (snd : ilβ tyVal fst) : Sigma (ilβ tyVal)

Used in checker metacode to construct il

Equations

• Auto.Embedding.Lam.ilSigmaMk tyVal = Sigma.mk

noncomputable def Auto.Embedding.Lam.ilVal.default (lamILTy : Nat → LamSort) (tyVal : Nat → Type u) (n : Nat) : ILLift (LamSort.interp tyVal (lamILTy n))

Equations

• Auto.Embedding.Lam.ilVal.default lamILTy tyVal n = Auto.Embedding.Lam.ILLift.default (Auto.Embedding.Lam.LamSort.interp tyVal (lamILTy n))

def Auto.Embedding.Lam.CVal.toLamTyVal {levt : BinTree LamSort} (cv : CVal levt) : LamTyVal

Equations

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

noncomputable def Auto.Embedding.Lam.CVal.toLamValuation {levt : BinTree LamSort} (cv : CVal levt) : LamValuation

Equations

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

def Auto.Embedding.Lam.CPVal.toLamVarTy (cpv : CPVal) : Nat → LamSort

Equations

• cpv.toLamVarTy n = ((cpv.var.get? n).getD ⟨Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop, { down := False }⟩).fst

def Auto.Embedding.Lam.CPVal.toLamILTy (cpv : CPVal) : Nat → LamSort

Equations

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

def Auto.Embedding.Lam.CPVal.toLamTyValWithLamEVarTy (cpv : CPVal) (levt : Nat → LamSort) : LamTyVal

Equations

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

def Auto.Embedding.Lam.CPVal.toLamTyValEraseEtom (cpv : CPVal) : LamTyVal

Equations

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

noncomputable def Auto.Embedding.Lam.CPVal.toLamValuationEraseEtom (cpv : CPVal) : LamValuation

Equations

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

noncomputable def Auto.Embedding.Lam.CPVal.toLamValuationWithEVar (cpv : CPVal) (letv : Nat → LamSort) (eVarVal : (n : Nat) → LamSort.interp cpv.tyVal (letv n)) : LamValuation

Equations

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

def Auto.Embedding.Lam.REntry.correct {levt : BinTree LamSort} (cv : CVal levt) (maxEVarSucc : Nat) : REntry → Prop

Equations

• Auto.Embedding.Lam.REntry.correct cv maxEVarSucc (Auto.Embedding.Lam.REntry.wf a a_1 a_2) = (Auto.Embedding.Lam.LamThmWFP cv.toLamValuation a a_1 a_2 ∧ a_2.maxEVarSucc ≤ maxEVarSucc)
• Auto.Embedding.Lam.REntry.correct cv maxEVarSucc (Auto.Embedding.Lam.REntry.valid a a_1) = (Auto.Embedding.Lam.LamThmValid cv.toLamValuation a a_1 ∧ a_1.maxEVarSucc ≤ maxEVarSucc)
• Auto.Embedding.Lam.REntry.correct cv maxEVarSucc (Auto.Embedding.Lam.REntry.nonempty a) = Auto.Embedding.Lam.LamNonempty cv.tyVal a

theorem Auto.Embedding.Lam.REntry.correct_eVarIrrelevance {maxEVarSucc : Nat} {re : REntry} (cpv : CPVal) (levt₁ levt₂ : BinTree LamSort) (val₁ : eVarTy cpv.tyVal levt₁) (val₂ : eVarTy cpv.tyVal levt₂) (hirr : ∀ (n : Nat), n < maxEVarSucc → (levt₁.get? n).getD (LamSort.base LamBaseSort.prop) = (levt₂.get? n).getD (LamSort.base LamBaseSort.prop) ∧ val₁ n ≍ val₂ n) (c₁ : correct { toCPVal := cpv, eVarVal := val₁ } maxEVarSucc re) : correct { toCPVal := cpv, eVarVal := val₂ } maxEVarSucc re

theorem Auto.Embedding.Lam.REntry.correct_increaseMaxEVarSucc {lamEVarTy✝ : BinTree LamSort} {cv : CVal lamEVarTy✝} {maxEVarSucc₁ : Nat} {re : REntry} {maxEVarSucc₂ : Nat} (c₁ : correct cv maxEVarSucc₁ re) (h : maxEVarSucc₁ ≤ maxEVarSucc₂) : correct cv maxEVarSucc₂ re

def Auto.Embedding.Lam.RTable.inv (r : RTable) (cv : CVal r.lamEVarTy) : Prop

Invariant of RTable

Equations

• r.inv cv = Auto.BinTree.allp (fun (re : Auto.Embedding.Lam.REntry) => Auto.Embedding.Lam.REntry.correct cv r.maxEVarSucc re) r.entries

theorem Auto.Embedding.Lam.RTable.inv_eVarIrrelevance {maxEVarSucc_ : Nat} {entries_ : BinTree REntry} (cpv : CPVal) (levt₁ levt₂ : BinTree LamSort) (val₁ : eVarTy cpv.tyVal levt₁) (val₂ : eVarTy cpv.tyVal levt₂) (hirr : ∀ (n : Nat), n < maxEVarSucc_ → (levt₁.get? n).getD (LamSort.base LamBaseSort.prop) = (levt₂.get? n).getD (LamSort.base LamBaseSort.prop) ∧ val₁ n ≍ val₂ n) (c₁ : { entries := entries_, maxEVarSucc := maxEVarSucc_, lamEVarTy := levt₁ }.inv { toCPVal := cpv, eVarVal := val₁ }) : { entries := entries_, maxEVarSucc := maxEVarSucc_, lamEVarTy := levt₂ }.inv { toCPVal := cpv, eVarVal := val₂ }

theorem Auto.Embedding.Lam.RTable.inv_increaseMaxEVarSucc {r : RTable} {cv : CVal r.lamEVarTy} {maxEVarSucc_ : Nat} (c₁ : r.inv cv) (h : r.maxEVarSucc ≤ maxEVarSucc_) : { entries := r.entries, maxEVarSucc := maxEVarSucc_, lamEVarTy := r.lamEVarTy }.inv cv

theorem Auto.Embedding.Lam.RTable.wfInv_get {n : Nat} {lctx : List LamSort} {s : LamSort} {t : LamTerm} {r : RTable} {cv : CVal r.lamEVarTy} (inv : r.inv cv) (h : r.get? n = some (REntry.wf lctx s t)) : LamThmWFP cv.toLamValuation lctx s t ∧ t.maxEVarSucc ≤ r.maxEVarSucc

theorem Auto.Embedding.Lam.RTable.validInv_get {n : Nat} {lctx : List LamSort} {t : LamTerm} {r : RTable} {cv : CVal r.lamEVarTy} (inv : r.inv cv) (h : r.get? n = some (REntry.valid lctx t)) : LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc

theorem Auto.Embedding.Lam.RTable.nonemptyInv_get {n : Nat} {s : LamSort} {r : RTable} {cv : CVal r.lamEVarTy} (inv : r.inv cv) (h : r.get? n = some (REntry.nonempty s)) : LamNonempty cv.tyVal s

def Auto.Embedding.Lam.RTable.getWF (r : RTable) (w : Nat) : Option (List LamSort × LamSort × LamTerm)

Equations

• r.getWF w = match r.get? w with | some (Auto.Embedding.Lam.REntry.wf lctx s t) => some (lctx, s, t) | x => none

theorem Auto.Embedding.Lam.RTable.getWF_correct {r : RTable} {cv : CVal r.lamEVarTy} {w : Nat} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (inv : r.inv cv) (heq : r.getWF w = some (lctx, s, t)) : LamThmWFP cv.toLamValuation lctx s t ∧ t.maxEVarSucc ≤ r.maxEVarSucc

def Auto.Embedding.Lam.RTable.getValid (r : RTable) (v : Nat) : Option (List LamSort × LamTerm)

Equations

• r.getValid v = match r.get? v with | some (Auto.Embedding.Lam.REntry.valid lctx t) => some (lctx, t) | x => none

theorem Auto.Embedding.Lam.RTable.getValid_correct {r : RTable} {cv : CVal r.lamEVarTy} {v : Nat} {lctx : List LamSort} {t : LamTerm} (inv : r.inv cv) (heq : r.getValid v = some (lctx, t)) : LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc

def Auto.Embedding.Lam.RTable.getValidEnsureLCtx (r : RTable) (lctx : List LamSort) (v : Nat) : Option LamTerm

Equations

• r.getValidEnsureLCtx lctx v = match r.getValid v with | some (lctx', t) => match lctx.beq lctx' with | true => some t | false => none | none => none

theorem Auto.Embedding.Lam.RTable.getValidEnsureLCtx_correct {r : RTable} {cv : CVal r.lamEVarTy} {lctx : List LamSort} {v : Nat} {t : LamTerm} (inv : r.inv cv) (heq : r.getValidEnsureLCtx lctx v = some t) : LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc

def Auto.Embedding.Lam.RTable.getValidExport (r : RTable) (v : Nat) : Option (List LamSort × LamTerm)

Equations

• r.getValidExport v = match r.getValid v with | some (lctx, t) => match t.maxEVarSucc with | 0 => some (lctx, t) | n.succ => none | none => none

theorem Auto.Embedding.Lam.RTable.getValidExport_correct {r : RTable} {cpv : CPVal} {v : Nat} {lctx : List LamSort} {t : LamTerm} (inv : ∃ (eV : (n : Nat) → LamSort.interp cpv.tyVal ((r.lamEVarTy.get? n).getD (LamSort.base LamBaseSort.prop))), r.inv { toCPVal := cpv, eVarVal := eV }) (heq : r.getValidExport v = some (lctx, t)) : LamThmValid cpv.toLamValuationEraseEtom lctx t

def Auto.Embedding.Lam.RTable.getValidsEnsureLCtx (r : RTable) (lctx : List LamSort) (vs : List Nat) : Option (List LamTerm)

Equations

• One or more equations did not get rendered due to their size.
• r.getValidsEnsureLCtx lctx [] = some []

@[irreducible]

noncomputable def Auto.Embedding.Lam.RTable.getValidsEnsureLCtx_correct {r : RTable} {cv : CVal r.lamEVarTy} {lctx : List LamSort} {vs : List Nat} {ts : List LamTerm} (inv : r.inv cv) (heq : r.getValidsEnsureLCtx lctx vs = some ts) : HList (fun (t : LamTerm) => LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc) ts

Equations

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

def Auto.Embedding.Lam.RTable.getNonempty (r : RTable) (v : Nat) : Option LamSort

Equations

• r.getNonempty v = match r.get? v with | some (Auto.Embedding.Lam.REntry.nonempty s) => some s | x => none

theorem Auto.Embedding.Lam.RTable.getNonempty_correct {r : RTable} {cv : CVal r.lamEVarTy} {w : Nat} {s : LamSort} (inv : r.inv cv) (heq : r.getNonempty w = some s) : LamNonempty cv.tyVal s

inductive Auto.Embedding.Lam.ImportEntry : Type

• valid : LamTerm → ImportEntry
• nonempty : LamSort → ImportEntry

def Auto.Embedding.Lam.ImportEntry.correct (lval : LamValuation) : ImportEntry → Prop

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.ImportEntry.correct lval (Auto.Embedding.Lam.ImportEntry.nonempty s) = Nonempty (Auto.Embedding.Lam.LamSort.interp lval.tyVal s)

@[reducible, inline]

abbrev Auto.Embedding.Lam.ImportTable (cpv : CPVal) : Type

The meta code of the checker will prepare this ImportTable

Equations

• Auto.Embedding.Lam.ImportTable cpv = Auto.BinTree (PSigma (Auto.Embedding.Lam.ImportEntry.correct cpv.toLamValuationEraseEtom))

@[reducible, inline]

abbrev Auto.Embedding.Lam.importTablePSigmaβ (cpv : CPVal) (ie : ImportEntry) : Prop

Used by the meta code of the checker to build ImportTable

Equations

• Auto.Embedding.Lam.importTablePSigmaβ cpv ie = Auto.Embedding.Lam.ImportEntry.correct cpv.toLamValuationEraseEtom ie

@[reducible, inline]

abbrev Auto.Embedding.Lam.importTablePSigmaMk (cpv : CPVal) (fst : ImportEntry) (snd : importTablePSigmaβ cpv fst) : PSigma (importTablePSigmaβ cpv)

Equations

• Auto.Embedding.Lam.importTablePSigmaMk cpv = PSigma.mk

def Auto.Embedding.Lam.ImportTable.importFacts {cpv : CPVal} (it : ImportTable cpv) : BinTree REntry

Equations

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

theorem Auto.Embedding.Lam.ImportTable.importFacts_correct {cpv : CPVal} {levt : BinTree LamSort} {eVarVal : (n : Nat) → LamSort.interp cpv.tyVal ((levt.get? n).getD (LamSort.base LamBaseSort.prop))} (it : ImportTable cpv) (n : Nat) : BinTree.allp (REntry.correct { toCPVal := cpv, eVarVal := eVarVal } n) it.importFacts

inductive Auto.Embedding.Lam.ConvStep : Type

• validOfHeadBeta (pos : Nat) : ConvStep
• validOfBetaBounded (pos bound : Nat) : ConvStep
• validOfExtensionalize (pos : Nat) : ConvStep

  Exhaustively rewrite using functional extensionality

• validOfEqSymm (pos : Nat) : ConvStep

  Symmetry to top-level equality

• validOfMp (pos rw : Nat) : ConvStep
• validOfMpAll (pos rw : Nat) : ConvStep

  Exhaustively rewrite using facts of form valid [] (lhs = rhs)

• validOfCongrArg (pos rw : Nat) : ConvStep
• validOfCongrFun (pos rw : Nat) : ConvStep
• validOfCongr (pos rwFn rwArg : Nat) : ConvStep
• validOfCongrArgs (pos : Nat) (rws : List Nat) : ConvStep
• validOfCongrFunN (pos rwFn n : Nat) : ConvStep
• validOfCongrs (pos rwFn : Nat) (rwArgs : List Nat) : ConvStep

instance Auto.Embedding.Lam.instInhabitedConvStep : Inhabited ConvStep

Equations

• Auto.Embedding.Lam.instInhabitedConvStep = { default := Auto.Embedding.Lam.ConvStep.validOfHeadBeta default }

instance Auto.Embedding.Lam.instHashableConvStep : Hashable ConvStep

Equations

• Auto.Embedding.Lam.instHashableConvStep = { hash := Auto.Embedding.Lam.hashConvStep✝ }

instance Auto.Embedding.Lam.instBEqConvStep : BEq ConvStep

Equations

• Auto.Embedding.Lam.instBEqConvStep = { beq := Auto.Embedding.Lam.beqConvStep✝ }

instance Auto.Embedding.Lam.instToExprConvStep : Lean.ToExpr ConvStep

Equations

• Auto.Embedding.Lam.instToExprConvStep = { toExpr := Auto.Embedding.Lam.toExprConvStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.ConvStep [] }

inductive Auto.Embedding.Lam.ConvAtStep : Type

• validOfEtaExpand1At (pos : Nat) (occ : List Bool) : ConvAtStep
• validOfEtaReduce1At (pos : Nat) (occ : List Bool) : ConvAtStep
• validOfEtaExpandNAt (pos n : Nat) (occ : List Bool) : ConvAtStep
• validOfEtaReduceNAt (pos n : Nat) (occ : List Bool) : ConvAtStep
• validOfExtensionalizeEqAt (pos : Nat) (occ : List Bool) : ConvAtStep

  Turn · f = g into ∀ x₁ x₂ ⋯ xₙ, f x₁ x₂ ⋯ xₙ = g x₁ x₂ ⋯ xₙ · f = into fun g => ∀ x₁ x₂ ⋯ xₙ, f x₁ x₂ ⋯ xₙ = g x₁ x₂ ⋯ xₙ · = into fun f g => ∀ x₁ x₂ ⋯ xₙ, f x₁ x₂ ⋯ xₙ = g x₁ x₂ ⋯ xₙ

• validOfExtensionalizeEqFNAt (pos n : Nat) (occ : List Bool) : ConvAtStep

  Turn f = g into ∀ x₁ x₂ ⋯ xₙ, f x₁ x₂ ⋯ xₙ = g x₁ x₂ ⋯ xₙ, where f and g must be of type s₀ → s₁ → ⋯ → sₙ₋₁ → ?

• validOfIntensionalizeEqAt (pos : Nat) (occ : List Bool) : ConvAtStep

  Turn ∀ x₁ x₂ ⋯ xₙ, f x₁ x₂ ⋯ xₙ = g x₁ x₂ ⋯ xₙ into f = g

instance Auto.Embedding.Lam.instInhabitedConvAtStep : Inhabited ConvAtStep

Equations

• Auto.Embedding.Lam.instInhabitedConvAtStep = { default := Auto.Embedding.Lam.ConvAtStep.validOfEtaExpand1At default default }

instance Auto.Embedding.Lam.instHashableConvAtStep : Hashable ConvAtStep

Equations

• Auto.Embedding.Lam.instHashableConvAtStep = { hash := Auto.Embedding.Lam.hashConvAtStep✝ }

instance Auto.Embedding.Lam.instBEqConvAtStep : BEq ConvAtStep

Equations

• Auto.Embedding.Lam.instBEqConvAtStep = { beq := Auto.Embedding.Lam.beqConvAtStep✝ }

instance Auto.Embedding.Lam.instToExprConvAtStep : Lean.ToExpr ConvAtStep

Equations

• Auto.Embedding.Lam.instToExprConvAtStep = { toExpr := Auto.Embedding.Lam.toExprConvAtStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.ConvAtStep [] }

inductive Auto.Embedding.Lam.EtomStep : Type

• skolemize (pos : Nat) : EtomStep
• define (t : LamTerm) : EtomStep

instance Auto.Embedding.Lam.instInhabitedEtomStep : Inhabited EtomStep

Equations

• Auto.Embedding.Lam.instInhabitedEtomStep = { default := Auto.Embedding.Lam.EtomStep.skolemize default }

instance Auto.Embedding.Lam.instHashableEtomStep : Hashable EtomStep

Equations

• Auto.Embedding.Lam.instHashableEtomStep = { hash := Auto.Embedding.Lam.hashEtomStep✝ }

instance Auto.Embedding.Lam.instBEqEtomStep : BEq EtomStep

Equations

• Auto.Embedding.Lam.instBEqEtomStep = { beq := Auto.Embedding.Lam.beqEtomStep✝ }

instance Auto.Embedding.Lam.instToExprEtomStep : Lean.ToExpr EtomStep

Equations

• Auto.Embedding.Lam.instToExprEtomStep = { toExpr := Auto.Embedding.Lam.toExprEtomStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.EtomStep [] }

inductive Auto.Embedding.Lam.FactStep : Type

• boolFacts : FactStep
• iteSpec : LamSort → FactStep

instance Auto.Embedding.Lam.instInhabitedFactStep : Inhabited FactStep

Equations

• Auto.Embedding.Lam.instInhabitedFactStep = { default := Auto.Embedding.Lam.FactStep.boolFacts }

instance Auto.Embedding.Lam.instHashableFactStep : Hashable FactStep

Equations

• Auto.Embedding.Lam.instHashableFactStep = { hash := Auto.Embedding.Lam.hashFactStep✝ }

instance Auto.Embedding.Lam.instBEqFactStep : BEq FactStep

Equations

• Auto.Embedding.Lam.instBEqFactStep = { beq := Auto.Embedding.Lam.beqFactStep✝ }

instance Auto.Embedding.Lam.instToExprFactStep : Lean.ToExpr FactStep

Equations

• Auto.Embedding.Lam.instToExprFactStep = { toExpr := Auto.Embedding.Lam.toExprFactStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.FactStep [] }

inductive Auto.Embedding.Lam.InferenceStep : Type

• validOfBVarLower (pv pn : Nat) : InferenceStep

  If t has no loose bvar 0 and s is inhabited (pn), then ∀ (_ : s), t (pv) implies LamTerm.instantiate1 (.atom 0) t

• validOfBVarLowers (pv : Nat) (pns : List Nat) : InferenceStep

  Equivalent to repeated validOfBVarLower

• validOfImp (p₁₂ p₁ : Nat) : InferenceStep

  t₁ → t₂ and t₁ implies t₂

• validOfImps (imp : Nat) (ps : List Nat) : InferenceStep

  t₁ → t₂ → ⋯ → tₖ → s and t₁, t₂, ⋯, tₖ implies s

• validOfInstantiate1 (pos : Nat) (arg : LamTerm) : InferenceStep

  .bvar 0 replaced with arg

• validOfInstantiate (pos : Nat) (args : List LamTerm) : InferenceStep

  Call validOfInstantiate1 sequentially on arg[0] ⋯ args[k-1] Note that .bvar i is not always replaced with args[i] because later instantiations will lower bvars in args[i] and may further instantiate bound variables occurring in args[i]

• validOfInstantiateRev (pos : Nat) (args : List LamTerm) : InferenceStep

  Call validOfInstantiate1 sequentially on arg[k-1] ⋯ args[0] Note that .bvar i is not always replaced with args.reverse[i] because later instantiations will lower bvars in args.reverse[i] and may further instantiate bound variables occurring in args.reverse[i]

• validOfEqualize (pos : Nat) (occ : List Bool) : InferenceStep
• validOfAndLeft (pos : Nat) (occ : List Bool) : InferenceStep
• validOfAndRight (pos : Nat) (occ : List Bool) : InferenceStep

instance Auto.Embedding.Lam.instInhabitedInferenceStep : Inhabited InferenceStep

Equations

• Auto.Embedding.Lam.instInhabitedInferenceStep = { default := Auto.Embedding.Lam.InferenceStep.validOfBVarLower default default }

instance Auto.Embedding.Lam.instHashableInferenceStep : Hashable InferenceStep

Equations

• Auto.Embedding.Lam.instHashableInferenceStep = { hash := Auto.Embedding.Lam.hashInferenceStep✝ }

instance Auto.Embedding.Lam.instBEqInferenceStep : BEq InferenceStep

Equations

• Auto.Embedding.Lam.instBEqInferenceStep = { beq := Auto.Embedding.Lam.beqInferenceStep✝ }

instance Auto.Embedding.Lam.instToExprInferenceStep : Lean.ToExpr InferenceStep

Equations

• Auto.Embedding.Lam.instToExprInferenceStep = { toExpr := Auto.Embedding.Lam.toExprInferenceStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.InferenceStep [] }

inductive Auto.Embedding.Lam.LCtxStep : Type

• validOfIntro1F (pos : Nat) : LCtxStep
• validOfIntro1H (pos : Nat) : LCtxStep
• validOfIntros (pos idx : Nat) : LCtxStep
• validOfRevert (pos : Nat) : LCtxStep
• validOfReverts (pos idx : Nat) : LCtxStep
• validOfAppend (pos : Nat) (ex : List LamSort) : LCtxStep

  valid lctx t => valid (lctx ++ ex) t

• validOfPrepend (pos : Nat) (ex : List LamSort) : LCtxStep

  valid lctx t => valid (ex ++ lctx) (t.bvarLifts ex.length)

instance Auto.Embedding.Lam.instInhabitedLCtxStep : Inhabited LCtxStep

Equations

• Auto.Embedding.Lam.instInhabitedLCtxStep = { default := Auto.Embedding.Lam.LCtxStep.validOfIntro1F default }

instance Auto.Embedding.Lam.instHashableLCtxStep : Hashable LCtxStep

Equations

• Auto.Embedding.Lam.instHashableLCtxStep = { hash := Auto.Embedding.Lam.hashLCtxStep✝ }

instance Auto.Embedding.Lam.instBEqLCtxStep : BEq LCtxStep

Equations

• Auto.Embedding.Lam.instBEqLCtxStep = { beq := Auto.Embedding.Lam.beqLCtxStep✝ }

instance Auto.Embedding.Lam.instToExprLCtxStep : Lean.ToExpr LCtxStep

Equations

• Auto.Embedding.Lam.instToExprLCtxStep = { toExpr := Auto.Embedding.Lam.toExprLCtxStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.LCtxStep [] }

inductive Auto.Embedding.Lam.NonemptyStep : Type

• nonemptyOfAtom (n : Nat) : NonemptyStep
• nonemptyOfEtom (n : Nat) : NonemptyStep

instance Auto.Embedding.Lam.instInhabitedNonemptyStep : Inhabited NonemptyStep

Equations

• Auto.Embedding.Lam.instInhabitedNonemptyStep = { default := Auto.Embedding.Lam.NonemptyStep.nonemptyOfAtom default }

instance Auto.Embedding.Lam.instHashableNonemptyStep : Hashable NonemptyStep

Equations

• Auto.Embedding.Lam.instHashableNonemptyStep = { hash := Auto.Embedding.Lam.hashNonemptyStep✝ }

instance Auto.Embedding.Lam.instBEqNonemptyStep : BEq NonemptyStep

Equations

• Auto.Embedding.Lam.instBEqNonemptyStep = { beq := Auto.Embedding.Lam.beqNonemptyStep✝ }

instance Auto.Embedding.Lam.instToExprNonemptyStep : Lean.ToExpr NonemptyStep

Equations

• Auto.Embedding.Lam.instToExprNonemptyStep = { toExpr := Auto.Embedding.Lam.toExprNonemptyStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.NonemptyStep [] }

inductive Auto.Embedding.Lam.PrepConvStep : Type

• validOfPropNeEquivEqNot : PrepConvStep

  (a ≠ b) ↔ (a = (¬ b))

• validOfTrueEqFalseEquivFalse : PrepConvStep

  (True = False) ↔ False

• validOfFalseEqTrueEquivFalse : PrepConvStep

  (False = True) ↔ False

• validOfEqTrueEquiv : PrepConvStep

  (a = True) ↔ a

• validOfEqFalseEquiv : PrepConvStep

  (a = False) ↔ (¬ a)

• validOfNeTrueEquivEqFalse : PrepConvStep

  (a ≠ True) ↔ (a = False)

• validOfNeFalseEquivEqTrue : PrepConvStep

  (a ≠ False) ↔ (a = True)

• validOfNotEqTrueEquivEqFalse : PrepConvStep

  ((¬ a) = True) ↔ (a = False)

• validOfNotEqFalseEquivEqTrue : PrepConvStep

  ((¬ a) = False) ↔ (a = True)

• validOfNotNotEquiv : PrepConvStep

  (¬¬a) ↔ a

• validOfNotEqEquivEqNot : PrepConvStep

  ((¬ a) = b) ↔ (a = (¬ b))

• validOfNotEqNotEquivEq : PrepConvStep

  ((¬ a) = (¬ b)) ↔ (a = b)

• validOfPropext : PrepConvStep

  (a ↔ b) ↔ (a = b)

• validOfNotAndEquivNotOrNot : PrepConvStep

  (¬ (a ∧ b)) ↔ (¬ a ∨ ¬ b)

• validOfNotOrEquivNotAndNot : PrepConvStep

  (¬ (a ∨ b)) ↔ (¬ a ∧ ¬ b)

• validOfImpEquivNotOr : PrepConvStep

  (a → b) ↔ (¬ a ∨ b)

• validOfNotImpEquivAndNot : PrepConvStep

  (¬ (a → b)) ↔ (a ∧ ¬ b)

• validOfPropEq : PrepConvStep

  (a = b) ↔ (a ∨ ¬ b) ∧ (¬ a ∨ b)

• validOfPropNe : PrepConvStep

  (a = b) ↔ (a ∨ b) ∧ (¬ a ∨ ¬ b)

• validOfPushBVCast : PrepConvStep

  Basic BitVec simplification operations

instance Auto.Embedding.Lam.instInhabitedPrepConvStep : Inhabited PrepConvStep

Equations

• Auto.Embedding.Lam.instInhabitedPrepConvStep = { default := Auto.Embedding.Lam.PrepConvStep.validOfPropNeEquivEqNot }

instance Auto.Embedding.Lam.instHashablePrepConvStep : Hashable PrepConvStep

Equations

• Auto.Embedding.Lam.instHashablePrepConvStep = { hash := Auto.Embedding.Lam.hashPrepConvStep✝ }

instance Auto.Embedding.Lam.instBEqPrepConvStep : BEq PrepConvStep

Equations

• Auto.Embedding.Lam.instBEqPrepConvStep = { beq := Auto.Embedding.Lam.beqPrepConvStep✝ }

instance Auto.Embedding.Lam.instToExprPrepConvStep : Lean.ToExpr PrepConvStep

Equations

• Auto.Embedding.Lam.instToExprPrepConvStep = { toExpr := Auto.Embedding.Lam.toExprPrepConvStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.PrepConvStep [] }

inductive Auto.Embedding.Lam.WFStep : Type

• wfOfCheck (lctx : List LamSort) (t : LamTerm) : WFStep
• wfOfAppend (pos : Nat) (ex : List LamSort) : WFStep

  wf lctx s t => wf (lctx ++ ex) s t

• wfOfPrepend (pos : Nat) (ex : List LamSort) : WFStep

  wf lctx s t => wf (ex ++ lctx) s (t.bvarLifts ex.length)

• wfOfHeadBeta (pos : Nat) : WFStep
• wfOfBetaBounded (pos bound : Nat) : WFStep

instance Auto.Embedding.Lam.instInhabitedWFStep : Inhabited WFStep

Equations

• Auto.Embedding.Lam.instInhabitedWFStep = { default := Auto.Embedding.Lam.WFStep.wfOfCheck default default }

instance Auto.Embedding.Lam.instHashableWFStep : Hashable WFStep

Equations

• Auto.Embedding.Lam.instHashableWFStep = { hash := Auto.Embedding.Lam.hashWFStep✝ }

instance Auto.Embedding.Lam.instBEqWFStep : BEq WFStep

Equations

• Auto.Embedding.Lam.instBEqWFStep = { beq := Auto.Embedding.Lam.beqWFStep✝ }

instance Auto.Embedding.Lam.instToExprWFStep : Lean.ToExpr WFStep

Equations

• Auto.Embedding.Lam.instToExprWFStep = { toExpr := Auto.Embedding.Lam.toExprWFStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.WFStep [] }

inductive Auto.Embedding.Lam.ChkStep : Type

• c : ConvStep → ChkStep
• ca : ConvAtStep → ChkStep
• e : EtomStep → ChkStep
• f : FactStep → ChkStep
• i : InferenceStep → ChkStep
• l : LCtxStep → ChkStep
• n : NonemptyStep → ChkStep
• p : PrepConvStep → Nat → List Bool → ChkStep
• w : WFStep → ChkStep

instance Auto.Embedding.Lam.instInhabitedChkStep : Inhabited ChkStep

Equations

• Auto.Embedding.Lam.instInhabitedChkStep = { default := Auto.Embedding.Lam.ChkStep.c default }

instance Auto.Embedding.Lam.instHashableChkStep : Hashable ChkStep

Equations

• Auto.Embedding.Lam.instHashableChkStep = { hash := Auto.Embedding.Lam.hashChkStep✝ }

instance Auto.Embedding.Lam.instBEqChkStep : BEq ChkStep

Equations

• Auto.Embedding.Lam.instBEqChkStep = { beq := Auto.Embedding.Lam.beqChkStep✝ }

instance Auto.Embedding.Lam.instToExprChkStep : Lean.ToExpr ChkStep

Equations

• Auto.Embedding.Lam.instToExprChkStep = { toExpr := Auto.Embedding.Lam.toExprChkStep✝, toTypeExpr := Lean.Expr.const `Auto.Embedding.Lam.ChkStep [] }

def Auto.Embedding.Lam.ConvStep.toString : ConvStep → String

Equations

• (Auto.Embedding.Lam.ConvStep.validOfHeadBeta a).toString = toString "validOfHeadBeta " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfBetaBounded a a_1).toString = toString "validOfBetaBounded " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfExtensionalize a).toString = toString "validOfExtensionalize " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfEqSymm a).toString = toString "validOfEqSymm " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfMp a a_1).toString = toString "validOfMp " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfMpAll a a_1).toString = toString "validOfMpAll " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfCongrArg a a_1).toString = toString "validOfCongrArg " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfCongrFun a a_1).toString = toString "validOfCongrFun " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfCongr a a_1 a_2).toString = toString "validOfCongr " ++ toString a ++ toString " " ++ toString a_1 ++ toString " " ++ toString a_2 ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfCongrArgs a a_1).toString = toString "validOfCongrArgs " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfCongrFunN a a_1 a_2).toString = toString "validOfCongrFunN " ++ toString a ++ toString " " ++ toString a_1 ++ toString " " ++ toString a_2 ++ toString ""
• (Auto.Embedding.Lam.ConvStep.validOfCongrs a a_1 a_2).toString = toString "validOfCongrs " ++ toString a ++ toString " " ++ toString a_1 ++ toString " " ++ toString a_2 ++ toString ""

def Auto.Embedding.Lam.ConvAtStep.toString : ConvAtStep → String

Equations

• One or more equations did not get rendered due to their size.
• (Auto.Embedding.Lam.ConvAtStep.validOfEtaExpand1At a a_1).toString = toString "validOfEtaExpand1At " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvAtStep.validOfEtaReduce1At a a_1).toString = toString "validOfEtaReduce1At " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvAtStep.validOfExtensionalizeEqAt a a_1).toString = toString "validOfExtensionalizeEqAt " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.ConvAtStep.validOfIntensionalizeEqAt a a_1).toString = toString "validOfIntensionalizeEqAt " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""

def Auto.Embedding.Lam.EtomStep.toString : EtomStep → String

Equations

• (Auto.Embedding.Lam.EtomStep.skolemize a).toString = toString "skolemize " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.EtomStep.define a).toString = toString "define " ++ toString a ++ toString ""

def Auto.Embedding.Lam.FactStep.toString : FactStep → String

Equations

• Auto.Embedding.Lam.FactStep.boolFacts.toString = toString "boolFacts"
• (Auto.Embedding.Lam.FactStep.iteSpec a).toString = toString "iteSpec " ++ toString a ++ toString ""

def Auto.Embedding.Lam.InferenceStep.toString : InferenceStep → String

Equations

• (Auto.Embedding.Lam.InferenceStep.validOfBVarLower a a_1).toString = toString "validOfBVarLower " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfBVarLowers a a_1).toString = toString "validOfBVarLowers " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfImp a a_1).toString = toString "validOfImp " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfImps a a_1).toString = toString "validOfImps " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfInstantiate1 a a_1).toString = toString "validOfInstantiate1 " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfInstantiate a a_1).toString = toString "validOfInstantiate " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfInstantiateRev a a_1).toString = toString "validOfInstantiateRev " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfEqualize a a_1).toString = toString "validOfEqualize " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfAndLeft a a_1).toString = toString "validOfAndLeft " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.InferenceStep.validOfAndRight a a_1).toString = toString "validOfAndRight " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""

def Auto.Embedding.Lam.LCtxStep.toString : LCtxStep → String

Equations

• (Auto.Embedding.Lam.LCtxStep.validOfIntro1F a).toString = toString "validOfIntro1F " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.LCtxStep.validOfIntro1H a).toString = toString "validOfIntro1H " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.LCtxStep.validOfIntros a a_1).toString = toString "validOfIntros " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.LCtxStep.validOfRevert a).toString = toString "validOfRevert " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.LCtxStep.validOfReverts a a_1).toString = toString "validOfReverts " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.LCtxStep.validOfAppend a a_1).toString = toString "validOfAppend " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.LCtxStep.validOfPrepend a a_1).toString = toString "validOfPrepend " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""

def Auto.Embedding.Lam.NonemptyStep.toString : NonemptyStep → String

Equations

• (Auto.Embedding.Lam.NonemptyStep.nonemptyOfAtom a).toString = toString "nonemptyOfAtom " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.NonemptyStep.nonemptyOfEtom a).toString = toString "nonemptyOfEtom " ++ toString a ++ toString ""

def Auto.Embedding.Lam.PrepConvStep.toString : PrepConvStep → String

Equations

• Auto.Embedding.Lam.PrepConvStep.validOfPropNeEquivEqNot.toString = toString "validOfPropNeEquivEqNot"
• Auto.Embedding.Lam.PrepConvStep.validOfTrueEqFalseEquivFalse.toString = toString "validOfTrueEqFalseEquivFalse"
• Auto.Embedding.Lam.PrepConvStep.validOfFalseEqTrueEquivFalse.toString = toString "validOfFalseEqTrueEquivFalse"
• Auto.Embedding.Lam.PrepConvStep.validOfEqTrueEquiv.toString = toString "validOfEqTrueEquiv"
• Auto.Embedding.Lam.PrepConvStep.validOfEqFalseEquiv.toString = toString "validOfEqFalseEquiv"
• Auto.Embedding.Lam.PrepConvStep.validOfNeTrueEquivEqFalse.toString = toString "validOfNeTrueEquivEqFalse"
• Auto.Embedding.Lam.PrepConvStep.validOfNeFalseEquivEqTrue.toString = toString "validOfNeFalseEquivEqTrue"
• Auto.Embedding.Lam.PrepConvStep.validOfNotEqTrueEquivEqFalse.toString = toString "validOfNotEqTrueEquivEqFalse"
• Auto.Embedding.Lam.PrepConvStep.validOfNotEqFalseEquivEqTrue.toString = toString "validOfNotEqFalseEquivEqTrue"
• Auto.Embedding.Lam.PrepConvStep.validOfNotNotEquiv.toString = toString "validOfNotNotEquiv"
• Auto.Embedding.Lam.PrepConvStep.validOfNotEqEquivEqNot.toString = toString "validOfNotEqEquivEqNot"
• Auto.Embedding.Lam.PrepConvStep.validOfNotEqNotEquivEq.toString = toString "validOfNotEqNotEquivEq"
• Auto.Embedding.Lam.PrepConvStep.validOfPropext.toString = toString "validOfPropext"
• Auto.Embedding.Lam.PrepConvStep.validOfNotAndEquivNotOrNot.toString = toString "validOfNotAndEquivNotOrNot"
• Auto.Embedding.Lam.PrepConvStep.validOfNotOrEquivNotAndNot.toString = toString "validOfNotOrEquivNotAndNot"
• Auto.Embedding.Lam.PrepConvStep.validOfImpEquivNotOr.toString = toString "validOfImpEquivNotOr"
• Auto.Embedding.Lam.PrepConvStep.validOfNotImpEquivAndNot.toString = toString "validOfNotImpEquivAndNot"
• Auto.Embedding.Lam.PrepConvStep.validOfPropEq.toString = toString "validOfPropEq"
• Auto.Embedding.Lam.PrepConvStep.validOfPropNe.toString = toString "validOfPropNe"
• Auto.Embedding.Lam.PrepConvStep.validOfPushBVCast.toString = toString "validOfPushBVCast"

def Auto.Embedding.Lam.WFStep.toString : WFStep → String

Equations

• (Auto.Embedding.Lam.WFStep.wfOfCheck a a_1).toString = toString "wfOfCheck " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.WFStep.wfOfAppend a a_1).toString = toString "wfOfAppend " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.WFStep.wfOfPrepend a a_1).toString = toString "wfOfPrepend " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Embedding.Lam.WFStep.wfOfHeadBeta a).toString = toString "wfOfHeadBeta " ++ toString a ++ toString ""
• (Auto.Embedding.Lam.WFStep.wfOfBetaBounded a a_1).toString = toString "wfOfBetaBounded " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""

def Auto.Embedding.Lam.ChkStep.toString : ChkStep → String

Equations

• (Auto.Embedding.Lam.ChkStep.c a).toString = a.toString
• (Auto.Embedding.Lam.ChkStep.ca a).toString = a.toString
• (Auto.Embedding.Lam.ChkStep.e a).toString = a.toString
• (Auto.Embedding.Lam.ChkStep.f a).toString = a.toString
• (Auto.Embedding.Lam.ChkStep.i a).toString = a.toString
• (Auto.Embedding.Lam.ChkStep.l a).toString = a.toString
• (Auto.Embedding.Lam.ChkStep.n a).toString = a.toString
• (Auto.Embedding.Lam.ChkStep.p a a_1 a_2).toString = toString "" ++ toString a.toString ++ toString " " ++ toString a_1 ++ toString " " ++ toString a_2 ++ toString ""
• (Auto.Embedding.Lam.ChkStep.w a).toString = a.toString

instance Auto.Embedding.Lam.instToStringChkStep : ToString ChkStep

Equations

• Auto.Embedding.Lam.instToStringChkStep = { toString := Auto.Embedding.Lam.ChkStep.toString }

def Auto.Embedding.Lam.ConvStep.premises : ConvStep → List Nat

Equations

• (Auto.Embedding.Lam.ConvStep.validOfHeadBeta a).premises = [a]
• (Auto.Embedding.Lam.ConvStep.validOfBetaBounded a a_1).premises = [a]
• (Auto.Embedding.Lam.ConvStep.validOfExtensionalize a).premises = [a]
• (Auto.Embedding.Lam.ConvStep.validOfEqSymm a).premises = [a]
• (Auto.Embedding.Lam.ConvStep.validOfMp a a_1).premises = [a, a_1]
• (Auto.Embedding.Lam.ConvStep.validOfMpAll a a_1).premises = [a, a_1]
• (Auto.Embedding.Lam.ConvStep.validOfCongrArg a a_1).premises = [a, a_1]
• (Auto.Embedding.Lam.ConvStep.validOfCongrFun a a_1).premises = [a, a_1]
• (Auto.Embedding.Lam.ConvStep.validOfCongr a a_1 a_2).premises = [a, a_1, a_2]
• (Auto.Embedding.Lam.ConvStep.validOfCongrArgs a a_1).premises = a :: a_1
• (Auto.Embedding.Lam.ConvStep.validOfCongrFunN a a_1 a_2).premises = [a, a_1]
• (Auto.Embedding.Lam.ConvStep.validOfCongrs a a_1 a_2).premises = a :: a_1 :: a_2

def Auto.Embedding.Lam.ConvAtStep.premises : ConvAtStep → List Nat

Equations

• (Auto.Embedding.Lam.ConvAtStep.validOfEtaExpand1At a a_1).premises = [a]
• (Auto.Embedding.Lam.ConvAtStep.validOfEtaReduce1At a a_1).premises = [a]
• (Auto.Embedding.Lam.ConvAtStep.validOfEtaExpandNAt a a_1 a_2).premises = [a]
• (Auto.Embedding.Lam.ConvAtStep.validOfEtaReduceNAt a a_1 a_2).premises = [a]
• (Auto.Embedding.Lam.ConvAtStep.validOfExtensionalizeEqAt a a_1).premises = [a]
• (Auto.Embedding.Lam.ConvAtStep.validOfExtensionalizeEqFNAt a a_1 a_2).premises = [a]
• (Auto.Embedding.Lam.ConvAtStep.validOfIntensionalizeEqAt a a_1).premises = [a]

def Auto.Embedding.Lam.EtomStep.premises : EtomStep → List Nat

Equations

• (Auto.Embedding.Lam.EtomStep.skolemize a).premises = [a]
• (Auto.Embedding.Lam.EtomStep.define a).premises = []

def Auto.Embedding.Lam.FactStep.premises : FactStep → List Nat

Equations

• Auto.Embedding.Lam.FactStep.boolFacts.premises = []
• (Auto.Embedding.Lam.FactStep.iteSpec a).premises = []

def Auto.Embedding.Lam.InferenceStep.premises : InferenceStep → List Nat

Equations

• (Auto.Embedding.Lam.InferenceStep.validOfBVarLower a a_1).premises = [a, a_1]
• (Auto.Embedding.Lam.InferenceStep.validOfBVarLowers a a_1).premises = a :: a_1
• (Auto.Embedding.Lam.InferenceStep.validOfImp a a_1).premises = [a, a_1]
• (Auto.Embedding.Lam.InferenceStep.validOfImps a a_1).premises = a :: a_1
• (Auto.Embedding.Lam.InferenceStep.validOfInstantiate1 a a_1).premises = [a]
• (Auto.Embedding.Lam.InferenceStep.validOfInstantiate a a_1).premises = [a]
• (Auto.Embedding.Lam.InferenceStep.validOfInstantiateRev a a_1).premises = [a]
• (Auto.Embedding.Lam.InferenceStep.validOfEqualize a a_1).premises = [a]
• (Auto.Embedding.Lam.InferenceStep.validOfAndLeft a a_1).premises = [a]
• (Auto.Embedding.Lam.InferenceStep.validOfAndRight a a_1).premises = [a]

def Auto.Embedding.Lam.LCtxStep.premises : LCtxStep → List Nat

Equations

• (Auto.Embedding.Lam.LCtxStep.validOfIntro1F a).premises = [a]
• (Auto.Embedding.Lam.LCtxStep.validOfIntro1H a).premises = [a]
• (Auto.Embedding.Lam.LCtxStep.validOfIntros a a_1).premises = [a]
• (Auto.Embedding.Lam.LCtxStep.validOfRevert a).premises = [a]
• (Auto.Embedding.Lam.LCtxStep.validOfReverts a a_1).premises = [a]
• (Auto.Embedding.Lam.LCtxStep.validOfAppend a a_1).premises = [a]
• (Auto.Embedding.Lam.LCtxStep.validOfPrepend a a_1).premises = [a]

def Auto.Embedding.Lam.NonemptyStep.premises : NonemptyStep → List Nat

Equations

• (Auto.Embedding.Lam.NonemptyStep.nonemptyOfAtom a).premises = []
• (Auto.Embedding.Lam.NonemptyStep.nonemptyOfEtom a).premises = []

def Auto.Embedding.Lam.WFStep.premises : WFStep → List Nat

Whether a term is well-formed or not does not depend on assertions. So, the premises of a WFStep is deemed empty (although for some WFSteps they seem to have premise syntactically)

Equations

• x✝.premises = []

def Auto.Embedding.Lam.ChkStep.premises : ChkStep → List Nat

Equations

• (Auto.Embedding.Lam.ChkStep.c a).premises = a.premises
• (Auto.Embedding.Lam.ChkStep.ca a).premises = a.premises
• (Auto.Embedding.Lam.ChkStep.e a).premises = a.premises
• (Auto.Embedding.Lam.ChkStep.f a).premises = a.premises
• (Auto.Embedding.Lam.ChkStep.i a).premises = a.premises
• (Auto.Embedding.Lam.ChkStep.l a).premises = a.premises
• (Auto.Embedding.Lam.ChkStep.n a).premises = a.premises
• (Auto.Embedding.Lam.ChkStep.p a a_1 a_2).premises = [a_1]
• (Auto.Embedding.Lam.ChkStep.w a).premises = a.premises

inductive Auto.Embedding.Lam.EvalResult : Type

• fail : EvalResult
• addEntry (e : REntry) : EvalResult
• newEtomWithValid (s : LamSort) (lctx : List LamSort) (t : LamTerm) : EvalResult

instance Auto.Embedding.Lam.instInhabitedEvalResult : Inhabited EvalResult

Equations

• Auto.Embedding.Lam.instInhabitedEvalResult = { default := Auto.Embedding.Lam.EvalResult.fail }

instance Auto.Embedding.Lam.instHashableEvalResult : Hashable EvalResult

Equations

• Auto.Embedding.Lam.instHashableEvalResult = { hash := Auto.Embedding.Lam.hashEvalResult✝ }

instance Auto.Embedding.Lam.instBEqEvalResult : BEq EvalResult

Equations

• Auto.Embedding.Lam.instBEqEvalResult = { beq := Auto.Embedding.Lam.beqEvalResult✝ }

def Auto.Embedding.Lam.EvalResult.toString : EvalResult → String

Equations

• Auto.Embedding.Lam.EvalResult.fail.toString = "fail"
• (Auto.Embedding.Lam.EvalResult.addEntry a).toString = toString "addEntry (" ++ toString a ++ toString ")"
• (Auto.Embedding.Lam.EvalResult.newEtomWithValid a a_1 a_2).toString = toString "newEtomWithValid " ++ toString a ++ toString " " ++ toString a_1 ++ toString " " ++ toString a_2 ++ toString ""

instance Auto.Embedding.Lam.instToStringEvalResult : ToString EvalResult

Equations

• Auto.Embedding.Lam.instToStringEvalResult = { toString := Auto.Embedding.Lam.EvalResult.toString }

def Auto.Embedding.Lam.EvalResult.correct (r : RTable) (cv : CVal r.lamEVarTy) (res : EvalResult) : Prop

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.EvalResult.correct r cv Auto.Embedding.Lam.EvalResult.fail = True
• Auto.Embedding.Lam.EvalResult.correct r cv (Auto.Embedding.Lam.EvalResult.addEntry a) = Auto.Embedding.Lam.REntry.correct cv r.maxEVarSucc a

theorem Auto.Embedding.Lam.EvalResult.correct_newEtomWithValid_mpLamEVarTy {s : LamSort} {lctx : List LamSort} {t : LamTerm} {r : RTable} {cv : CVal r.lamEVarTy} (levt : Nat → LamSort) (heq : ∀ (n : Nat), levt n = ((r.lamEVarTy.insert r.maxEVarSucc s).get? n).getD (LamSort.base LamBaseSort.prop)) (H : ∃ (eVarVal' : (n : Nat) → LamSort.interp cv.tyVal (levt n)), (∀ (n : Nat), n < r.maxEVarSucc → eVarVal' n ≍ cv.eVarVal n) ∧ LamThmValid (cv.toLamValuationWithEVar levt eVarVal') lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc.succ) : correct r cv (newEtomWithValid s lctx t)

def Auto.Embedding.Lam.LCtxStep.evalValidOfIntros (lctx : List LamSort) (t : LamTerm) (idx : Nat) : EvalResult

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LCtxStep.evalValidOfIntros lctx t 0 = Auto.Embedding.Lam.EvalResult.addEntry (Auto.Embedding.Lam.REntry.valid lctx t)

def Auto.Embedding.Lam.LCtxStep.evalValidOfReverts (lctx : List LamSort) (t : LamTerm) (idx : Nat) : EvalResult

Equations

• Auto.Embedding.Lam.LCtxStep.evalValidOfReverts lctx t 0 = Auto.Embedding.Lam.EvalResult.addEntry (Auto.Embedding.Lam.REntry.valid lctx t)
• Auto.Embedding.Lam.LCtxStep.evalValidOfReverts [] t n.succ = Auto.Embedding.Lam.EvalResult.fail
• Auto.Embedding.Lam.LCtxStep.evalValidOfReverts (s :: lctx_2) t n.succ = Auto.Embedding.Lam.LCtxStep.evalValidOfReverts lctx_2 (Auto.Embedding.Lam.LamTerm.mkForallEF s t) n

def Auto.Embedding.Lam.InferenceStep.evalValidOfInstantiate (n : Nat) (ltv : LamTyVal) (lctx : List LamSort) (t : LamTerm) (args : List LamTerm) : EvalResult

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.InferenceStep.evalValidOfInstantiate n ltv lctx t [] = Auto.Embedding.Lam.EvalResult.addEntry (Auto.Embedding.Lam.REntry.valid lctx t)
• Auto.Embedding.Lam.InferenceStep.evalValidOfInstantiate n ltv [] t (arg :: args) = Auto.Embedding.Lam.EvalResult.fail

def Auto.Embedding.Lam.InferenceStep.evalValidOfBVarLowers (r : RTable) (lctx : List LamSort) (pns : List Nat) : Option (List LamSort)

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.InferenceStep.evalValidOfBVarLowers r lctx [] = some lctx

@[reducible]

def Auto.Embedding.Lam.ConvStep.eval (r : RTable) (cs : ConvStep) : EvalResult

Equations

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

@[reducible]

def Auto.Embedding.Lam.ConvAtStep.eval (r : RTable) (cs : ConvAtStep) : EvalResult

Equations

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

@[reducible]

def Auto.Embedding.Lam.EtomStep.eval (lvt lit : Nat → LamSort) (r : RTable) (cs : EtomStep) : EvalResult

Equations

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

@[reducible]

def Auto.Embedding.Lam.FactStep.eval (cs : FactStep) : EvalResult

Equations

• Auto.Embedding.Lam.FactStep.boolFacts.eval = Auto.Embedding.Lam.EvalResult.addEntry (Auto.Embedding.Lam.REntry.valid [] Auto.Embedding.Lam.LamTerm.boolFacts)
• (Auto.Embedding.Lam.FactStep.iteSpec a).eval = Auto.Embedding.Lam.EvalResult.addEntry (Auto.Embedding.Lam.REntry.valid [] (Auto.Embedding.Lam.LamTerm.iteSpec a))

@[reducible]

def Auto.Embedding.Lam.InferenceStep.eval (lvt lit : Nat → LamSort) (r : RTable) (cs : InferenceStep) : EvalResult

Equations

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

@[reducible]

def Auto.Embedding.Lam.LCtxStep.eval (r : RTable) (cs : LCtxStep) : EvalResult

Equations

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

@[reducible]

def Auto.Embedding.Lam.NonemptyStep.eval (lvt : Nat → LamSort) (r : RTable) (cs : NonemptyStep) : EvalResult

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.NonemptyStep.eval lvt r (Auto.Embedding.Lam.NonemptyStep.nonemptyOfAtom a) = Auto.Embedding.Lam.EvalResult.addEntry (Auto.Embedding.Lam.REntry.nonempty (lvt a))

@[reducible]

def Auto.Embedding.Lam.PrepConvStep.eval (cs : PrepConvStep) : LamTerm → Option LamTerm

Equations

• Auto.Embedding.Lam.PrepConvStep.validOfPropNeEquivEqNot.eval = Auto.Embedding.Lam.LamTerm.prop_ne_equiv_eq_not?
• Auto.Embedding.Lam.PrepConvStep.validOfTrueEqFalseEquivFalse.eval = Auto.Embedding.Lam.LamTerm.true_eq_false_equiv_false?
• Auto.Embedding.Lam.PrepConvStep.validOfFalseEqTrueEquivFalse.eval = Auto.Embedding.Lam.LamTerm.false_eq_true_equiv_false?
• Auto.Embedding.Lam.PrepConvStep.validOfEqTrueEquiv.eval = Auto.Embedding.Lam.LamTerm.eq_true_equiv?
• Auto.Embedding.Lam.PrepConvStep.validOfEqFalseEquiv.eval = Auto.Embedding.Lam.LamTerm.eq_false_equiv?
• Auto.Embedding.Lam.PrepConvStep.validOfNeTrueEquivEqFalse.eval = Auto.Embedding.Lam.LamTerm.ne_true_equiv_eq_false?
• Auto.Embedding.Lam.PrepConvStep.validOfNeFalseEquivEqTrue.eval = Auto.Embedding.Lam.LamTerm.ne_false_equiv_eq_true?
• Auto.Embedding.Lam.PrepConvStep.validOfNotEqTrueEquivEqFalse.eval = Auto.Embedding.Lam.LamTerm.not_eq_true_equiv_eq_false?
• Auto.Embedding.Lam.PrepConvStep.validOfNotEqFalseEquivEqTrue.eval = Auto.Embedding.Lam.LamTerm.not_eq_false_equiv_eq_true?
• Auto.Embedding.Lam.PrepConvStep.validOfNotNotEquiv.eval = Auto.Embedding.Lam.LamTerm.not_not_equiv?
• Auto.Embedding.Lam.PrepConvStep.validOfNotEqEquivEqNot.eval = Auto.Embedding.Lam.LamTerm.not_eq_equiv_eq_not?
• Auto.Embedding.Lam.PrepConvStep.validOfNotEqNotEquivEq.eval = Auto.Embedding.Lam.LamTerm.not_eq_not_equiv_eq?
• Auto.Embedding.Lam.PrepConvStep.validOfPropext.eval = Auto.Embedding.Lam.LamTerm.propext?
• Auto.Embedding.Lam.PrepConvStep.validOfNotAndEquivNotOrNot.eval = Auto.Embedding.Lam.LamTerm.not_and_equiv_not_or_not?
• Auto.Embedding.Lam.PrepConvStep.validOfNotOrEquivNotAndNot.eval = Auto.Embedding.Lam.LamTerm.not_or_equiv_not_and_not?
• Auto.Embedding.Lam.PrepConvStep.validOfImpEquivNotOr.eval = Auto.Embedding.Lam.LamTerm.imp_equiv_not_or?
• Auto.Embedding.Lam.PrepConvStep.validOfNotImpEquivAndNot.eval = Auto.Embedding.Lam.LamTerm.not_imp_equiv_and_not?
• Auto.Embedding.Lam.PrepConvStep.validOfPropEq.eval = Auto.Embedding.Lam.LamTerm.propeq?
• Auto.Embedding.Lam.PrepConvStep.validOfPropNe.eval = Auto.Embedding.Lam.LamTerm.propne?
• Auto.Embedding.Lam.PrepConvStep.validOfPushBVCast.eval = fun (t : Auto.Embedding.Lam.LamTerm) => some (Auto.Embedding.Lam.LamTerm.pushBVCast Auto.Embedding.Lam.BVCastType.none t)

@[reducible]

def Auto.Embedding.Lam.WFStep.eval (lvt lit : Nat → LamSort) (r : RTable) (cs : WFStep) : EvalResult

Equations

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

def Auto.Embedding.Lam.ChkStep.eval (lvt lit : Nat → LamSort) (r : RTable) (cs : ChkStep) : EvalResult

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.ChkStep.eval lvt lit r (Auto.Embedding.Lam.ChkStep.c a) = Auto.Embedding.Lam.ConvStep.eval r a
• Auto.Embedding.Lam.ChkStep.eval lvt lit r (Auto.Embedding.Lam.ChkStep.ca a) = Auto.Embedding.Lam.ConvAtStep.eval r a
• Auto.Embedding.Lam.ChkStep.eval lvt lit r (Auto.Embedding.Lam.ChkStep.e a) = Auto.Embedding.Lam.EtomStep.eval lvt lit r a
• Auto.Embedding.Lam.ChkStep.eval lvt lit r (Auto.Embedding.Lam.ChkStep.f a) = a.eval
• Auto.Embedding.Lam.ChkStep.eval lvt lit r (Auto.Embedding.Lam.ChkStep.i a) = Auto.Embedding.Lam.InferenceStep.eval lvt lit r a
• Auto.Embedding.Lam.ChkStep.eval lvt lit r (Auto.Embedding.Lam.ChkStep.l a) = Auto.Embedding.Lam.LCtxStep.eval r a
• Auto.Embedding.Lam.ChkStep.eval lvt lit r (Auto.Embedding.Lam.ChkStep.n a) = Auto.Embedding.Lam.NonemptyStep.eval lvt r a
• Auto.Embedding.Lam.ChkStep.eval lvt lit r (Auto.Embedding.Lam.ChkStep.w a) = Auto.Embedding.Lam.WFStep.eval lvt lit r a

theorem Auto.Embedding.Lam.LCtxStep.evalValidOfIntros_correct {lctx : List LamSort} {t : LamTerm} {idx : Nat} {r : RTable} (cv : CVal r.lamEVarTy) (tV : LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc) : EvalResult.correct r cv (evalValidOfIntros lctx t idx)

theorem Auto.Embedding.Lam.LCtxStep.evalValidOfReverts_correct {lctx : List LamSort} {t : LamTerm} {idx : Nat} {r : RTable} (cv : CVal r.lamEVarTy) (tV : LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc) : EvalResult.correct r cv (evalValidOfReverts lctx t idx)

theorem Auto.Embedding.Lam.InferenceStep.evalValidOfBVarLowers_correct {lctx : List LamSort} {pns : List Nat} {lctx' : List LamSort} {r : RTable} (cv : CVal r.lamEVarTy) (inv : r.inv cv) (heq : evalValidOfBVarLowers r lctx pns = some lctx') : ∃ (ss : List LamSort), ∃ (x : HList (LamNonempty cv.tyVal) ss), ss.length = pns.length ∧ lctx = ss ++ lctx'

theorem Auto.Embedding.Lam.InferenceStep.evalValidOfInstantiate_correct {lctx : List LamSort} {t : LamTerm} {args : List LamTerm} {r : RTable} (cv : CVal r.lamEVarTy) (tV : LamThmValid cv.toLamValuation lctx t ∧ t.maxEVarSucc ≤ r.maxEVarSucc) : EvalResult.correct r cv (evalValidOfInstantiate r.maxEVarSucc cv.toLamTyVal lctx t args)

theorem Auto.Embedding.Lam.ConvStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (inv : r.inv cv) (cs : ConvStep) : EvalResult.correct r cv (eval r cs)

theorem Auto.Embedding.Lam.EtomStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (inv : r.inv cv) (cs : EtomStep) : EvalResult.correct r cv (eval cv.toLamVarTy cv.toLamILTy r cs)

theorem Auto.Embedding.Lam.FactStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (cs : FactStep) : EvalResult.correct r cv cs.eval

theorem Auto.Embedding.Lam.InferenceStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (inv : r.inv cv) (cs : InferenceStep) : EvalResult.correct r cv (eval cv.toLamVarTy cv.toLamILTy r cs)

theorem Auto.Embedding.Lam.ConvAtStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (inv : r.inv cv) (cs : ConvAtStep) : EvalResult.correct r cv (eval r cs)

theorem Auto.Embedding.Lam.LCtxStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (inv : r.inv cv) (cs : LCtxStep) : EvalResult.correct r cv (eval r cs)

theorem Auto.Embedding.Lam.NonemptyStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (cs : NonemptyStep) : EvalResult.correct r cv (eval cv.toLamVarTy r cs)

theorem Auto.Embedding.Lam.PrepConvStep.eval_correct (lval : LamValuation) (cs : PrepConvStep) : LamGenConv lval cs.eval ∧ LamTerm.evarBounded cs.eval 0

theorem Auto.Embedding.Lam.WFStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (inv : r.inv cv) (cs : WFStep) : EvalResult.correct r cv (eval cv.toLamVarTy cv.toLamILTy r cs)

theorem Auto.Embedding.Lam.ChkStep.eval_correct (r : RTable) (cv : CVal r.lamEVarTy) (inv : r.inv cv) (cs : ChkStep) : EvalResult.correct r cv (eval cv.toLamVarTy cv.toLamILTy r cs)

def Auto.Embedding.Lam.RTable.runEvalResult (r : RTable) (n : Nat) : EvalResult → RTable

Equations

• One or more equations did not get rendered due to their size.
• r.runEvalResult n Auto.Embedding.Lam.EvalResult.fail = r
• r.runEvalResult n (Auto.Embedding.Lam.EvalResult.addEntry a) = { entries := r.entries.insert n a, maxEVarSucc := r.maxEVarSucc, lamEVarTy := r.lamEVarTy }

@[reducible, inline]

abbrev Auto.Embedding.Lam.ChkSteps : Type

The first ChkStep specifies the checker step The second Nat specifies the position to insert the resulting term Note that

1. All entries (x : ChkStep × Nat) that insert result into the wf table should have distinct second component
2. All entries (x : ChkStep × Nat) that insert result into the valid table should have distinct second component Note that we decide where (wf or valid) to insert the resulting term by looking at (c : ChkStep).eval

Equations

• Auto.Embedding.Lam.ChkSteps = Auto.BinTree (Auto.Embedding.Lam.ChkStep × Nat)

def Auto.Embedding.Lam.ChkStep.run (lvt lit : Nat → LamSort) (r : RTable) (c : ChkStep) (n : Nat) : RTable

Equations

• Auto.Embedding.Lam.ChkStep.run lvt lit r c n = r.runEvalResult n (Auto.Embedding.Lam.ChkStep.eval lvt lit r c)

theorem Auto.Embedding.Lam.ChkStep.run_correct (r : RTable) (cpv : CPVal) (inv : ∃ (eV : (n : Nat) → LamSort.interp cpv.tyVal ((r.lamEVarTy.get? n).getD (LamSort.base LamBaseSort.prop))), r.inv { toCPVal := cpv, eVarVal := eV }) (c : ChkStep) (n : Nat) : ∃ (eV' : (n_1 : Nat) → LamSort.interp cpv.tyVal (((run cpv.toLamVarTy cpv.toLamILTy r c n).lamEVarTy.get? n_1).getD (LamSort.base LamBaseSort.prop))), (run cpv.toLamVarTy cpv.toLamILTy r c n).inv { toCPVal := cpv, eVarVal := eV' }

def Auto.Embedding.Lam.ChkSteps.run (lvt lit : Nat → LamSort) (r : RTable) (cs : ChkSteps) : RTable

Equations

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

theorem Auto.Embedding.Lam.ChkSteps.run_correct (r : RTable) (cpv : CPVal) (inv : ∃ (eV : (n : Nat) → LamSort.interp cpv.tyVal ((r.lamEVarTy.get? n).getD (LamSort.base LamBaseSort.prop))), r.inv { toCPVal := cpv, eVarVal := eV }) (cs : ChkSteps) : ∃ (eV' : (n : Nat) → LamSort.interp cpv.tyVal (((run cpv.toLamVarTy cpv.toLamILTy r cs).lamEVarTy.get? n).getD (LamSort.base LamBaseSort.prop))), (run cpv.toLamVarTy cpv.toLamILTy r cs).inv { toCPVal := cpv, eVarVal := eV' }

def Auto.Embedding.Lam.ChkSteps.runFromBeginning (cpv : CPVal) (it : ImportTable cpv) (cs : ChkSteps) : RTable

Equations

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

theorem Auto.Embedding.Lam.CheckerAux (cpv : CPVal) (it : ImportTable cpv) (cs : ChkSteps) : ∃ (eV : (n : Nat) → LamSort.interp cpv.tyVal (((ChkSteps.runFromBeginning cpv it cs).lamEVarTy.get? n).getD (LamSort.base LamBaseSort.prop))), (ChkSteps.runFromBeginning cpv it cs).inv { toCPVal := cpv, eVarVal := eV }

Note : Using this theorem directly in the checker will cause performance issue, especially when there are a lot of etoms. This is probably caused by the type of eV in ∃ eV being dependent on the result of ChkSteps.runFromBeginning

theorem Auto.Embedding.Lam.Checker.getValidExport_directReduce {lctx : List LamSort} {t : LamTerm} (cpv : CPVal) (it : ImportTable cpv) (cs : ChkSteps) (v : Nat) (heq : (ChkSteps.runFromBeginning cpv it cs).getValidExport v = some (lctx, t)) : LamThmValid cpv.toLamValuationEraseEtom lctx t

theorem Auto.Embedding.Lam.Checker.getValidExport_indirectReduceAux (cpv : CPVal) (it : ImportTable cpv) (cs : ChkSteps) (v : Nat) (importFacts : BinTree REntry) (hImport : it.importFacts = importFacts) (lvt lit : BinTree LamSort) (hlvt : lvt = BinTree.mapOpt (fun (x : (s : LamSort) × LamSort.interp cpv.tyVal s) => some x.fst) cpv.var) (hlit : lit = BinTree.mapOpt (fun (x : (s : LamSort) × ILLift (LamSort.interp cpv.tyVal s)) => some x.fst) cpv.il) (runResult : RTable) (runEq : ChkSteps.run (fun (n : Nat) => (lvt.get? n).getD (LamSort.base LamBaseSort.prop)) (fun (n : Nat) => (lit.get? n).getD (LamSort.base LamBaseSort.prop)) { entries := importFacts, maxEVarSucc := 0, lamEVarTy := BinTree.leaf } cs = runResult) (lctx : List LamSort) (t : LamTerm) (heq : runResult.getValidExport v = some (lctx, t)) : LamThmValid cpv.toLamValuationEraseEtom lctx t

Note : Do not use the counterpart of this theorem in proof by reflection. Surprisingly, if we use this theorem in proof by reflection, the performance issue will not be the ChkSteps.run in runEq. Instead, it would be caused by compiling the definition of runResult. I'm not sure why it's the case, but Lean sometimes exhibit superlinear (even quadratic) compilation time with respect to the size of runResult.

theorem Auto.Embedding.Lam.Checker.getValidExport_indirectReduce (cpv : CPVal) (it : ImportTable cpv) (cs : ChkSteps) (v : Nat) (importFacts : BinTree REntry) (hImport : it.importFacts = importFacts) (lvt lit : BinTree LamSort) (hlvt : lvt = BinTree.mapOpt (fun (x : (s : LamSort) × LamSort.interp cpv.tyVal s) => some x.fst) cpv.var) (hlit : lit = BinTree.mapOpt (fun (x : (s : LamSort) × ILLift (LamSort.interp cpv.tyVal s)) => some x.fst) cpv.il) (lctx : List LamSort) (t : LamTerm) (heq : (ChkSteps.run (fun (n : Nat) => (lvt.get? n).getD (LamSort.base LamBaseSort.prop)) (fun (n : Nat) => (lit.get? n).getD (LamSort.base LamBaseSort.prop)) { entries := importFacts, maxEVarSucc := 0, lamEVarTy := BinTree.leaf } cs).getValidExport v = some (lctx, t)) : LamThmValid cpv.toLamValuationEraseEtom lctx t

def Auto.Embedding.Lam.Checker.getValidExport_indirectReduce_reflection_runEq (lvt lit : BinTree LamSort) (importFacts : BinTree REntry) (cs : ChkSteps) (v : Nat) (lctx : List LamSort) (t : LamTerm) : Bool

Equations

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

theorem Auto.Embedding.Lam.Checker.getValidExport_indirectReduce_reflection (cpv : CPVal) (it : ImportTable cpv) (cs : ChkSteps) (v : Nat) (importFacts : BinTree REntry) (hImport : it.importFacts = importFacts) (lvt lit : BinTree LamSort) (hlvt : lvt = BinTree.mapOpt (fun (x : (s : LamSort) × LamSort.interp cpv.tyVal s) => some x.fst) cpv.var) (hlit : lit = BinTree.mapOpt (fun (x : (s : LamSort) × ILLift (LamSort.interp cpv.tyVal s)) => some x.fst) cpv.il) (lctx : List LamSort) (t : LamTerm) (heq : getValidExport_indirectReduce_reflection_runEq lvt lit importFacts cs v lctx t = true) : LamThmValid cpv.toLamValuationEraseEtom lctx t

structure Auto.Embedding.Lam.RTableStatus : Type

Checker utility

• rTable : Array REntry
• rTableTree : BinTree REntry
• nonemptyMap : Std.HashMap LamSort Nat
• wfMap : Std.HashMap (List LamSort × LamSort × LamTerm) Nat
• validMap : Std.HashMap (List LamSort × LamTerm) Nat
• maxEVarSucc : Nat
• lamEVarTy : Array LamSort
• lamEVarTyTree : BinTree LamSort
• chkMap : Std.HashMap REntry ChkStep

instance Auto.Embedding.Lam.instInhabitedRTableStatus : Inhabited RTableStatus

Equations

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

def Auto.Embedding.Lam.RTableStatus.push (rs : RTableStatus) (re : REntry) : RTableStatus

Equations

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

def Auto.Embedding.Lam.RTableStatus.addEntry (rs : RTableStatus) (c : ChkStep) (re : REntry) : RTableStatus

Equations

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

def Auto.Embedding.Lam.RTableStatus.newEtomWithValid (rs : RTableStatus) (c : ChkStep) (re : REntry) (s : LamSort) : RTableStatus

Equations

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

def Auto.Embedding.Lam.RTableStatus.findPos? (rs : RTableStatus) (re : REntry) : Option Nat

Equations

• rs.findPos? (Auto.Embedding.Lam.REntry.nonempty s) = rs.nonemptyMap.get? s
• rs.findPos? (Auto.Embedding.Lam.REntry.wf lctx s t) = rs.wfMap.get? (lctx, s, t)
• rs.findPos? (Auto.Embedding.Lam.REntry.valid lctx t) = rs.validMap.get? (lctx, t)