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 #
@[simp, reducible]
Calls the given function on a pair of entries n, encoded via the pairing function.
Equations
- nat.unpaired f n = f (nat.unpair n).fst (nat.unpair n).snd
- zero : nat.primrec (λ (n : ℕ), 0)
- succ : nat.primrec nat.succ
- left : nat.primrec (λ (n : ℕ), (nat.unpair n).fst)
- right : nat.primrec (λ (n : ℕ), (nat.unpair n).snd)
- pair : ∀ {f g : ℕ → ℕ}, nat.primrec f → nat.primrec g → nat.primrec (λ (n : ℕ), nat.mkpair (f n) (g n))
- comp : ∀ {f g : ℕ → ℕ}, nat.primrec f → nat.primrec g → nat.primrec (λ (n : ℕ), f (g n))
- prec : ∀ {f g : ℕ → ℕ}, nat.primrec f → nat.primrec g → nat.primrec (nat.unpaired (λ (z n : ℕ), nat.elim (f z) (λ (y IH : ℕ), g (nat.mkpair z (nat.mkpair y IH))) n))
The primitive recursive functions ℕ → ℕ.
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.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))
@[protected]
@[class]
- to_encodable : encodable α
- prim : nat.primrec (λ (n : ℕ), encodable.encode (encodable.decode α n))
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
- primcodable.of_denumerable α = {to_encodable := denumerable.to_encodable _inst_1, prim := _}
Builds a primcodable instance from an equivalence to a primcodable type.
Equations
- primcodable.of_equiv α e = {to_encodable := {encode := encodable.encode (encodable.of_equiv α e), decode := encodable.decode β (encodable.of_equiv α e), encodek := _}, prim := _}
@[protected, instance]
Equations
@[protected, instance]
Equations
- primcodable.unit = {to_encodable := punit.encodable, prim := primcodable.unit._proof_1}
@[protected, instance]
Equations
@[protected, instance]
Equations
- primcodable.bool = {to_encodable := bool.encodable, prim := primcodable.bool._proof_1}
primrec f means f is primitive recursive (after
encoding its input and output as natural numbers).
Equations
- primrec f = nat.primrec (λ (n : ℕ), encodable.encode (option.map f (encodable.decode α n)))
@[protected]
@[protected]
theorem
primrec.dom_denumerable
{α : Type u_1}
{β : Type u_2}
[denumerable α]
[primcodable β]
{f : α → β} :
primrec f ↔ nat.primrec (λ (n : ℕ), encodable.encode (f (denumerable.of_nat α n)))
theorem
primrec.encdec
{α : Type u_1}
[primcodable α] :
primrec (λ (n : ℕ), encodable.encode (encodable.decode α n))
theorem
primrec.of_eq
{α : Type u_1}
{σ : Type u_3}
[primcodable α]
[primcodable σ]
{f g : α → σ}
(hf : primrec f)
(H : ∀ (n : α), f n = g n) :
primrec g
theorem
primrec.const
{α : Type u_1}
{σ : Type u_3}
[primcodable α]
[primcodable σ]
(x : σ) :
primrec (λ (a : α), x)
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.option_some_iff
{α : Type u_1}
{σ : Type u_3}
[primcodable α]
[primcodable σ]
{f : α → σ} :
primrec (λ (a : α), option.some (f a)) ↔ primrec f
theorem
primrec.of_equiv_iff
{α : Type u_1}
{σ : Type u_3}
[primcodable α]
[primcodable σ]
{β : Type u_2}
(e : β ≃ α)
{f : σ → β} :
theorem
primrec.of_equiv_symm_iff
{α : Type u_1}
{σ : Type u_3}
[primcodable α]
[primcodable σ]
{β : Type u_2}
(e : β ≃ α)
{f : σ → α} :
@[protected, instance]
def
primcodable.prod
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β] :
primcodable (α × β)
Equations
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))
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.
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
- primrec_pred p = primrec (λ (a : α), decidable.to_bool (p a))
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
- primrec_rel s = primrec₂ (λ (a : α) (b : β), decidable.to_bool (s a b))
theorem
primrec₂.of_eq
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
{f g : α → β → σ}
(hg : primrec₂ f)
(H : ∀ (a : α) (b : β), f a b = g a b) :
primrec₂ g
theorem
primrec₂.const
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
(x : σ) :
primrec₂ (λ (a : α) (b : β), x)
@[protected]
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 : ℕ → ℕ → α} :
primrec (nat.unpaired f) ↔ primrec₂ 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 : α → β → σ} :
primrec₂ f ↔ primrec₂ (λ (m n : ℕ), f (denumerable.of_nat α m) (denumerable.of_nat β n))
theorem
primrec₂.uncurry
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α → β → σ} :
primrec (function.uncurry f) ↔ primrec₂ f
theorem
primrec₂.curry
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α × β → σ} :
primrec₂ (function.curry f) ↔ primrec f
theorem
primrec.comp₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{σ : Type u_5}
[primcodable α]
[primcodable β]
[primcodable γ]
[primcodable σ]
{f : γ → σ}
{g : α → β → γ}
(hf : primrec f)
(hg : primrec₂ g) :
primrec₂ (λ (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 p → primrec 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_rel R → primrec f → primrec 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 R → primrec₂ f → primrec₂ g → primrec_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 : α → β → σ} :
primrec₂ f ↔ nat.primrec (nat.unpaired (λ (m n : ℕ), encodable.encode ((encodable.decode α m).bind (λ (a : α), option.map (f a) (encodable.decode β n)))))
theorem
primrec₂.nat_iff'
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α → β → σ} :
primrec₂ f ↔ primrec₂ (λ (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}
[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) :
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) :
theorem
primrec.option_bind₁
{α : Type u_1}
{σ : Type u_5}
[primcodable α]
[primcodable σ]
{f : α → option σ}
(hf : primrec 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) :
primrec (option.map f)
theorem
primrec.bind_decode_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_5}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α → β → option σ} :
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) :
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) :
@[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.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.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 : α → σ) :
primrec f
@[protected, instance]
def
primcodable.sum
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β] :
primcodable (α ⊕ β)
Equations
@[protected, instance]
Equations
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_foldl
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α → list β}
{g : α → σ}
{h : α → σ × β → σ} :
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_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) :
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) :
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)) :
primrec₂ f
def
primcodable.subtype
{α : Type u_1}
[primcodable α]
{p : α → Prop}
[decidable_pred p]
(hp : primrec_pred p) :
primcodable (subtype p)
A subtype of a primitive recursive predicate is primcodable.
Equations
- primcodable.subtype hp = {to_encodable := subtype.encodable (λ (a : α), _inst_3 a), prim := _}
@[protected, instance]
Equations
- primcodable.fin = primcodable.of_equiv {a // id a < n} fin.equiv_subtype
@[protected, instance]
Equations
- primcodable.vector = primcodable.subtype primcodable.vector._proof_1
@[protected, instance]
Equations
@[protected, instance]
Equations
- primcodable.array = primcodable.of_equiv (fin n → α) (equiv.array_equiv_fin n α)
@[protected, instance]
Equations
- primcodable.ulower = have this : primrec_pred (λ (n : ℕ), encodable.decode₂ α n ≠ option.none), from primcodable.ulower._proof_2, primcodable.subtype _
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} :
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) :
theorem
primrec.option_get
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{f : α → option β}
{h : ∀ (a : α), ↥((f a).is_some)} :
primrec f → primrec (λ (a : α), option.get _)
theorem
primrec.vector_to_list_iff
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{n : ℕ}
{f : α → vector β n} :
theorem
primrec.list_of_fn
{α : Type u_1}
{σ : Type u_4}
[primcodable α]
[primcodable σ]
{n : ℕ}
{f : fin n → α → σ} :
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.fin_curry₁
{α : Type u_1}
{σ : Type u_4}
[primcodable α]
[primcodable σ]
{n : ℕ}
{f : fin n → α → σ} :
theorem
primrec.fin_curry
{α : Type u_1}
{σ : Type u_4}
[primcodable α]
[primcodable σ]
{n : ℕ}
{f : α → fin n → σ} :
- zero : nat.primrec' (λ (_x : vector ℕ 0), 0)
- succ : nat.primrec' (λ (v : vector ℕ 1), v.head.succ)
- nth : ∀ {n : ℕ} (i : fin n), nat.primrec' (λ (v : vector ℕ n), v.nth i)
- comp : ∀ {m n : ℕ} {f : vector ℕ n → ℕ} (g : fin n → vector ℕ m → ℕ), nat.primrec' f → (∀ (i : fin n), nat.primrec' (g i)) → nat.primrec' (λ (a : vector ℕ m), f (vector.of_fn (λ (i : fin n), g i a)))
- prec : ∀ {n : ℕ} {f : vector ℕ n → ℕ} {g : vector ℕ (n + 2) → ℕ}, nat.primrec' f → nat.primrec' g → nat.primrec' (λ (v : vector ℕ (n + 1)), nat.elim (f v.tail) (λ (y IH : ℕ), g (y ::ᵥ IH ::ᵥ v.tail)) v.head)
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'.tail
{n : ℕ}
{f : vector ℕ n → ℕ}
(hf : nat.primrec' f) :
nat.primrec' (λ (v : vector ℕ n.succ), f v.tail)
@[protected]
@[protected]
theorem
nat.primrec'.cons
{n m : ℕ}
{f : vector ℕ n → ℕ}
{g : vector ℕ n → vector ℕ 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 ℕ n → vector ℕ 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) :
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)