Flypitch.Compat.Core collects small compatibility definitions that emulate the dependent-vector utilities used by the original development. They provide the lightweight data structures and arity helpers that the first-order syntax layer builds on.

theorem Flypitch.Function.Injective.ne_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Injective f) {a₁ a₂ : α} : f a₁ ≠ f a₂ ↔ a₁ ≠ a₂

inductive Flypitch.dvector (α : Type u) : ℕ → Type u

• nil {α : Type u} : dvector α 0
• cons {α : Type u} {n : ℕ} : α → dvector α n → dvector α (n + 1)

inductive Flypitch.dfin : ℕ → Type

• fz {n : ℕ} : dfin (n + 1)
• fs {n : ℕ} : dfin n → dfin (n + 1)

@[implicit_reducible]

instance Flypitch.instOfNatDfinHAddNatOfNat {n : ℕ} : OfNat (dfin (n + 1)) 0

Equations

• Flypitch.instOfNatDfinHAddNatOfNat = { ofNat := Flypitch.dfin.fz }

theorem Flypitch.dvector.zero_eq {α : Type u} (xs : dvector α 0) : xs = nil

def Flypitch.dvector.concat {α : Type u} {n : ℕ} : dvector α n → α → dvector α (n + 1)

Equations

• Flypitch.dvector.nil.concat x✝ = Flypitch.dvector.cons x✝ Flypitch.dvector.nil
• (Flypitch.dvector.cons y ys).concat x✝ = Flypitch.dvector.cons y (ys.concat x✝)

def Flypitch.dvector.nth {α : Type u} {n : ℕ} (xs : dvector α n) (m : ℕ) : m < n → α

Equations

• Flypitch.dvector.nil.nth x✝¹ x✝ = ⋯.elim
• (Flypitch.dvector.cons x_4 a).nth 0 x_5 = x_4
• (Flypitch.dvector.cons a xs).nth m.succ h = xs.nth m ⋯

@[simp]

theorem Flypitch.dvector.nth_cons {α : Type u} {n : ℕ} (x : α) (xs : dvector α n) (m : ℕ) (h : m < n) : (cons x xs).nth (m + 1) ⋯ = xs.nth m h

@[reducible]

def Flypitch.dvector.last {α : Type u} {n : ℕ} (xs : dvector α (n + 1)) : α

Equations

• xs.last = xs.nth n ⋯

def Flypitch.dvector.nth' {α : Type u} {n : ℕ} (xs : dvector α n) (m : Fin n) : α

Equations

• xs.nth' m = xs.nth ↑m ⋯

def Flypitch.dvector.nth'' {α : Type u} {n : ℕ} : dvector α n → dfin n → α

Equations

• (Flypitch.dvector.cons x_3 a).nth'' Flypitch.dfin.fz = x_3
• (Flypitch.dvector.cons a xs).nth'' m.fs = xs.nth'' m

def Flypitch.dvector.mem {α : Type u} (x : α) {n : ℕ} : dvector α n → Prop

Equations

• Flypitch.dvector.mem x Flypitch.dvector.nil = False
• Flypitch.dvector.mem x (Flypitch.dvector.cons y ys) = (x = y ∨ Flypitch.dvector.mem x ys)

@[implicit_reducible]

instance Flypitch.dvector.instMembership {α : Type u} {n : ℕ} : Membership α (dvector α n)

Equations

• Flypitch.dvector.instMembership = { mem := fun (xs : Flypitch.dvector α n) (x : α) => Flypitch.dvector.mem x xs }

def Flypitch.dvector.pmem {α : Type u} (x : α) {n : ℕ} : dvector α n → Type

Equations

• Flypitch.dvector.pmem x Flypitch.dvector.nil = Empty
• Flypitch.dvector.pmem x (Flypitch.dvector.cons y ys) = (x = y ⊕' Flypitch.dvector.pmem x ys)

theorem Flypitch.dvector.mem_of_pmem {α : Type u} {x : α} {n : ℕ} {xs : dvector α n} : ∀ (a : pmem x xs), x ∈ xs

def Flypitch.dvector.map {α : Type u} {β : Type v} (f : α → β) {n : ℕ} : dvector α n → dvector β n

Equations

• Flypitch.dvector.map f Flypitch.dvector.nil = Flypitch.dvector.nil
• Flypitch.dvector.map f (Flypitch.dvector.cons y ys) = Flypitch.dvector.cons (f y) (Flypitch.dvector.map f ys)

theorem Flypitch.dvector.map_congr_pmem {α : Type u} {β : Type v} {f g : α → β} {n : ℕ} {xs : dvector α n} (h : ∀ (x : α) (a : pmem x xs), f x = g x) : map f xs = map g xs

theorem Flypitch.dvector.map_congr_mem {α : Type u} {β : Type v} {f g : α → β} {n : ℕ} {xs : dvector α n} (h : ∀ (x : α), x ∈ xs → f x = g x) : map f xs = map g xs

@[simp]

theorem Flypitch.dvector.map_id {α : Type u} {n : ℕ} (xs : dvector α n) : map (fun (x : α) => x) xs = xs

@[simp]

theorem Flypitch.dvector.map_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) {n : ℕ} (xs : dvector α n) : map g (map f xs) = map (fun (x : α) => g (f x)) xs

@[simp]

theorem Flypitch.dvector.map_nth {α : Type u} {β : Type v} (f : α → β) {n : ℕ} (xs : dvector α n) (m : ℕ) (h : m < n) : (map f xs).nth m h = f (xs.nth m h)

def Flypitch.arity' (α β : Type u) : ℕ → Type u

The type α → (α → ... (α → β)...) with n copies of α.

Equations

• Flypitch.arity' α β 0 = β
• Flypitch.arity' α β n.succ = (α → Flypitch.arity' α β n)

def Flypitch.arity'.constant {α β : Type u} {n : ℕ} : β → arity' α β n

Equations

• Flypitch.arity'.constant x✝ = x✝
• Flypitch.arity'.constant x✝ = fun (x : α) => Flypitch.arity'.constant x✝

def Flypitch.arity'.ofDVectorMap {α β : Type u} {l : ℕ} : (dvector α l → β) → arity' α β l

Equations

• Flypitch.arity'.ofDVectorMap f = f Flypitch.dvector.nil
• Flypitch.arity'.ofDVectorMap f = fun (x : α) => Flypitch.arity'.ofDVectorMap fun (xs : Flypitch.dvector α n) => f (Flypitch.dvector.cons x xs)

def Flypitch.arity'.app {α β : Type u} {l : ℕ} : arity' α β l → dvector α l → β

Equations

• b.app Flypitch.dvector.nil = b
• f.app (Flypitch.dvector.cons x_3 xs) = (f x_3).app xs

@[simp]

theorem Flypitch.arity'.app_zero {α β : Type u} (f : arity' α β 0) (xs : dvector α 0) : f.app xs = f

def Flypitch.arity'.postcompose {α β γ : Type u} (g : β → γ) {n : ℕ} : arity' α β n → arity' α γ n

Equations

• Flypitch.arity'.postcompose g b = g b
• Flypitch.arity'.postcompose g f = fun (x : α) => Flypitch.arity'.postcompose g (f x)

def Flypitch.arity'.precompose {α β γ : Type u} {n : ℕ} : arity' β γ n → (α → β) → arity' α γ n

Equations

• g.precompose x✝ = g
• g.precompose x✝ = fun (x : α) => (g (x✝ x)).precompose x✝