# mathlib3documentation

computability.primrec

# The primitive recursive functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The primitive recursive functions are the least collection of functions `nat → nat` 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

The non-dependent recursor on naturals.

Equations
@[simp]
theorem nat.elim_zero {C : Sort u_1} (a : C) (f : C C) :
f 0 = a
@[simp]
theorem nat.elim_succ {C : Sort u_1} (a : C) (f : C C) (n : ) :
f n.succ = f n (nat.elim a f n)
def nat.cases {C : Sort u_1} (a : C) (f : C) :

Cases on whether the input is 0 or a successor.

Equations
• f = (λ (n : ) (_x : C), f n)
@[simp]
theorem nat.cases_zero {C : Sort u_1} (a : C) (f : C) :
f 0 = a
@[simp]
theorem nat.cases_succ {C : Sort u_1} (a : C) (f : C) (n : ) :
f n.succ = f n
@[simp, 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
inductive nat.primrec  :
( ) Prop

The primitive recursive functions `ℕ → ℕ`.

theorem nat.primrec.of_eq {f g : } (hf : nat.primrec f) (H : (n : ), f n = g n) :
theorem nat.primrec.const (n : ) :
nat.primrec (λ (_x : ), n)
@[protected]
theorem nat.primrec.id  :
theorem nat.primrec.prec1 {f : } (m : ) (hf : nat.primrec f) :
nat.primrec (λ (n : ), (λ (y IH : ), f IH)) n)
theorem nat.primrec.cases1 {f : } (m : ) (hf : nat.primrec f) :
theorem nat.primrec.cases {f g : } (hf : nat.primrec f) (hg : nat.primrec g) :
nat.primrec (nat.unpaired (λ (z n : ), nat.cases (f z) (λ (y : ), g y)) n))
@[protected]
theorem nat.primrec.swap' {f : } (hf : nat.primrec (nat.unpaired f)) :
theorem nat.primrec.pred  :
@[class]
structure primcodable (α : Type u_1) :
Type u_1

A `primcodable` type is an `encodable` type for which the encode/decode functions are primitive recursive.

Instances of this typeclass
Instances of other typeclasses for `primcodable`
• primcodable.has_sizeof_inst
@[protected, instance]
Equations
def primcodable.of_equiv (α : Type u_1) {β : Type u_2} [primcodable α] (e : β α) :

Builds a `primcodable` instance from an equivalence to a `primcodable` type.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def primcodable.option {α : Type u_1} [h : primcodable α] :
Equations
@[protected, instance]
Equations
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
@[protected]
theorem primrec.encode {α : Type u_1} [primcodable α] :
@[protected]
theorem primrec.decode {α : Type u_1} [primcodable α] :
theorem primrec.dom_denumerable {α : Type u_1} {β : Type u_2} [denumerable α] [primcodable β] {f : α β} :
nat.primrec (λ (n : ), encodable.encode (f n)))
theorem primrec.nat_iff {f : } :
theorem primrec.encdec {α : Type u_1} [primcodable α] :
primrec (λ (n : ),
theorem primrec.option_some {α : Type u_1} [primcodable α] :
theorem primrec.of_eq {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable σ] {f g : α σ} (hf : primrec f) (H : (n : α), f n = g n) :
theorem primrec.const {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable σ] (x : σ) :
primrec (λ (a : α), x)
@[protected]
theorem primrec.id {α : Type u_1} [primcodable α] :
theorem primrec.comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] {f : β σ} {g : α β} (hf : primrec f) (hg : primrec g) :
primrec (λ (a : α), f (g a))
theorem primrec.succ  :
theorem primrec.pred  :
theorem primrec.encode_iff {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable σ] {f : α σ} :
primrec (λ (a : α), encodable.encode (f a))
theorem primrec.of_nat_iff {α : Type u_1} {β : Type u_2} [denumerable α] [primcodable β] {f : α β} :
primrec (λ (n : ), f n))
@[protected]
theorem primrec.of_nat (α : Type u_1) [denumerable α] :
theorem primrec.option_some_iff {α : Type u_1} {σ : Type u_3} [primcodable α] [primcodable σ] {f : α σ} :
primrec (λ (a : α), option.some (f a))
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))
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))
@[protected, 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 : α γ} (hf : primrec f) (hg : primrec g) :
primrec (λ (a : α), (f a, g a))
theorem primrec.unpair  :
theorem primrec.list_nth₁ {α : Type u_1} [primcodable α] (l : list α) :
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
def primrec_pred {α : Type u_1} [primcodable α] (p : α Prop)  :
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 : α β σ} (hg : primrec₂ f) (H : (a : α) (b : β), f a b = g a b) :
theorem primrec₂.const {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] (x : σ) :
primrec₂ (λ (a : α) (b : β), x)
@[protected]
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₂.unpaired' {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))
theorem primrec₂.option_some_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] {f : α β σ} :
primrec₂ (λ (a : α) (b : β), option.some (f a b))
theorem primrec₂.of_nat_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [denumerable α] [denumerable β] [primcodable σ] {f : α β σ} :
primrec₂ (λ (m n : ), f m) n))
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 : α β γ} (hf : primrec f) (hg : primrec₂ g) :
primrec₂ (λ (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 (λ (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₂ (λ (a : α) (b : β), f (g a b) (h a b))
theorem primrec_pred.comp {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : β Prop} {f : α β} :
primrec_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_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 (λ (a : α) (b : β), R (f a b) (g a b))
theorem primrec_pred.of_eq {α : Type u_1} [primcodable α] {p q : α Prop} (hp : primrec_pred p) (H : (a : α), p a q a) :
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)] (hr : primrec_rel r) (H : (a : α) (b : β), r a b s a b) :
theorem primrec₂.swap {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] {f : α β σ} (h : primrec₂ f) :
theorem primrec₂.nat_iff {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] {f : α β σ} :
nat.primrec (nat.unpaired (λ (m n : ), encodable.encode m).bind (λ (a : α), option.map (f a) n)))))
theorem primrec₂.nat_iff' {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] {f : α β σ} :
primrec₂ (λ (m n : ), m).bind (λ (a : α), option.map (f a) n)))
theorem primrec.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable σ] {f : α × β σ} (hf : primrec f) :
primrec₂ (λ (a : α) (b : β), f (a, b))
theorem primrec.nat_elim {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α β} {g : α × β β} (hf : primrec f) (hg : primrec₂ g) :
primrec₂ (λ (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 : α × β β} (hf : primrec f) (hg : primrec g) (hh : primrec₂ h) :
primrec (λ (a : α), nat.elim (g a) (λ (n : ) (IH : β), h a (n, IH)) (f a))
theorem primrec.nat_elim₁ {α : Type u_1} [primcodable α] {f : α α} (a : α) (hf : primrec₂ f) :
theorem primrec.nat_cases' {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α β} {g : α β} (hf : primrec f) (hg : primrec₂ g) :
primrec₂ (λ (a : α), nat.cases (f a) (g a))
theorem primrec.nat_cases {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α } {g : α β} {h : α β} (hf : primrec f) (hg : primrec g) (hh : primrec₂ h) :
primrec (λ (a : α), nat.cases (g a) (h a) (f a))
theorem primrec.nat_cases₁ {α : Type u_1} [primcodable α] {f : α} (a : α) (hf : primrec 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 (λ (a : α), h a^[f a] (g a))
theorem primrec.option_cases {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable σ] {o : α } {f : α σ} {g : α β σ} (ho : primrec o) (hf : primrec f) (hg : primrec₂ g) :
primrec (λ (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 : α } {g : α β } (hf : primrec f) (hg : primrec₂ g) :
primrec (λ (a : α), (f a).bind (g a))
theorem primrec.option_bind₁ {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable σ] {f : α } (hf : primrec f) :
primrec (λ (o : option α), o.bind f)
theorem primrec.option_map {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable σ] {f : α } {g : α β σ} (hf : primrec f) (hg : primrec₂ g) :
primrec (λ (a : α), option.map (g a) (f a))
theorem primrec.option_map₁ {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable σ] {f : α σ} (hf : primrec f) :
theorem primrec.option_iget {α : Type u_1} [primcodable α] [inhabited α] :
theorem primrec.option_is_some {α : Type u_1} [primcodable α] :
theorem primrec.option_get_or_else {α : Type u_1} [primcodable α] :
theorem primrec.bind_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_5} [primcodable α] [primcodable β] [primcodable σ] {f : α β } :
primrec₂ (λ (a : α) (n : ), n).bind (f a))
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) n))
theorem primrec.nat_sub  :
theorem primrec.nat_mul  :
theorem primrec.cond {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable σ] {c : α bool} {f g : α σ} (hc : primrec c) (hf : primrec f) (hg : primrec g) :
primrec (λ (a : α), cond (c a) (f a) (g a))
theorem primrec.ite {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable σ] {c : α Prop} {f g : α σ} (hc : primrec_pred c) (hf : primrec f) (hg : primrec g) :
primrec (λ (a : α), ite (c a) (f a) (g a))
theorem primrec.nat_le  :
theorem primrec.dom_bool {α : Type u_1} [primcodable α] (f : bool α) :
theorem primrec.dom_bool₂ {α : Type u_1} [primcodable α] (f : bool ) :
@[protected]
theorem primrec.bnot  :
@[protected]
theorem primrec.band  :
@[protected]
theorem primrec.bor  :
@[protected]
theorem primrec.not {α : Type u_1} [primcodable α] {p : α Prop} (hp : primrec_pred p) :
primrec_pred (λ (a : α), ¬p a)
@[protected]
theorem primrec.and {α : Type u_1} [primcodable α] {p q : α Prop} (hp : primrec_pred p) (hq : primrec_pred q) :
primrec_pred (λ (a : α), p a q a)
@[protected]
theorem primrec.or {α : Type u_1} [primcodable α] {p q : α Prop} (hp : primrec_pred p) (hq : primrec_pred q) :
primrec_pred (λ (a : α), p a q a)
@[protected]
theorem primrec.eq {α : Type u_1} [primcodable α] [decidable_eq α] :
theorem primrec.nat_lt  :
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 : α β} (hf : primrec f) :
primrec (λ (a : α), option.guard (p a) (f a))
theorem primrec.option_orelse {α : Type u_1} [primcodable α] :
@[protected]
theorem primrec.decode₂ {α : 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 : α), l)
theorem primrec.dom_fintype {α : Type u_1} {σ : Type u_5} [primcodable α] [primcodable σ] [fintype α] (f : α σ) :
theorem primrec.nat_bodd  :
theorem primrec.nat_div2  :
theorem primrec.nat_bit0  :
theorem primrec.nat_bit1  :
theorem primrec.nat_bit  :
theorem primrec.nat_div_mod  :
primrec₂ (λ (n k : ), (n / k, n % k))
theorem primrec.nat_div  :
theorem primrec.nat_mod  :
@[protected, instance]
def primcodable.sum {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
Equations
@[protected, instance]
def primcodable.list {α : Type u_1} [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 : α γ σ} (hf : primrec f) (hg : primrec₂ g) (hh : primrec₂ h) :
primrec (λ (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 (λ (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 (λ (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 : α β × σ σ} (hf : primrec f) (hg : primrec g) (hh : primrec₂ h) :
primrec (λ (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 β × σ σ} (hf : primrec f) (hg : primrec g) (hh : primrec₂ h) :
primrec (λ (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_nthd {α : Type u_1} [primcodable α] (d : α) :
primrec₂ (λ (l : list α) (n : ), l.nthd n d)
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 : α β σ} (hf : primrec f) (hg : primrec₂ g) :
primrec (λ (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)] (hf : primrec f) (hp : primrec_rel p) :
primrec (λ (a : α), list.find_index (p a) (f a))
theorem primrec.list_index_of {α : Type u_1} [primcodable α] [decidable_eq α] :
theorem primrec.nat_strong_rec {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] (f : α σ) {g : α list σ } (hg : primrec₂ g) (H : (a : α) (n : ), g a (list.map (f a) (list.range n)) = option.some (f a n)) :
def primcodable.subtype {α : Type u_1} [primcodable α] {p : α Prop} (hp : primrec_pred p) :

A subtype of a primitive recursive predicate is `primcodable`.

Equations
@[protected, instance]
def primcodable.fin {n : } :
Equations
@[protected, instance]
def primcodable.vector {α : Type u_1} [primcodable α] {n : } :
Equations
@[protected, instance]
def primcodable.fin_arrow {α : Type u_1} [primcodable α] {n : } :
Equations
@[protected, instance]
def primcodable.array {α : Type u_1} [primcodable α] {n : } :
Equations
@[protected, instance]
def primcodable.ulower {α : Type u_1} [primcodable α] :
Equations
theorem primrec.subtype_val {α : Type u_1} [primcodable α] {p : α Prop} {hp : primrec_pred p} :
theorem primrec.subtype_val_iff {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : β Prop} {hp : primrec_pred p} {f : α } :
primrec (λ (a : α), (f a).val)
theorem primrec.subtype_mk {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {p : β Prop} {hp : primrec_pred p} {f : α β} {h : (a : α), p (f a)} (hf : primrec f) :
primrec (λ (a : α), f a, _⟩)
theorem primrec.option_get {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α } {h : (a : α), ((f a).is_some)} :
primrec (λ (a : α),
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)
theorem primrec.fin_val {n : } :
theorem primrec.fin_succ {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 : α n} :
primrec (λ (a : α), (f a).to_list)
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 α σ} (hf : (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 α σ} :
(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 : } :
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 : n } (pf : nat.primrec' f) :
theorem nat.primrec'.of_eq {n : } {f g : n } (hf : nat.primrec' f) (H : (i : n), f i = g i) :
theorem nat.primrec'.const {n : } (m : ) :
nat.primrec' (λ (v : n), m)
theorem nat.primrec'.head {n : } :
theorem nat.primrec'.tail {n : } {f : n } (hf : nat.primrec' f) :
nat.primrec' (λ (v : n.succ), f v.tail)
def nat.primrec'.vec {n m : } (f : n m) :
Prop

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

Equations
@[protected]
theorem nat.primrec'.nil {n : } :
@[protected]
theorem nat.primrec'.cons {n m : } {f : n } {g : n m} (hf : nat.primrec' f) (hg : nat.primrec'.vec g) :
nat.primrec'.vec (λ (v : n), f v ::ᵥ g v)
theorem nat.primrec'.idv {n : } :
theorem nat.primrec'.comp' {n m : } {f : m } {g : n m} (hf : nat.primrec' f) (hg : nat.primrec'.vec g) :
nat.primrec' (λ (v : n), f (g v))
theorem nat.primrec'.comp₁ (f : ) (hf : nat.primrec' (λ (v : 1), f v.head)) {n : } {g : n } (hg : nat.primrec' g) :
nat.primrec' (λ (v : n), f (g v))
theorem nat.primrec'.comp₂ (f : ) (hf : nat.primrec' (λ (v : 2), f v.head v.tail.head)) {n : } {g h : n } (hg : nat.primrec' g) (hh : nat.primrec' h) :
nat.primrec' (λ (v : n), f (g v) (h v))
theorem nat.primrec'.prec' {n : } {f g : n } {h : (n + 2) } (hf : nat.primrec' f) (hg : nat.primrec' g) (hh : nat.primrec' h) :
nat.primrec' (λ (v : n), nat.elim (g v) (λ (y IH : ), h (y ::ᵥ IH ::ᵥ v)) (f v))
theorem nat.primrec'.pred  :
nat.primrec' (λ (v : 1), v.head.pred)
theorem nat.primrec'.sub  :
theorem nat.primrec'.mul  :
theorem nat.primrec'.if_lt {n : } {a b f g : n } (ha : nat.primrec' a) (hb : nat.primrec' b) (hf : nat.primrec' f) (hg : nat.primrec' g) :
nat.primrec' (λ (v : n), ite (a v < b v) (f v) (g v))
theorem nat.primrec'.mkpair  :
nat.primrec' (λ (v : 2), v.tail.head)
@[protected]
theorem nat.primrec'.encode {n : } :
theorem nat.primrec'.sqrt  :
nat.primrec' (λ (v : 1), nat.sqrt v.head)
theorem nat.primrec'.unpair₁ {n : } {f : n } (hf : nat.primrec' f) :
nat.primrec' (λ (v : n), (nat.unpair (f v)).fst)
theorem nat.primrec'.unpair₂ {n : } {f : n } (hf : nat.primrec' f) :
nat.primrec' (λ (v : n), (nat.unpair (f v)).snd)
theorem nat.primrec'.of_prim {n : } {f : n } :
theorem nat.primrec'.prim_iff {n : } {f : n } :
theorem nat.primrec'.prim_iff₁ {f : } :
nat.primrec' (λ (v : 1), f v.head)
theorem nat.primrec'.prim_iff₂ {f : } :