def Auto.Embedding.Lam.LamTerm.app_bvarLift_bvar0 (s : LamSort) (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.app_bvarLift_bvar0 s t = Auto.Embedding.Lam.LamTerm.app s t.bvarLift (Auto.Embedding.Lam.LamTerm.bvar 0)

def Auto.Embedding.Lam.LamWF.app_bvarLift_bvar0 {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {argTy resTy : LamSort} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := argTy.func resTy }) : LamWF ltv { lctx := pushLCtx argTy lctx, rterm := LamTerm.app_bvarLift_bvar0 argTy t, rty := resTy }

Equations

• wft.app_bvarLift_bvar0 = Auto.Embedding.Lam.LamWF.ofApp argTy (Auto.Embedding.Lam.LamWF.bvarLift t wft) Auto.Embedding.Lam.LamWF.pushLCtx_ofBVar

theorem Auto.Embedding.Lam.LamWF.interp_app_bvarLift_bvar0 {lctx : Nat → LamSort} {t : LamTerm} {argTy resTy : LamSort} {lval : LamValuation} {x : LamSort.interp lval.tyVal argTy} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := argTy.func resTy }) : interp lval (pushLCtx argTy lctx) (pushLCtxDep x lctxTerm) wft.app_bvarLift_bvar0 = interp lval lctx lctxTerm wft x

def Auto.Embedding.Lam.LamTerm.etaExpand1 (s : LamSort) (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.etaExpand1 s t = Auto.Embedding.Lam.LamTerm.lam s (Auto.Embedding.Lam.LamTerm.app s t.bvarLift (Auto.Embedding.Lam.LamTerm.bvar 0))

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_etaExpand1 {s : LamSort} {t : LamTerm} : (etaExpand1 s t).maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.etaExpand1 {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {argTy resTy : LamSort} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := argTy.func resTy }) : LamWF ltv { lctx := lctx, rterm := LamTerm.etaExpand1 argTy t, rty := argTy.func resTy }

Equations

• wft.etaExpand1 = Auto.Embedding.Lam.LamWF.ofLam resTy (Auto.Embedding.Lam.LamWF.ofApp argTy (Auto.Embedding.Lam.LamWF.bvarLift t wft) Auto.Embedding.Lam.LamWF.pushLCtx_ofBVar)

theorem Auto.Embedding.Lam.LamEquiv.etaExpand1 {lctx : Nat → LamSort} {t : LamTerm} {argTy resTy : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := argTy.func resTy }) : LamEquiv lval lctx (argTy.func resTy) t (LamTerm.etaExpand1 argTy t)

def Auto.Embedding.Lam.LamTerm.etaExpand1? (s : LamSort) (t : LamTerm) : Option LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.etaExpand1? (argTy.func a) t = some (Auto.Embedding.Lam.LamTerm.etaExpand1 argTy t)
• Auto.Embedding.Lam.LamTerm.etaExpand1? s t = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_etaExpand1? {s : LamSort} {t t' : LamTerm} (heq : etaExpand1? s t = some t') : t'.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamGenConvWith.etaExpand1? {lval : LamValuation} : LamGenConvWith lval LamTerm.etaExpand1?

def Auto.Embedding.Lam.LamTerm.etaExpandAux (argTys : List LamSort) (t : LamTerm) : LamTerm

This is meant to eta-expand a term t which has type argTys₀ → ⋯ → argTysᵢ₋₁ → resTy

Equations

• Auto.Embedding.Lam.LamTerm.etaExpandAux argTys t = (Auto.Embedding.Lam.LamTerm.bvarLifts argTys.length t).bvarAppsRev argTys

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_etaExpandAux {argTys : List LamSort} {t : LamTerm} : (etaExpandAux argTys t).maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamTerm.etaExpandAux_nil {t : LamTerm} : etaExpandAux [] t = t

theorem Auto.Embedding.Lam.LamTerm.etaExpandAux_cons {argTy : LamSort} {argTys : List LamSort} {t : LamTerm} : etaExpandAux (argTy :: argTys) t = etaExpandAux argTys (app argTy t.bvarLift (bvar 0))

theorem Auto.Embedding.Lam.LamTerm.etaExpandAux_append {argTys₁ argTys₂ : List LamSort} {t : LamTerm} : etaExpandAux (argTys₁ ++ argTys₂) t = etaExpandAux argTys₂ (etaExpandAux argTys₁ t)

theorem Auto.Embedding.Lam.LamTerm.etaExpandAux_append_singleton {argTys₁ : List LamSort} {argTy : LamSort} {t : LamTerm} : etaExpandAux (argTys₁ ++ [argTy]) t = app argTy (etaExpandAux argTys₁ t).bvarLift (bvar 0)

def Auto.Embedding.Lam.LamWF.etaExpandAux {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {resTy : LamSort} {argTys : List LamSort} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := resTy.mkFuncs argTys }) : LamWF ltv { lctx := pushLCtxs argTys.reverse lctx, rterm := LamTerm.etaExpandAux argTys t, rty := resTy }

Equations

• wft.etaExpandAux = (⋯.mpr (Auto.Embedding.Lam.LamWF.bvarLifts ⋯ t wft)).bvarAppsRev

def Auto.Embedding.Lam.LamWF.fromEtaExpandAux {ltv : LamTyVal} {lctx : Nat → LamSort} {resTy : LamSort} {t : LamTerm} {argTys : List LamSort} (wft : LamWF ltv { lctx := pushLCtxs argTys.reverse lctx, rterm := LamTerm.etaExpandAux argTys t, rty := resTy }) : LamWF ltv { lctx := lctx, rterm := t, rty := resTy.mkFuncs argTys }

Equations

• wft.fromEtaExpandAux = Auto.Embedding.Lam.LamWF.fromBVarLifts ⋯ t wft.fromBVarAppsRev

def Auto.Embedding.Lam.LamTerm.etaExpandWith (l : List LamSort) (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.etaExpandWith l t = (Auto.Embedding.Lam.LamTerm.etaExpandAux l t).mkLamFN l

theorem Auto.Embedding.Lam.LamTerm.etaExpandWith_nil {t : LamTerm} : etaExpandWith [] t = t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_etaExpandWith {l : List LamSort} {t : LamTerm} : (etaExpandWith l t).maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.etaExpandWith {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {l : List LamSort} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s.mkFuncs l }) : LamWF ltv { lctx := lctx, rterm := LamTerm.etaExpandWith l t, rty := s.mkFuncs l }

Equations

• wft.etaExpandWith = wft.etaExpandAux.mkLamFN

def Auto.Embedding.Lam.LamWF.fromEtaExpandWith {ltv : LamTyVal} {lctx : Nat → LamSort} {s : LamSort} {t : LamTerm} {l : List LamSort} (wft : LamWF ltv { lctx := lctx, rterm := LamTerm.etaExpandWith l t, rty := s }) : LamWF ltv { lctx := lctx, rterm := t, rty := s }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.etaExpandWith {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} {l : List LamSort} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s.mkFuncs l }) : LamEquiv lval lctx (s.mkFuncs l) t (LamTerm.etaExpandWith l t)

def Auto.Embedding.Lam.LamTerm.etaExpand (s : LamSort) (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.etaExpand s t = Auto.Embedding.Lam.LamTerm.etaExpandWith s.getArgTys t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_etaExpand {s : LamSort} {t : LamTerm} : (etaExpand s t).maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.etaExpand {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) : LamWF ltv { lctx := lctx, rterm := LamTerm.etaExpand s t, rty := s }

Equations

• wft.etaExpand = ⋯.mp (⋯.mp wft).etaExpandWith

def Auto.Embedding.Lam.LamWF.fromEtaExpand {ltv : LamTyVal} {lctx : Nat → LamSort} {s : LamSort} {t : LamTerm} (wfEx : LamWF ltv { lctx := lctx, rterm := LamTerm.etaExpand s t, rty := s }) : LamWF ltv { lctx := lctx, rterm := t, rty := s }

Equations

• wfEx.fromEtaExpand = wfEx.fromEtaExpandWith

theorem Auto.Embedding.Lam.LamEquiv.etaExpand {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) : LamEquiv lval lctx s t (LamTerm.etaExpand s t)

theorem Auto.Embedding.Lam.LamGenConvWith.etaExpand {lval : LamValuation} : LamGenConvWith lval fun (s : LamSort) (t : LamTerm) => some (LamTerm.etaExpand s t)

def Auto.Embedding.Lam.LamTerm.etaExpandN? (n : Nat) (s : LamSort) (t : LamTerm) : Option LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.etaExpandN? n s t = match Auto.Embedding.Lam.LamSort.getArgTysN n s with | some l => some (Auto.Embedding.Lam.LamTerm.etaExpandWith l t) | none => none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_etaExpandN? {n : Nat} {s : LamSort} {t t' : LamTerm} (heq : etaExpandN? n s t = some t') : t'.maxEVarSucc = t.maxEVarSucc

@[irreducible]

def Auto.Embedding.Lam.LamWF.etaExpandN? {n : Nat} {s : LamSort} {t t' : LamTerm} {ltv : LamTyVal} {lctx : Nat → LamSort} (heq : LamTerm.etaExpandN? n s t = some t') (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) : LamWF ltv { lctx := lctx, rterm := t', rty := s }

Equations

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

@[irreducible]

def Auto.Embedding.Lam.LamWF.fromEtaExpandN? {n : Nat} {s : LamSort} {t t' : LamTerm} {ltv : LamTyVal} {lctx : Nat → LamSort} (heq : LamTerm.etaExpandN? n s t = some t') (wfEx : LamWF ltv { lctx := lctx, rterm := t', rty := s }) : LamWF ltv { lctx := lctx, rterm := t, rty := s }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.etaExpandN? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {n : Nat} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : LamTerm.etaExpandN? n s t = some t') : LamEquiv lval lctx s t t'

theorem Auto.Embedding.Lam.LamGenConvWith.etaExpandN? {lval : LamValuation} {n : Nat} : LamGenConvWith lval (LamTerm.etaExpandN? n)

def Auto.Embedding.Lam.LamTerm.etaReduce1? (t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• t.etaReduce1? = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_etaReduce1? {t t' : LamTerm} (heq : t.etaReduce1? = some t') : t'.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.etaReduce1? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (heq : t.etaReduce1? = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamGenConv.etaReduce1? {lval : LamValuation} : LamGenConv lval LamTerm.etaReduce1?

def Auto.Embedding.Lam.LamTerm.etaReduceNAux? (n : Nat) (t : LamTerm) : Option LamTerm

Equations

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

def Auto.Embedding.Lam.LamTerm.etaReduceN? (n : Nat) (t : LamTerm) : Option LamTerm

Equations

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

theorem Auto.Embedding.Lam.LamTerm.etaReduceNAux?_etaExpandWith_length_eq {n : Nat} {l : List LamSort} {t' : LamTerm} (h : l.length = n) : etaReduceNAux? n (etaExpandWith l t') = some t'

theorem Auto.Embedding.Lam.LamTerm.etaReduceN?_spec {n : Nat} {t t' : LamTerm} : etaReduceN? n t = some t' ↔ ∃ (l : List LamSort), l.length = n ∧ etaExpandWith l t' = t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_etaReduceN? {n : Nat} {t t' : LamTerm} (heq : etaReduceN? n t = some t') : t'.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.etaReduceN? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {n : Nat} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (heq : LamTerm.etaReduceN? n t = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamGenConv.etaReduceN? {lval : LamValuation} {n : Nat} : LamGenConv lval (LamTerm.etaReduceN? n)

def Auto.Embedding.Lam.LamTerm.extensionalizeEqFWith (argTys : List LamSort) (resTy : LamSort) (lhs rhs : LamTerm) : LamTerm

Equations

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

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_extensionalizeEqFWith {argTys : List LamSort} {resTy : LamSort} {lhs rhs : LamTerm} : (extensionalizeEqFWith argTys resTy lhs rhs).maxEVarSucc = max lhs.maxEVarSucc rhs.maxEVarSucc

def Auto.Embedding.Lam.LamWF.extensionalizeEqFWith {ltv : LamTyVal} {lctx : Nat → LamSort} {lhs : LamTerm} {s : LamSort} {l : List LamSort} {rhs : LamTerm} (wfl : LamWF ltv { lctx := lctx, rterm := lhs, rty := s.mkFuncs l }) (wfr : LamWF ltv { lctx := lctx, rterm := rhs, rty := s.mkFuncs l }) : LamWF ltv { lctx := lctx, rterm := LamTerm.extensionalizeEqFWith l s lhs rhs, rty := LamSort.base LamBaseSort.prop }

Equations

• wfl.extensionalizeEqFWith wfr = (wfl.etaExpandAux.mkEq wfr.etaExpandAux).mkForallEFN

theorem Auto.Embedding.Lam.LamEquiv.ofExtensionalizeEqFWith {lctx : Nat → LamSort} {lhs : LamTerm} {s : LamSort} {rhs : LamTerm} {lval : LamValuation} {l : List LamSort} (wfl : LamWF lval.toLamTyVal { lctx := lctx, rterm := lhs, rty := s.mkFuncs l }) (wfr : LamWF lval.toLamTyVal { lctx := lctx, rterm := rhs, rty := s.mkFuncs l }) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (LamTerm.mkEq (s.mkFuncs l) lhs rhs) (LamTerm.extensionalizeEqFWith l s lhs rhs)

def Auto.Embedding.Lam.LamTerm.extensionalizeEqF (s : LamSort) (lhs rhs : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.extensionalizeEqF s lhs rhs = Auto.Embedding.Lam.LamTerm.extensionalizeEqFWith s.getArgTys s.getResTy lhs rhs

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_extensionalizeEqF {s : LamSort} {lhs rhs : LamTerm} : (extensionalizeEqF s lhs rhs).maxEVarSucc = max lhs.maxEVarSucc rhs.maxEVarSucc

def Auto.Embedding.Lam.LamWF.extensionalizeEqF {ltv : LamTyVal} {lctx : Nat → LamSort} {s : LamSort} {lhs rhs : LamTerm} {s' : LamSort} (wf : LamWF ltv { lctx := lctx, rterm := LamTerm.mkEq s lhs rhs, rty := s' }) : LamWF ltv { lctx := lctx, rterm := LamTerm.extensionalizeEqF s lhs rhs, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.ofExtensionalizeEqF {lctx : Nat → LamSort} {s : LamSort} {lhs rhs : LamTerm} {s' : LamSort} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := LamTerm.mkEq s lhs rhs, rty := s' }) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (LamTerm.mkEq s lhs rhs) (LamTerm.extensionalizeEqF s lhs rhs)

def Auto.Embedding.Lam.LamTerm.extensionalizeEq?F? (t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• t.extensionalizeEq?F? = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_extensionalizeEq?F? {t t' : LamTerm} (heq : t.extensionalizeEq?F? = some t') : t'.maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.extensionalizeEq?F? {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) (heq : t.extensionalizeEq?F? = some t') : LamWF ltv { lctx := lctx, rterm := t', rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.ofExtensionalizeEq?F? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.extensionalizeEq?F? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

def Auto.Embedding.Lam.LamTerm.extensionalizeEqFN? (n : Nat) (s : LamSort) (lhs rhs : LamTerm) : Option LamTerm

Equations

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

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_extensionalizeEqFN? {n : Nat} {s : LamSort} {lhs rhs t' : LamTerm} (heq : extensionalizeEqFN? n s lhs rhs = some t') : t'.maxEVarSucc = max lhs.maxEVarSucc rhs.maxEVarSucc

def Auto.Embedding.Lam.LamWF.extensionalizeEqFN? {ltv : LamTyVal} {lctx : Nat → LamSort} {s : LamSort} {lhs rhs : LamTerm} {s' : LamSort} {n : Nat} {t' : LamTerm} (wf : LamWF ltv { lctx := lctx, rterm := LamTerm.mkEq s lhs rhs, rty := s' }) (heq : LamTerm.extensionalizeEqFN? n s lhs rhs = some t') : LamWF ltv { lctx := lctx, rterm := t', rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.ofExtensionalizeEqFN? {lctx : Nat → LamSort} {s : LamSort} {lhs rhs : LamTerm} {s' : LamSort} {n : Nat} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := LamTerm.mkEq s lhs rhs, rty := s' }) (heq : LamTerm.extensionalizeEqFN? n s lhs rhs = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (LamTerm.mkEq s lhs rhs) t'

def Auto.Embedding.Lam.LamTerm.extensionalizeEq?FN? (n : Nat) (t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.extensionalizeEq?FN? n t = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_extensionalizeEq?FN? {n : Nat} {t t' : LamTerm} (heq : extensionalizeEq?FN? n t = some t') : t'.maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.extensionalizeEq?FN? {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {n : Nat} {t' : LamTerm} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) (heq : LamTerm.extensionalizeEq?FN? n t = some t') : LamWF ltv { lctx := lctx, rterm := t', rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamWF.s_eq_prop_of_extensionalizeEq?FN?_eq_some {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {n : Nat} {t' : LamTerm} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) (heq : LamTerm.extensionalizeEq?FN? n t = some t') : s = LamSort.base LamBaseSort.prop

theorem Auto.Embedding.Lam.LamEquiv.ofExtensionalizeEq?FN? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {n : Nat} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : LamTerm.extensionalizeEq?FN? n t = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.ofExtensionalizeEq?FN? {lval : LamValuation} {n : Nat} : LamGenConv lval (LamTerm.extensionalizeEq?FN? n)

def Auto.Embedding.Lam.LamTerm.extensionalizeEq (t : LamTerm) : LamTerm

Equations

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

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_extensionalizeEq {t : LamTerm} : t.extensionalizeEq.maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.extensionalizeEq {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} (wf : LamWF ltv { lctx := lctx, rterm := t, rty := s }) : LamWF ltv { lctx := lctx, rterm := t.extensionalizeEq, rty := s }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.ofExtensionalizeEq {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) : LamEquiv lval lctx s t t.extensionalizeEq

theorem Auto.Embedding.Lam.LamThmEquiv.ofExtensionalizeEq {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (wf : LamThmWF lval lctx s t) : LamThmEquiv lval lctx s t t.extensionalizeEq

theorem Auto.Embedding.Lam.LamGenConv.ofExtensionalizeEq {lval : LamValuation} : LamGenConv lval fun (t : LamTerm) => some t.extensionalizeEq

def Auto.Embedding.Lam.LamTerm.extensionalizeAux (isAppFn : Bool) (t : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.extensionalizeAux isAppFn (Auto.Embedding.Lam.LamTerm.atom n) = Auto.Embedding.Lam.LamTerm.atom n
• Auto.Embedding.Lam.LamTerm.extensionalizeAux isAppFn (Auto.Embedding.Lam.LamTerm.etom n) = Auto.Embedding.Lam.LamTerm.etom n
• Auto.Embedding.Lam.LamTerm.extensionalizeAux isAppFn (Auto.Embedding.Lam.LamTerm.bvar n) = Auto.Embedding.Lam.LamTerm.bvar n
• Auto.Embedding.Lam.LamTerm.extensionalizeAux isAppFn (Auto.Embedding.Lam.LamTerm.lam s body) = Auto.Embedding.Lam.LamTerm.lam s (Auto.Embedding.Lam.LamTerm.extensionalizeAux false body)

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_extensionalizeAux {isAppFn : Bool} {t : LamTerm} : (extensionalizeAux isAppFn t).maxEVarSucc = t.maxEVarSucc

@[reducible, inline]

abbrev Auto.Embedding.Lam.LamTerm.extensionalize (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.extensionalize = Auto.Embedding.Lam.LamTerm.extensionalizeAux false

def Auto.Embedding.Lam.LamWF.extensionalizeAux {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {isAppFn : Bool} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) : LamWF ltv { lctx := lctx, rterm := LamTerm.extensionalizeAux isAppFn t, rty := s }

Equations

• One or more equations did not get rendered due to their size.
• (Auto.Embedding.Lam.LamWF.ofAtom n).extensionalizeAux = Auto.Embedding.Lam.LamWF.ofAtom n
• (Auto.Embedding.Lam.LamWF.ofEtom n).extensionalizeAux = Auto.Embedding.Lam.LamWF.ofEtom n
• (Auto.Embedding.Lam.LamWF.ofBase b_1).extensionalizeAux = id (Auto.Embedding.Lam.LamWF.ofBase b_1)
• (Auto.Embedding.Lam.LamWF.ofBase b_1).extensionalizeAux = id (Auto.Embedding.Lam.LamWF.ofBase b_1).extensionalizeEq
• (Auto.Embedding.Lam.LamWF.ofBVar n).extensionalizeAux = Auto.Embedding.Lam.LamWF.ofBVar n
• (Auto.Embedding.Lam.LamWF.ofLam bodyTy wfBody).extensionalizeAux = Auto.Embedding.Lam.LamWF.ofLam bodyTy wfBody.extensionalizeAux
• (Auto.Embedding.Lam.LamWF.ofApp argTy wfFn wfArg).extensionalizeAux = id (have wfAp := Auto.Embedding.Lam.LamWF.ofApp argTy wfFn.extensionalizeAux wfArg.extensionalizeAux; wfAp)

theorem Auto.Embedding.Lam.LamEquiv.ofExtensionalize {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {isAppFn : Bool} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) : LamEquiv lval lctx s t (LamTerm.extensionalizeAux isAppFn t)

theorem Auto.Embedding.Lam.LamThmEquiv.ofExtensionalize {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} {isAppFn : Bool} (wf : LamThmWF lval lctx s t) : LamThmEquiv lval lctx s t (LamTerm.extensionalizeAux isAppFn t)

def Auto.Embedding.Lam.LamWF.intensionalizeEq1 {ltv : LamTyVal} {argTy : LamSort} {lctx : Nat → LamSort} {s : LamSort} {lhs rhs : LamTerm} {s' : LamSort} (wfEq : LamWF ltv { lctx := pushLCtx argTy lctx, rterm := LamTerm.mkEq s lhs rhs, rty := s' }) : LamWF ltv { lctx := lctx, rterm := LamTerm.mkEq (argTy.func s) (LamTerm.lam argTy lhs) (LamTerm.lam argTy rhs), rty := LamSort.base LamBaseSort.prop }

Equations

• (Auto.Embedding.Lam.LamWF.ofApp s (Auto.Embedding.Lam.LamWF.ofApp s HFn wfl) wfr).intensionalizeEq1 = (Auto.Embedding.Lam.LamWF.ofLam s wfl).mkEq (Auto.Embedding.Lam.LamWF.ofLam s wfr)

def Auto.Embedding.Lam.LamWF.fromIntensionalizeEq1 {ltv : LamTyVal} {lctx : Nat → LamSort} {argTy s : LamSort} {lhs rhs : LamTerm} {s' : LamSort} (wfEq : LamWF ltv { lctx := lctx, rterm := LamTerm.mkEq (argTy.func s) (LamTerm.lam argTy lhs) (LamTerm.lam argTy rhs), rty := s' }) : LamWF ltv { lctx := pushLCtx argTy lctx, rterm := LamTerm.mkEq s lhs rhs, rty := LamSort.base LamBaseSort.prop }

Equations

• (Auto.Embedding.Lam.LamWF.ofApp (argTy.func s) (Auto.Embedding.Lam.LamWF.ofApp (argTy.func s) HFn wfl) wfr).fromIntensionalizeEq1 = wfl.getLam.mkEq wfr.getLam

theorem Auto.Embedding.Lam.LamEquiv.ofIntensionalizeEq1 {argTy : LamSort} {lctx : Nat → LamSort} {s : LamSort} {lhs rhs : LamTerm} {s' : LamSort} {lval : LamValuation} (wfEq : LamWF lval.toLamTyVal { lctx := pushLCtx argTy lctx, rterm := LamTerm.mkEq s lhs rhs, rty := s' }) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (LamTerm.mkForallEF argTy (LamTerm.mkEq s lhs rhs)) (LamTerm.mkEq (argTy.func s) (LamTerm.lam argTy lhs) (LamTerm.lam argTy rhs))

def Auto.Embedding.Lam.LamTerm.intensionalizeEqWith (argTys : List LamSort) (resTy : LamSort) (lhs rhs : LamTerm) : LamTerm

Equations

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

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_intensionalizeEqWith {argTys : List LamSort} {resTy : LamSort} {lhs rhs : LamTerm} : (intensionalizeEqWith argTys resTy lhs rhs).maxEVarSucc = max lhs.maxEVarSucc rhs.maxEVarSucc

def Auto.Embedding.Lam.LamWF.intensionalizeEqWith {ltv : LamTyVal} {lctx : Nat → LamSort} {s : LamSort} {lhs rhs : LamTerm} {l : List LamSort} {s' : LamSort} (wfEq : LamWF ltv { lctx := lctx, rterm := (LamTerm.mkEq s lhs rhs).mkForallEFN l, rty := s' }) : LamWF ltv { lctx := lctx, rterm := LamTerm.intensionalizeEqWith l s lhs rhs, rty := LamSort.base LamBaseSort.prop }

Equations

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

def Auto.Embedding.Lam.LamWF.fromIntensionalizeEqWith {ltv : LamTyVal} {lctx : Nat → LamSort} {l : List LamSort} {s : LamSort} {lhs rhs : LamTerm} {s' : LamSort} (wfInt : LamWF ltv { lctx := lctx, rterm := LamTerm.intensionalizeEqWith l s lhs rhs, rty := s' }) : LamWF ltv { lctx := lctx, rterm := (LamTerm.mkEq s lhs rhs).mkForallEFN l, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.ofIntensionalizeEqWith {lctx : Nat → LamSort} {s : LamSort} {lhs rhs : LamTerm} {l : List LamSort} {s' : LamSort} {lval : LamValuation} (wfEq : LamWF lval.toLamTyVal { lctx := lctx, rterm := (LamTerm.mkEq s lhs rhs).mkForallEFN l, rty := s' }) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) ((LamTerm.mkEq s lhs rhs).mkForallEFN l) (LamTerm.intensionalizeEqWith l s lhs rhs)

def Auto.Embedding.Lam.LamTerm.intensionalizeEq? (t : LamTerm) : Option LamTerm

Equations

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

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_intensionalizeEq? {t t' : LamTerm} (heq : t.intensionalizeEq? = some t') : t'.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamWF.s_eq_prop_of_intensionalizeEq?_eq_some {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s' : LamSort} {t' : LamTerm} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s' }) (heq : t.intensionalizeEq? = some t') : s' = LamSort.base LamBaseSort.prop

theorem Auto.Embedding.Lam.LamEquiv.ofIntensionalizeEq? {lctx : Nat → LamSort} {t : LamTerm} {s' : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s' }) (heq : t.intensionalizeEq? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.ofIntensionalizeEq? {lval : LamValuation} : LamGenConv lval LamTerm.intensionalizeEq?

def Auto.Embedding.Lam.LamTerm.instantiateAt (idx : Nat) (arg body : LamTerm) : LamTerm

Suppose we have (λ x. func[body]) arg and body is a subterm of func under idx levels of binders in func. We want to compute what body will become when we reduce the top-level redex Suppose lctx ⊢ body : ty. It's easy to see that the lctx which arg resides in is fun n => lctx (n + idx + 1) and the type of arg is lctx idx

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.instantiateAt idx arg (Auto.Embedding.Lam.LamTerm.atom n) = Auto.Embedding.Lam.LamTerm.atom n
• Auto.Embedding.Lam.LamTerm.instantiateAt idx arg (Auto.Embedding.Lam.LamTerm.etom n) = Auto.Embedding.Lam.LamTerm.etom n
• Auto.Embedding.Lam.LamTerm.instantiateAt idx arg (Auto.Embedding.Lam.LamTerm.base a) = Auto.Embedding.Lam.LamTerm.base a
• Auto.Embedding.Lam.LamTerm.instantiateAt idx arg (Auto.Embedding.Lam.LamTerm.bvar n) = Auto.Embedding.pushLCtxAt (Auto.Embedding.Lam.LamTerm.bvarLifts idx arg) idx Auto.Embedding.Lam.LamTerm.bvar n
• Auto.Embedding.Lam.LamTerm.instantiateAt idx arg (Auto.Embedding.Lam.LamTerm.lam s body) = Auto.Embedding.Lam.LamTerm.lam s (Auto.Embedding.Lam.LamTerm.instantiateAt idx.succ arg body)

theorem Auto.Embedding.Lam.LamTerm.instantiateAt_bVarIrrelevance {idx : Nat} {t arg₁ arg₂ : LamTerm} (h : hasLooseBVarEq idx t = false) : instantiateAt idx arg₁ t = instantiateAt idx arg₂ t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_instantiateAt {idx : Nat} {arg body : LamTerm} : (instantiateAt idx arg body).maxEVarSucc = match hasLooseBVarEq idx body with | true => arg.maxEVarSucc.max body.maxEVarSucc | false => body.maxEVarSucc

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_instantiateAt_le {idx : Nat} {arg body : LamTerm} : (instantiateAt idx arg body).maxEVarSucc ≤ arg.maxEVarSucc.max body.maxEVarSucc

def Auto.Embedding.Lam.LamWF.instantiateAt (ltv : LamTyVal) (idx : Nat) {arg : LamTerm} {argTy : LamSort} {body : LamTerm} {bodyTy : LamSort} (lctx : Nat → LamSort) (wfArg : LamWF ltv { lctx := lctx, rterm := LamTerm.bvarLifts idx arg, rty := argTy }) (wfBody : LamWF ltv { lctx := pushLCtxAt argTy idx lctx, rterm := body, rty := bodyTy }) : LamWF ltv { lctx := lctx, rterm := LamTerm.instantiateAt idx arg body, rty := bodyTy }

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamWF.instantiateAt ltv idx x✝¹ x✝ (Auto.Embedding.Lam.LamWF.ofAtom n) = Auto.Embedding.Lam.LamWF.ofAtom n
• Auto.Embedding.Lam.LamWF.instantiateAt ltv idx x✝¹ x✝ (Auto.Embedding.Lam.LamWF.ofEtom n) = Auto.Embedding.Lam.LamWF.ofEtom n
• Auto.Embedding.Lam.LamWF.instantiateAt ltv idx x✝¹ x✝ (Auto.Embedding.Lam.LamWF.ofBase H) = Auto.Embedding.Lam.LamWF.ofBase H

theorem Auto.Embedding.Lam.LamWF.interp_instantiateAt (lval : LamValuation) (idx : Nat) {arg : LamTerm} {argTy : LamSort} {body : LamTerm} {bodyTy : LamSort} (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (wfArg : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := LamTerm.bvarLifts idx arg, rty := argTy }) (wfBody : LamWF lval.toLamTyVal { lctx := pushLCtxAt argTy idx lctxTy, rterm := body, rty := bodyTy }) : let wfInstantiateAt' := instantiateAt lval.toLamTyVal idx lctxTy wfArg wfBody; interp lval (pushLCtxAt argTy idx lctxTy) (pushLCtxAtDep (interp lval lctxTy lctxTerm wfArg) idx lctxTerm) wfBody = interp lval lctxTy lctxTerm wfInstantiateAt'

def Auto.Embedding.Lam.LamTerm.instantiate1 (arg body : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.instantiate1 = Auto.Embedding.Lam.LamTerm.instantiateAt 0

theorem Auto.Embedding.Lam.LamTerm.instantiate1_bVarIrrelevance {t arg₁ arg₂ : LamTerm} (h : hasLooseBVarEq 0 t = false) : arg₁.instantiate1 t = arg₂.instantiate1 t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_instantiate1 {arg body : LamTerm} : (arg.instantiate1 body).maxEVarSucc = match hasLooseBVarEq 0 body with | true => arg.maxEVarSucc.max body.maxEVarSucc | false => body.maxEVarSucc

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_instantiate1_le {arg body : LamTerm} : (arg.instantiate1 body).maxEVarSucc ≤ arg.maxEVarSucc.max body.maxEVarSucc

def Auto.Embedding.Lam.LamWF.instantiate1 (ltv : LamTyVal) {arg : LamTerm} {argTy : LamSort} {body : LamTerm} {bodyTy : LamSort} (lctx : Nat → LamSort) (wfArg : LamWF ltv { lctx := lctx, rterm := arg, rty := argTy }) (wfBody : LamWF ltv { lctx := pushLCtx argTy lctx, rterm := body, rty := bodyTy }) : LamWF ltv { lctx := lctx, rterm := arg.instantiate1 body, rty := bodyTy }

Equations

• Auto.Embedding.Lam.LamWF.instantiate1 ltv = ⋯.mp (Auto.Embedding.Lam.LamWF.instantiateAt ltv 0)

def Auto.Embedding.Lam.LamThmWF.instantiate1 {lval : LamValuation} {lctx : List LamSort} {argTy : LamSort} {arg : LamTerm} {bodyTy : LamSort} {body : LamTerm} (wfArg : LamThmWF lval lctx argTy arg) (wfBody : LamThmWF lval (argTy :: lctx) bodyTy body) : LamThmWF lval lctx bodyTy (arg.instantiate1 body)

Equations

• wfArg.instantiate1 wfBody lctx' = Auto.Embedding.Lam.LamWF.instantiate1 lval.toLamTyVal (Auto.Embedding.pushLCtxs lctx lctx') (wfArg lctx') (⋯.mp (wfBody lctx'))

theorem Auto.Embedding.Lam.LamWF.interp_instantiate1 (lval : LamValuation) {arg : LamTerm} {argTy : LamSort} {body : LamTerm} {bodyTy : LamSort} (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (wfArg : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := arg, rty := argTy }) (wfBody : LamWF lval.toLamTyVal { lctx := pushLCtx argTy lctxTy, rterm := body, rty := bodyTy }) : let wfInstantiate1' := instantiate1 lval.toLamTyVal lctxTy wfArg wfBody; interp lval (pushLCtx argTy lctxTy) (pushLCtxDep (interp lval lctxTy lctxTerm wfArg) lctxTerm) wfBody = interp lval lctxTy lctxTerm wfInstantiate1'

theorem Auto.Embedding.Lam.LamThmValid.instantiate1 {lval : LamValuation} {lctx : List LamSort} {argTy : LamSort} {arg body : LamTerm} (hw : LamThmWF lval lctx argTy arg) (hv : LamThmValid lval (argTy :: lctx) body) : LamThmValid lval lctx (arg.instantiate1 body)

def Auto.Embedding.Lam.LamBaseTerm.resolveImport (ltv : LamTyVal) : LamBaseTerm → LamBaseTerm

Equations

• Auto.Embedding.Lam.LamBaseTerm.resolveImport ltv (Auto.Embedding.Lam.LamBaseTerm.eqI n) = Auto.Embedding.Lam.LamBaseTerm.eq (ltv.lamILTy n)
• Auto.Embedding.Lam.LamBaseTerm.resolveImport ltv (Auto.Embedding.Lam.LamBaseTerm.forallEI n) = Auto.Embedding.Lam.LamBaseTerm.forallE (ltv.lamILTy n)
• Auto.Embedding.Lam.LamBaseTerm.resolveImport ltv (Auto.Embedding.Lam.LamBaseTerm.existEI n) = Auto.Embedding.Lam.LamBaseTerm.existE (ltv.lamILTy n)
• Auto.Embedding.Lam.LamBaseTerm.resolveImport ltv (Auto.Embedding.Lam.LamBaseTerm.iteI n) = Auto.Embedding.Lam.LamBaseTerm.ite (ltv.lamILTy n)
• Auto.Embedding.Lam.LamBaseTerm.resolveImport ltv x✝ = x✝

def Auto.Embedding.Lam.LamBaseTerm.LamWF.resolveImport {ltv : LamTyVal} {b : LamBaseTerm} {ty : LamSort} (wfB : LamWF ltv b ty) : LamWF ltv (LamBaseTerm.resolveImport ltv b) ty

Equations

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

theorem Auto.Embedding.Lam.LamBaseTerm.LamWF.interp_resolveImport (lval : LamValuation) {b : LamBaseTerm} {ty : LamSort} (wfB : LamWF lval.toLamTyVal b ty) : let wfRB := wfB.resolveImport; interp lval wfB = interp lval wfRB

def Auto.Embedding.Lam.LamTerm.resolveImport (ltv : LamTyVal) : LamTerm → LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.resolveImport ltv (Auto.Embedding.Lam.LamTerm.atom n) = Auto.Embedding.Lam.LamTerm.atom n
• Auto.Embedding.Lam.LamTerm.resolveImport ltv (Auto.Embedding.Lam.LamTerm.etom n) = Auto.Embedding.Lam.LamTerm.etom n
• Auto.Embedding.Lam.LamTerm.resolveImport ltv (Auto.Embedding.Lam.LamTerm.base a) = Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.resolveImport ltv a)
• Auto.Embedding.Lam.LamTerm.resolveImport ltv (Auto.Embedding.Lam.LamTerm.bvar n) = Auto.Embedding.Lam.LamTerm.bvar n
• Auto.Embedding.Lam.LamTerm.resolveImport ltv (Auto.Embedding.Lam.LamTerm.lam s body) = Auto.Embedding.Lam.LamTerm.lam s (Auto.Embedding.Lam.LamTerm.resolveImport ltv body)

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_resolveImport {ltv : LamTyVal} {t : LamTerm} : (resolveImport ltv t).maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.resolveImport {ltv : LamTyVal} {t : LamTerm} {ty : LamSort} {lctx : Nat → LamSort} (wfT : LamWF ltv { lctx := lctx, rterm := t, rty := ty }) : LamWF ltv { lctx := lctx, rterm := LamTerm.resolveImport ltv t, rty := ty }

Equations

• (Auto.Embedding.Lam.LamWF.ofAtom n).resolveImport = Auto.Embedding.Lam.LamWF.ofAtom n
• (Auto.Embedding.Lam.LamWF.ofEtom n).resolveImport = Auto.Embedding.Lam.LamWF.ofEtom n
• (Auto.Embedding.Lam.LamWF.ofBase b_1).resolveImport = Auto.Embedding.Lam.LamWF.ofBase b_1.resolveImport
• (Auto.Embedding.Lam.LamWF.ofBVar n).resolveImport = Auto.Embedding.Lam.LamWF.ofBVar n
• (Auto.Embedding.Lam.LamWF.ofLam bodyTy wfBody).resolveImport = Auto.Embedding.Lam.LamWF.ofLam bodyTy wfBody.resolveImport
• (Auto.Embedding.Lam.LamWF.ofApp argTy wfFn wfArg).resolveImport = Auto.Embedding.Lam.LamWF.ofApp argTy wfFn.resolveImport wfArg.resolveImport

def Auto.Embedding.Lam.LamThmWF.resolveImport {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (wf : LamThmWF lval lctx rty t) : LamThmWF lval lctx rty (LamTerm.resolveImport lval.toLamTyVal t)

Equations

• wf.resolveImport lctx = (wf lctx).resolveImport

theorem Auto.Embedding.Lam.LamWF.interp_resolveImport {lval : LamValuation} {t : LamTerm} {ty : LamSort} (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (wfT : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t, rty := ty }) : let wfRB := wfT.resolveImport; interp lval lctxTy lctxTerm wfT = interp lval lctxTy lctxTerm wfRB

theorem Auto.Embedding.Lam.LamThmValid.resolveImport {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval lctx t) : LamThmValid lval lctx (LamTerm.resolveImport lval.toLamTyVal t)

def Auto.Embedding.Lam.LamTerm.topBetaAux (s : LamSort) (arg fn : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.topBetaAux s arg (Auto.Embedding.Lam.LamTerm.lam a body) = arg.instantiate1 body
• Auto.Embedding.Lam.LamTerm.topBetaAux s arg x✝ = Auto.Embedding.Lam.LamTerm.app s x✝ arg

def Auto.Embedding.Lam.LamWF.topBetaAux (ltv : LamTyVal) {arg : LamTerm} {argTy : LamSort} {fn : LamTerm} {resTy : LamSort} (lctx : Nat → LamSort) (wfArg : LamWF ltv { lctx := lctx, rterm := arg, rty := argTy }) (wfFn : LamWF ltv { lctx := lctx, rterm := fn, rty := argTy.func resTy }) : LamWF ltv { lctx := lctx, rterm := LamTerm.topBetaAux argTy arg fn, rty := resTy }

Equations

• Auto.Embedding.Lam.LamWF.topBetaAux ltv lctx wfArg wfFn_2 = Auto.Embedding.Lam.LamWF.ofApp argTy wfFn_2 wfArg
• Auto.Embedding.Lam.LamWF.topBetaAux ltv lctx wfArg wfFn_2 = Auto.Embedding.Lam.LamWF.ofApp argTy wfFn_2 wfArg
• Auto.Embedding.Lam.LamWF.topBetaAux ltv lctx wfArg wfFn_2 = Auto.Embedding.Lam.LamWF.ofApp argTy wfFn_2 wfArg
• Auto.Embedding.Lam.LamWF.topBetaAux ltv lctx wfArg wfFn_2 = Auto.Embedding.Lam.LamWF.ofApp argTy wfFn_2 wfArg
• Auto.Embedding.Lam.LamWF.topBetaAux ltv lctx wfArg_2 (Auto.Embedding.Lam.LamWF.ofLam resTy wfBody) = Auto.Embedding.Lam.LamWF.instantiate1 ltv lctx wfArg_2 wfBody
• Auto.Embedding.Lam.LamWF.topBetaAux ltv lctx wfArg wfFn_2 = Auto.Embedding.Lam.LamWF.ofApp argTy wfFn_2 wfArg

def Auto.Embedding.Lam.LamWF.interp_topBetaAux (lval : LamValuation) {arg : LamTerm} {argTy : LamSort} {fn : LamTerm} {resTy : LamSort} (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (wfArg : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := arg, rty := argTy }) (wfFn : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := fn, rty := argTy.func resTy }) : let wfHB := topBetaAux lval.toLamTyVal lctxTy wfArg wfFn; interp lval lctxTy lctxTerm (ofApp argTy wfFn wfArg) = interp lval lctxTy lctxTerm wfHB

Equations

• ⋯ = ⋯

def Auto.Embedding.Lam.LamTerm.topBeta : LamTerm → LamTerm

Equations

• (Auto.Embedding.Lam.LamTerm.app s fn arg).topBeta = Auto.Embedding.Lam.LamTerm.topBetaAux s arg fn
• x✝.topBeta = x✝

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_topBeta {t : LamTerm} : t.topBeta.maxEVarSucc ≤ t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.topBeta (ltv : LamTyVal) {t : LamTerm} {ty : LamSort} (lctx : Nat → LamSort) (wf : LamWF ltv { lctx := lctx, rterm := t, rty := ty }) : LamWF ltv { lctx := lctx, rterm := t.topBeta, rty := ty }

Equations

• Auto.Embedding.Lam.LamWF.topBeta ltv lctx wf_2 = wf_2
• Auto.Embedding.Lam.LamWF.topBeta ltv lctx wf_2 = wf_2
• Auto.Embedding.Lam.LamWF.topBeta ltv lctx wf_2 = wf_2
• Auto.Embedding.Lam.LamWF.topBeta ltv lctx wf_2 = wf_2
• Auto.Embedding.Lam.LamWF.topBeta ltv lctx wf_2 = wf_2
• Auto.Embedding.Lam.LamWF.topBeta ltv lctx (Auto.Embedding.Lam.LamWF.ofApp a wfFn wfArg) = Auto.Embedding.Lam.LamWF.topBetaAux ltv lctx wfArg wfFn

def Auto.Embedding.Lam.LamThmWF.topBeta {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (wf : LamThmWF lval lctx rty t) : LamThmWF lval lctx rty t.topBeta

Equations

• wf.topBeta lctx = Auto.Embedding.Lam.LamWF.topBeta lval.toLamTyVal (Auto.Embedding.pushLCtxs lctx✝ lctx) (wf lctx)

theorem Auto.Embedding.Lam.LamWF.interp_topBeta {lval : LamValuation} {t : LamTerm} {ty : LamSort} (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (wfT : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t, rty := ty }) : let wfHB := topBeta lval.toLamTyVal lctxTy wfT; interp lval lctxTy lctxTerm wfT = interp lval lctxTy lctxTerm wfHB

theorem Auto.Embedding.Lam.LamThmValid.topBeta {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval lctx t) : LamThmValid lval lctx t.topBeta

theorem Auto.Embedding.Lam.LamEquiv.ofTopBeta {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) : LamEquiv lval lctx s t t.topBeta

theorem Auto.Embedding.Lam.LamThmEquiv.ofTopBeta {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (wf : LamThmWF lval lctx s t) : LamThmEquiv lval lctx s t t.topBeta

def Auto.Embedding.Lam.LamTerm.beta (t : LamTerm) : List (LamSort × LamTerm) → LamTerm

Equations

• t.beta [] = t
• (Auto.Embedding.Lam.LamTerm.lam a body).beta (arg :: args) = (arg.snd.instantiate1 body).beta args
• t.beta (arg :: args) = t.mkAppN (arg :: args)

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_beta {args : List (LamSort × LamTerm)} {n : Nat} {t : LamTerm} (hs : HList (fun (x : LamSort × LamTerm) => match x with | (fst, arg) => arg.maxEVarSucc ≤ n) args) (ht : t.maxEVarSucc ≤ n) : (t.beta args).maxEVarSucc ≤ n

def Auto.Embedding.Lam.LamWF.ofBeta {ltv : LamTyVal} {lctx : Nat → LamSort} {resTy : LamSort} (fn : LamTerm) (args : List (LamSort × LamTerm)) (wf : LamWF ltv { lctx := lctx, rterm := fn.mkAppN args, rty := resTy }) : LamWF ltv { lctx := lctx, rterm := fn.beta args, rty := resTy }

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamWF.ofBeta fn [] wf_2 = wf_2
• Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.atom a) (arg :: args_2) wf_3 = wf_3
• Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.etom a) (arg :: args_2) wf_3 = wf_3
• Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.base a) (arg :: args_2) wf_3 = wf_3
• Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.bvar a) (arg :: args_2) wf_3 = wf_3
• Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.app a a_1 a_2) (arg :: args_2) wf_3 = wf_3

theorem Auto.Embedding.Lam.LamEquiv.ofBeta {lctx : Nat → LamSort} {resTy : LamSort} {lval : LamValuation} (fn : LamTerm) (args : List (LamSort × LamTerm)) (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := fn.mkAppN args, rty := resTy }) : LamEquiv lval lctx resTy (fn.mkAppN args) (fn.beta args)

def Auto.Embedding.Lam.LamTerm.headBetaAux : List (LamSort × LamTerm) → LamTerm → LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.headBetaAux x✝ (Auto.Embedding.Lam.LamTerm.app s fn arg) = Auto.Embedding.Lam.LamTerm.headBetaAux ((s, arg) :: x✝) fn
• Auto.Embedding.Lam.LamTerm.headBetaAux x✝¹ x✝ = x✝.beta x✝¹

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_headBetaAux {args : List (LamSort × LamTerm)} {n : Nat} {t : LamTerm} (hs : HList (fun (x : LamSort × LamTerm) => match x with | (fst, arg) => arg.maxEVarSucc ≤ n) args) (ht : t.maxEVarSucc ≤ n) : (headBetaAux args t).maxEVarSucc ≤ n

def Auto.Embedding.Lam.LamWF.ofHeadBetaAux {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {args : List (LamSort × LamTerm)} {rty : LamSort} (wf : LamWF ltv { lctx := lctx, rterm := t.mkAppN args, rty := rty }) : LamWF ltv { lctx := lctx, rterm := LamTerm.headBetaAux args t, rty := rty }

Equations

• wf_2.ofHeadBetaAux = Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.atom a) args wf_2
• wf_2.ofHeadBetaAux = Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.etom a) args wf_2
• wf_2.ofHeadBetaAux = Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.base a) args wf_2
• wf_2.ofHeadBetaAux = Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.bvar a) args wf_2
• wf_2.ofHeadBetaAux = Auto.Embedding.Lam.LamWF.ofBeta (Auto.Embedding.Lam.LamTerm.lam a a_1) args wf_2
• wf_2.ofHeadBetaAux = wf_2.ofHeadBetaAux

theorem Auto.Embedding.Lam.LamEquiv.ofHeadBetaAux {lctx : Nat → LamSort} {t : LamTerm} {args : List (LamSort × LamTerm)} {rty : LamSort} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t.mkAppN args, rty := rty }) : LamEquiv lval lctx rty (t.mkAppN args) (LamTerm.headBetaAux args t)

def Auto.Embedding.Lam.LamTerm.headBeta : LamTerm → LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.headBeta = Auto.Embedding.Lam.LamTerm.headBetaAux []

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_headBeta {t : LamTerm} : t.headBeta.maxEVarSucc ≤ t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.ofHeadBeta {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} (wf : LamWF ltv { lctx := lctx, rterm := t, rty := s }) : LamWF ltv { lctx := lctx, rterm := t.headBeta, rty := s }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.ofHeadBeta {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) : LamEquiv lval lctx s t t.headBeta

theorem Auto.Embedding.Lam.LamThmEquiv.ofHeadBeta {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (wf : LamThmWF lval lctx s t) : LamThmEquiv lval lctx s t t.headBeta

def Auto.Embedding.Lam.LamTerm.headBetaBounded (n : Nat) (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.headBetaBounded 0 t = t
• Auto.Embedding.Lam.LamTerm.headBetaBounded n_1.succ t = match t.isHeadBetaTarget with | true => Auto.Embedding.Lam.LamTerm.headBetaBounded n_1 t.headBeta | false => t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_headBetaBounded {n : Nat} {t : LamTerm} : (headBetaBounded n t).maxEVarSucc ≤ t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.ofHeadBetaBounded {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {n : Nat} (wf : LamWF ltv { lctx := lctx, rterm := t, rty := s }) : LamWF ltv { lctx := lctx, rterm := LamTerm.headBetaBounded n t, rty := s }

Equations

• wf.ofHeadBetaBounded = wf
• wf.ofHeadBetaBounded = id (match t.isHeadBetaTarget with | true => wf.ofHeadBeta.ofHeadBetaBounded | false => wf)

theorem Auto.Embedding.Lam.LamEquiv.ofHeadBetaBounded {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} {n : Nat} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) : LamEquiv lval lctx s t (LamTerm.headBetaBounded n t)

theorem Auto.Embedding.Lam.LamThmEquiv.ofHeadBetaBounded {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} {n : Nat} (wf : LamThmWF lval lctx s t) : LamThmEquiv lval lctx s t (LamTerm.headBetaBounded n t)

def Auto.Embedding.Lam.LamTerm.betaBounded (n : Nat) (t : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.betaBounded 0 t = t
• Auto.Embedding.Lam.LamTerm.betaBounded n_1.succ (Auto.Embedding.Lam.LamTerm.atom n) = Auto.Embedding.Lam.LamTerm.atom n
• Auto.Embedding.Lam.LamTerm.betaBounded n_1.succ (Auto.Embedding.Lam.LamTerm.etom n) = Auto.Embedding.Lam.LamTerm.etom n
• Auto.Embedding.Lam.LamTerm.betaBounded n_1.succ (Auto.Embedding.Lam.LamTerm.base a) = Auto.Embedding.Lam.LamTerm.base a
• Auto.Embedding.Lam.LamTerm.betaBounded n_1.succ (Auto.Embedding.Lam.LamTerm.bvar n) = Auto.Embedding.Lam.LamTerm.bvar n
• Auto.Embedding.Lam.LamTerm.betaBounded n_1.succ (Auto.Embedding.Lam.LamTerm.lam s body) = Auto.Embedding.Lam.LamTerm.lam s (Auto.Embedding.Lam.LamTerm.betaBounded n_1 body)

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_betaBounded {n : Nat} {t : LamTerm} : (betaBounded n t).maxEVarSucc ≤ t.maxEVarSucc

def Auto.Embedding.Lam.LamTerm.betaReduced (t : LamTerm) : Bool

Equations

• (Auto.Embedding.Lam.LamTerm.app a fn arg).betaReduced = (!fn.isLam && fn.betaReduced && arg.betaReduced)
• (Auto.Embedding.Lam.LamTerm.lam a body).betaReduced = body.betaReduced
• t.betaReduced = true

theorem Auto.Embedding.Lam.LamEquiv.ofBetaBounded {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} {n : Nat} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) : LamEquiv lval lctx s t (LamTerm.betaBounded n t)

theorem Auto.Embedding.Lam.LamThmEquiv.ofBetaBounded {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} {n : Nat} (wf : LamThmWF lval lctx rty t) : LamThmEquiv lval lctx rty t (LamTerm.betaBounded n t)

opaque Auto.Embedding.Lam.LamTerm.betaReduceHackyAux (t : LamTerm) : LamTerm × Nat

def Auto.Embedding.Lam.LamTerm.betaReduceHacky (t : LamTerm) : LamTerm

Equations

• t.betaReduceHacky = t.betaReduceHackyAux.fst

def Auto.Embedding.Lam.LamTerm.betaReduceHackyIdx (t : LamTerm) : Nat

Equations

• t.betaReduceHackyIdx = t.betaReduceHackyAux.snd

theorem Auto.Embedding.Lam.LamThmEquiv.ofResolveImport {lctx : List LamSort} {s : LamSort} {t : LamTerm} {lval : LamValuation} (wfT : LamThmWF lval lctx s t) : LamThmEquiv lval lctx s t (LamTerm.resolveImport lval.toLamTyVal t)

def Auto.Embedding.Lam.LamTerm.eqSymm? (t : LamTerm) : Option LamTerm

(a = b) ↔ (b = a)

Equations

• One or more equations did not get rendered due to their size.
• t.eqSymm? = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_eqSymm? {t t' : LamTerm} (heq : t.eqSymm? = some t') : t'.maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.eqSymm? {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) (heq : t.eqSymm? = some t') : LamWF ltv { lctx := lctx, rterm := t', rty := s }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.eqSymm? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.eqSymm? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamThmEquiv.eqSymm? {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t t' : LamTerm} (wft : LamThmWF lval lctx s t) (heq : t.eqSymm? = some t') : LamThmEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

def Auto.Embedding.Lam.LamTerm.neSymm? (t : LamTerm) : Option LamTerm

(a ≠ b) ↔ (b ≠ a)

Equations

• One or more equations did not get rendered due to their size.
• t.neSymm? = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_neSymm? {t t' : LamTerm} (heq : t.neSymm? = some t') : t'.maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamWF.neSymm? {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) (heq : t.neSymm? = some t') : LamWF ltv { lctx := lctx, rterm := t', rty := s }

Equations

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

theorem Auto.Embedding.Lam.LamEquiv.neSymm? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.neSymm? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamThmEquiv.neSymm? {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t t' : LamTerm} (wft : LamThmWF lval lctx s t) (heq : t.neSymm? = some t') : LamThmEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

def Auto.Embedding.Lam.LamTerm.mpEq? (lhs rhs t : LamTerm) : Option LamTerm

Equations

• lhs.mpEq? rhs t = match t.beq lhs with | true => some rhs | false => none

theorem Auto.Embedding.Lam.LamTerm.evarBounded_mpEq? {lhs rhs : LamTerm} : evarBounded (lhs.mpEq? rhs) rhs.maxEVarSucc

theorem Auto.Embedding.Lam.LamGenConv.mpEq? {lval : LamValuation} {rty : LamSort} {lhs rhs : LamTerm} (hequiv : LamThmEquiv lval [] rty lhs rhs) : LamGenConv lval (lhs.mpEq? rhs)

def Auto.Embedding.Lam.LamTerm.mp? (rw t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• rw.mp? t = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_mp? {rw t t' : LamTerm} (heq : rw.mp? t = some t') : t'.maxEVarSucc ≤ rw.maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.mp? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {lval : LamValuation} {rw t' : LamTerm} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (Hrw : LamValid lval lctx rw) (heq : rw.mp? t = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamThmEquiv.mp? {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t rw t' : LamTerm} (wft : LamThmWF lval lctx rty t) (Hrw : LamThmValid lval lctx rw) (heq : rw.mp? t = some t') : LamThmEquiv lval lctx rty t t'

def Auto.Embedding.Lam.LamTerm.mpAll (lhs rhs t : LamTerm) : Option LamTerm

Equations

• lhs.mpAll rhs t = Auto.Embedding.Lam.LamTerm.rwGenAll (lhs.mpEq? rhs) t

theorem Auto.Embedding.Lam.LamGenConv.mpAll {lval : LamValuation} {s : LamSort} {lhs rhs : LamTerm} (hequiv : LamThmEquiv lval [] s lhs rhs) : LamGenConv lval (lhs.mpAll rhs)

theorem Auto.Embedding.Lam.LamTerm.evarBounded_mpAll {lhs rhs : LamTerm} : evarBounded (lhs.mpAll rhs) rhs.maxEVarSucc

def Auto.Embedding.Lam.LamTerm.mpAll? (rw t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• rw.mpAll? t = none

theorem Auto.Embedding.Lam.LamTerm.evarBounded_mpAll? {rw : LamTerm} : evarBounded rw.mpAll? rw.maxEVarSucc

theorem Auto.Embedding.Lam.LamGenConv.mpAll? {lval : LamValuation} {rw : LamTerm} (hvalid : LamThmValid lval [] rw) : LamGenConv lval rw.mpAll?

def Auto.Embedding.Lam.LamTerm.congrArg? (t rw : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• (Auto.Embedding.Lam.LamTerm.app s fn arg).congrArg? rw = none
• t.congrArg? rw = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_congrArg? {n : Nat} {t rw t' : LamTerm} (ht : t.maxEVarSucc ≤ n) (hrw : rw.maxEVarSucc ≤ n) (heq : t.congrArg? rw = some t') : t'.maxEVarSucc ≤ n

theorem Auto.Embedding.Lam.LamEquiv.congrArg? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {lval : LamValuation} {rw t' : LamTerm} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (Hrw : LamValid lval lctx rw) (heq : t.congrArg? rw = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamThmEquiv.congrArg? {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t rw t' : LamTerm} (wft : LamThmWF lval lctx rty t) (Hrw : LamThmValid lval lctx rw) (heq : t.congrArg? rw = some t') : LamThmEquiv lval lctx rty t t'

def Auto.Embedding.Lam.LamTerm.congrFun? (t rw : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• (Auto.Embedding.Lam.LamTerm.app s fn arg).congrFun? rw = none
• t.congrFun? rw = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_congrFun? {n : Nat} {t rw t' : LamTerm} (ht : t.maxEVarSucc ≤ n) (hrw : rw.maxEVarSucc ≤ n) (heq : t.congrFun? rw = some t') : t'.maxEVarSucc ≤ n

theorem Auto.Embedding.Lam.LamEquiv.congrFun? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {lval : LamValuation} {rw t' : LamTerm} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (Hrw : LamValid lval lctx rw) (heq : t.congrFun? rw = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamThmEquiv.congrFun? {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t rw t' : LamTerm} (wft : LamThmWF lval lctx rty t) (Hrw : LamThmValid lval lctx rw) (heq : t.congrFun? rw = some t') : LamThmEquiv lval lctx rty t t'

def Auto.Embedding.Lam.LamTerm.congr? (t rwFn rwArg : LamTerm) : Option LamTerm

Equations

• t.congr? rwFn rwArg = (t.congrFun? rwFn).bind fun (x : Auto.Embedding.Lam.LamTerm) => x.congrArg? rwArg

theorem Auto.Embedding.Lam.LamEquiv.congr? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {lval : LamValuation} {rwFn rwArg t' : LamTerm} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (HrwFn : LamValid lval lctx rwFn) (HrwArg : LamValid lval lctx rwArg) (heq : t.congr? rwFn rwArg = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_congr? {n : Nat} {t rwFn rwArg t' : LamTerm} (ht : t.maxEVarSucc ≤ n) (hrwFn : rwFn.maxEVarSucc ≤ n) (hrwArg : rwArg.maxEVarSucc ≤ n) (heq : t.congr? rwFn rwArg = some t') : t'.maxEVarSucc ≤ n

theorem Auto.Embedding.Lam.LamThmEquiv.congr? {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t rwFn rwArg t' : LamTerm} (wft : LamThmWF lval lctx rty t) (HrwFn : LamThmValid lval lctx rwFn) (HrwArg : LamThmValid lval lctx rwArg) (heq : t.congr? rwFn rwArg = some t') : LamThmEquiv lval lctx rty t t'

def Auto.Embedding.Lam.LamTerm.congrArgs? (t : LamTerm) (rwArgs : List LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• t.congrArgs? [] = some t
• t.congrArgs? (rwArg :: rwArgs_2) = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_congrArgs? {n : Nat} {rwArgs : List LamTerm} {t t' : LamTerm} (ht : t.maxEVarSucc ≤ n) (hrwArgs : HList (fun (rw : LamTerm) => rw.maxEVarSucc ≤ n) rwArgs) (heq : t.congrArgs? rwArgs = some t') : t'.maxEVarSucc ≤ n

theorem Auto.Embedding.Lam.LamEquiv.congrArgs? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {lval : LamValuation} {rwArgs : List LamTerm} {t' : LamTerm} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (HrwArgs : HList (LamValid lval lctx) rwArgs) (heq : t.congrArgs? rwArgs = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamThmEquiv.congrArgs? {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} {rwArgs : List LamTerm} {t' : LamTerm} (wft : LamThmWF lval lctx rty t) (HrwArgs : HList (LamThmValid lval lctx) rwArgs) (heq : t.congrArgs? rwArgs = some t') : LamThmEquiv lval lctx rty t t'

def Auto.Embedding.Lam.LamTerm.congrFunN? (t rwFn : LamTerm) (idx : Nat) : Option LamTerm

Equations

• (Auto.Embedding.Lam.LamTerm.app s fn arg).congrFunN? rwFn 0 = (Auto.Embedding.Lam.LamTerm.app s fn arg).congrFun? rwFn
• (Auto.Embedding.Lam.LamTerm.app s fn arg).congrFunN? rwFn n.succ = (fun (x : Auto.Embedding.Lam.LamTerm) => Auto.Embedding.Lam.LamTerm.app s x arg) <$> fn.congrFunN? rwFn n
• t.congrFunN? rwFn idx = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_congrFunN? {n : Nat} {t rwFn : LamTerm} {idx : Nat} {t' : LamTerm} (ht : t.maxEVarSucc ≤ n) (hrwFn : rwFn.maxEVarSucc ≤ n) (heq : t.congrFunN? rwFn idx = some t') : t'.maxEVarSucc ≤ n

theorem Auto.Embedding.Lam.LamEquiv.congrFunN? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {lval : LamValuation} {rwFn : LamTerm} {n : Nat} {t' : LamTerm} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (HrwFn : LamValid lval lctx rwFn) (heq : t.congrFunN? rwFn n = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamThmEquiv.congrFunN? {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t rwFn : LamTerm} {n : Nat} {t' : LamTerm} (wft : LamThmWF lval lctx rty t) (HrwFn : LamThmValid lval lctx rwFn) (heq : t.congrFunN? rwFn n = some t') : LamThmEquiv lval lctx rty t t'

def Auto.Embedding.Lam.LamTerm.congrs? (t rwFn : LamTerm) (rwArgs : List LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• t.congrs? rwFn [] = rwFn.mp? t
• t.congrs? rwFn (rwArg :: rwArgs_2) = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_congrs? {n : Nat} {rwArgs : List LamTerm} {t rwFn t' : LamTerm} (ht : t.maxEVarSucc ≤ n) (hrwFn : rwFn.maxEVarSucc ≤ n) (hrwArgs : HList (fun (rw : LamTerm) => rw.maxEVarSucc ≤ n) rwArgs) (heq : t.congrs? rwFn rwArgs = some t') : t'.maxEVarSucc ≤ n

theorem Auto.Embedding.Lam.LamEquiv.congrs? {lctx : Nat → LamSort} {t : LamTerm} {rty : LamSort} {lval : LamValuation} {rwFn : LamTerm} {rwArgs : List LamTerm} {t' : LamTerm} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := rty }) (HrwFn : LamValid lval lctx rwFn) (HrwArgs : HList (LamValid lval lctx) rwArgs) (heq : t.congrs? rwFn rwArgs = some t') : LamEquiv lval lctx rty t t'

theorem Auto.Embedding.Lam.LamThmEquiv.congrs? {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t rwFn : LamTerm} {rwArgs : List LamTerm} {t' : LamTerm} (wft : LamThmWF lval lctx rty t) (HrwFn : LamThmValid lval lctx rwFn) (HrwArgs : HList (LamThmValid lval lctx) rwArgs) (heq : t.congrs? rwFn rwArgs = some t') : LamThmEquiv lval lctx rty t t'

def Auto.Embedding.Lam.LamTerm.replace (t : LamTerm) (f : LamTerm → Option LamTerm) (lvl : Nat) : LamTerm

Equations

• One or more equations did not get rendered due to their size.
• t.replace f lvl = match f (Auto.Embedding.Lam.LamTerm.bvarLifts lvl t) with | some t' => Auto.Embedding.Lam.LamTerm.bvarLifts lvl t' | none => t

def Auto.Embedding.Lam.LamTerm.abstractsImp (t : LamTerm) (ts : Array LamTerm) : LamTerm

Turn ts[i] into .bvar i

Equations

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

def Auto.Embedding.Lam.LamTerm.abstractsRevImp (t : LamTerm) (ts : Array LamTerm) : LamTerm

Equations

• t.abstractsRevImp ts = t.abstractsImp ts.reverse

def Auto.Embedding.Lam.LamTerm.instantiatesAtImp (idx : Nat) (args : Array LamTerm) (body : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.instantiatesAtImp idx args (Auto.Embedding.Lam.LamTerm.atom n) = Auto.Embedding.Lam.LamTerm.atom n
• Auto.Embedding.Lam.LamTerm.instantiatesAtImp idx args (Auto.Embedding.Lam.LamTerm.etom n) = Auto.Embedding.Lam.LamTerm.etom n
• Auto.Embedding.Lam.LamTerm.instantiatesAtImp idx args (Auto.Embedding.Lam.LamTerm.base a) = Auto.Embedding.Lam.LamTerm.base a
• Auto.Embedding.Lam.LamTerm.instantiatesAtImp idx args (Auto.Embedding.Lam.LamTerm.lam s body) = Auto.Embedding.Lam.LamTerm.lam s (Auto.Embedding.Lam.LamTerm.instantiatesAtImp idx.succ args body)

def Auto.Embedding.Lam.LamTerm.instantiatesImp (args : Array LamTerm) (body : LamTerm) : LamTerm

Turn .bvar i into args[i]

Equations

• Auto.Embedding.Lam.LamTerm.instantiatesImp = Auto.Embedding.Lam.LamTerm.instantiatesAtImp 0

def Auto.Embedding.Lam.LamTerm.findTerm? (p : LamTerm → Bool) (t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.findTerm? p t = if p t = true then some t else none

def Auto.Embedding.Lam.LamTerm.isGeneral (k : Nat) (t : LamTerm) : Option (Array Nat)

Determine whether a λ term t (within LamThmValid lval lctx t) is of the form LamTerm.mkAppN ((.atom i) <|> (.etom i)) [.bvar iₖ₋₁, ⋯, .bvar i₁, .bvar i₀] where i₀, i₁, ⋯, iₖ₋₁ is a permutation of 0, 1, 2, ⋯, k - 1 and k is the length of lctx. If t is of the above form, return a list l of length k where ∀ 0 ≤ j < k, l[iⱼ] = j · This is an auxiliary function for definition unfolding. If we identify equalities in the input formulas with lhs or rhs being general, for example lhs = LamTerm.mkAppN (.atom i) [.bvar iₖ₋₁, ⋯, .bvar i₁, .bvar i₀], then we can · First, reorder local context and intensionalize the above equation to make it look like a definition of .atom i · Then, exhaustively unfold .atom i in all input formulas using this definition · Finally, remove the original equation (i.e. lhs = rhs) from the set of input formulas It's easy to see that the above procedure is sound and complete if rhs does not contains lhs. · Note that the above procedure will not be complete if we relax the iteition `i₀, i₁, ⋯, iₖ₋₁` is a permutation of `0, 1, 2, ⋯, k - 1` to `i₀, i₁, ⋯, iₖ₋₁` is a permutation of a subsequence of `0, 1, 2, ⋯, k - 1` even if we require that rhs does not contain lhs. To see this, consider the following example with two input formulas: (Note: #i is type atom, !i is term atom, ⟨i⟩ is .bvar i)

1. LamThmValid [#0, #0, #0] (!0 ⟨0⟩ ⟨1⟩ = !1 ⟨0⟩ ⟨1⟩ ⟨0⟩ ⟨2⟩) (lhs is (relaxed) general)
2. LamThmValid [] (!1 !2 !2 !2 !2 = !1 !2 !2 !2 !3)

Equations

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