Variable environments for first-order logic.

Since Fin.cons is absent from Lean 4 core, we define our own environment machinery for mapping de Bruijn variables to universe elements.

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Env (card n : Nat) : Type

An environment maps n de Bruijn variables to elements of Fin card.

Equations

• Complexity.DescriptiveComplexity.Env card n = (Fin n → Fin card)

def Complexity.DescriptiveComplexity.envCons {card n : Nat} (a : Fin card) (σ : Env card n) : Env card (n + 1)

Extend an environment with a new element at index 0.

Equations

• Complexity.DescriptiveComplexity.envCons a σ i = if h : ↑i = 0 then a else σ ⟨↑i - 1, ⋯⟩

def Complexity.DescriptiveComplexity.emptyEnv (card : Nat) : Env card 0

The empty environment (no free variables).

Equations

• Complexity.DescriptiveComplexity.emptyEnv card = Fin.elim0

theorem Complexity.DescriptiveComplexity.envCons_zero {card n : Nat} (a : Fin card) (σ : Env card n) : envCons a σ ⟨0, ⋯⟩ = a

theorem Complexity.DescriptiveComplexity.envCons_succ {card n : Nat} (a : Fin card) (σ : Env card n) (i : Fin n) : envCons a σ ⟨↑i + 1, ⋯⟩ = σ i

theorem Complexity.DescriptiveComplexity.envCons_comp {m k n : Nat} (f : Fin m → Fin k) (a : Fin m) (σ : Env m n) : f ∘ envCons a σ = envCons (f a) (f ∘ σ)

theorem Complexity.DescriptiveComplexity.emptyEnv_comp {m k : Nat} (f : Fin m → Fin k) : f ∘ emptyEnv m = emptyEnv k