noncomputable def Auto.Embedding.Lam.LamTerm.interp (lval : LamValuation) (lctxTy : Nat → LamSort) (t : LamTerm) : (s : LamSort) × (((n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) → LamSort.interp lval.tyVal s)

Interpreting while typechecking a λ term. If the term fails to typecheck at some point, return ⟨.base .prop, GLift.up False⟩ as a default value.

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.interp lval lctxTy (Auto.Embedding.Lam.LamTerm.atom n) = ⟨lval.lamVarTy n, fun (x : (n : Nat) → Auto.Embedding.Lam.LamSort.interp lval.tyVal (lctxTy n)) => lval.varVal n⟩
• Auto.Embedding.Lam.LamTerm.interp lval lctxTy (Auto.Embedding.Lam.LamTerm.bvar n) = ⟨lctxTy n, fun (lctxTerm : (n : Nat) → Auto.Embedding.Lam.LamSort.interp lval.tyVal (lctxTy n)) => lctxTerm n⟩

theorem Auto.Embedding.Lam.LamTerm.interp_substLCtxTerm {t : LamTerm} (lval : LamValuation) {lctxTy lctxTy' : Nat → LamSort} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} {lctxTerm' : (n : Nat) → LamSort.interp lval.tyVal (lctxTy' n)} (HLCtxTyEq : lctxTy = lctxTy') (HLCtxTermEq : lctxTerm ≍ lctxTerm') : (interp lval lctxTy t).snd lctxTerm ≍ (interp lval lctxTy' t).snd lctxTerm'

noncomputable def Auto.Embedding.Lam.LamTerm.interpAsProp (lval : LamValuation) (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (t : LamTerm) : GLift Prop

Equations

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

theorem Auto.Embedding.Lam.LamTerm.interp_equiv {t : LamTerm} {rty : LamSort} (lval : LamValuation) (lctxTy : Nat → LamSort) (lwf : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t, rty := rty }) : ⟨rty, fun (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) => LamWF.interp lval lctxTy lctxTerm lwf⟩ = interp lval lctxTy t

theorem Auto.Embedding.Lam.LamThmValid.getDefault {lval : LamValuation} {t : LamTerm} (H : LamThmValid lval [] t) : (LamTerm.interpAsProp lval dfLCtxTy (dfLCtxTerm lval.tyVal) t).down

theorem Auto.Embedding.Lam.LamThmValid.getFalse {lval : LamValuation} (H : LamThmValid lval [] (LamTerm.base LamBaseTerm.falseE)) : False

theorem Auto.Embedding.Lam.LamThmValid.ofInterpAsProp (lval : LamValuation) (p : LamTerm) (h₁ : LamTerm.lamCheck? lval.toLamTyVal dfLCtxTy p = some (LamSort.base LamBaseSort.prop)) (h₂ : (LamTerm.interpAsProp lval dfLCtxTy (dfLCtxTerm lval.tyVal) p).down) (h₃ : p.maxLooseBVarSucc = 0) : LamThmValid lval [] p

Only accepts propositions p without loose bound variables

def Auto.Embedding.Lam.LamTerm.lamCheck?Eq (lval : LamValuation) (lctx : List LamSort) (t : LamTerm) (s : LamSort) : Prop

Equations

• Auto.Embedding.Lam.LamTerm.lamCheck?Eq lval lctx t s = (Auto.Embedding.Lam.LamTerm.lamCheck? lval.toLamTyVal (Auto.Embedding.pushLCtxs lctx Auto.Embedding.Lam.dfLCtxTy) t = some s)

def Auto.Embedding.Lam.LamTerm.lamCheck?Eq' (lval : LamValuation) (lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)) (t : LamTerm) (s : LamSort) : Prop

Equations

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

theorem Auto.Embedding.Lam.LamTerm.lamCheck?Eq'_ofLamCheck?Eq {lval : LamValuation} {t : LamTerm} {s : LamSort} {lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)} (H : lamCheck?Eq lval (List.map Sigma.fst lctx) t s) : lamCheck?Eq' lval lctx t s

def Auto.Embedding.Lam.LamTerm.interpEq (lval : LamValuation) (lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)) (t : LamTerm) {α : Type u} (val : α) : Prop

Equations

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

theorem Auto.Embedding.Lam.LamTerm.interpAsProp_of_interpEq {lval : LamValuation} {p : LamTerm} {ty : Prop} (proof : ty) (h₁ : lamCheck?Eq' lval [] p (LamSort.base LamBaseSort.prop)) (h₂ : interpEq lval [] p { down := ty }) : (interpAsProp lval dfLCtxTy (dfLCtxTerm lval.tyVal) p).down

theorem Auto.Embedding.Lam.LamTerm.lamCheck?Eq'_atom {lval : LamValuation} {lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)} {n : Nat} : lamCheck?Eq' lval lctx (atom n) (lval.lamVarTy n)

theorem Auto.Embedding.Lam.LamTerm.lamCheck?Eq'_etom {lval : LamValuation} {lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)} {n : Nat} : lamCheck?Eq' lval lctx (etom n) (lval.lamEVarTy n)

theorem Auto.Embedding.Lam.LamTerm.lamCheck?Eq'_base {lval : LamValuation} {lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)} {b : LamBaseTerm} : lamCheck?Eq' lval lctx (base b) (LamBaseTerm.lamCheck lval.toLamTyVal b)

theorem Auto.Embedding.Lam.LamTerm.lamCheck?Eq'_bvar {lval : LamValuation} {lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)} {n : Nat} {s : LamSort} {val : LamSort.interp lval.tyVal s} (h : lctx[n]? = some ⟨s, val⟩) : lamCheck?Eq' lval lctx (bvar n) s

theorem Auto.Embedding.Lam.LamTerm.lamCheck?Eq'_lam {lval : LamValuation} {argTy : LamSort} {val : LamSort.interp lval.tyVal argTy} {lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)} {body : LamTerm} {s : LamSort} (h : lamCheck?Eq' lval (⟨argTy, val⟩ :: lctx) body s) : lamCheck?Eq' lval lctx (lam argTy body) (argTy.func s)

theorem Auto.Embedding.Lam.LamTerm.lamCheck?Eq'_app {lval : LamValuation} {lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)} {fn : LamTerm} {argTy resTy : LamSort} {arg : LamTerm} (hFn : lamCheck?Eq' lval lctx fn (argTy.func resTy)) (hArg : lamCheck?Eq' lval lctx arg argTy) : lamCheck?Eq' lval lctx (app argTy fn arg) resTy

theorem Auto.Embedding.Lam.LamTerm.interpEq_atom {n : Nat} (lval : LamValuation) (lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)) (val : LamSort.interp lval.tyVal (lval.lamVarTy n)) (h : lval.varVal n = val) : interpEq lval lctx (atom n) val

theorem Auto.Embedding.Lam.LamTerm.interpEq_etom {n : Nat} (lval : LamValuation) (lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)) (val : LamSort.interp lval.tyVal (lval.lamEVarTy n)) (h : lval.eVarVal n = val) : interpEq lval lctx (etom n) val

theorem Auto.Embedding.Lam.LamTerm.interpEq_base {b : LamBaseTerm} (lval : LamValuation) (lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)) (val : LamSort.interp lval.tyVal (LamBaseTerm.lamCheck lval.toLamTyVal b)) (h : LamBaseTerm.interp lval b = val) : interpEq lval lctx (base b) val

theorem Auto.Embedding.Lam.LamTerm.interpEq_bvar {n : Nat} (lval : LamValuation) (lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)) (s : LamSort) (val : LamSort.interp lval.tyVal s) (h : lctx[n]? = some ⟨s, val⟩) : interpEq lval lctx (bvar n) val

theorem Auto.Embedding.Lam.LamTerm.interpEq_lam {β : Type u_1} {argTy : LamSort} {t : LamTerm} (lval : LamValuation) (lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)) (val : LamSort.interp lval.tyVal argTy → β) (hBody : ∀ (x : LamSort.interp lval.tyVal argTy), interpEq lval (⟨argTy, x⟩ :: lctx) t (val x)) : interpEq lval lctx (lam argTy t) val

theorem Auto.Embedding.Lam.LamTerm.interpEq_app {fn arg : LamTerm} (lval : LamValuation) (lctx : List ((s : LamSort) × LamSort.interp lval.tyVal s)) {argTy resTy : LamSort} (fnChk : lamCheck?Eq' lval lctx fn (argTy.func resTy)) (argChk : lamCheck?Eq' lval lctx arg argTy) (fnVal : LamSort.interp lval.tyVal argTy → LamSort.interp lval.tyVal resTy) (argVal : LamSort.interp lval.tyVal argTy) (hFn : interpEq lval lctx fn fnVal) (hArg : interpEq lval lctx arg argVal) : interpEq lval lctx (app argTy fn arg) (fnVal argVal)

structure Auto.Embedding.Lam.Interp.State : Type

• sortFVars : Array Lean.FVarId
• sortMap : Std.HashMap LamSort Lean.FVarId
• lctxTyRev : Array LamSort
• lctxTermRev : Array Lean.FVarId
• lctxTyDrop : Array Lean.FVarId
• typeEqFact : Std.HashMap (Nat × Nat) Lean.FVarId
• lctxTermDrop : Array Lean.FVarId
• termEqFact : Std.HashMap (Nat × Nat) Lean.FVarId
• lctxCon : Array Lean.FVarId

@[reducible, inline]

abbrev Auto.Embedding.Lam.Interp.InterpM (α : Type) : Type

Equations

• Auto.Embedding.Lam.Interp.InterpM = StateRefT' IO.RealWorld Auto.Embedding.Lam.Interp.State Auto.MetaState.MetaStateM

def Auto.Embedding.Lam.Interp.getLctxTyRev : InterpM (Array LamSort)

Equations

• Auto.Embedding.Lam.Interp.getLctxTyRev = do let st ← get pure st.lctxTyRev

def Auto.Embedding.Lam.Interp.getLctxTermRev : InterpM (Array Lean.FVarId)

Equations

• Auto.Embedding.Lam.Interp.getLctxTermRev = do let st ← get pure st.lctxTermRev

def Auto.Embedding.Lam.Interp.getLctxTermDrop : InterpM (Array Lean.FVarId)

Equations

• Auto.Embedding.Lam.Interp.getLctxTermDrop = do let st ← get pure st.lctxTermDrop

def Auto.Embedding.Lam.Interp.setTypeEqFact (field : Std.HashMap (Nat × Nat) Lean.FVarId) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.setLctxTermRev (field : Array Lean.FVarId) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.setLctxTyRev (field : Array LamSort) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.setLctxTermDrop (field : Array Lean.FVarId) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.getSortMap : InterpM (Std.HashMap LamSort Lean.FVarId)

Equations

• Auto.Embedding.Lam.Interp.getSortMap = do let st ← get pure st.sortMap

def Auto.Embedding.Lam.Interp.setLctxCon (field : Array Lean.FVarId) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.getLctxCon : InterpM (Array Lean.FVarId)

Equations

• Auto.Embedding.Lam.Interp.getLctxCon = do let st ← get pure st.lctxCon

def Auto.Embedding.Lam.Interp.setTermEqFact (field : Std.HashMap (Nat × Nat) Lean.FVarId) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.getTypeEqFact : InterpM (Std.HashMap (Nat × Nat) Lean.FVarId)

Equations

• Auto.Embedding.Lam.Interp.getTypeEqFact = do let st ← get pure st.typeEqFact

def Auto.Embedding.Lam.Interp.setSortMap (field : Std.HashMap LamSort Lean.FVarId) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.getLctxTyDrop : InterpM (Array Lean.FVarId)

Equations

• Auto.Embedding.Lam.Interp.getLctxTyDrop = do let st ← get pure st.lctxTyDrop

def Auto.Embedding.Lam.Interp.getSortFVars : InterpM (Array Lean.FVarId)

Equations

• Auto.Embedding.Lam.Interp.getSortFVars = do let st ← get pure st.sortFVars

def Auto.Embedding.Lam.Interp.getTermEqFact : InterpM (Std.HashMap (Nat × Nat) Lean.FVarId)

Equations

• Auto.Embedding.Lam.Interp.getTermEqFact = do let st ← get pure st.termEqFact

def Auto.Embedding.Lam.Interp.setLctxTyDrop (field : Array Lean.FVarId) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.setSortFVars (field : Array Lean.FVarId) : InterpM PUnit

Equations

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

def Auto.Embedding.Lam.Interp.getLCtxTy! (idx : Nat) : InterpM LamSort

Equations

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

def Auto.Embedding.Lam.Interp.sort2FVarId (s : LamSort) : InterpM Lean.FVarId

Turning a sort into fvar in a hash-consing manner For example, for .func (.atom 0) (.atom 0), we'll have

1. .atom 0 → fvar₀ := .atom 0
2. .func (.atom 0) (.atom 0) → fvar₁ := .func fvar₀ fvar₀

Equations

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

def Auto.Embedding.Lam.Interp.collectSortFor (ltv : LamTyVal) : LamTerm → InterpM LamSort

Turning all sorts occurring in a LamTerm into fvar, in a hash-consing manner

Equations

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

def Auto.Embedding.Lam.Interp.collectSortFor.withLCtxTy {α : Type} (s : LamSort) (k : InterpM α) : InterpM α

Equations

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