# 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.)

## References #

• [Mario Carneiro, Formalizing computability theory via partial recursive functions][carneiro2019]
@[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
• = f n.unpair.1 n.unpair.2
Instances For
inductive Nat.Primrec :
()Prop

The primitive recursive functions ℕ → ℕ.

Instances For
theorem Nat.Primrec.of_eq {f : } {g : } (hf : ) (H : ∀ (n : ), f n = g n) :
theorem Nat.Primrec.const (n : ) :
Nat.Primrec fun (x : ) => n
theorem Nat.Primrec.prec1 {f : } (m : ) (hf : ) :
Nat.Primrec fun (n : ) => Nat.rec m (fun (y IH : ) => f (y.pair IH)) n
theorem Nat.Primrec.casesOn1 {f : } (m : ) (hf : ) :
Nat.Primrec fun (x : ) => Nat.casesOn x m f
theorem Nat.Primrec.casesOn' {f : } {g : } (hf : ) (hg : ) :
Nat.Primrec (Nat.unpaired fun (z n : ) => Nat.casesOn n (f z) fun (y : ) => g (z.pair y))
theorem Nat.Primrec.swap' {f : } (hf : ) :
Nat.Primrec (Nat.unpaired fun (x x_1 : ) => x + x_1)
theorem Nat.Primrec.sub :
Nat.Primrec (Nat.unpaired fun (x x_1 : ) => x - x_1)
theorem Nat.Primrec.mul :
Nat.Primrec (Nat.unpaired fun (x x_1 : ) => x * x_1)
theorem Nat.Primrec.pow :
Nat.Primrec (Nat.unpaired fun (x x_1 : ) => x ^ x_1)
class Primcodable (α : Type u_1) extends :
Type u_1

A Primcodable type is an Encodable type for which the encode/decode functions are primitive recursive.

Instances
theorem Primcodable.prim {α : Type u_1} [self : ] :
Nat.Primrec fun (n : ) =>
@[instance 10]
instance Primcodable.ofDenumerable (α : Type u_1) [] :
Equations
def Primcodable.ofEquiv (α : Type u_1) {β : Type u_2} [] (e : β α) :

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

Equations
• = let __spread.0 := ;
Instances For
Equations
instance Primcodable.option {α : Type u_1} [h : ] :
Equations
• Primcodable.option =
instance Primcodable.bool :
Equations
def Primrec {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :

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

Equations
Instances For
theorem Primrec.encode {α : Type u_1} [] :
Primrec Encodable.encode
theorem Primrec.decode {α : Type u_1} [] :
Primrec Encodable.decode
theorem Primrec.dom_denumerable {α : Type u_4} {β : Type u_5} [] [] {f : αβ} :
Nat.Primrec fun (n : ) => Encodable.encode (f ())
theorem Primrec.nat_iff {f : } :
theorem Primrec.encdec {α : Type u_1} [] :
Primrec fun (n : ) =>
theorem Primrec.option_some {α : Type u_1} [] :
Primrec some
theorem Primrec.of_eq {α : Type u_1} {σ : Type u_3} [] [] {f : ασ} {g : ασ} (hf : ) (H : ∀ (n : α), f n = g n) :
theorem Primrec.const {α : Type u_1} {σ : Type u_3} [] [] (x : σ) :
Primrec fun (x_1 : α) => x
theorem Primrec.id {α : Type u_1} [] :
theorem Primrec.comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : βσ} {g : αβ} (hf : ) (hg : ) :
Primrec fun (a : α) => f (g a)
theorem Primrec.encode_iff {α : Type u_1} {σ : Type u_3} [] [] {f : ασ} :
(Primrec fun (a : α) => Encodable.encode (f a))
theorem Primrec.ofNat_iff {α : Type u_4} {β : Type u_5} [] [] {f : αβ} :
Primrec fun (n : ) => f ()
theorem Primrec.ofNat (α : Type u_4) [] :
theorem Primrec.option_some_iff {α : Type u_1} {σ : Type u_3} [] [] {f : ασ} :
(Primrec fun (a : α) => some (f a))
theorem Primrec.of_equiv {α : Type u_1} [] {β : Type u_4} {e : β α} :
Primrec e
theorem Primrec.of_equiv_symm {α : Type u_1} [] {β : Type u_4} {e : β α} :
Primrec e.symm
theorem Primrec.of_equiv_iff {α : Type u_1} {σ : Type u_3} [] [] {β : Type u_4} (e : β α) {f : σβ} :
(Primrec fun (a : σ) => e (f a))
theorem Primrec.of_equiv_symm_iff {α : Type u_1} {σ : Type u_3} [] [] {β : Type u_4} (e : β α) {f : σα} :
(Primrec fun (a : σ) => e.symm (f a))
instance Primcodable.prod {α : Type u_1} {β : Type u_2} [] [] :
Primcodable (α × β)
Equations
• Primcodable.prod =
theorem Primrec.fst {α : Type u_3} {β : Type u_4} [] [] :
Primrec Prod.fst
theorem Primrec.snd {α : Type u_3} {β : Type u_4} [] [] :
Primrec Prod.snd
theorem Primrec.pair {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] [] [] {f : αβ} {g : αγ} (hf : ) (hg : ) :
Primrec fun (a : α) => (f a, g a)
theorem Primrec.list_get?₁ {α : Type u_1} [] (l : List α) :
Primrec l.get?
def Primrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] (f : αβσ) :

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
Instances For
def PrimrecPred {α : Type u_1} [] (p : αProp) [] :

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

Equations
Instances For
def PrimrecRel {α : Type u_1} {β : Type u_2} [] [] (s : αβProp) [(a : α) → (b : β) → Decidable (s a b)] :

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

Equations
Instances For
theorem Primrec₂.mk {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : αβσ} (hf : Primrec fun (p : α × β) => f p.1 p.2) :
theorem Primrec₂.of_eq {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : αβσ} {g : αβσ} (hg : ) (H : ∀ (a : α) (b : β), f a b = g a b) :
theorem Primrec₂.const {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] (x : σ) :
Primrec₂ fun (x_1 : α) (x_2 : β) => x
theorem Primrec₂.pair {α : Type u_1} {β : Type u_2} [] [] :
Primrec₂ Prod.mk
theorem Primrec₂.left {α : Type u_1} {β : Type u_2} [] [] :
Primrec₂ fun (a : α) (x : β) => a
theorem Primrec₂.right {α : Type u_1} {β : Type u_2} [] [] :
Primrec₂ fun (x : α) (b : β) => b
theorem Primrec₂.unpaired {α : Type u_1} [] {f : α} :
theorem Primrec₂.unpaired' {f : } :
theorem Primrec₂.encode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : αβσ} :
(Primrec₂ fun (a : α) (b : β) => Encodable.encode (f a b))
theorem Primrec₂.option_some_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : αβσ} :
(Primrec₂ fun (a : α) (b : β) => some (f a b))
theorem Primrec₂.ofNat_iff {α : Type u_4} {β : Type u_5} {σ : Type u_6} [] [] [] {f : αβσ} :
Primrec₂ fun (m n : ) => f () ()
theorem Primrec₂.uncurry {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : αβσ} :
theorem Primrec₂.curry {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : α × βσ} :
theorem Primrec.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [] [] [] [] {f : γσ} {g : αβγ} (hf : ) (hg : ) :
Primrec₂ fun (a : α) (b : β) => f (g a b)
theorem Primrec₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [] [] [] [] {f : βγσ} {g : αβ} {h : αγ} (hf : ) (hg : ) (hh : ) :
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} [] [] [] [] [] {f : γδσ} {g : αβγ} {h : αβδ} (hf : ) (hg : ) (hh : ) :
Primrec₂ fun (a : α) (b : β) => f (g a b) (h a b)
theorem PrimrecPred.comp {α : Type u_1} {β : Type u_2} [] [] {p : βProp} [] {f : αβ} :
PrimrecPred fun (a : α) => p (f a)
theorem PrimrecRel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {R : βγProp} [(a : β) → (b : γ) → Decidable (R a b)] {f : αβ} {g : αγ} :
PrimrecPred fun (a : α) => R (f a) (g a)
theorem PrimrecRel.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] [] [] [] {R : γδProp} [(a : γ) → (b : δ) → Decidable (R a b)] {f : αβγ} {g : αβδ} :
PrimrecRel fun (a : α) (b : β) => R (f a b) (g a b)
theorem PrimrecPred.of_eq {α : Type u_1} [] {p : αProp} {q : αProp} [] [] (hp : ) (H : ∀ (a : α), p a q a) :
theorem PrimrecRel.of_eq {α : Type u_1} {β : Type u_2} [] [] {r : αβProp} {s : αβProp} [(a : α) → (b : β) → Decidable (r a b)] [(a : α) → (b : β) → Decidable (s a b)] (hr : ) (H : ∀ (a : α) (b : β), r a b s a b) :
theorem Primrec₂.swap {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : αβσ} (h : ) :
theorem Primrec₂.nat_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : αβσ} :
Nat.Primrec (Nat.unpaired fun (m n : ) => Encodable.encode (().bind fun (a : α) => Option.map (f a) ()))
theorem Primrec₂.nat_iff' {α : Type u_1} {β : Type u_2} {σ : Type u_3} [] [] [] {f : αβσ} :
Primrec₂ fun (m n : ) => ().bind fun (a : α) => Option.map (f a) ()
theorem Primrec.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [] [] [] {f : α × βσ} (hf : ) :
Primrec₂ fun (a : α) (b : β) => f (a, b)
theorem Primrec.nat_rec {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : α × ββ} (hf : ) (hg : ) :
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} [] [] {f : α} {g : αβ} {h : α × ββ} (hf : ) (hg : ) (hh : ) :
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} [] {f : αα} (a : α) (hf : ) :
Primrec fun (t : ) => Nat.rec a f t
theorem Primrec.nat_casesOn' {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Primrec₂ fun (a : α) (n : ) => Nat.casesOn n (f a) (g a)
theorem Primrec.nat_casesOn {α : Type u_1} {β : Type u_2} [] [] {f : α} {g : αβ} {h : αβ} (hf : ) (hg : ) (hh : ) :
Primrec fun (a : α) => Nat.casesOn (f a) (g a) (h a)
theorem Primrec.nat_casesOn₁ {α : Type u_1} [] {f : α} (a : α) (hf : ) :
Primrec fun (n : ) => Nat.casesOn n a f
theorem Primrec.nat_iterate {α : Type u_1} {β : Type u_2} [] [] {f : α} {g : αβ} {h : αββ} (hf : ) (hg : ) (hh : ) :
Primrec fun (a : α) => (h a)^[f a] (g a)
theorem Primrec.option_casesOn {α : Type u_1} {β : Type u_2} {σ : Type u_5} [] [] [] {o : α} {f : ασ} {g : αβσ} (ho : ) (hf : ) (hg : ) :
Primrec fun (a : α) => Option.casesOn (o a) (f a) (g a)
theorem Primrec.option_bind {α : Type u_1} {β : Type u_2} {σ : Type u_5} [] [] [] {f : α} {g : αβ} (hf : ) (hg : ) :
Primrec fun (a : α) => (f a).bind (g a)
theorem Primrec.option_bind₁ {α : Type u_1} {σ : Type u_5} [] [] {f : α} (hf : ) :
Primrec fun (o : ) => o.bind f
theorem Primrec.option_map {α : Type u_1} {β : Type u_2} {σ : Type u_5} [] [] [] {f : α} {g : αβσ} (hf : ) (hg : ) :
Primrec fun (a : α) => Option.map (g a) (f a)
theorem Primrec.option_map₁ {α : Type u_1} {σ : Type u_5} [] [] {f : ασ} (hf : ) :
theorem Primrec.option_iget {α : Type u_1} [] [] :
Primrec Option.iget
theorem Primrec.option_isSome {α : Type u_1} [] :
Primrec Option.isSome
theorem Primrec.option_getD {α : Type u_1} [] :
Primrec₂ Option.getD
theorem Primrec.bind_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_5} [] [] [] {f : αβ} :
(Primrec₂ fun (a : α) (n : ) => ().bind (f a))
theorem Primrec.map_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_5} [] [] [] {f : αβσ} :
(Primrec₂ fun (a : α) (n : ) => Option.map (f a) ())
Primrec₂ fun (x x_1 : ) => x + x_1
theorem Primrec.nat_sub :
Primrec₂ fun (x x_1 : ) => x - x_1
theorem Primrec.nat_mul :
Primrec₂ fun (x x_1 : ) => x * x_1
theorem Primrec.cond {α : Type u_1} {σ : Type u_5} [] [] {c : αBool} {f : ασ} {g : ασ} (hc : ) (hf : ) (hg : ) :
Primrec fun (a : α) => bif c a then f a else g a
theorem Primrec.ite {α : Type u_1} {σ : Type u_5} [] [] {c : αProp} [] {f : ασ} {g : ασ} (hc : ) (hf : ) (hg : ) :
Primrec fun (a : α) => if c a then f a else g a
theorem Primrec.nat_le :
PrimrecRel fun (x x_1 : ) => x x_1
theorem Primrec.dom_bool {α : Type u_1} [] (f : Boolα) :
theorem Primrec.dom_bool₂ {α : Type u_1} [] (f : BoolBoolα) :
theorem PrimrecPred.not {α : Type u_1} [] {p : αProp} [] (hp : ) :
PrimrecPred fun (a : α) => ¬p a
theorem PrimrecPred.and {α : Type u_1} [] {p : αProp} {q : αProp} [] [] (hp : ) (hq : ) :
PrimrecPred fun (a : α) => p a q a
theorem PrimrecPred.or {α : Type u_1} [] {p : αProp} {q : αProp} [] [] (hp : ) (hq : ) :
PrimrecPred fun (a : α) => p a q a
theorem Primrec.beq {α : Type u_1} [] [] :
Primrec₂ BEq.beq
theorem Primrec.eq {α : Type u_1} [] [] :
theorem Primrec.nat_lt :
PrimrecRel fun (x x_1 : ) => x < x_1
theorem Primrec.option_guard {α : Type u_1} {β : Type u_2} [] [] {p : αβProp} [(a : α) → (b : β) → Decidable (p a b)] (hp : ) {f : αβ} (hf : ) :
Primrec fun (a : α) => Option.guard (p a) (f a)
theorem Primrec.option_orElse {α : Type u_1} [] :
Primrec₂ fun (x x_1 : ) => HOrElse.hOrElse x fun (x : Unit) => x_1
theorem Primrec.decode₂ {α : Type u_1} [] :
theorem Primrec.list_findIdx₁ {α : Type u_1} {β : Type u_2} [] [] {p : αβBool} (hp : ) (l : List β) :
Primrec fun (a : α) => List.findIdx (p a) l
theorem Primrec.list_indexOf₁ {α : Type u_1} [] [] (l : List α) :
Primrec fun (a : α) =>
theorem Primrec.dom_fintype {α : Type u_1} {σ : Type u_5} [] [] [] (f : ασ) :
def Primrec.PrimrecBounded {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :

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

Equations
Instances For
theorem Primrec.nat_findGreatest {α : Type u_1} [] {f : α} {p : α} [(x : α) → (n : ) → Decidable (p x n)] (hf : ) (hp : ) :
Primrec fun (x : α) => Nat.findGreatest (p x) (f x)
theorem Primrec.of_graph {α : Type u_1} [] {f : α} (h₁ : ) (h₂ : PrimrecRel fun (a : α) (b : ) => f a = b) :

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 (x x_1 : ) => x / x_1
theorem Primrec.nat_mod :
Primrec₂ fun (x x_1 : ) => x % x_1
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} [] [] :
Equations
• Primcodable.sum =
instance Primcodable.list {α : Type u_1} [] :
Equations
• Primcodable.list =
theorem Primrec.sum_inl {α : Type u_1} {β : Type u_2} [] [] :
Primrec Sum.inl
theorem Primrec.sum_inr {α : Type u_1} {β : Type u_2} [] [] :
Primrec Sum.inr
theorem Primrec.sum_casesOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [] [] [] [] {f : αβ γ} {g : αβσ} {h : αγσ} (hf : ) (hg : ) (hh : ) :
Primrec fun (a : α) => Sum.casesOn (f a) (g a) (h a)
theorem Primrec.list_cons {α : Type u_1} [] :
Primrec₂ List.cons
theorem Primrec.list_casesOn {α : Type u_1} {β : Type u_2} {σ : Type u_4} [] [] [] {f : αList β} {g : ασ} {h : αβ × List βσ} :
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} [] [] [] {f : αList β} {g : ασ} {h : ασ × βσ} :
Primrec fun (a : α) => List.foldl (fun (s : σ) (b : β) => h a (s, b)) (g a) (f a)
theorem Primrec.list_reverse {α : Type u_1} [] :
Primrec List.reverse
theorem Primrec.list_foldr {α : Type u_1} {β : Type u_2} {σ : Type u_4} [] [] [] {f : αList β} {g : ασ} {h : αβ × σσ} (hf : ) (hg : ) (hh : ) :
Primrec fun (a : α) => List.foldr (fun (b : β) (s : σ) => h a (b, s)) (g a) (f a)
theorem Primrec.list_head? {α : Type u_1} [] :
theorem Primrec.list_headI {α : Type u_1} [] [] :
theorem Primrec.list_tail {α : Type u_1} [] :
Primrec List.tail
theorem Primrec.list_rec {α : Type u_1} {β : Type u_2} {σ : Type u_4} [] [] [] {f : αList β} {g : ασ} {h : αβ × List β × σσ} (hf : ) (hg : ) (hh : ) :
Primrec fun (a : α) => List.recOn (f a) (g a) fun (b : β) (l : List β) (IH : σ) => h a (b, l, IH)
theorem Primrec.list_get? {α : Type u_1} [] :
Primrec₂ List.get?
theorem Primrec.list_getD {α : Type u_1} [] (d : α) :
Primrec₂ fun (l : List α) (n : ) => l.getD n d
theorem Primrec.list_getI {α : Type u_1} [] [] :
Primrec₂ List.getI
theorem Primrec.list_append {α : Type u_1} [] :
Primrec₂ fun (x x_1 : List α) => x ++ x_1
theorem Primrec.list_concat {α : Type u_1} [] :
Primrec₂ fun (l : List α) (a : α) => l ++ [a]
theorem Primrec.list_map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [] [] [] {f : αList β} {g : αβσ} (hf : ) (hg : ) :
Primrec fun (a : α) => List.map (g a) (f a)
theorem Primrec.list_join {α : Type u_1} [] :
Primrec List.join
theorem Primrec.list_length {α : Type u_1} [] :
Primrec List.length
theorem Primrec.list_findIdx {α : Type u_1} {β : Type u_2} [] [] {f : αList β} {p : αβBool} (hf : ) (hp : ) :
Primrec fun (a : α) => List.findIdx (p a) (f a)
theorem Primrec.list_indexOf {α : Type u_1} [] [] :
Primrec₂ List.indexOf
theorem Primrec.nat_strong_rec {α : Type u_1} {σ : Type u_4} [] [] (f : ασ) {g : αList σ} (hg : ) (H : ∀ (a : α) (n : ), g a (List.map (f a) ()) = some (f a n)) :
def Primcodable.subtype {α : Type u_1} [] {p : αProp} [] (hp : ) :

A subtype of a primitive recursive predicate is Primcodable.

Equations
Instances For
instance Primcodable.fin {n : } :
Equations
instance Primcodable.vector {α : Type u_1} [] {n : } :
Equations
• Primcodable.vector =
instance Primcodable.finArrow {α : Type u_1} [] {n : } :
Primcodable (Fin nα)
Equations
theorem Primcodable.mem_range_encode {α : Type u_1} [] :
PrimrecPred fun (n : ) => n Set.range Encodable.encode
instance Primcodable.ulower {α : Type u_1} [] :
Equations
• Primcodable.ulower =
theorem Primrec.subtype_val {α : Type u_1} [] {p : αProp} [] {hp : } :
Primrec Subtype.val
theorem Primrec.subtype_val_iff {α : Type u_1} {β : Type u_2} [] [] {p : βProp} [] {hp : } {f : α} :
(Primrec fun (a : α) => (f a))
theorem Primrec.subtype_mk {α : Type u_1} {β : Type u_2} [] [] {p : βProp} [] {hp : } {f : αβ} {h : ∀ (a : α), p (f a)} (hf : ) :
Primrec fun (a : α) => f a,
theorem Primrec.option_get {α : Type u_1} {β : Type u_2} [] [] {f : α} {h : ∀ (a : α), (f a).isSome = true} :
Primrec fun (a : α) => (f a).get
theorem Primrec.ulower_down {α : Type u_1} [] :
Primrec ULower.down
theorem Primrec.ulower_up {α : Type u_1} [] :
Primrec ULower.up
theorem Primrec.fin_val_iff {α : Type u_1} [] {n : } {f : αFin n} :
(Primrec fun (a : α) => (f a))
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} [] {n : } :
Primrec Vector.toList
theorem Primrec.vector_toList_iff {α : Type u_1} {β : Type u_2} [] [] {n : } {f : αVector β n} :
(Primrec fun (a : α) => (f a).toList)
theorem Primrec.vector_cons {α : Type u_1} [] {n : } :
Primrec₂ Vector.cons
theorem Primrec.vector_length {α : Type u_1} [] {n : } :
Primrec Vector.length
theorem Primrec.vector_head {α : Type u_1} [] {n : } :
theorem Primrec.vector_tail {α : Type u_1} [] {n : } :
Primrec Vector.tail
theorem Primrec.vector_get {α : Type u_1} [] {n : } :
Primrec₂ Vector.get
theorem Primrec.list_ofFn {α : Type u_1} {σ : Type u_4} [] [] {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_4} [] [] {n : } {f : Fin nασ} (hf : ∀ (i : Fin n), Primrec (f i)) :
Primrec fun (a : α) => Vector.ofFn fun (i : Fin n) => f i a
theorem Primrec.vector_get' {α : Type u_1} [] {n : } :
Primrec Vector.get
theorem Primrec.vector_ofFn' {α : Type u_1} [] {n : } :
Primrec Vector.ofFn
theorem Primrec.fin_app {σ : Type u_4} [] {n : } :
theorem Primrec.fin_curry₁ {α : Type u_1} {σ : Type u_4} [] [] {n : } {f : Fin nασ} :
∀ (i : Fin n), Primrec (f i)
theorem Primrec.fin_curry {α : Type u_1} {σ : Type u_4} [] [] {n : } {f : αFin nσ} :
inductive Nat.Primrec' {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.

Instances For
theorem Nat.Primrec'.to_prim {n : } {f : } (pf : ) :
theorem Nat.Primrec'.of_eq {n : } {f : } {g : } (hf : ) (H : ∀ (i : ), f i = g i) :
theorem Nat.Primrec'.const {n : } (m : ) :
Nat.Primrec' fun (x : ) => m
theorem Nat.Primrec'.head {n : } :
theorem Nat.Primrec'.tail {n : } {f : } (hf : ) :
Nat.Primrec' fun (v : Vector n.succ) => f v.tail
def Nat.Primrec'.Vec {n : } {m : } (f : ) :

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

Equations
Instances For
theorem Nat.Primrec'.nil {n : } :
Nat.Primrec'.Vec fun (x : ) => Vector.nil
theorem Nat.Primrec'.cons {n : } {m : } {f : } {g : } (hf : ) (hg : ) :
Nat.Primrec'.Vec fun (v : ) => f v ::ᵥ g v
theorem Nat.Primrec'.idv {n : } :
theorem Nat.Primrec'.comp' {n : } {m : } {f : } {g : } (hf : ) (hg : ) :
Nat.Primrec' fun (v : ) => f (g v)
theorem Nat.Primrec'.comp₁ (f : ) (hf : Nat.Primrec' fun (v : ) => f v.head) {n : } {g : } (hg : ) :
Nat.Primrec' fun (v : ) => f (g v)
theorem Nat.Primrec'.comp₂ (f : ) (hf : Nat.Primrec' fun (v : ) => f v.head v.tail.head) {n : } {g : } {h : } (hg : ) (hh : ) :
Nat.Primrec' fun (v : ) => f (g v) (h v)
theorem Nat.Primrec'.prec' {n : } {f : } {g : } {h : Vector (n + 2)} (hf : ) (hg : ) (hh : ) :
Nat.Primrec' fun (v : ) => Nat.rec (g v) (fun (y IH : ) => h (y ::ᵥ IH ::ᵥ v)) (f v)
theorem Nat.Primrec'.pred :
Nat.Primrec' fun (v : ) => v.head.pred
theorem Nat.Primrec'.sub :
theorem Nat.Primrec'.mul :
theorem Nat.Primrec'.if_lt {n : } {a : } {b : } {f : } {g : } (ha : ) (hb : ) (hf : ) (hg : ) :
Nat.Primrec' fun (v : ) => if a v < b v then f v else g v
theorem Nat.Primrec'.natPair :
theorem Nat.Primrec'.encode {n : } :
Nat.Primrec' Encodable.encode
theorem Nat.Primrec'.sqrt :
Nat.Primrec' fun (v : ) => v.head.sqrt
theorem Nat.Primrec'.unpair₁ {n : } {f : } (hf : ) :
Nat.Primrec' fun (v : ) => (f v).unpair.1
theorem Nat.Primrec'.unpair₂ {n : } {f : } (hf : ) :
Nat.Primrec' fun (v : ) => (f v).unpair.2
theorem Nat.Primrec'.of_prim {n : } {f : } :
theorem Nat.Primrec'.prim_iff {n : } {f : } :
theorem Nat.Primrec'.prim_iff₁ {f : } :
(Nat.Primrec' fun (v : ) => f v.head)
theorem Nat.Primrec'.prim_iff₂ {f : } :