Equations
- Auto.Embedding.coPairAt f restore = ∀ (pos : Nat) (lctx : Nat → α) (n : Nat), Auto.Embedding.restoreAt pos restore lctx (Auto.Embedding.mapAt pos f n) = lctx n
Instances For
theorem
Auto.Embedding.contraPairAt.ofContraPair
{f : Nat → Nat}
{α✝ : Sort u_1}
{cstr : (Nat → α✝) → Prop}
{restore : (Nat → α✝) → Nat → α✝}
(cp : contraPair f cstr restore)
:
contraPairAt f cstr restore
def
Auto.Embedding.restoreAtDep
{α : Sort u_1}
{lctxty : α → Sort u}
(pos : Nat)
{restore : (Nat → α) → Nat → α}
(restoreDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n))
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
(n : Nat)
:
lctxty (restoreAt pos restore rty n)
Equations
Instances For
theorem
Auto.Embedding.restoreAtDep_succ_succ
{α : Sort u_1}
{lctxty : α → Sort u}
(pos : Nat)
{restore : (Nat → α) → Nat → α}
(restoreDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n))
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
(n : Nat)
:
restoreAtDep pos.succ (fun {rty : Nat → α} => restoreDep) lctx n.succ ≍ restoreAtDep pos (fun {rty : Nat → α} => restoreDep) (fun (n : Nat) => lctx n.succ) n
theorem
Auto.Embedding.restoreAtDep_succ_succ_Fn
{α : Sort u_1}
{lctxty : α → Sort u}
(pos : Nat)
{restore : (Nat → α) → Nat → α}
(restoreDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n))
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
:
(fun (n : Nat) => restoreAtDep pos.succ (fun {rty : Nat → α} => restoreDep) lctx n.succ) ≍ restoreAtDep pos (fun {rty : Nat → α} => restoreDep) fun (n : Nat) => lctx n.succ
def
Auto.Embedding.coPairDep
{α : Sort u_1}
(lctxty : α → Sort u)
(f : Nat → Nat)
(restore : (Nat → α) → Nat → α)
(restoreDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n))
:
Equations
- Auto.Embedding.coPairDep lctxty f restore restoreDep = (Auto.Embedding.coPair f restore ∧ ∀ {rty : Nat → α} (lctx : (n : Nat) → lctxty (rty n)) (n : Nat), restoreDep lctx (f n) ≍ lctx n)
Instances For
theorem
Auto.Embedding.coPairDepAt.ofCoPairDep
{α✝ : Sort u_1}
{lctxty : α✝ → Sort u_2}
{f : Nat → Nat}
{restore : (Nat → α✝) → Nat → α✝}
{restoreDep : {rty : Nat → α✝} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n)}
(cpd : coPairDep lctxty f restore restoreDep)
:
coPairDepAt lctxty f restore fun {rty : Nat → α✝} => restoreDep
def
Auto.Embedding.contraPairDep
{α : Sort u_1}
(lctxty : α → Sort u)
(f : Nat → Nat)
(cstr : (Nat → α) → Prop)
(restore : (Nat → α) → Nat → α)
(cstrDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → Prop)
(restoreDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Auto.Embedding.contraPairDepAt
{α : Sort u_1}
(lctxty : α → Sort u)
(f : Nat → Nat)
(cstr : (Nat → α) → Prop)
(restore : (Nat → α) → Nat → α)
(cstrDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → Prop)
(restoreDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n))
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Auto.Embedding.contraPairDep.ofContraPairDep
{α✝ : Sort u_1}
{lctxty : α✝ → Sort u_2}
{f : Nat → Nat}
{cstr : (Nat → α✝) → Prop}
{restore : (Nat → α✝) → Nat → α✝}
{cstrDep : {rty : Nat → α✝} → ((n : Nat) → lctxty (rty n)) → Prop}
{restoreDep : {rty : Nat → α✝} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n)}
(cpd : contraPairDep lctxty f cstr restore cstrDep restoreDep)
:
contraPairDepAt lctxty f cstr restore (fun {rty : Nat → α✝} => cstrDep) fun {rty : Nat → α✝} => restoreDep
@[reducible]
Equations
- Auto.Embedding.pushLCtx x lctx 0 = x
- Auto.Embedding.pushLCtx x lctx n'.succ = lctx n'
Instances For
@[reducible]
Equations
Instances For
theorem
Auto.Embedding.pushLCtxAt_lt
{α : Sort u_1}
{lctx : Nat → α}
(x : α)
(pos n : Nat)
(hlt : n < pos)
:
theorem
Auto.Embedding.pushLCtxAt_gt
{α : Sort u_1}
{lctx : Nat → α}
(x : α)
(pos n : Nat)
(hle : n > pos)
:
theorem
Auto.Embedding.pushLCtxAt_succ_succ
{α : Sort u_1}
(x : α)
(pos : Nat)
(lctx : Nat → α)
(n : Nat)
:
theorem
Auto.Embedding.pushLCtxAt_succ_succ_Fn
{α : Sort u_1}
(x : α)
(pos : Nat)
(lctx : Nat → α)
:
(fun (n : Nat) => pushLCtxAt x pos.succ lctx n.succ) = pushLCtxAt x pos fun (n : Nat) => lctx n.succ
theorem
Auto.Embedding.pushLCtxAt_commFn
{α : Sort u_1}
{β : Sort u_2}
(f : α → β)
(x : α)
(pos : Nat)
(lctx : Nat → α)
:
(fun (n : Nat) => f (pushLCtxAt x pos lctx n)) = fun (n : Nat) => pushLCtxAt (f x) pos (fun (n : Nat) => f (lctx n)) n
@[reducible]
def
Auto.Embedding.pushLCtxDep
{α : Sort u_1}
{lctxty : α → Sort u}
{xty : α}
(x : lctxty xty)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
(n : Nat)
:
lctxty (pushLCtx xty rty n)
Equations
- Auto.Embedding.pushLCtxDep x lctx 0 = id x
- Auto.Embedding.pushLCtxDep x lctx n'.succ = id (lctx n')
Instances For
theorem
Auto.Embedding.pushLCtxDep_heq
{α₁ α₂ : Sort u_1}
{lctxty₁ : α₁ → Sort u}
{ty₁ : α₁}
(x₁ : lctxty₁ ty₁)
(rty₁ : Nat → α₁)
(lctx₁ : (n : Nat) → lctxty₁ (rty₁ n))
{lctxty₂ : α₂ → Sort u}
{ty₂ : α₂}
(x₂ : lctxty₂ ty₂)
(rty₂ : Nat → α₂)
(lctx₂ : (n : Nat) → lctxty₂ (rty₂ n))
(h₁ : α₁ = α₂)
(h₂ : lctxty₁ ≍ lctxty₂)
(h₃ : ty₁ ≍ ty₂)
(h₄ : x₁ ≍ x₂)
(h₅ : rty₁ ≍ rty₂)
(h₆ : lctx₁ ≍ lctx₂)
:
def
Auto.Embedding.pushLCtxAtDep
{α : Sort u_1}
{lctxty : α → Sort u}
{xty : α}
(x : lctxty xty)
(pos : Nat)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
(n : Nat)
:
lctxty (pushLCtxAt xty pos rty n)
Equations
- Auto.Embedding.pushLCtxAtDep x pos lctx n = Auto.Embedding.restoreAtDep pos (fun {rty : Nat → α} => Auto.Embedding.pushLCtxDep x) lctx n
Instances For
theorem
Auto.Embedding.pushLCtxAtDep_heq
{α₁ α₂ : Sort u_1}
{lctxty₁ : α₁ → Sort u}
{ty₁ : α₁}
(x₁ : lctxty₁ ty₁)
(pos₁ : Nat)
(rty₁ : Nat → α₁)
(lctx₁ : (n : Nat) → lctxty₁ (rty₁ n))
{lctxty₂ : α₂ → Sort u}
{ty₂ : α₂}
(x₂ : lctxty₂ ty₂)
(pos₂ : Nat)
(rty₂ : Nat → α₂)
(lctx₂ : (n : Nat) → lctxty₂ (rty₂ n))
(h₁ : α₁ = α₂)
(h₂ : lctxty₁ ≍ lctxty₂)
(h₃ : ty₁ ≍ ty₂)
(h₄ : x₁ ≍ x₂)
(h₅ : pos₁ = pos₂)
(h₆ : rty₁ ≍ rty₂)
(h₇ : lctx₁ ≍ lctx₂)
:
theorem
Auto.Embedding.pushLCtxAtDep_zero
{α : Sort u_1}
{lctxty : α → Sort u}
{xty : α}
(x : lctxty xty)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
:
theorem
Auto.Embedding.pushLCtxAtDep_succ_succ_Fn
{α : Sort u_1}
{rty : Nat → α}
{lctxty : α → Sort u}
{xty : α}
(x : lctxty xty)
(pos : Nat)
(lctx : (n : Nat) → lctxty (rty n))
:
(fun (n : Nat) => pushLCtxAtDep x pos.succ lctx n.succ) ≍ pushLCtxAtDep x pos fun (n : Nat) => lctx n.succ
def
Auto.Embedding.pushLCtxAtDep_comm
{α : Sort w}
{β : α → Sort x}
{rty : Nat → α}
{lctxty : α → Sort u}
(f : (x : α) → lctxty x → β x)
{xty : α}
(x : lctxty xty)
(pos : Nat)
(lctx : (n : Nat) → lctxty (rty n))
(n : Nat)
:
f (pushLCtxAt xty pos rty n) (pushLCtxAtDep x pos lctx n) = pushLCtxAtDep (f xty x) pos (fun (n : Nat) => f (rty n) (lctx n)) n
Equations
- ⋯ = ⋯
Instances For
theorem
Auto.Embedding.pushLCtxDep_zero
{α : Sort u_1}
{lctxty : α → Sort u}
{xty : α}
(x : lctxty xty)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
:
theorem
Auto.Embedding.pushLCtxDep_succ_Fn
{α : Sort u_1}
{lctxty : α → Sort u}
{xty : α}
(x : lctxty xty)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
:
theorem
Auto.Embedding.pushLCtxDep_comm
{α : Sort w}
{β : α → Sort x}
{rty : Nat → α}
{lctxty : α → Sort u}
(f : (x : α) → lctxty x → β x)
(lctx : (n : Nat) → lctxty (rty n))
{xty : α}
(x : lctxty xty)
(n : Nat)
:
f (pushLCtx xty rty n) (pushLCtxDep x lctx n) = pushLCtxDep (f xty x) (fun (n : Nat) => f (rty n) (lctx n)) n
theorem
Auto.Embedding.pushLCtx_commDep
{α : Sort u_1}
{n : Nat}
{β : α → Sort x}
{x : α}
{lctx : Nat → α}
(f : (x : α) → β x)
:
theorem
Auto.Embedding.pushLCtxDep_absorb
{α : Sort u_1}
{rty : Nat → α}
{lctxty : α → Sort u}
(lctx : (n : Nat) → lctxty (rty n))
{xty : α}
(x : lctxty xty)
:
@[reducible]
def
Auto.Embedding.pushLCtxsAt
{α : Type u_1}
(xs : List α)
(pos : Nat)
(lctx : Nat → α)
(n : Nat)
:
α
Equations
- Auto.Embedding.pushLCtxsAt xs pos = Auto.Embedding.restoreAt pos (Auto.Embedding.pushLCtxs xs)
Instances For
theorem
Auto.Embedding.pushLCtxsAt_succ_zero
{α : Type u_1}
(xs : List α)
(pos : Nat)
(lctx : Nat → α)
:
theorem
Auto.Embedding.pushLCtxsAt_succ_succ_Fn
{α : Type u_1}
(xs : List α)
(pos : Nat)
(lctx : Nat → α)
:
(fun (n : Nat) => pushLCtxsAt xs pos.succ lctx n.succ) = pushLCtxsAt xs pos fun (n : Nat) => lctx n.succ
@[reducible]
def
Auto.Embedding.pushLCtxsDep
{α : Type u_1}
{lctxty : α → Sort u}
{tys : List α}
(xs : HList lctxty tys)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
(n : Nat)
:
lctxty (pushLCtxs tys rty n)
Equations
- Auto.Embedding.pushLCtxsDep xs lctx n = id (match n.blt tys.length with | true => Auto.HList.getD (lctx 0) xs n | false => lctx (n - tys.length))
Instances For
theorem
Auto.Embedding.pushLCtxsDep_heq
{α₁ α₂ : Type u_1}
{lctxty₁ : α₁ → Sort u}
{tys₁ : List α₁}
(xs₁ : HList lctxty₁ tys₁)
(rty₁ : Nat → α₁)
(lctx₁ : (n : Nat) → lctxty₁ (rty₁ n))
{lctxty₂ : α₂ → Sort u}
{tys₂ : List α₂}
(xs₂ : HList lctxty₂ tys₂)
(rty₂ : Nat → α₂)
(lctx₂ : (n : Nat) → lctxty₂ (rty₂ n))
(h₁ : α₁ = α₂)
(h₂ : lctxty₁ ≍ lctxty₂)
(h₃ : tys₁ ≍ tys₂)
(h₄ : xs₁ ≍ xs₂)
(h₅ : rty₁ ≍ rty₂)
(h₆ : lctx₁ ≍ lctx₂)
:
theorem
Auto.Embedding.pushLCtxsDep_nil
{α : Type u_1}
{lctxty : α → Sort u}
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
:
theorem
Auto.Embedding.pushLCtxsDep_singleton
{α : Type u_1}
{lctxty : α → Sort u}
{ty : α}
(x : lctxty ty)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
:
@[reducible]
def
Auto.Embedding.pushLCtxsAtDep
{α : Type u_1}
{lctxty : α → Sort u}
{tys : List α}
(xs : HList lctxty tys)
(pos : Nat)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
(n : Nat)
:
Equations
- Auto.Embedding.pushLCtxsAtDep xs pos lctx = Auto.Embedding.restoreAtDep pos (fun {rty : Nat → α} => Auto.Embedding.pushLCtxsDep xs) lctx
Instances For
theorem
Auto.Embedding.pushLCtxsAtDep_heq
{α₁ α₂ : Type u_1}
{lctxty₁ : α₁ → Sort u}
{tys₁ : List α₁}
(xs₁ : HList lctxty₁ tys₁)
(pos₁ : Nat)
(rty₁ : Nat → α₁)
(lctx₁ : (n : Nat) → lctxty₁ (rty₁ n))
{lctxty₂ : α₂ → Sort u}
{tys₂ : List α₂}
(xs₂ : HList lctxty₂ tys₂)
(pos₂ : Nat)
(rty₂ : Nat → α₂)
(lctx₂ : (n : Nat) → lctxty₂ (rty₂ n))
(h₁ : α₁ = α₂)
(h₂ : lctxty₁ ≍ lctxty₂)
(h₃ : tys₁ ≍ tys₂)
(h₄ : xs₁ ≍ xs₂)
(h₅ : pos₁ = pos₂)
(h₆ : rty₁ ≍ rty₂)
(h₇ : lctx₁ ≍ lctx₂)
:
theorem
Auto.Embedding.pushLCtxsAtDep_succ_succ_Fn
{α : Type u_1}
{lctxty : α → Sort u}
{tys : List α}
(xs : HList lctxty tys)
(pos : Nat)
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
:
(fun (n : Nat) => pushLCtxsAtDep xs pos.succ lctx n.succ) ≍ pushLCtxsAtDep xs pos fun (n : Nat) => lctx n.succ
def
Auto.Embedding.HList.ofFun
{α : Type u_1}
{tyf : Nat → α}
{β : α → Sort u_2}
(f : (n : Nat) → β (tyf n))
(n : Nat)
:
HList β (List.ofFun tyf n)
Equations
- Auto.Embedding.HList.ofFun f 0 = Auto.HList.nil
- Auto.Embedding.HList.ofFun f n'.succ = Auto.HList.cons (f 0) (Auto.Embedding.HList.ofFun (fun (n : Nat) => f n.succ) n')
Instances For
theorem
Auto.Embedding.pushDep_popDep_eq
{α : Sort u_1}
{lctxty : α → Sort u}
{rty : Nat → α}
(lctx : (n : Nat) → lctxty (rty n))
:
@[reducible]
Equations
- Auto.Embedding.addAt lvl pos = Auto.Embedding.mapAt pos fun (x : Nat) => x + lvl
Instances For
@[reducible]
Equations
Instances For
theorem
Auto.Embedding.restoreAtDep_succ_pushLCtxDep
{α : Sort u_1}
{lctxty : α → Sort u}
(restore : (Nat → α) → Nat → α)
(restoreDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n))
{rty : Nat → α}
{xty : α}
(x : lctxty xty)
(pos : Nat)
(lctx : (n : Nat) → lctxty (rty n))
(n : Nat)
:
restoreAtDep pos.succ (fun {rty : Nat → α} => restoreDep) (pushLCtxDep x lctx) n ≍ pushLCtxDep x (restoreAtDep pos (fun {rty : Nat → α} => restoreDep) lctx) n
theorem
Auto.Embedding.restoreAtDep_succ_pushLCtxDep_Fn
{α : Sort u_1}
{lctxty : α → Sort u}
(restore : (Nat → α) → Nat → α)
(restoreDep : {rty : Nat → α} → ((n : Nat) → lctxty (rty n)) → (n : Nat) → lctxty (restore rty n))
{rty : Nat → α}
{xty : α}
(x : lctxty xty)
(pos : Nat)
(lctx : (n : Nat) → lctxty (rty n))
:
restoreAtDep pos.succ (fun {rty : Nat → α} => restoreDep) (pushLCtxDep x lctx) ≍ pushLCtxDep x (restoreAtDep pos (fun {rty : Nat → α} => restoreDep) lctx)
theorem
Auto.Embedding.contraPair.ofPushPop
{α : Sort u_1}
(x : α)
:
contraPair Nat.succ (fun (lctx : Nat → α) => lctx 0 = x) (pushLCtx x)
theorem
Auto.Embedding.coPairDep.ofPushDepPopDep
{α : Sort u_1}
{lctxty : α → Sort u}
{xty : α}
(x : lctxty xty)
:
coPairDep lctxty Nat.succ (pushLCtx xty) fun {rty : Nat → α} => pushLCtxDep x
theorem
Auto.Embedding.contraPairDep.ofPushDepPopDep
{α : Sort u_1}
{lctxty : α → Sort u}
{xty : α}
(x : lctxty xty)
:
contraPairDep lctxty Nat.succ (fun (lctxty : Nat → α) => lctxty 0 = xty) (pushLCtx xty)
(fun {rty : Nat → α} (lctx : (n : Nat) → lctxty (rty n)) => lctx 0 ≍ x) fun {rty : Nat → α} => pushLCtxDep x
theorem
Auto.Embedding.contraPair.ofPushsPops
{α : Type u_1}
(lvl : Nat)
(xs : List α)
(heq : xs.length = lvl)
:
contraPair (fun (n : Nat) => n + lvl) (fun (lctx : Nat → α) => List.ofFun lctx lvl = xs) (pushLCtxs xs)
theorem
Auto.Embedding.contraPairDep.ofPushsDepPopsDep
{α : Type u_1}
{lctxty : α → Sort u}
(lvl : Nat)
{tys : List α}
(xs : HList lctxty tys)
(heq : tys.length = lvl)
:
contraPairDep lctxty (fun (n : Nat) => n + lvl) (fun (lctxty : Nat → α) => List.ofFun lctxty lvl = tys) (pushLCtxs tys)
(fun {rty : Nat → α} (lctx : (n : Nat) → lctxty (rty n)) => HList.ofFun lctx lvl ≍ xs) fun {rty : Nat → α} =>
pushLCtxsDep xs