The primitive recursive functions

The primitive recursive functions are the least collection of functions ℕ → ℕ which are closed under projections (using the pair pairing function), composition, zero, successor, and primitive recursion (i.e. Nat.rec where the motive is C n := ℕ).

We can extend this definition to a large class of basic types by using canonical encodings of types as natural numbers (Gödel numbering), which we implement through the type class Encodable. (More precisely, we need that the composition of encode with decode yields a primitive recursive function, so we have the Primcodable type class for this.)

In the above, the pairing function is primitive recursive by definition. This deviates from the textbook definition of primitive recursive functions, which instead work with n-ary functions. We formalize the textbook definition in Nat.Primrec'. Nat.Primrec'.prim_iff then proves it is equivalent to our chosen formulation. For more discussion of this and other design choices in this formalization, see [Car19].

Main definitions

• Nat.Primrec f: f is primitive recursive, for functions f : ℕ → ℕ
• Primrec f: f is primitive recursive, for functions between Primcodable types
• Primcodable α: well-behaved encoding of α into ℕ, i.e. one such that roundtripping through the encoding functions adds no computational power

References

• Mario Carneiro, Formalizing computability theory via partial recursive functions

@[reducible]

def Nat.unpaired {α : Sort u_1} (f : ℕ → ℕ → α) (n : ℕ) : α

Calls the given function on a pair of entries n, encoded via the pairing function.

Equations

• Nat.unpaired f n = f (Nat.unpair n).1 (Nat.unpair n).2

inductive Nat.Primrec : (ℕ → ℕ) → Prop

The primitive recursive functions ℕ → ℕ.

• zero : Nat.Primrec fun (x : ℕ) => 0
• succ : Nat.Primrec succ
• left : Nat.Primrec fun (n : ℕ) => (unpair n).1
• right : Nat.Primrec fun (n : ℕ) => (unpair n).2
• pair {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun (n : ℕ) => Nat.pair (f n) (g n)
• comp {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun (n : ℕ) => f (g n)
• prec {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec (unpaired fun (z n : ℕ) => Nat.rec (f z) (fun (y IH : ℕ) => g (Nat.pair z (Nat.pair y IH))) n)

theorem Nat.Primrec.of_eq {f g : ℕ → ℕ} (hf : Nat.Primrec f) (H : ∀ (n : ℕ), f n = g n) : Nat.Primrec g

theorem Nat.Primrec.const (n : ℕ) : Nat.Primrec fun (x : ℕ) => n

theorem Nat.Primrec.id : Nat.Primrec id

theorem Nat.Primrec.prec1 {f : ℕ → ℕ} (m : ℕ) (hf : Nat.Primrec f) : Nat.Primrec fun (n : ℕ) => Nat.rec m (fun (y IH : ℕ) => f (Nat.pair y IH)) n

theorem Nat.Primrec.casesOn1 {f : ℕ → ℕ} (m : ℕ) (hf : Nat.Primrec f) : Nat.Primrec fun (x : ℕ) => Nat.casesOn x m f

theorem Nat.Primrec.casesOn' {f g : ℕ → ℕ} (hf : Nat.Primrec f) (hg : Nat.Primrec g) : Nat.Primrec (unpaired fun (z n : ℕ) => Nat.casesOn n (f z) fun (y : ℕ) => g (Nat.pair z y))

theorem Nat.Primrec.swap : Nat.Primrec (unpaired (Function.swap Nat.pair))

theorem Nat.Primrec.swap' {f : ℕ → ℕ → ℕ} (hf : Nat.Primrec (unpaired f)) : Nat.Primrec (unpaired (Function.swap f))

theorem Nat.Primrec.pred : Nat.Primrec Nat.pred

theorem Nat.Primrec.add : Nat.Primrec (unpaired fun (x1 x2 : ℕ) => x1 + x2)

theorem Nat.Primrec.sub : Nat.Primrec (unpaired fun (x1 x2 : ℕ) => x1 - x2)

theorem Nat.Primrec.mul : Nat.Primrec (unpaired fun (x1 x2 : ℕ) => x1 * x2)

theorem Nat.Primrec.pow : Nat.Primrec (unpaired fun (x1 x2 : ℕ) => x1 ^ x2)

class Primcodable (α : Type u_1) extends Encodable α : Type u_1

A Primcodable type is, essentially, an Encodable type for which the encode/decode functions are primitive recursive. However, such a definition is circular.

Instead, we ask that the composition of decode : ℕ → Option α with encode : Option α → ℕ is primitive recursive. Said composition is the identity function, restricted to the image of encode. Thus, in a way, the added requirement ensures that no predicates can be smuggled in through a cunning choice of the subset of ℕ into which the type is encoded.

• encode : α → ℕ
• decode : ℕ → Option α
• encodek (a : α) : decode (encode a) = some a
• prim : Nat.Primrec fun (n : ℕ) => Encodable.encode (Encodable.decode n)

@[instance 10]

instance Primcodable.ofDenumerable (α : Type u_1) [Denumerable α] : Primcodable α

Equations

• Primcodable.ofDenumerable α = { toEncodable := inst✝.toEncodable, prim := ⋯ }

def Primcodable.ofEquiv (α : Type u_1) {β : Type u_2} [Primcodable α] (e : β ≃ α) : Primcodable β

Builds a Primcodable instance from an equivalence to a Primcodable type.

Equations

• Primcodable.ofEquiv α e = { toEncodable := Encodable.ofEquiv α e, prim := ⋯ }

instance Primcodable.empty : Primcodable Empty

Equations

• Primcodable.empty = { toEncodable := IsEmpty.toEncodable, prim := Nat.Primrec.zero }

instance Primcodable.unit : Primcodable PUnit.{u_1 + 1}

Equations

• Primcodable.unit = { toEncodable := PUnit.encodable, prim := Primcodable.unit._proof_1 }

instance Primcodable.option {α : Type u_1} [h : Primcodable α] : Primcodable (Option α)

Equations

• Primcodable.option = { toEncodable := Option.encodable, prim := ⋯ }

instance Primcodable.bool : Primcodable Bool

Equations

• Primcodable.bool = { toEncodable := Bool.encodable, prim := Primcodable.bool._proof_1 }

def Primrec {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (f : α → β) : Prop

Primrec f means f is primitive recursive (after encoding its input and output as natural numbers).

Equations

• Primrec f = Nat.Primrec fun (n : ℕ) => Encodable.encode (Option.map f (Encodable.decode n))

theorem Primrec.encode {α : Type u_1} [Primcodable α] : Primrec Encodable.encode

theorem Primrec.decode {α : Type u_1} [Primcodable α] : Primrec Encodable.decode

theorem Primrec.dom_denumerable {α : Type u_4} {β : Type u_5} [Denumerable α] [Primcodable β] {f : α → β} : Primrec f ↔ Nat.Primrec fun (n : ℕ) => Encodable.encode (f (Denumerable.ofNat α n))

theorem Primrec.nat_iff {f : ℕ → ℕ} : Primrec f ↔ Nat.Primrec f

theorem Primrec.encdec {α : Type u_1} [Primcodable α] : Primrec fun (n : ℕ) => Encodable.encode (Encodable.decode n)

theorem Primrec.option_some {α : Type u_1} [Primcodable α] : Primrec some

theorem Primrec.of_eq {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f g : α → σ} (hf : Primrec f) (H : ∀ (n : α), f n = g n) : Primrec g

theorem Primrec.const {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] (x : σ) : Primrec fun (x_1 : α) => x

theorem Primrec.id {α : Type u_1} [Primcodable α] : Primrec id

theorem Primrec.comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : β → σ} {g : α → β} (hf : Primrec f) (hg : Primrec g) : Primrec fun (a : α) => f (g a)

theorem Primrec.succ : Primrec Nat.succ

theorem Primrec.pred : Primrec Nat.pred

theorem Primrec.encode_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : α → σ} : (Primrec fun (a : α) => Encodable.encode (f a)) ↔ Primrec f

theorem Primrec.ofNat_iff {α : Type u_4} {β : Type u_5} [Denumerable α] [Primcodable β] {f : α → β} : Primrec f ↔ Primrec fun (n : ℕ) => f (Denumerable.ofNat α n)

theorem Primrec.ofNat (α : Type u_4) [Denumerable α] : Primrec (Denumerable.ofNat α)

theorem Primrec.option_some_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : α → σ} : (Primrec fun (a : α) => some (f a)) ↔ Primrec f

theorem Primrec.of_equiv {α : Type u_1} [Primcodable α] {β : Type u_4} {e : β ≃ α} : Primrec ⇑e

theorem Primrec.of_equiv_symm {α : Type u_1} [Primcodable α] {β : Type u_4} {e : β ≃ α} : Primrec ⇑e.symm

theorem Primrec.of_equiv_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {β : Type u_4} (e : β ≃ α) {f : σ → β} : (Primrec fun (a : σ) => e (f a)) ↔ Primrec f

theorem Primrec.of_equiv_symm_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {β : Type u_4} (e : β ≃ α) {f : σ → α} : (Primrec fun (a : σ) => e.symm (f a)) ↔ Primrec f

instance Primcodable.prod {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Primcodable (α × β)

Equations

• Primcodable.prod = { toEncodable := Encodable.Prod.encodable, prim := ⋯ }

theorem Primrec.fst {α : Type u_2} {β : Type u_3} [Primcodable α] [Primcodable β] : Primrec Prod.fst

theorem Primrec.snd {α : Type u_2} {β : Type u_3} [Primcodable α] [Primcodable β] : Primrec Prod.snd

theorem Primrec.pair {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] {f : α → β} {g : α → γ} (hf : Primrec f) (hg : Primrec g) : Primrec fun (a : α) => (f a, g a)

theorem Primrec.unpair : Primrec Nat.unpair

theorem Primrec.list_getElem?₁ {α : Type u_1} [Primcodable α] (l : List α) : Primrec fun (x : ℕ) => l[x]?

@[deprecated Primrec.list_getElem?₁ (since := "2025-02-14")]

theorem Primrec.list_get?₁ {α : Type u_1} [Primcodable α] (l : List α) : Primrec fun (x : ℕ) => l[x]?

Alias of Primrec.list_getElem?₁.

def Primrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (f : α → β → σ) : Prop

Primrec₂ f means f is a binary primitive recursive function. This is technically unnecessary since we can always curry all the arguments together, but there are enough natural two-arg functions that it is convenient to express this directly.

Equations

• Primrec₂ f = Primrec fun (p : α × β) => f p.1 p.2

def PrimrecPred {α : Type u_1} [Primcodable α] (p : α → Prop) : Prop

PrimrecPred p means p : α → Prop is a primitive recursive predicate, which is to say that decide ∘ p : α → Bool is primitive recursive.

Equations

• PrimrecPred p = ∃ (x : DecidablePred p), Primrec fun (a : α) => decide (p a)

def PrimrecRel {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (s : α → β → Prop) : Prop

PrimrecRel p means p : α → β → Prop is a primitive recursive relation, which is to say that decide ∘ p : α → β → Bool is primitive recursive.

Equations

• PrimrecRel s = PrimrecPred fun (p : α × β) => s p.1 p.2

theorem Primrec₂.mk {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (hf : Primrec fun (p : α × β) => f p.1 p.2) : Primrec₂ f

theorem Primrec₂.of_eq {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f g : α → β → σ} (hg : Primrec₂ f) (H : ∀ (a : α) (b : β), f a b = g a b) : Primrec₂ g

theorem Primrec₂.const {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (x : σ) : Primrec₂ fun (x_1 : α) (x_2 : β) => x

theorem Primrec₂.pair {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Primrec₂ Prod.mk

theorem Primrec₂.left {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Primrec₂ fun (a : α) (x : β) => a

theorem Primrec₂.right {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Primrec₂ fun (x : α) (b : β) => b

theorem Primrec₂.natPair : Primrec₂ Nat.pair

theorem Primrec₂.unpaired {α : Type u_1} [Primcodable α] {f : ℕ → ℕ → α} : Primrec (Nat.unpaired f) ↔ Primrec₂ f

theorem Primrec₂.unpaired' {f : ℕ → ℕ → ℕ} : Nat.Primrec (Nat.unpaired f) ↔ Primrec₂ f

theorem Primrec₂.encode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : (Primrec₂ fun (a : α) (b : β) => Encodable.encode (f a b)) ↔ Primrec₂ f

theorem Primrec₂.option_some_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : (Primrec₂ fun (a : α) (b : β) => some (f a b)) ↔ Primrec₂ f

theorem Primrec₂.ofNat_iff {α : Type u_4} {β : Type u_5} {σ : Type u_6} [Denumerable α] [Denumerable β] [Primcodable σ] {f : α → β → σ} : Primrec₂ f ↔ Primrec₂ fun (m n : ℕ) => f (Denumerable.ofNat α m) (Denumerable.ofNat β n)

theorem Primrec₂.uncurry {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : Primrec (Function.uncurry f) ↔ Primrec₂ f

theorem Primrec₂.curry {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × β → σ} : Primrec₂ (Function.curry f) ↔ Primrec f

theorem Primrec.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : γ → σ} {g : α → β → γ} (hf : Primrec f) (hg : Primrec₂ g) : Primrec₂ fun (a : α) (b : β) => f (g a b)

theorem Primrec₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : β → γ → σ} {g : α → β} {h : α → γ} (hf : Primrec₂ f) (hg : Primrec g) (hh : Primrec h) : Primrec fun (a : α) => f (g a) (h a)

theorem Primrec₂.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] [Primcodable σ] {f : γ → δ → σ} {g : α → β → γ} {h : α → β → δ} (hf : Primrec₂ f) (hg : Primrec₂ g) (hh : Primrec₂ h) : Primrec₂ fun (a : α) (b : β) => f (g a b) (h a b)

theorem PrimrecPred.decide {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] (hp : PrimrecPred p) : Primrec fun (a : α) => decide (p a)

theorem Primrec.primrecPred {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] (hp : Primrec fun (a : α) => decide (p a)) : PrimrecPred p

theorem primrecPred_iff_primrec_decide {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] : PrimrecPred p ↔ Primrec fun (a : α) => decide (p a)

theorem PrimrecPred.comp {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : β → Prop} {f : α → β} (hp : PrimrecPred p) (hf : Primrec f) : PrimrecPred fun (a : α) => p (f a)

theorem PrimrecRel.decide {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {R : α → β → Prop} [DecidableRel R] (hR : PrimrecRel R) : Primrec₂ fun (a : α) (b : β) => decide (R a b)

theorem Primrec₂.primrecRel {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {R : α → β → Prop} [DecidableRel R] (hp : Primrec₂ fun (a : α) (b : β) => decide (R a b)) : PrimrecRel R

theorem primrecRel_iff_primrec_decide {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {R : α → β → Prop} [DecidableRel R] : PrimrecRel R ↔ Primrec₂ fun (a : α) (b : β) => decide (R a b)

theorem PrimrecRel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {R : β → γ → Prop} {f : α → β} {g : α → γ} (hR : PrimrecRel R) (hf : Primrec f) (hg : Primrec g) : PrimrecPred fun (a : α) => R (f a) (g a)

theorem PrimrecRel.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] {R : γ → δ → Prop} {f : α → β → γ} {g : α → β → δ} : PrimrecRel R → Primrec₂ f → Primrec₂ g → PrimrecRel fun (a : α) (b : β) => R (f a b) (g a b)

theorem PrimrecPred.of_eq {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : PrimrecPred p) (H : ∀ (a : α), p a ↔ q a) : PrimrecPred q

theorem PrimrecRel.of_eq {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {r s : α → β → Prop} (hr : PrimrecRel r) (H : ∀ (a : α) (b : β), r a b ↔ s a b) : PrimrecRel s

theorem Primrec₂.swap {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (h : Primrec₂ f) : Primrec₂ (Function.swap f)

theorem PrimrecRel.swap {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {r : α → β → Prop} (h : PrimrecRel r) : PrimrecRel (Function.swap r)

theorem Primrec₂.nat_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : Primrec₂ f ↔ Nat.Primrec (Nat.unpaired fun (m n : ℕ) => Encodable.encode ((Encodable.decode m).bind fun (a : α) => Option.map (f a) (Encodable.decode n)))

theorem Primrec₂.nat_iff' {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : Primrec₂ f ↔ Primrec₂ fun (m n : ℕ) => (Encodable.decode m).bind fun (a : α) => Option.map (f a) (Encodable.decode n)

theorem Primrec.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × β → σ} (hf : Primrec f) : Primrec₂ fun (a : α) (b : β) => f (a, b)

theorem PrimrecPred.primrecRel {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α × β → Prop} (hp : PrimrecPred p) : PrimrecRel fun (a : α) (b : β) => p (a, b)

theorem Primrec.nat_rec {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → β} {g : α → ℕ × β → β} (hf : Primrec f) (hg : Primrec₂ g) : Primrec₂ fun (a : α) (n : ℕ) => Nat.rec (f a) (fun (n : ℕ) (IH : (fun (x : ℕ) => β) n) => g a (n, IH)) n

theorem Primrec.nat_rec' {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → ℕ} {g : α → β} {h : α → ℕ × β → β} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) : Primrec fun (a : α) => Nat.rec (g a) (fun (n : ℕ) (IH : (fun (x : ℕ) => β) n) => h a (n, IH)) (f a)

theorem Primrec.nat_rec₁ {α : Type u_1} [Primcodable α] {f : ℕ → α → α} (a : α) (hf : Primrec₂ f) : Primrec fun (t : ℕ) => Nat.rec a f t

theorem Primrec.nat_casesOn' {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → β} {g : α → ℕ → β} (hf : Primrec f) (hg : Primrec₂ g) : Primrec₂ fun (a : α) (n : ℕ) => Nat.casesOn n (f a) (g a)

theorem Primrec.nat_casesOn {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → ℕ} {g : α → β} {h : α → ℕ → β} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) : Primrec fun (a : α) => Nat.casesOn (f a) (g a) (h a)

theorem Primrec.nat_casesOn₁ {α : Type u_1} [Primcodable α] {f : ℕ → α} (a : α) (hf : Primrec f) : Primrec fun (n : ℕ) => Nat.casesOn n a f

theorem Primrec.nat_iterate {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → ℕ} {g : α → β} {h : α → β → β} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) : Primrec fun (a : α) => (h a)^[f a] (g a)

theorem Primrec.option_casesOn {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {o : α → Option β} {f : α → σ} {g : α → β → σ} (ho : Primrec o) (hf : Primrec f) (hg : Primrec₂ g) : Primrec fun (a : α) => Option.casesOn (o a) (f a) (g a)

theorem Primrec.option_bind {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → Option β} {g : α → β → Option σ} (hf : Primrec f) (hg : Primrec₂ g) : Primrec fun (a : α) => (f a).bind (g a)

theorem Primrec.option_bind₁ {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : α → Option σ} (hf : Primrec f) : Primrec fun (o : Option α) => o.bind f

theorem Primrec.option_map {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → Option β} {g : α → β → σ} (hf : Primrec f) (hg : Primrec₂ g) : Primrec fun (a : α) => Option.map (g a) (f a)

theorem Primrec.option_map₁ {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : α → σ} (hf : Primrec f) : Primrec (Option.map f)

theorem Primrec.option_iget {α : Type u_1} [Primcodable α] [Inhabited α] : Primrec Option.iget

theorem Primrec.option_isSome {α : Type u_1} [Primcodable α] : Primrec Option.isSome

theorem Primrec.option_getD {α : Type u_1} [Primcodable α] : Primrec₂ Option.getD

theorem Primrec.bind_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → Option σ} : (Primrec₂ fun (a : α) (n : ℕ) => (Encodable.decode n).bind (f a)) ↔ Primrec₂ f

theorem Primrec.map_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : (Primrec₂ fun (a : α) (n : ℕ) => Option.map (f a) (Encodable.decode n)) ↔ Primrec₂ f

theorem Primrec.nat_add : Primrec₂ fun (x1 x2 : ℕ) => x1 + x2

theorem Primrec.nat_sub : Primrec₂ fun (x1 x2 : ℕ) => x1 - x2

theorem Primrec.nat_mul : Primrec₂ fun (x1 x2 : ℕ) => x1 * x2

theorem Primrec.cond {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {c : α → Bool} {f g : α → σ} (hc : Primrec c) (hf : Primrec f) (hg : Primrec g) : Primrec fun (a : α) => bif c a then f a else g a

theorem Primrec.ite {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {c : α → Prop} [DecidablePred c] {f g : α → σ} (hc : PrimrecPred c) (hf : Primrec f) (hg : Primrec g) : Primrec fun (a : α) => if c a then f a else g a

theorem Primrec.nat_le : PrimrecRel fun (x1 x2 : ℕ) => x1 ≤ x2

theorem Primrec.nat_min : Primrec₂ min

theorem Primrec.nat_max : Primrec₂ max

theorem Primrec.dom_bool {α : Type u_1} [Primcodable α] (f : Bool → α) : Primrec f

theorem Primrec.dom_bool₂ {α : Type u_1} [Primcodable α] (f : Bool → Bool → α) : Primrec₂ f

theorem Primrec.not : Primrec not

theorem Primrec.and : Primrec₂ and

theorem Primrec.or : Primrec₂ or

theorem PrimrecPred.not {α : Type u_1} [Primcodable α] {p : α → Prop} (hp : PrimrecPred p) : PrimrecPred fun (a : α) => ¬p a

theorem PrimrecPred.and {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : PrimrecPred p) (hq : PrimrecPred q) : PrimrecPred fun (a : α) => p a ∧ q a

theorem PrimrecPred.or {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : PrimrecPred p) (hq : PrimrecPred q) : PrimrecPred fun (a : α) => p a ∨ q a

theorem Primrec.eq {α : Type u_1} [Primcodable α] : PrimrecRel Eq

theorem Primrec.beq {α : Type u_1} [Primcodable α] [DecidableEq α] : Primrec₂ BEq.beq

theorem Primrec.nat_lt : PrimrecRel fun (x1 x2 : ℕ) => x1 < x2

theorem Primrec.option_guard {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → β → Prop} [DecidableRel p] (hp : PrimrecRel p) {f : α → β} (hf : Primrec f) : Primrec fun (a : α) => Option.guard (fun (b : β) => decide (p a b)) (f a)

theorem Primrec.option_orElse {α : Type u_1} [Primcodable α] : Primrec₂ fun (x1 x2 : Option α) => x1 <|> x2

theorem Primrec.decode₂ {α : Type u_1} [Primcodable α] : Primrec (Encodable.decode₂ α)

theorem Primrec.list_findIdx₁ {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → β → Bool} (hp : Primrec₂ p) (l : List β) : Primrec fun (a : α) => List.findIdx (p a) l

theorem Primrec.list_idxOf₁ {α : Type u_1} [Primcodable α] [DecidableEq α] (l : List α) : Primrec fun (a : α) => List.idxOf a l

theorem Primrec.dom_finite {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] [Finite α] (f : α → σ) : Primrec f

@[deprecated Primrec.dom_finite (since := "2025-08-23")]

theorem Primrec.dom_fintype {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] [Finite α] (f : α → σ) : Primrec f

Alias of Primrec.dom_finite.

def Primrec.PrimrecBounded {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (f : α → β) : Prop

A function is PrimrecBounded if its size is bounded by a primitive recursive function

Equations

• Primrec.PrimrecBounded f = ∃ (g : α → ℕ), Primrec g ∧ ∀ (x : α), Encodable.encode (f x) ≤ g x

theorem Primrec.nat_findGreatest {α : Type u_1} [Primcodable α] {f : α → ℕ} {p : α → ℕ → Prop} [DecidableRel p] (hf : Primrec f) (hp : PrimrecRel p) : Primrec fun (x : α) => Nat.findGreatest (p x) (f x)

theorem Primrec.of_graph {α : Type u_1} [Primcodable α] {f : α → ℕ} (h₁ : PrimrecBounded f) (h₂ : PrimrecRel fun (a : α) (b : ℕ) => f a = b) : Primrec f

To show a function f : α → ℕ is primitive recursive, it is enough to show that the function is bounded by a primitive recursive function and that its graph is primitive recursive

theorem Primrec.nat_div : Primrec₂ fun (x1 x2 : ℕ) => x1 / x2

theorem Primrec.nat_mod : Primrec₂ fun (x1 x2 : ℕ) => x1 % x2

theorem Primrec.nat_bodd : Primrec Nat.bodd

theorem Primrec.nat_div2 : Primrec Nat.div2

theorem Primrec.nat_double : Primrec fun (n : ℕ) => 2 * n

theorem Primrec.nat_double_succ : Primrec fun (n : ℕ) => 2 * n + 1

instance Primcodable.sum {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Primcodable (α ⊕ β)

Equations

• Primcodable.sum = { toEncodable := Sum.encodable, prim := ⋯ }

instance Primcodable.list {α : Type u_1} [Primcodable α] : Primcodable (List α)

Equations

• Primcodable.list = { toEncodable := List.encodable, prim := ⋯ }

theorem Primrec.sumInl {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Primrec Sum.inl

theorem Primrec.sumInr {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Primrec Sum.inr

theorem Primrec.sumCasesOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ} (hf : Primrec f) (hg : Primrec₂ g) (hh : Primrec₂ h) : Primrec fun (a : α) => Sum.casesOn (f a) (g a) (h a)

theorem Primrec.list_cons {α : Type u_1} [Primcodable α] : Primrec₂ List.cons

theorem Primrec.list_casesOn {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → List β} {g : α → σ} {h : α → β × List β → σ} : Primrec f → Primrec g → Primrec₂ h → Primrec fun (a : α) => List.casesOn (f a) (g a) fun (b : β) (l : List β) => h a (b, l)

theorem Primrec.list_foldl {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → List β} {g : α → σ} {h : α → σ × β → σ} : Primrec f → Primrec g → Primrec₂ h → Primrec fun (a : α) => List.foldl (fun (s : σ) (b : β) => h a (s, b)) (g a) (f a)

theorem Primrec.list_reverse {α : Type u_1} [Primcodable α] : Primrec List.reverse

theorem Primrec.list_foldr {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → List β} {g : α → σ} {h : α → β × σ → σ} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) : Primrec fun (a : α) => List.foldr (fun (b : β) (s : σ) => h a (b, s)) (g a) (f a)

theorem Primrec.list_head? {α : Type u_1} [Primcodable α] : Primrec List.head?

theorem Primrec.list_headI {α : Type u_1} [Primcodable α] [Inhabited α] : Primrec List.headI

theorem Primrec.list_tail {α : Type u_1} [Primcodable α] : Primrec List.tail

theorem Primrec.list_rec {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → List β} {g : α → σ} {h : α → β × List β × σ → σ} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) : Primrec fun (a : α) => List.recOn (f a) (g a) fun (b : β) (l : List β) (IH : σ) => h a (b, l, IH)

theorem Primrec.list_getElem? {α : Type u_1} [Primcodable α] : Primrec₂ fun (x1 : List α) (x2 : ℕ) => x1[x2]?

@[deprecated Primrec.list_getElem? (since := "2025-02-14")]

theorem Primrec.list_get? {α : Type u_1} [Primcodable α] : Primrec₂ fun (x1 : List α) (x2 : ℕ) => x1[x2]?

Alias of Primrec.list_getElem?.

theorem Primrec.list_getD {α : Type u_1} [Primcodable α] (d : α) : Primrec₂ fun (l : List α) (n : ℕ) => l.getD n d

theorem Primrec.list_getI {α : Type u_1} [Primcodable α] [Inhabited α] : Primrec₂ List.getI

theorem Primrec.list_append {α : Type u_1} [Primcodable α] : Primrec₂ fun (x1 x2 : List α) => x1 ++ x2

theorem Primrec.list_concat {α : Type u_1} [Primcodable α] : Primrec₂ fun (l : List α) (a : α) => l ++ [a]

theorem Primrec.list_map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → List β} {g : α → β → σ} (hf : Primrec f) (hg : Primrec₂ g) : Primrec fun (a : α) => List.map (g a) (f a)

theorem Primrec.list_range : Primrec List.range

theorem Primrec.list_flatten {α : Type u_1} [Primcodable α] : Primrec List.flatten

theorem Primrec.list_flatMap {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → List β} {g : α → β → List σ} (hf : Primrec f) (hg : Primrec₂ g) : Primrec fun (a : α) => List.flatMap (g a) (f a)

theorem Primrec.optionToList {α : Type u_1} [Primcodable α] : Primrec Option.toList

theorem Primrec.listFilterMap {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → List β} {g : α → β → Option σ} (hf : Primrec f) (hg : Primrec₂ g) : Primrec fun (a : α) => List.filterMap (g a) (f a)

theorem Primrec.list_length {α : Type u_1} [Primcodable α] : Primrec List.length

theorem Primrec.listFilter {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] (hf : PrimrecPred p) : Primrec fun (L : List α) => List.filter (fun (x : α) => decide (p x)) L

Filtering a list for elements that satisfy a decidable predicate is primitive recursive.

theorem Primrec.list_findIdx {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → List β} {p : α → β → Bool} (hf : Primrec f) (hp : Primrec₂ p) : Primrec fun (a : α) => List.findIdx (p a) (f a)

theorem Primrec.list_idxOf {α : Type u_1} [Primcodable α] [DecidableEq α] : Primrec₂ List.idxOf

theorem Primrec.nat_strong_rec {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (f : α → ℕ → σ) {g : α → List σ → Option σ} (hg : Primrec₂ g) (H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)) : Primrec₂ f

theorem Primrec.listLookup {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] [DecidableEq α] : Primrec₂ List.lookup

theorem Primrec.nat_omega_rec' {β : Type u_2} {σ : Type u_4} [Primcodable β] [Primcodable σ] (f : β → σ) {m : β → ℕ} {l : β → List β} {g : β → List σ → Option σ} (hm : Primrec m) (hl : Primrec l) (hg : Primrec₂ g) (Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b) (H : ∀ (b : β), g b (List.map f (l b)) = some (f b)) : Primrec f

theorem Primrec.nat_omega_rec {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] (f : α → β → σ) {m : α → β → ℕ} {l : α → β → List β} {g : α → β × List σ → Option σ} (hm : Primrec₂ m) (hl : Primrec₂ l) (hg : Primrec₂ g) (Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b) (H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)) : Primrec₂ f

theorem PrimrecPred.exists_mem_list {α : Type u_1} {p : α → Prop} [Primcodable α] (hf : PrimrecPred p) : PrimrecPred fun (L : List α) => ∃ a ∈ L, p a

Checking if any element of a list satisfies a decidable predicate is primitive recursive.

theorem PrimrecPred.forall_mem_list {α : Type u_1} {p : α → Prop} [Primcodable α] (hf : PrimrecPred p) : PrimrecPred fun (L : List α) => ∀ a ∈ L, p a

Checking if every element of a list satisfies a decidable predicate is primitive recursive.

theorem PrimrecPred.exists_lt {p : ℕ → Prop} (hf : PrimrecPred p) : PrimrecPred fun (n : ℕ) => ∃ x < n, p x

Bounded existential quantifiers are primitive recursive.

theorem PrimrecPred.forall_lt {p : ℕ → Prop} (hf : PrimrecPred p) : PrimrecPred fun (n : ℕ) => ∀ x < n, p x

Bounded universal quantifiers are primitive recursive.

theorem PrimrecPred.listFilter_listRange {R : ℕ → ℕ → Prop} (s : ℕ) [DecidableRel R] (hf : PrimrecRel R) : Primrec fun (n : ℕ) => List.filter (fun (y : ℕ) => decide (R y n)) (List.range s)

A helper lemma for proofs about bounded quantifiers on decidable relations.

theorem PrimrecRel.not {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [Primcodable α] [Primcodable β] (hf : PrimrecRel R) : PrimrecRel fun (a : α) (b : β) => ¬R a b

theorem PrimrecRel.listFilter {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [Primcodable α] [Primcodable β] (hf : PrimrecRel R) [DecidableRel R] : Primrec₂ fun (L : List α) (b : β) => List.filter (fun (a : α) => decide (R a b)) L

If R a b is decidable, then given L : List α and b : β, it is primitive recursive to filter L for elements a with R a b

theorem PrimrecRel.exists_mem_list {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [Primcodable α] [Primcodable β] (hf : PrimrecRel R) : PrimrecRel fun (L : List α) (b : β) => ∃ a ∈ L, R a b

If R a b is decidable, then given L : List α and b : β, g L b ↔ ∃ a L, R a b is a primitive recursive relation.

theorem PrimrecRel.forall_mem_list {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [Primcodable α] [Primcodable β] (hf : PrimrecRel R) : PrimrecRel fun (L : List α) (b : β) => ∀ a ∈ L, R a b

If R a b is decidable, then given L : List α and b : β, g L b ↔ ∀ a L, R a b is a primitive recursive relation.

theorem PrimrecRel.exists_lt {R : ℕ → ℕ → Prop} (hf : PrimrecRel R) : PrimrecRel fun (n y : ℕ) => ∃ x < n, R x y

If R a b is decidable, then for any fixed n and y, g n y ↔ ∃ x < n, R x y is a primitive recursive relation.

theorem PrimrecRel.forall_lt {R : ℕ → ℕ → Prop} (hf : PrimrecRel R) : PrimrecRel fun (n y : ℕ) => ∀ x < n, R x y

If R a b is decidable, then for any fixed n and y, g n y ↔ ∀ x < n, R x y is a primitive recursive relation.

def Primcodable.subtype {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] (hp : PrimrecPred p) : Primcodable (Subtype p)

A subtype of a primitive recursive predicate is Primcodable.

Equations

• Primcodable.subtype hp = { toEncodable := Subtype.encodable, prim := ⋯ }

instance Primcodable.fin {n : ℕ} : Primcodable (Fin n)

Equations

• Primcodable.fin = Primcodable.ofEquiv { a : ℕ // id a < n } Fin.equivSubtype

instance Primcodable.vector {α : Type u_1} [Primcodable α] {n : ℕ} : Primcodable (List.Vector α n)

Equations

• Primcodable.vector = Primcodable.subtype ⋯

instance Primcodable.finArrow {α : Type u_1} [Primcodable α] {n : ℕ} : Primcodable (Fin n → α)

Equations

• Primcodable.finArrow = Primcodable.ofEquiv (List.Vector α n) (Equiv.vectorEquivFin α n).symm

theorem Primcodable.mem_range_encode {α : Type u_1} [Primcodable α] : PrimrecPred fun (n : ℕ) => n ∈ Set.range Encodable.encode

instance Primcodable.ulower {α : Type u_1} [Primcodable α] : Primcodable (ULower α)

Equations

• Primcodable.ulower = Primcodable.subtype ⋯

theorem Primrec.subtype_val {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] {hp : PrimrecPred p} : Primrec Subtype.val

theorem Primrec.subtype_val_iff {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : β → Prop} [DecidablePred p] {hp : PrimrecPred p} {f : α → Subtype p} : (Primrec fun (a : α) => ↑(f a)) ↔ Primrec f

theorem Primrec.subtype_mk {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : β → Prop} [DecidablePred p] {hp : PrimrecPred p} {f : α → β} {h : ∀ (a : α), p (f a)} (hf : Primrec f) : Primrec fun (a : α) => ⟨f a, ⋯⟩

theorem Primrec.option_get {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → Option β} {h : ∀ (a : α), (f a).isSome = true} : Primrec f → Primrec fun (a : α) => (f a).get ⋯

theorem Primrec.ulower_down {α : Type u_1} [Primcodable α] : Primrec ULower.down

theorem Primrec.ulower_up {α : Type u_1} [Primcodable α] : Primrec ULower.up

theorem Primrec.fin_val_iff {α : Type u_1} [Primcodable α] {n : ℕ} {f : α → Fin n} : (Primrec fun (a : α) => ↑(f a)) ↔ Primrec f

theorem Primrec.fin_val {n : ℕ} : Primrec fun (i : Fin n) => ↑i

theorem Primrec.fin_succ {n : ℕ} : Primrec Fin.succ

theorem Primrec.vector_toList {α : Type u_1} [Primcodable α] {n : ℕ} : Primrec List.Vector.toList

theorem Primrec.vector_toList_iff {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {n : ℕ} {f : α → List.Vector β n} : (Primrec fun (a : α) => (f a).toList) ↔ Primrec f

theorem Primrec.vector_cons {α : Type u_1} [Primcodable α] {n : ℕ} : Primrec₂ List.Vector.cons

theorem Primrec.vector_length {α : Type u_1} [Primcodable α] {n : ℕ} : Primrec List.Vector.length

theorem Primrec.vector_head {α : Type u_1} [Primcodable α] {n : ℕ} : Primrec List.Vector.head

theorem Primrec.vector_tail {α : Type u_1} [Primcodable α] {n : ℕ} : Primrec List.Vector.tail

theorem Primrec.vector_get {α : Type u_1} [Primcodable α] {n : ℕ} : Primrec₂ List.Vector.get

theorem Primrec.list_ofFn {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {n : ℕ} {f : Fin n → α → σ} : (∀ (i : Fin n), Primrec (f i)) → Primrec fun (a : α) => List.ofFn fun (i : Fin n) => f i a

theorem Primrec.vector_ofFn {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {n : ℕ} {f : Fin n → α → σ} (hf : ∀ (i : Fin n), Primrec (f i)) : Primrec fun (a : α) => List.Vector.ofFn fun (i : Fin n) => f i a

theorem Primrec.vector_get' {α : Type u_1} [Primcodable α] {n : ℕ} : Primrec List.Vector.get

theorem Primrec.vector_ofFn' {α : Type u_1} [Primcodable α] {n : ℕ} : Primrec List.Vector.ofFn

theorem Primrec.fin_app {σ : Type u_3} [Primcodable σ] {n : ℕ} : Primrec₂ id

theorem Primrec.fin_curry₁ {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {n : ℕ} {f : Fin n → α → σ} : Primrec₂ f ↔ ∀ (i : Fin n), Primrec (f i)

theorem Primrec.fin_curry {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {n : ℕ} {f : α → Fin n → σ} : Primrec f ↔ Primrec₂ f

inductive Nat.Primrec' {n : ℕ} : (List.Vector ℕ n → ℕ) → Prop

An alternative inductive definition of Primrec which does not use the pairing function on ℕ, and so has to work with n-ary functions on ℕ instead of unary functions. We prove that this is equivalent to the regular notion in to_prim and of_prim.

• zero : Primrec' fun (x : List.Vector ℕ 0) => 0
• succ : Primrec' fun (v : List.Vector ℕ 1) => v.head.succ
• get {n : ℕ} (i : Fin n) : Primrec' fun (v : List.Vector ℕ n) => v.get i
• comp {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ) : Primrec' f → (∀ (i : Fin n), Primrec' (g i)) → Primrec' fun (a : List.Vector ℕ m) => f (List.Vector.ofFn fun (i : Fin n) => g i a)
• prec {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ} : Primrec' f → Primrec' g → Primrec' fun (v : List.Vector ℕ (n + 1)) => Nat.rec (f v.tail) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v.tail)) v.head

theorem Nat.Primrec'.to_prim {n : ℕ} {f : List.Vector ℕ n → ℕ} (pf : Primrec' f) : Primrec f

theorem Nat.Primrec'.of_eq {n : ℕ} {f g : List.Vector ℕ n → ℕ} (hf : Primrec' f) (H : ∀ (i : List.Vector ℕ n), f i = g i) : Primrec' g

theorem Nat.Primrec'.const {n : ℕ} (m : ℕ) : Primrec' fun (x : List.Vector ℕ n) => m

theorem Nat.Primrec'.head {n : ℕ} : Primrec' List.Vector.head

theorem Nat.Primrec'.tail {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec' f) : Primrec' fun (v : List.Vector ℕ n.succ) => f v.tail

def Nat.Primrec'.Vec {n m : ℕ} (f : List.Vector ℕ n → List.Vector ℕ m) : Prop

A function from vectors to vectors is primitive recursive when all of its projections are.

Equations

• Nat.Primrec'.Vec f = ∀ (i : Fin m), Nat.Primrec' fun (v : List.Vector ℕ n) => (f v).get i

theorem Nat.Primrec'.nil {n : ℕ} : Vec fun (x : List.Vector ℕ n) => List.Vector.nil

theorem Nat.Primrec'.cons {n m : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ n → List.Vector ℕ m} (hf : Primrec' f) (hg : Vec g) : Vec fun (v : List.Vector ℕ n) => f v ::ᵥ g v

theorem Nat.Primrec'.idv {n : ℕ} : Vec id

theorem Nat.Primrec'.comp' {n m : ℕ} {f : List.Vector ℕ m → ℕ} {g : List.Vector ℕ n → List.Vector ℕ m} (hf : Primrec' f) (hg : Vec g) : Primrec' fun (v : List.Vector ℕ n) => f (g v)

theorem Nat.Primrec'.comp₁ (f : ℕ → ℕ) (hf : Primrec' fun (v : List.Vector ℕ 1) => f v.head) {n : ℕ} {g : List.Vector ℕ n → ℕ} (hg : Primrec' g) : Primrec' fun (v : List.Vector ℕ n) => f (g v)

theorem Nat.Primrec'.comp₂ (f : ℕ → ℕ → ℕ) (hf : Primrec' fun (v : List.Vector ℕ 2) => f v.head v.tail.head) {n : ℕ} {g h : List.Vector ℕ n → ℕ} (hg : Primrec' g) (hh : Primrec' h) : Primrec' fun (v : List.Vector ℕ n) => f (g v) (h v)

theorem Nat.Primrec'.prec' {n : ℕ} {f g : List.Vector ℕ n → ℕ} {h : List.Vector ℕ (n + 2) → ℕ} (hf : Primrec' f) (hg : Primrec' g) (hh : Primrec' h) : Primrec' fun (v : List.Vector ℕ n) => Nat.rec (g v) (fun (y IH : ℕ) => h (y ::ᵥ IH ::ᵥ v)) (f v)

theorem Nat.Primrec'.pred : Primrec' fun (v : List.Vector ℕ 1) => v.head.pred

theorem Nat.Primrec'.add : Primrec' fun (v : List.Vector ℕ 2) => v.head + v.tail.head

theorem Nat.Primrec'.sub : Primrec' fun (v : List.Vector ℕ 2) => v.head - v.tail.head

theorem Nat.Primrec'.mul : Primrec' fun (v : List.Vector ℕ 2) => v.head * v.tail.head

theorem Nat.Primrec'.if_lt {n : ℕ} {a b f g : List.Vector ℕ n → ℕ} (ha : Primrec' a) (hb : Primrec' b) (hf : Primrec' f) (hg : Primrec' g) : Primrec' fun (v : List.Vector ℕ n) => if a v < b v then f v else g v

theorem Nat.Primrec'.natPair : Primrec' fun (v : List.Vector ℕ 2) => pair v.head v.tail.head

theorem Nat.Primrec'.encode {n : ℕ} : Primrec' Encodable.encode

theorem Nat.Primrec'.sqrt : Primrec' fun (v : List.Vector ℕ 1) => v.head.sqrt

theorem Nat.Primrec'.unpair₁ {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec' f) : Primrec' fun (v : List.Vector ℕ n) => (unpair (f v)).1

theorem Nat.Primrec'.unpair₂ {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec' f) : Primrec' fun (v : List.Vector ℕ n) => (unpair (f v)).2

theorem Nat.Primrec'.of_prim {n : ℕ} {f : List.Vector ℕ n → ℕ} : Primrec f → Primrec' f

theorem Nat.Primrec'.prim_iff {n : ℕ} {f : List.Vector ℕ n → ℕ} : Primrec' f ↔ Primrec f

theorem Nat.Primrec'.prim_iff₁ {f : ℕ → ℕ} : (Primrec' fun (v : List.Vector ℕ 1) => f v.head) ↔ Primrec f

theorem Nat.Primrec'.prim_iff₂ {f : ℕ → ℕ → ℕ} : (Primrec' fun (v : List.Vector ℕ 2) => f v.head v.tail.head) ↔ Primrec₂ f

theorem Nat.Primrec'.vec_iff {m n : ℕ} {f : List.Vector ℕ m → List.Vector ℕ n} : Vec f ↔ Primrec f

theorem Primrec.nat_sqrt : Primrec Nat.sqrt