Documentation

Auto.Embedding.LamInference

theorem Auto.Embedding.Lam.LamValid.bvarLowers? {lval : LamValuation} {ss : List LamSort} {lctx : NatLamSort} {t : LamTerm} {lvl : Nat} {t' : LamTerm} (hv : LamValid lval (pushLCtxs ss lctx) t) (hlvl : ss.length = lvl) (heq : LamTerm.bvarLowers? lvl t = some t') (hInh : HList (LamNonempty lval.tyVal) ss) :
LamValid lval lctx t'
theorem Auto.Embedding.Lam.LamThmValid.bvarLowers? {lval : LamValuation} {ss lctx : List LamSort} {t : LamTerm} {lvl : Nat} {t' : LamTerm} (hv : LamThmValid lval (ss ++ lctx) t) (hlvl : ss.length = lvl) (heq : LamTerm.bvarLowers? lvl t = some t') (hInh : HList (LamNonempty lval.tyVal) ss) :
LamThmValid lval lctx t'
theorem Auto.Embedding.Lam.LamValid.bvarLower? {lval : LamValuation} {s : LamSort} {lctx : NatLamSort} {t t' : LamTerm} (hv : LamValid lval (pushLCtx s lctx) t) (heq : t.bvarLower? = some t') (hInh : LamNonempty lval.tyVal s) :
LamValid lval lctx t'
theorem Auto.Embedding.Lam.LamThmValid.bvarLower? {lval : LamValuation} {s : LamSort} {lctx : List LamSort} {t t' : LamTerm} (hv : LamThmValid lval (s :: lctx) t) (heq : t.bvarLower? = some t') (hInh : LamNonempty lval.tyVal s) :
LamThmValid lval lctx t'
Equations
Instances For
    theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_impApp? {t₁₂ t₁ t' : LamTerm} (heq : t₁₂.impApp? t₁ = some t') :
    theorem Auto.Embedding.Lam.LamValid.impApp {lval : LamValuation} {lctx : NatLamSort} {t₁₂ t₁ t₂ : LamTerm} (v₁₂ : LamValid lval lctx t₁₂) (v₁ : LamValid lval lctx t₁) (heq : t₁₂.impApp? t₁ = some t₂) :
    LamValid lval lctx t₂
    theorem Auto.Embedding.Lam.LamThmValid.impApp {lval : LamValuation} {lctx : List LamSort} {t₁₂ t₁ res : LamTerm} (H₁₂ : LamThmValid lval lctx t₁₂) (H₁ : LamThmValid lval lctx t₁) (heq : t₁₂.impApp? t₁ = some res) :
    LamThmValid lval lctx res
    Equations
    Instances For
      theorem Auto.Embedding.Lam.LamValid.impApps {lval : LamValuation} {lctx : NatLamSort} {t : LamTerm} {ps : List LamTerm} {t' : LamTerm} (vt : LamValid lval lctx t) (vps : HList (LamValid lval lctx) ps) (heq : t.impApps? ps = some t') :
      LamValid lval lctx t'
      theorem Auto.Embedding.Lam.LamThmValid.impApps {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} {ps : List LamTerm} {t' : LamTerm} (vt : LamThmValid lval lctx t) (vps : HList (LamThmValid lval lctx) ps) (heq : t.impApps? ps = some t') :
      LamThmValid lval lctx t'
      theorem Auto.Embedding.Lam.LamThmValid.define {s : LamSort} {t : LamTerm} {eidx : Nat} {lval : LamValuation} (wft : LamThmWF lval [] s t) (heVar : t.maxEVarSucc eidx) :
      (val : LamSort.interp lval.tyVal s), LamThmValid (lval.insertEVarAt s val eidx) [] (LamTerm.mkEq s (LamTerm.etom eidx) t)
      Equations
      • One or more equations did not get rendered due to their size.
      • t.skolemize? eidx lctx = none
      Instances For
        theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_skolemize? {t : LamTerm} {eidx : Nat} {lctx : List LamSort} {s : LamSort} {t' : LamTerm} (heq : t.skolemize? eidx lctx = some (s, t')) :
        theorem Auto.Embedding.Lam.choose_spec' {α : Sort u_1} {β : Sort u_2} {p : αβProp} (h : ∀ (q : β), (x : α), p x q) :
        (y : βα), ∀ (q : β), p (y q) q
        theorem Auto.Embedding.Lam.LamThmValid.skolemize {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {p : LamTerm} {eidx : Nat} (vt : LamThmValid lval lctx (LamTerm.mkExistE s p)) (heVar : p.maxEVarSucc eidx) :
        (val : LamSort.interp lval.tyVal (s.mkFuncsRev lctx)), LamThmValid (lval.insertEVarAt (s.mkFuncsRev lctx) val eidx) lctx (LamTerm.app s p ((LamTerm.etom eidx).bvarApps lctx 0))
        theorem Auto.Embedding.Lam.LamThmValid.skolemize? {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} {eidx : Nat} {s : LamSort} {t' : LamTerm} (vt : LamThmValid lval lctx t) (heq : t.skolemize? eidx lctx = some (s, t')) (heVar : t.maxEVarSucc eidx) :
        (val : LamSort.interp lval.tyVal (s.mkFuncsRev lctx)), LamThmValid (lval.insertEVarAt (s.mkFuncsRev lctx) val eidx) lctx t'