De Bruijn indices and variable renamings for CC.

inductive CC.Kind : Type

Kind of a variable.

• var : Kind

  Term variable

• tvar : Kind

  Type variable

• cvar : Kind

  Capture variable

@[reducible]

def CC.Sig : Type

A Sig describes the shape of a context, which is a list of variable kinds.

Equations

• CC.Sig = List CC.Kind

instance CC.Sig.instEmptyCollection : EmptyCollection Sig

Equations

• CC.Sig.instEmptyCollection = { emptyCollection := [] }

def CC.Sig.extend_var : Sig → Sig

Extends a signature with a term variable.

Equations

• s,x = CC.Kind.var :: s

def CC.Sig.extend_tvar : Sig → Sig

Extends a signature with a type variable.

Equations

• s,X = CC.Kind.tvar :: s

def CC.Sig.extend_cvar : Sig → Sig

Extends a signature with a capture variable.

Equations

• s,C = CC.Kind.cvar :: s

def CC.Sig.extend : Sig → Kind → Sig

Extends a signature with a variable of the given kind.

Equations

• s,,k = k :: s

def CC.Sig.extendMany : Sig → Sig → Sig

Extends a signature with multiple variables.

Equations

• x✝.extendMany [] = x✝
• x✝.extendMany (k :: K) = x✝.extendMany K,,k

def CC.«term_,x» : Lean.TrailingParserDescr

Equations

• CC.«term_,x» = Lean.ParserDescr.trailingNode `CC.«term_,x» 80 80 (Lean.ParserDescr.symbol ",x")

def CC.«term_,X» : Lean.TrailingParserDescr

Equations

• CC.«term_,X» = Lean.ParserDescr.trailingNode `CC.«term_,X» 80 80 (Lean.ParserDescr.symbol ",X")

def CC.«term_,C» : Lean.TrailingParserDescr

Equations

• CC.«term_,C» = Lean.ParserDescr.trailingNode `CC.«term_,C» 80 80 (Lean.ParserDescr.symbol ",C")

def CC.«term_,,_» : Lean.TrailingParserDescr

Equations

• CC.«term_,,_» = Lean.ParserDescr.trailingNode `CC.«term_,,_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol ",,") (Lean.ParserDescr.cat `term 66))

instance CC.Sig.instAppend : Append Sig

Equations

• CC.Sig.instAppend = { append := CC.Sig.extendMany }

inductive CC.BVar : Sig → Kind → Type

A bound variable, de Bruijn indexed.

• here {s : Sig} {k : Kind} : BVar (s,,k) k
• there {s : Sig} {k k0 : Kind} : BVar s k → BVar (s,,k0) k

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

A Rename maps bound variables in one context to another.

• var {k : Kind} : BVar s1 k → BVar s2 k

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

The identity Rename.

Equations

• CC.Rename.id = { var := fun {k : CC.Kind} (x : CC.BVar s k) => x }

def CC.Rename.comp {s1 s2 s3 : Sig} (f1 : Rename s1 s2) (f2 : Rename s2 s3) : Rename s1 s3

Composition of two renamings.

Equations

• f1.comp f2 = { var := fun {k : CC.Kind} (x : CC.BVar s1 k) => f2.var (f1.var x) }

def CC.Rename.lift {s1 s2 : Sig} {k : Kind} (f : Rename s1 s2) : Rename (s1,,k) (s2,,k)

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

Equations

• f.lift = { var := fun {k_1 : CC.Kind} (x : CC.BVar (s1,,k) k_1) => match k_1, x with | .(k), CC.BVar.here => CC.BVar.here | x, x_1.there => (f.var x_1).there }

def CC.Rename.liftMany {s1 s2 : Sig} (f : Rename s1 s2) (K : Sig) : Rename (s1 ++ K) (s2 ++ K)

Lifts a renaming under multiple binders.

Equations

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

def CC.Rename.succ {s : Sig} {k : Kind} : Rename s (s,,k)

The "successor" renaming that weakens all variables by one level.

Equations

• CC.Rename.succ = { var := fun {k_1 : CC.Kind} (x : CC.BVar s k_1) => x.there }

theorem CC.Rename.funext {s1 s2 : Sig} {f1 f2 : Rename s1 s2} (hvar : ∀ {k : Kind} (x : BVar s1 k), f1.var x = f2.var x) : f1 = f2

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

theorem CC.Rename.succ_lift_comm {s1 s2 : Sig} {k0 : Kind} {f : Rename s1 s2} : succ.comp f.lift = f.comp succ

The successor renaming commutes with lifting.

theorem CC.Rename.lift_id {s : Sig} {k0 : Kind} : id.lift = id

Lifting the identity renaming yields the identity.

theorem CC.Rename.lift_comp {s1 s2 s3 : Sig} {k0 : Kind} {f1 : Rename s1 s2} {f2 : Rename s2 s3} : (f1.comp f2).lift = f1.lift.comp f2.lift

Lifting distributes over composition of renamings.