mathlib documentation

computability.primrec

The primitive recursive functions

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

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

def nat.elim {C : Sort u_1} :
C → (C → C) → C

Equations
@[simp]
theorem nat.elim_zero {C : Sort u_1} (a : C) (f : C → C) :
nat.elim a f 0 = a

@[simp]
theorem nat.elim_succ {C : Sort u_1} (a : C) (f : C → C) (n : ) :
nat.elim a f n.succ = f n (nat.elim a f n)

def nat.cases {C : Sort u_1} :
C → ( → C) → C

Equations
@[simp]
theorem nat.cases_zero {C : Sort u_1} (a : C) (f : → C) :
nat.cases a f 0 = a

@[simp]
theorem nat.cases_succ {C : Sort u_1} (a : C) (f : → C) (n : ) :
nat.cases a f n.succ = f n

@[simp]
def nat.unpaired {α : Sort u_1} :
( → α) → α

Equations
inductive nat.primrec  :
() → Prop

The primitive recursive functions ℕ → ℕ.

theorem nat.primrec.of_eq {f g : } :
nat.primrec f(∀ (n : ), f n = g n)nat.primrec g

theorem nat.primrec.const (n : ) :
nat.primrec (λ (_x : ), n)

theorem nat.primrec.prec1 {f : } (m : ) :
nat.primrec fnat.primrec (λ (n : ), nat.elim m (λ (y IH : ), f (y.mkpair IH)) n)

theorem nat.primrec.cases1 {f : } (m : ) :

theorem nat.primrec.cases {f g : } :
nat.primrec fnat.primrec gnat.primrec (nat.unpaired (λ (z n : ), nat.cases (f z) (λ (y : ), g (z.mkpair y)) n))

@[instance]
def primcodable.of_denumerable (α : Type u_1) [denumerable α] :

Equations
def primcodable.of_equiv (α : Type u_1) {β : Type u_2} [primcodable α] :
β αprimcodable β

Equations
@[instance]

Equations
@[instance]

Equations
def primrec {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
(α → β) → Prop

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

Equations
theorem primrec.encode {α : Type u_1} [primcodable α] :

theorem primrec.decode {α : Type u_1} [primcodable α] :

theorem primrec.dom_denumerable {α : Type u_1} {β : Type u_2} [denumerable α] [primcodable β] {f : α → β} :

theorem primrec.nat_iff {f : } :

theorem primrec.encdec {α : Type u_1} [primcodable α] :

theorem primrec.option_some {α : Type u_1} [primcodable α] :

theorem primrec.of_eq {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable «σ»] {f g : α → «σ»} :
primrec f(∀ (n : α), f n = g n)primrec g

theorem primrec.const {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable «σ»] (x : «σ») :
primrec (λ (a : α), x)

theorem primrec.id {α : Type u_1} [primcodable α] :

theorem primrec.comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] {f : β → «σ»} {g : α → β} :
primrec fprimrec gprimrec (λ (a : α), f (g a))

theorem primrec.encode_iff {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable «σ»] {f : α → «σ»} :
primrec (λ (a : α), encodable.encode (f a)) primrec f

theorem primrec.of_nat_iff {α : Type u_1} {β : Type u_2} [denumerable α] [primcodable β] {f : α → β} :
primrec f primrec (λ (n : ), f (denumerable.of_nat α n))

theorem primrec.of_nat (α : Type u_1) [denumerable α] :

theorem primrec.option_some_iff {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable «σ»] {f : α → «σ»} :
primrec (λ (a : α), some (f a)) primrec f

theorem primrec.of_equiv {α : Type u_1} [primcodable α] {β : Type u_2} {e : β α} :

theorem primrec.of_equiv_symm {α : Type u_1} [primcodable α] {β : Type u_2} {e : β α} :

theorem primrec.of_equiv_iff {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable «σ»] {β : Type u_2} (e : β α) {f : «σ» → β} :
primrec (λ (a : «σ»), e (f a)) primrec f

theorem primrec.of_equiv_symm_iff {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable «σ»] {β : Type u_2} (e : β α) {f : «σ» → α} :
primrec (λ (a : «σ»), (e.symm) (f a)) primrec f

@[instance]
def primcodable.prod {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
primcodable × β)

Equations
theorem primrec.fst {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :

theorem primrec.snd {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :

theorem primrec.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {f : α → β} {g : α → γ} :
primrec fprimrec gprimrec (λ (a : α), (f a, g a))

theorem primrec.list_nth₁ {α : Type u_1} [primcodable α] (l : list α) :

def primrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] :
(α → β → «σ») → 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
def primrec_pred {α : Type u_1} [primcodable α] (p : α → Prop) [decidable_pred p] :
Prop

primrec_pred p means p : α → Prop is a (decidable) primitive recursive predicate, which is to say that to_bool ∘ p : α → bool is primitive recursive.

Equations
def primrec_rel {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] (s : α → β → Prop) [Π (a : α) (b : β), decidable (s a b)] :
Prop

primrec_rel p means p : α → β → Prop is a (decidable) primitive recursive relation, which is to say that to_bool ∘ p : α → β → bool is primitive recursive.

Equations
theorem primrec₂.of_eq {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] {f g : α → β → «σ»} :
primrec₂ f(∀ (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₂ (λ (a : α) (b : β), x)

theorem primrec₂.pair {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :

theorem primrec₂.left {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
primrec₂ (λ (a : α) (b : β), a)

theorem primrec₂.right {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
primrec₂ (λ (a : α) (b : β), b)

theorem primrec₂.unpaired {α : Type u_1} [primcodable α] {f : → α} :

theorem primrec₂.encode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → β → «σ»} :
primrec₂ (λ (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₂ (λ (a : α) (b : β), some (f a b)) primrec₂ f

theorem primrec₂.of_nat_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [denumerable α] [denumerable β] [primcodable «σ»] {f : α → β → «σ»} :

theorem primrec₂.uncurry {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → β → «σ»} :

theorem primrec₂.curry {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] {f : α × β → «σ»} :

theorem primrec.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable γ] [primcodable «σ»] {f : γ → «σ»} {g : α → β → γ} :
primrec fprimrec₂ gprimrec₂ (λ (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 : α → γ} :
primrec₂ fprimrec gprimrec hprimrec (λ (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 : α → β → δ} :
primrec₂ fprimrec₂ gprimrec₂ hprimrec₂ (λ (a : α) (b : β), f (g a b) (h a b))

theorem primrec_pred.comp {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : β → Prop} [decidable_pred p] {f : α → β} :
primrec_pred pprimrec fprimrec_pred (λ (a : α), p (f a))

theorem primrec_rel.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {R : β → γ → Prop} [Π (a : β) (b : γ), decidable (R a b)] {f : α → β} {g : α → γ} :
primrec_rel Rprimrec fprimrec gprimrec_pred (λ (a : α), R (f a) (g a))

theorem primrec_rel.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] {R : γ → δ → Prop} [Π (a : γ) (b : δ), decidable (R a b)] {f : α → β → γ} {g : α → β → δ} :
primrec_rel Rprimrec₂ fprimrec₂ gprimrec_rel (λ (a : α) (b : β), R (f a b) (g a b))

theorem primrec_pred.of_eq {α : Type u_1} [primcodable α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] :
primrec_pred p(∀ (a : α), p a q a)primrec_pred q

theorem primrec_rel.of_eq {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {r s : α → β → Prop} [Π (a : α) (b : β), decidable (r a b)] [Π (a : α) (b : β), decidable (s a b)] :
primrec_rel r(∀ (a : α) (b : β), r a b s a b)primrec_rel s

theorem primrec₂.swap {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → β → «σ»} :

theorem primrec₂.nat_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → β → «σ»} :

theorem primrec₂.nat_iff' {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → β → «σ»} :
primrec₂ f primrec₂ (λ (m n : ), (encodable.decode α m).bind (λ (a : α), option.map (f a) (encodable.decode β n)))

theorem primrec.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable «σ»] {f : α × β → «σ»} :
primrec fprimrec₂ (λ (a : α) (b : β), f (a, b))

theorem primrec.nat_elim {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → β} {g : α → × β → β} :
primrec fprimrec₂ gprimrec₂ (λ (a : α) (n : ), nat.elim (f a) (λ (n : ) (IH : β), g a (n, IH)) n)

theorem primrec.nat_elim' {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → } {g : α → β} {h : α → × β → β} :
primrec fprimrec gprimrec₂ hprimrec (λ (a : α), nat.elim (g a) (λ (n : ) (IH : β), h a (n, IH)) (f a))

theorem primrec.nat_elim₁ {α : Type u_1} [primcodable α] {f : α → α} (a : α) :

theorem primrec.nat_cases' {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → β} {g : α → → β} :
primrec fprimrec₂ gprimrec₂ (λ (a : α), nat.cases (f a) (g a))

theorem primrec.nat_cases {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → } {g : α → β} {h : α → → β} :
primrec fprimrec gprimrec₂ hprimrec (λ (a : α), nat.cases (g a) (h a) (f a))

theorem primrec.nat_cases₁ {α : Type u_1} [primcodable α] {f : → α} (a : α) :

theorem primrec.nat_iterate {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → } {g : α → β} {h : α → β → β} :
primrec fprimrec gprimrec₂ hprimrec (λ (a : α), h a^[f a] (g a))

theorem primrec.option_cases {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable «σ»] {o : α → option β} {f : α → «σ»} {g : α → β → «σ»} :
primrec oprimrec fprimrec₂ gprimrec (λ (a : α), (o a).cases_on (f a) (g a))

theorem primrec.option_bind {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → option β} {g : α → β → option «σ»} :
primrec fprimrec₂ gprimrec (λ (a : α), (f a).bind (g a))

theorem primrec.option_bind₁ {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable «σ»] {f : α → option «σ»} :
primrec fprimrec (λ (o : option α), o.bind f)

theorem primrec.option_map {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → option β} {g : α → β → «σ»} :
primrec fprimrec₂ gprimrec (λ (a : α), option.map (g a) (f a))

theorem primrec.option_map₁ {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable «σ»] {f : α → «σ»} :

theorem primrec.option_iget {α : Type u_1} [primcodable α] [inhabited α] :

theorem primrec.bind_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → β → option «σ»} :
primrec₂ (λ (a : α) (n : ), (encodable.decode β n).bind (f a)) primrec₂ f

theorem primrec.map_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → β → «σ»} :
primrec₂ (λ (a : α) (n : ), option.map (f a) (encodable.decode β n)) primrec₂ f

theorem primrec.cond {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable «σ»] {c : α → bool} {f g : α → «σ»} :
primrec cprimrec fprimrec gprimrec (λ (a : α), cond (c a) (f a) (g a))

theorem primrec.ite {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable «σ»] {c : α → Prop} [decidable_pred c] {f g : α → «σ»} :
primrec_pred cprimrec fprimrec gprimrec (λ (a : α), ite (c a) (f a) (g a))

theorem primrec.dom_bool {α : Type u_1} [primcodable α] (f : bool → α) :

theorem primrec.dom_bool₂ {α : Type u_1} [primcodable α] (f : boolbool → α) :

theorem primrec.not {α : Type u_1} [primcodable α] {p : α → Prop} [decidable_pred p] :
primrec_pred pprimrec_pred (λ (a : α), ¬p a)

theorem primrec.and {α : Type u_1} [primcodable α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] :
primrec_pred pprimrec_pred qprimrec_pred (λ (a : α), p a q a)

theorem primrec.or {α : Type u_1} [primcodable α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] :
primrec_pred pprimrec_pred qprimrec_pred (λ (a : α), p a q a)

theorem primrec.eq {α : Type u_1} [primcodable α] [decidable_eq α] :

theorem primrec.option_guard {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → β → Prop} [Π (a : α) (b : β), decidable (p a b)] (hp : primrec_rel p) {f : α → β} :
primrec fprimrec (λ (a : α), option.guard (p a) (f a))

theorem primrec.decode2 {α : Type u_1} [primcodable α] :

theorem primrec.list_find_index₁ {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : α → β → Prop} [Π (a : α) (b : β), decidable (p a b)] (hp : primrec_rel p) (l : list β) :
primrec (λ (a : α), list.find_index (p a) l)

theorem primrec.list_index_of₁ {α : Type u_1} [primcodable α] [decidable_eq α] (l : list α) :
primrec (λ (a : α), list.index_of a l)

theorem primrec.dom_fintype {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable «σ»] [fintype α] (f : α → «σ») :

theorem primrec.nat_div_mod  :
primrec₂ (λ (n k : ), (n / k, n % k))

@[instance]
def primcodable.sum {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :

Equations
theorem primrec.sum_inl {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :

theorem primrec.sum_inr {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :

theorem primrec.sum_cases {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable γ] [primcodable «σ»] {f : α → β γ} {g : α → β → «σ»} {h : α → γ → «σ»} :
primrec fprimrec₂ gprimrec₂ hprimrec (λ (a : α), (f a).cases_on (g a) (h a))

theorem primrec.list_cons {α : Type u_1} [primcodable α] :

theorem primrec.list_cases {α : Type u_1} {β : Type u_2} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → list β} {g : α → «σ»} {h : α → β × list β → «σ»} :
primrec fprimrec gprimrec₂ hprimrec (λ (a : α), (f a).cases_on (g a) (λ (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 fprimrec gprimrec₂ hprimrec (λ (a : α), list.foldl (λ (s : «σ») (b : β), h a (s, b)) (g a) (f a))

theorem primrec.list_reverse {α : Type u_1} [primcodable α] :

theorem primrec.list_foldr {α : Type u_1} {β : Type u_2} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → list β} {g : α → «σ»} {h : α → β × «σ» → «σ»} :
primrec fprimrec gprimrec₂ hprimrec (λ (a : α), list.foldr (λ (b : β) (s : «σ»), h a (b, s)) (g a) (f a))

theorem primrec.list_head' {α : Type u_1} [primcodable α] :

theorem primrec.list_head {α : Type u_1} [primcodable α] [inhabited α] :

theorem primrec.list_tail {α : Type u_1} [primcodable α] :

theorem primrec.list_rec {α : Type u_1} {β : Type u_2} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → list β} {g : α → «σ»} {h : α → β × list β × «σ» → «σ»} :
primrec fprimrec gprimrec₂ hprimrec (λ (a : α), (f a).rec_on (g a) (λ (b : β) (l : list β) (IH : «σ»), h a (b, l, IH)))

theorem primrec.list_nth {α : Type u_1} [primcodable α] :

theorem primrec.list_inth {α : Type u_1} [primcodable α] [inhabited α] :

theorem primrec.list_append {α : Type u_1} [primcodable α] :

theorem primrec.list_concat {α : Type u_1} [primcodable α] :
primrec₂ (λ (l : list α) (a : α), l ++ [a])

theorem primrec.list_map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable «σ»] {f : α → list β} {g : α → β → «σ»} :
primrec fprimrec₂ gprimrec (λ (a : α), list.map (g a) (f a))

theorem primrec.list_join {α : Type u_1} [primcodable α] :

theorem primrec.list_length {α : Type u_1} [primcodable α] :

theorem primrec.list_find_index {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → list β} {p : α → β → Prop} [Π (a : α) (b : β), decidable (p a b)] :
primrec fprimrec_rel pprimrec (λ (a : α), list.find_index (p a) (f a))

theorem primrec.nat_strong_rec {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable «σ»] (f : α → → «σ») {g : α → list «σ»option «σ»} :
primrec₂ g(∀ (a : α) (n : ), g a (list.map (f a) (list.range n)) = some (f a n))primrec₂ f

def primcodable.subtype {α : Type u_1} [primcodable α] {p : α → Prop} [decidable_pred p] :

Equations
@[instance]
def primcodable.vector {α : Type u_1} [primcodable α] {n : } :

Equations
@[instance]
def primcodable.fin_arrow {α : Type u_1} [primcodable α] {n : } :
primcodable (fin n → α)

Equations
@[instance]
def primcodable.array {α : Type u_1} [primcodable α] {n : } :

Equations
@[instance]
def primcodable.ulower {α : Type u_1} [primcodable α] :

Equations
theorem primrec.subtype_val {α : Type u_1} [primcodable α] {p : α → Prop} [decidable_pred p] {hp : primrec_pred p} :

theorem primrec.subtype_val_iff {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : β → Prop} [decidable_pred p] {hp : primrec_pred p} {f : α → subtype p} :
primrec (λ (a : α), (f a).val) primrec f

theorem primrec.subtype_mk {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : β → Prop} [decidable_pred p] {hp : primrec_pred p} {f : α → β} {h : ∀ (a : α), p (f a)} :
primrec fprimrec (λ (a : α), f a, _⟩)

theorem primrec.option_get {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → option β} {h : ∀ (a : α), ((f a).is_some)} :
primrec fprimrec (λ (a : α), option.get _)

theorem primrec.ulower_down {α : Type u_1} [primcodable α] :

theorem primrec.ulower_up {α : Type u_1} [primcodable α] :

theorem primrec.fin_val_iff {α : Type u_1} [primcodable α] {n : } {f : α → fin n} :
primrec (λ (a : α), (f a).val) primrec f

theorem primrec.fin_val {n : } :

theorem primrec.vector_to_list {α : Type u_1} [primcodable α] {n : } :

theorem primrec.vector_to_list_iff {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {n : } {f : α → vector β n} :
primrec (λ (a : α), (f a).to_list) primrec f

theorem primrec.vector_cons {α : Type u_1} [primcodable α] {n : } :

theorem primrec.vector_length {α : Type u_1} [primcodable α] {n : } :

theorem primrec.vector_head {α : Type u_1} [primcodable α] {n : } :

theorem primrec.vector_tail {α : Type u_1} [primcodable α] {n : } :

theorem primrec.vector_nth {α : Type u_1} [primcodable α] {n : } :

theorem primrec.list_of_fn {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable «σ»] {n : } {f : fin nα → «σ»} :
(∀ (i : fin n), primrec (f i))primrec (λ (a : α), list.of_fn (λ (i : fin n), f i a))

theorem primrec.vector_of_fn {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable «σ»] {n : } {f : fin nα → «σ»} :
(∀ (i : fin n), primrec (f i))primrec (λ (a : α), vector.of_fn (λ (i : fin n), f i a))

theorem primrec.vector_nth' {α : Type u_1} [primcodable α] {n : } :

theorem primrec.vector_of_fn' {α : Type u_1} [primcodable α] {n : } :

theorem primrec.fin_app {σ : Type u_4} [primcodable «σ»] {n : } :

theorem primrec.fin_curry₁ {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable «σ»] {n : } {f : fin nα → «σ»} :
primrec₂ f ∀ (i : fin n), primrec (f i)

theorem primrec.fin_curry {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable «σ»] {n : } {f : α → fin n → «σ»} :

inductive nat.primrec' {n : } :
(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.

theorem nat.primrec'.to_prim {n : } {f : vector n} :

theorem nat.primrec'.of_eq {n : } {f g : vector n} :
nat.primrec' f(∀ (i : vector n), f i = g i)nat.primrec' g

theorem nat.primrec'.const {n : } (m : ) :
nat.primrec' (λ (v : vector n), m)

theorem nat.primrec'.tail {n : } {f : vector n} :
nat.primrec' fnat.primrec' (λ (v : vector n.succ), f v.tail)

def nat.primrec'.vec {n m : } :
(vector nvector m) → Prop

Equations
theorem nat.primrec'.nil {n : } :

theorem nat.primrec'.cons {n m : } {f : vector n} {g : vector nvector m} :

theorem nat.primrec'.comp' {n m : } {f : vector m} {g : vector nvector m} :
nat.primrec' fnat.primrec'.vec gnat.primrec' (λ (v : vector n), f (g v))

theorem nat.primrec'.comp₁ (f : ) (hf : nat.primrec' (λ (v : vector 1), f v.head)) {n : } {g : vector n} :
nat.primrec' gnat.primrec' (λ (v : vector n), f (g v))

theorem nat.primrec'.comp₂ (f : ) (hf : nat.primrec' (λ (v : vector 2), f v.head v.tail.head)) {n : } {g h : vector n} :
nat.primrec' gnat.primrec' hnat.primrec' (λ (v : vector n), f (g v) (h v))

theorem nat.primrec'.prec' {n : } {f g : vector n} {h : vector (n + 2)} :
nat.primrec' fnat.primrec' gnat.primrec' hnat.primrec' (λ (v : vector n), nat.elim (g v) (λ (y IH : ), h (y::ᵥIH::ᵥv)) (f v))

theorem nat.primrec'.pred  :
nat.primrec' (λ (v : vector 1), v.head.pred)

theorem nat.primrec'.add  :
nat.primrec' (λ (v : vector 2), v.head + v.tail.head)

theorem nat.primrec'.sub  :
nat.primrec' (λ (v : vector 2), v.head - v.tail.head)

theorem nat.primrec'.mul  :
nat.primrec' (λ (v : vector 2), (v.head) * v.tail.head)

theorem nat.primrec'.if_lt {n : } {a b f g : vector n} :
nat.primrec' anat.primrec' bnat.primrec' fnat.primrec' gnat.primrec' (λ (v : vector n), ite (a v < b v) (f v) (g v))

theorem nat.primrec'.unpair₁ {n : } {f : vector n} :
nat.primrec' fnat.primrec' (λ (v : vector n), (f v).unpair.fst)

theorem nat.primrec'.unpair₂ {n : } {f : vector n} :
nat.primrec' fnat.primrec' (λ (v : vector n), (f v).unpair.snd)

theorem nat.primrec'.of_prim {n : } {f : vector n} :

theorem nat.primrec'.prim_iff {n : } {f : vector n} :

theorem nat.primrec'.prim_iff₁ {f : } :
nat.primrec' (λ (v : vector 1), f v.head) primrec f

theorem nat.primrec'.prim_iff₂ {f : } :