structure CC.Subst (s1 s2 : Sig) : Type

A substitution maps bound variables of each kind to terms of the appropriate sort.

• var : BVar s1 Kind.var → Var Kind.var s2
• tvar : BVar s1 Kind.tvar → Ty TySort.shape s2
• cvar : BVar s1 Kind.cvar → CaptureSet s2

def CC.Subst.lift {s1 s2 : Sig} {k : Kind} (s : Subst s1 s2) : Subst (s1,,k) (s2,,k)

Lifts a substitution under a binder. The newly bound variable maps to itself.

Equations

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

def CC.Subst.liftMany {s1 s2 : Sig} (s : Subst s1 s2) (K : Sig) : Subst (s1 ++ K) (s2 ++ K)

Lifts a substitution under multiple binders.

Equations

• s.liftMany [] = s
• s.liftMany (k :: K_2) = (s.liftMany K_2).lift

def CC.Subst.id {s : Sig} : Subst s s

The identity substitution.

Equations

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

def CC.Var.subst {s1 s2 : Sig} : Var Kind.var s1 → Subst s1 s2 → Var Kind.var s2

Applies a substitution to a variable. Free variables remain unchanged.

Equations

• (CC.Var.bound x_2).subst x✝ = x✝.var x_2
• (CC.Var.free n).subst x✝ = CC.Var.free n

def CC.CaptureSet.subst {s1 s2 : Sig} : CaptureSet s1 → Subst s1 s2 → CaptureSet s2

Applies a substitution to all bound variables in a capture set.

Equations

• CC.CaptureSet.empty.subst x✝ = CC.CaptureSet.empty
• (cs1.union cs2).subst x✝ = (cs1.subst x✝).union (cs2.subst x✝)
• (CC.CaptureSet.var x_2).subst x✝ = CC.CaptureSet.var (x_2.subst x✝)
• (CC.CaptureSet.cvar x_2).subst x✝ = x✝.cvar x_2

def CC.CaptureBound.subst {s1 s2 : Sig} : CaptureBound s1 → Subst s1 s2 → CaptureBound s2

Applies a substitution to a capture bound.

Equations

• CC.CaptureBound.unbound.subst x✝ = CC.CaptureBound.unbound
• (CC.CaptureBound.bound cs).subst x✝ = CC.CaptureBound.bound (cs.subst x✝)

def CC.Ty.subst {sort : TySort} {s1 s2 : Sig} : Ty sort s1 → Subst s1 s2 → Ty sort s2

Applies a substitution to a type.

Equations

• CC.Ty.top.subst x✝ = CC.Ty.top
• (CC.Ty.tvar x_2).subst x✝ = x✝.tvar x_2
• (T1.arrow T2).subst x✝ = (T1.subst x✝).arrow (T2.subst x✝.lift)
• (T1.poly T2).subst x✝ = (T1.subst x✝).poly (T2.subst x✝.lift)
• (CC.Ty.cpoly cb T).subst x✝ = CC.Ty.cpoly (cb.subst x✝) (T.subst x✝.lift)
• CC.Ty.unit.subst x✝ = CC.Ty.unit
• CC.Ty.cap.subst x✝ = CC.Ty.cap
• CC.Ty.bool.subst x✝ = CC.Ty.bool
• CC.Ty.cell.subst x✝ = CC.Ty.cell
• (CC.Ty.capt cs T).subst x✝ = CC.Ty.capt (cs.subst x✝) (T.subst x✝)
• T.exi.subst x✝ = (T.subst x✝.lift).exi
• T.typ.subst x✝ = (T.subst x✝).typ

def CC.Exp.subst {s1 s2 : Sig} : Exp s1 → Subst s1 s2 → Exp s2

Applies a substitution to an expression.

Equations

• (CC.Exp.var x_2).subst x✝ = CC.Exp.var (x_2.subst x✝)
• (CC.Exp.abs cs T e).subst x✝ = CC.Exp.abs (cs.subst x✝) (T.subst x✝) (e.subst x✝.lift)
• (CC.Exp.tabs cs T e).subst x✝ = CC.Exp.tabs (cs.subst x✝) (T.subst x✝) (e.subst x✝.lift)
• (CC.Exp.cabs cs cb e).subst x✝ = CC.Exp.cabs (cs.subst x✝) (cb.subst x✝) (e.subst x✝.lift)
• (CC.Exp.pack cs x_2).subst x✝ = CC.Exp.pack (cs.subst x✝) (x_2.subst x✝)
• (CC.Exp.app x_2 y).subst x✝ = CC.Exp.app (x_2.subst x✝) (y.subst x✝)
• (CC.Exp.tapp x_2 T).subst x✝ = CC.Exp.tapp (x_2.subst x✝) (T.subst x✝)
• (CC.Exp.capp x_2 cs).subst x✝ = CC.Exp.capp (x_2.subst x✝) (cs.subst x✝)
• (e1.letin e2).subst x✝ = (e1.subst x✝).letin (e2.subst x✝.lift)
• (e1.unpack e2).subst x✝ = (e1.subst x✝).unpack (e2.subst x✝.lift.lift)
• CC.Exp.unit.subst x✝ = CC.Exp.unit
• CC.Exp.btrue.subst x✝ = CC.Exp.btrue
• CC.Exp.bfalse.subst x✝ = CC.Exp.bfalse
• (CC.Exp.read x_2).subst x✝ = CC.Exp.read (x_2.subst x✝)
• (CC.Exp.write x_2 y).subst x✝ = CC.Exp.write (x_2.subst x✝) (y.subst x✝)
• (CC.Exp.cond x_2 e2 e3).subst x✝ = CC.Exp.cond (x_2.subst x✝) (e2.subst x✝) (e3.subst x✝)

def CC.Subst.openVar {s : Sig} (x : Var Kind.var s) : Subst (s,x) s

Substitution that opens a variable binder by replacing the innermost bound variable with x.

Equations

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

def CC.Subst.openTVar {s : Sig} (U : Ty TySort.shape s) : Subst (s,X) s

Opens a type variable binder, substituting U for the innermost bound.

Equations

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

def CC.Subst.openCVar {s : Sig} (C : CaptureSet s) : Subst (s,C) s

Opens a capture variable binder, substituting C for the innermost bound.

Equations

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

def CC.Subst.unpack {s : Sig} (C : CaptureSet s) (x : Var Kind.var s) : Subst (s,C,x) s

Opens an existential package, substituting C and x for the two innermost binders.

Equations

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

theorem CC.Subst.funext {s1 s2 : Sig} {σ1 σ2 : Subst s1 s2} (hvar : ∀ (x : BVar s1 Kind.var), σ1.var x = σ2.var x) (htvar : ∀ (x : BVar s1 Kind.tvar), σ1.tvar x = σ2.tvar x) (hcvar : ∀ (x : BVar s1 Kind.cvar), σ1.cvar x = σ2.cvar x) : σ1 = σ2

Function extensionality for substitutions. Two substitutions are equal if they map all variables equally.

def CC.Subst.comp {s1 s2 s3 : Sig} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) : Subst s1 s3

Composition of substitutions.

Equations

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

theorem CC.Subst.lift_there_var_eq {s1 s2 : Sig} {k : Kind} {σ : Subst s1 s2} {x : BVar s1 Kind.var} : σ.lift.var x.there = (σ.var x).rename Rename.succ

theorem CC.Subst.lift_there_tvar_eq {s1 s2 : Sig} {k : Kind} {σ : Subst s1 s2} {X : BVar s1 Kind.tvar} : σ.lift.tvar X.there = (σ.tvar X).rename Rename.succ

theorem CC.Rename.lift_there_tvar_eq {s1 s2 : Sig} {k : Kind} {f : Rename s1 s2} {x : BVar s1 Kind.tvar} : f.lift.var x.there = (f.var x).there

theorem CC.Rename.lift_there_var_eq {s1 s2 : Sig} {k : Kind} {f : Rename s1 s2} {x : BVar s1 Kind.var} : f.lift.var x.there = (f.var x).there

theorem CC.Subst.lift_there_cvar_eq {s1 s2 : Sig} {k : Kind} {σ : Subst s1 s2} {C : BVar s1 Kind.cvar} : σ.lift.cvar C.there = (σ.cvar C).rename Rename.succ

theorem CC.Rename.lift_there_cvar_eq {s1 s2 : Sig} {k : Kind} {f : Rename s1 s2} {C : BVar s1 Kind.cvar} : f.lift.var C.there = (f.var C).there

theorem CC.CaptureSet.weaken_rename_comm {s1 s2 : Sig} {k0 : Kind} {cs : CaptureSet s1} {f : Rename s1 s2} : (cs.rename Rename.succ).rename f.lift = (cs.rename f).rename Rename.succ

theorem CC.TVar.weaken_subst_comm_liftMany {s1 K s2 : Sig} {k0 : Kind} {X : BVar (s1 ++ K) Kind.tvar} {σ : Subst s1 s2} : ((σ.liftMany K).tvar X).rename (Rename.succ.liftMany K) = (σ.lift.liftMany K).tvar ((Rename.succ.liftMany K).var X)

theorem CC.Var.weaken_subst_comm_liftMany {s1 K s2 : Sig} {k0 : Kind} {x : Var Kind.var (s1 ++ K)} {σ : Subst s1 s2} : (x.subst (σ.liftMany K)).rename (Rename.succ.liftMany K) = (x.rename (Rename.succ.liftMany K)).subst (σ.lift.liftMany K)

theorem CC.CVar.weaken_subst_comm_liftMany {s1 K s2 : Sig} {k0 : Kind} {C : BVar (s1 ++ K) Kind.cvar} {σ : Subst s1 s2} : ((σ.liftMany K).cvar C).rename (Rename.succ.liftMany K) = (σ.lift.liftMany K).cvar ((Rename.succ.liftMany K).var C)

theorem CC.CaptureSet.weaken_subst_comm_liftMany {s1 K s2 : Sig} {k0 : Kind} {cs : CaptureSet (s1 ++ K)} {σ : Subst s1 s2} : (cs.subst (σ.liftMany K)).rename (Rename.succ.liftMany K) = (cs.rename (Rename.succ.liftMany K)).subst (σ.lift.liftMany K)

theorem CC.CaptureBound.weaken_subst_comm_liftMany {s1 K s2 : Sig} {k0 : Kind} {cb : CaptureBound (s1 ++ K)} {σ : Subst s1 s2} : (cb.subst (σ.liftMany K)).rename (Rename.succ.liftMany K) = (cb.rename (Rename.succ.liftMany K)).subst (σ.lift.liftMany K)

@[irreducible]

theorem CC.Ty.weaken_subst_comm {sort : TySort} {s1 K s2 : Sig} {k0 : Kind} {T : Ty sort (s1 ++ K)} {σ : Subst s1 s2} : (T.subst (σ.liftMany K)).rename (Rename.succ.liftMany K) = (T.rename (Rename.succ.liftMany K)).subst (σ.lift.liftMany K)

theorem CC.Ty.weaken_subst_comm_base {sort : TySort} {s1 s2 : Sig} {k : Kind} {T : Ty sort s1} {σ : Subst s1 s2} : (T.subst σ).rename Rename.succ = (T.rename Rename.succ).subst σ.lift

theorem CC.Var.weaken_subst_comm_base {s1 s2 : Sig} {k : Kind} {x : Var Kind.var s1} {σ : Subst s1 s2} : (x.subst σ).rename Rename.succ = (x.rename Rename.succ).subst σ.lift

theorem CC.CVar.weaken_subst_comm_base {s1 s2 : Sig} {k : Kind} {C : BVar s1 Kind.cvar} {σ : Subst s1 s2} : (σ.cvar C).rename Rename.succ = σ.lift.cvar (Rename.succ.var C)

theorem CC.CaptureSet.weaken_subst_comm_base {s1 s2 : Sig} {k : Kind} {cs : CaptureSet s1} {σ : Subst s1 s2} : (cs.subst σ).rename Rename.succ = (cs.rename Rename.succ).subst σ.lift

theorem CC.Subst.comp_lift {s1 s2 s3 : Sig} {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} {k : Kind} : σ1.lift.comp σ2.lift = (σ1.comp σ2).lift

Composition of substitutions commutes with lifting.

theorem CC.Subst.comp_liftMany {s1 s2 s3 : Sig} {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} {K : Sig} : (σ1.liftMany K).comp (σ2.liftMany K) = (σ1.comp σ2).liftMany K

Composition of substitutions commutes with lifting many levels.

theorem CC.Var.subst_comp {s1 s2 s3 : Sig} {x : Var Kind.var s1} {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : (x.subst σ1).subst σ2 = x.subst (σ1.comp σ2)

Substituting a composition of substitutions is the same as substituting one after the other.

theorem CC.CaptureSet.subst_comp {s1 s2 s3 : Sig} {cs : CaptureSet s1} {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : (cs.subst σ1).subst σ2 = cs.subst (σ1.comp σ2)

Substitution on capture sets distributes over composition of substitutions.

theorem CC.CaptureBound.subst_comp {s1 s2 s3 : Sig} {cb : CaptureBound s1} {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : (cb.subst σ1).subst σ2 = cb.subst (σ1.comp σ2)

Substitution on capture bounds distributes over composition of substitutions.

theorem CC.Ty.subst_comp {sort : TySort} {s1 s2 s3 : Sig} {T : Ty sort s1} {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : (T.subst σ1).subst σ2 = T.subst (σ1.comp σ2)

Substitution on types distributes over composition of substitutions.

theorem CC.Exp.subst_comp {s1 s2 s3 : Sig} {e : Exp s1} {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} : (e.subst σ1).subst σ2 = e.subst (σ1.comp σ2)

Substitution on terms distributes over composition of substitutions.

theorem CC.Var.subst_id {s : Sig} {x : Var Kind.var s} : x.subst Subst.id = x

Substituting with the identity substitution leaves a variable unchanged.

theorem CC.CaptureSet.subst_id {s : Sig} {cs : CaptureSet s} : cs.subst Subst.id = cs

Substituting with the identity substitution leaves a capture set unchanged.

theorem CC.CaptureBound.subst_id {s : Sig} {cb : CaptureBound s} : cb.subst Subst.id = cb

Substituting with the identity substitution leaves a capture bound unchanged.

theorem CC.Subst.lift_id {s : Sig} {k : Kind} : id.lift = id

Lifting the identity substitution yields the identity.

theorem CC.Ty.subst_id {sort : TySort} {s : Sig} {T : Ty sort s} : T.subst Subst.id = T

Substituting with the identity substitution leaves a type unchanged.

theorem CC.Exp.subst_id {s : Sig} {e : Exp s} : e.subst Subst.id = e

Substituting with the identity substitution leaves an expression unchanged.

def CC.Rename.asSubst {s1 s2 : Sig} (f : Rename s1 s2) : Subst s1 s2

Converts a renaming to a substitution.

Equations

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

theorem CC.Rename.asSubst_lift {s1 s2 : Sig} {k : Kind} {f : Rename s1 s2} : f.lift.asSubst = f.asSubst.lift

Lifting a renaming and then converting to a substitution is the same as converting to a substitution and then lifting the substitution.

theorem CC.Var.subst_asSubst {s1 s2 : Sig} {x : Var Kind.var s1} {f : Rename s1 s2} : x.subst f.asSubst = x.rename f

Substituting a substitution lifted from a renaming is the same as renaming.

theorem CC.CaptureSet.subst_asSubst {s1 s2 : Sig} {cs : CaptureSet s1} {f : Rename s1 s2} : cs.subst f.asSubst = cs.rename f

Substituting a substitution lifted from a renaming is the same as renaming.

theorem CC.CaptureBound.subst_asSubst {s1 s2 : Sig} {cb : CaptureBound s1} {f : Rename s1 s2} : cb.subst f.asSubst = cb.rename f

Substituting a substitution lifted from a renaming is the same as renaming.

theorem CC.Ty.subst_asSubst {sort : TySort} {s1 s2 : Sig} {T : Ty sort s1} {f : Rename s1 s2} : T.subst f.asSubst = T.rename f

Substituting a substitution lifted from a renaming is the same as renaming.

theorem CC.Exp.subst_asSubst {s1 s2 : Sig} {e : Exp s1} {f : Rename s1 s2} : e.subst f.asSubst = e.rename f

Substituting a substitution lifted from a renaming is the same as renaming.

theorem CC.Subst.weaken_openVar {s : Sig} {z : Var Kind.var s} : Rename.succ.asSubst.comp (openVar z) = id

theorem CC.Subst.weaken_openTVar {s : Sig} {U : Ty TySort.shape s} : Rename.succ.asSubst.comp (openTVar U) = id

theorem CC.Subst.weaken_openCVar {s : Sig} {C : CaptureSet s} : Rename.succ.asSubst.comp (openCVar C) = id

theorem CC.CaptureSet.weaken_openVar {s : Sig} {C : CaptureSet s} {z : Var Kind.var s} : (C.rename Rename.succ).subst (Subst.openVar z) = C

theorem CC.CaptureSet.weaken_openTVar {s : Sig} {C : CaptureSet s} {U : Ty TySort.shape s} : (C.rename Rename.succ).subst (Subst.openTVar U) = C

theorem CC.CaptureSet.weaken_openCVar {s : Sig} {C C' : CaptureSet s} : (C.rename Rename.succ).subst (Subst.openCVar C') = C

theorem CC.CaptureSet.ground_rename_invariant {f : Rename ∅ ∅} {C : CaptureSet ∅} : C.rename f = C

theorem CC.CaptureSet.ground_subst_invariant {σ : Subst ∅ ∅} {C : CaptureSet ∅} : C.subst σ = C

structure CC.Subst.IsClosed {s1 s2 : Sig} (σ : Subst s1 s2) : Prop

A substitution is closed if all its images are closed.

• var_closed (x : BVar s1 Kind.var) : (σ.var x).IsClosed
• tvar_closed (X : BVar s1 Kind.tvar) : (σ.tvar X).IsClosed
• cvar_closed (C : BVar s1 Kind.cvar) : (σ.cvar C).IsClosed

def CC.Var.is_closed_subst {s1 s2 : Sig} {x : Var Kind.var s1} {σ : Subst s1 s2} (hc : x.IsClosed) (hsubst : σ.IsClosed) : (x.subst σ).IsClosed

Substitution preserves closedness for variables.

Equations

• ⋯ = ⋯

def CC.CaptureSet.is_closed_subst {s1 s2 : Sig} {cs : CaptureSet s1} {σ : Subst s1 s2} (hc : cs.IsClosed) (hsubst : σ.IsClosed) : (cs.subst σ).IsClosed

Substitution preserves closedness for capture sets.

Equations

• ⋯ = ⋯

def CC.CaptureBound.is_closed_subst {s1 s2 : Sig} {cb : CaptureBound s1} {σ : Subst s1 s2} (hc : cb.IsClosed) (hsubst : σ.IsClosed) : (cb.subst σ).IsClosed

Substitution preserves closedness for capture bounds.

Equations

• ⋯ = ⋯

theorem CC.Subst.lift_closed {s1 s2 : Sig} {k : Kind} {σ : Subst s1 s2} (hσ : σ.IsClosed) : σ.lift.IsClosed

Lifting preserves closedness of substitutions.

def CC.Ty.is_closed_subst {sort : TySort} {s1 s2 : Sig} {T : Ty sort s1} {σ : Subst s1 s2} (hc : T.IsClosed) (hsubst : σ.IsClosed) : (T.subst σ).IsClosed

Substitution preserves closedness for types.

Equations

• ⋯ = ⋯

def CC.Exp.is_closed_subst {s1 s2 : Sig} {e : Exp s1} {σ : Subst s1 s2} (hc : e.IsClosed) (hsubst : σ.IsClosed) : (e.subst σ).IsClosed

Substitution preserves closedness for expressions.

Equations

• ⋯ = ⋯

theorem CC.Subst.openVar_is_closed {s : Sig} {z : Var Kind.var s} (hz : z.IsClosed) : (openVar z).IsClosed

The openVar substitution is closed if the variable is closed.

theorem CC.Subst.openTVar_is_closed {s : Sig} {U : Ty TySort.shape s} (hU : U.IsClosed) : (openTVar U).IsClosed

The openTVar substitution is closed if the type is closed.

theorem CC.Subst.openCVar_is_closed {s : Sig} {C : CaptureSet s} (hC : C.IsClosed) : (openCVar C).IsClosed

The openCVar substitution is closed if the capture set is closed.

theorem CC.Var.subst_closed_inv {s1 s2 : Sig} {x : Var Kind.var s1} {σ : Subst s1 s2} (hclosed : (x.subst σ).IsClosed) : x.IsClosed

If the result of substitution is closed, the original variable was closed.

theorem CC.CaptureSet.subst_closed_inv {s1 s2 : Sig} {cs : CaptureSet s1} {σ : Subst s1 s2} (hclosed : (cs.subst σ).IsClosed) : cs.IsClosed

If the result of substitution is closed, the original capture set was closed.

theorem CC.CaptureBound.subst_closed_inv {s1 s2 : Sig} {cb : CaptureBound s1} {σ : Subst s1 s2} (hclosed : (cb.subst σ).IsClosed) : cb.IsClosed

If the result of substitution is closed, the original capture bound was closed.

theorem CC.Ty.subst_closed_inv {sort : TySort} {s1 s2 : Sig} {T : Ty sort s1} {σ : Subst s1 s2} (hclosed : (T.subst σ).IsClosed) : T.IsClosed

If the result of substitution is closed, the original type was closed.

theorem CC.Exp.subst_closed_inv {s1 s2 : Sig} {e : Exp s1} {σ : Subst s1 s2} (hclosed : (e.subst σ).IsClosed) : e.IsClosed

If the result of substitution is closed, the original expression was closed.