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} (a : C) (f : → 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, reducible]
def nat.unpaired {α : Sort u_1} (f : → α) (n : ) :
α
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.prec1 {f : } (m : ) (hf : nat.primrec f) :
nat.primrec (λ (n : ), nat.elim m (λ (y IH : ), f (nat.mkpair y 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 (nat.mkpair z y)) n))
@[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]
def primcodable.of_denumerable (α : Type u_1) [denumerable α] :
Equations
def primcodable.of_equiv (α : Type u_1) {β : Type u_2} [primcodable α] (e : β α) :
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 : α → β} :
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 : α → σ} (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.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))
@[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)) 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
@[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.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) [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 : α → β → σ} (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₂.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 : β), option.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 : α → β → γ} (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} [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] (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 : α → β → σ} :
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 : α × β → σ} (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 : α → option β} {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 : α → option β} {g : α → β → option σ} (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 : α → option σ} (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 : α → option β} {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.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 : α → σ} (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} [decidable_pred c] {f g : α → σ} (hc : primrec_pred c) (hf : primrec f) (hg : primrec g) :
primrec (λ (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 → α) :
@[protected]
theorem primrec.bnot  :
@[protected]
@[protected]
theorem primrec.bor  :
@[protected]
theorem primrec.not {α : Type u_1} [primcodable α] {p : α → Prop} [decidable_pred p] (hp : primrec_pred p) :
primrec_pred (λ (a : α), ¬p a)
@[protected]
theorem primrec.and {α : Type u_1} [primcodable α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] (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} [decidable_pred p] [decidable_pred q] (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.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))
@[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 : α), 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))
@[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 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 : α → β × σ → σ} (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 : α) :
theorem primrec.list_inth {α : Type u_1} [primcodable α] [inhabited α] :
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.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)) = option.some (f a n)) :
def primcodable.subtype {α : Type u_1} [primcodable α] {p : α → Prop} [decidable_pred p] (hp : primrec_pred p) :
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 : } :
primcodable (fin 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} [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)} (hf : primrec f) :
primrec (λ (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α → σ} (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α → σ} :
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} (pf : nat.primrec' f) :
theorem nat.primrec'.of_eq {n : } {f g : vector n} (hf : nat.primrec' f) (H : ∀ (i : vector n), f i = g i) :
theorem nat.primrec'.const {n : } (m : ) :
nat.primrec' (λ (v : vector n), m)
theorem nat.primrec'.tail {n : } {f : vector n} (hf : nat.primrec' f) :
nat.primrec' (λ (v : vector n.succ), f v.tail)
def nat.primrec'.vec {n m : } (f : vector nvector m) :
Prop
Equations
@[protected]
theorem nat.primrec'.nil {n : } :
@[protected]
theorem nat.primrec'.cons {n m : } {f : vector n} {g : vector nvector m} (hf : nat.primrec' f) (hg : nat.primrec'.vec g) :
nat.primrec'.vec (λ (v : vector n), f v ::ᵥ g v)
theorem nat.primrec'.comp' {n m : } {f : vector m} {g : vector nvector m} (hf : nat.primrec' f) (hg : nat.primrec'.vec g) :
nat.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} (hg : nat.primrec' g) :
nat.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} (hg : nat.primrec' g) (hh : nat.primrec' h) :
nat.primrec' (λ (v : vector n), f (g v) (h v))
theorem nat.primrec'.prec' {n : } {f g : vector n} {h : vector (n + 2)} (hf : nat.primrec' f) (hg : nat.primrec' g) (hh : nat.primrec' h) :
nat.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} (ha : nat.primrec' a) (hb : nat.primrec' b) (hf : nat.primrec' f) (hg : nat.primrec' g) :
nat.primrec' (λ (v : vector n), ite (a v < b v) (f v) (g v))
theorem nat.primrec'.unpair₁ {n : } {f : vector n} (hf : nat.primrec' f) :
nat.primrec' (λ (v : vector n), (nat.unpair (f v)).fst)
theorem nat.primrec'.unpair₂ {n : } {f : vector n} (hf : nat.primrec' f) :
nat.primrec' (λ (v : vector n), (nat.unpair (f v)).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 : } :