The primitive recursive functions #
The primitive recursive functions are the least collection of functions
ℕ → ℕ which are closed under projections (using the pair
pairing function), composition, zero, successor, and primitive recursion
(i.e. Nat.rec where the motive is C n := ℕ).
We can extend this definition to a large class of basic types by
using canonical encodings of types as natural numbers (Gödel numbering),
which we implement through the type class Encodable. (More precisely,
we need that the composition of encode with decode yields a
primitive recursive function, so we have the Primcodable type class
for this.)
In the above, the pairing function is primitive recursive by definition.
This deviates from the textbook definition of primitive recursive functions,
which instead work with n-ary functions. We formalize the textbook
definition in Nat.Primrec'. Nat.Primrec'.prim_iff then proves it is
equivalent to our chosen formulation. For more discussionn of this and
other design choices in this formalization, see [carneiro2019].
Main definitions #
Nat.Primrec f:fis primitive recursive, for functionsf : ℕ → ℕPrimrec f:fis primitive recursive, for functions betweenPrimcodabletypesPrimcodable α: well-behaved encoding ofαintoℕ, i.e. one such that roundtripping through the encoding functions adds no computational power
References #
- [Mario Carneiro, Formalizing computability theory via partial recursive functions][carneiro2019]
@[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).1 (Nat.unpair n).2
Instances For
The primitive recursive functions ℕ → ℕ.
- zero : Nat.Primrec fun (x : ℕ) => 0
- succ : Nat.Primrec succ
- left : Nat.Primrec fun (n : ℕ) => (unpair n).1
- right : Nat.Primrec fun (n : ℕ) => (unpair n).2
- pair {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun (n : ℕ) => Nat.pair (f n) (g n)
- comp {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun (n : ℕ) => f (g n)
- prec {f g : ℕ → ℕ} : Nat.Primrec f → Nat.Primrec g → Nat.Primrec (unpaired fun (z n : ℕ) => Nat.rec (f z) (fun (y IH : ℕ) => g (Nat.pair z (Nat.pair y IH))) n)
Instances For
theorem
Nat.Primrec.prec1
{f : ℕ → ℕ}
(m : ℕ)
(hf : Nat.Primrec f)
:
Nat.Primrec fun (n : ℕ) => Nat.rec m (fun (y IH : ℕ) => f (Nat.pair y IH)) n
theorem
Nat.Primrec.casesOn1
{f : ℕ → ℕ}
(m : ℕ)
(hf : Nat.Primrec f)
:
Nat.Primrec fun (x : ℕ) => Nat.casesOn x m f
theorem
Nat.Primrec.casesOn'
{f g : ℕ → ℕ}
(hf : Nat.Primrec f)
(hg : Nat.Primrec g)
:
Nat.Primrec (unpaired fun (z n : ℕ) => Nat.casesOn n (f z) fun (y : ℕ) => g (Nat.pair z y))
theorem
Nat.Primrec.swap'
{f : ℕ → ℕ → ℕ}
(hf : Nat.Primrec (unpaired f))
:
Nat.Primrec (unpaired (Function.swap f))
A Primcodable type is, essentially, an Encodable type for which
the encode/decode functions are primitive recursive.
However, such a definition is circular.
Instead, we ask that the composition of decode : ℕ → Option α with
encode : Option α → ℕ is primitive recursive. Said composition is
the identity function, restricted to the image of encode.
Thus, in a way, the added requirement ensures that no predicates
can be smuggled in through a cunning choice of the subset of ℕ into
which the type is encoded.
- prim : Nat.Primrec fun (n : ℕ) => Encodable.encode (Encodable.decode n)
Instances
@[instance 10]
Equations
- Primcodable.ofDenumerable α = { toEncodable := Denumerable.toEncodable, prim := ⋯ }
Builds a Primcodable instance from an equivalence to a Primcodable type.
Equations
- Primcodable.ofEquiv α e = { toEncodable := Encodable.ofEquiv α e, prim := ⋯ }
Instances For
Equations
- Primcodable.empty = { toEncodable := IsEmpty.toEncodable, prim := Nat.Primrec.zero }
Equations
- Primcodable.unit = { toEncodable := PUnit.encodable, prim := Primcodable.unit._proof_3 }
Equations
- Primcodable.option = { toEncodable := Option.encodable, prim := ⋯ }
Equations
- Primcodable.bool = { toEncodable := Bool.encodable, prim := Primcodable.bool._proof_5 }
Primrec f means f is primitive recursive (after
encoding its input and output as natural numbers).
Equations
- Primrec f = Nat.Primrec fun (n : ℕ) => Encodable.encode (Option.map f (Encodable.decode n))
Instances For
theorem
Primrec.dom_denumerable
{α : Type u_4}
{β : Type u_5}
[Denumerable α]
[Primcodable β]
{f : α → β}
:
theorem
Primrec.encdec
{α : Type u_1}
[Primcodable α]
:
Primrec fun (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 fun (x_1 : α) => 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 fun (a : α) => f (g a)
theorem
Primrec.encode_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
:
theorem
Primrec.ofNat_iff
{α : Type u_4}
{β : Type u_5}
[Denumerable α]
[Primcodable β]
{f : α → β}
:
theorem
Primrec.option_some_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
:
theorem
Primrec.of_equiv_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{β : Type u_4}
(e : β ≃ α)
{f : σ → β}
:
theorem
Primrec.of_equiv_symm_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{β : Type u_4}
(e : β ≃ α)
{f : σ → α}
:
instance
Primcodable.prod
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primcodable (α × β)
Equations
- Primcodable.prod = { toEncodable := Encodable.Prod.encodable, prim := ⋯ }
theorem
Primrec.pair
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{f : α → β}
{g : α → γ}
(hf : Primrec f)
(hg : Primrec g)
:
@[deprecated Primrec.list_getElem?₁ (since := "2025-02-14")]
Alias of Primrec.list_getElem?₁.
def
Primrec₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
(f : α → β → σ)
:
Primrec₂ f means f is a binary primitive recursive function.
This is technically unnecessary since we can always curry all
the arguments together, but there are enough natural two-arg
functions that it is convenient to express this directly.
Instances For
PrimrecPred p means p : α → Prop is a (decidable)
primitive recursive predicate, which is to say that
decide ∘ p : α → Bool is primitive recursive.
Equations
- PrimrecPred p = Primrec fun (a : α) => decide (p a)
Instances For
def
PrimrecRel
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
(s : α → β → Prop)
[(a : α) → (b : β) → Decidable (s a b)]
:
PrimrecRel p means p : α → β → Prop is a (decidable)
primitive recursive relation, which is to say that
decide ∘ p : α → β → Bool is primitive recursive.
Equations
- PrimrecRel s = Primrec₂ fun (a : α) (b : β) => decide (s a b)
Instances For
theorem
Primrec₂.mk
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
(hf : Primrec fun (p : α × β) => f p.1 p.2)
:
Primrec₂ f
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₂ fun (x_1 : α) (x_2 : β) => x
theorem
Primrec₂.left
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primrec₂ fun (a : α) (x : β) => a
theorem
Primrec₂.right
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primrec₂ fun (x : α) (b : β) => b
theorem
Primrec₂.encode_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
theorem
Primrec₂.option_some_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
theorem
Primrec₂.ofNat_iff
{α : Type u_4}
{β : Type u_5}
{σ : Type u_6}
[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₂ fun (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 fun (a : α) => f (g a) (h a)
theorem
Primrec₂.comp₂
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{σ : Type u_5}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
[Primcodable δ]
[Primcodable σ]
{f : γ → δ → σ}
{g : α → β → γ}
{h : α → β → δ}
(hf : Primrec₂ f)
(hg : Primrec₂ g)
(hh : Primrec₂ h)
:
Primrec₂ fun (a : α) (b : β) => f (g a b) (h a b)
theorem
PrimrecPred.comp
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : β → Prop}
[DecidablePred p]
{f : α → β}
:
PrimrecPred p → Primrec f → PrimrecPred fun (a : α) => p (f a)
theorem
PrimrecRel.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{R : β → γ → Prop}
[(a : β) → (b : γ) → Decidable (R a b)]
{f : α → β}
{g : α → γ}
:
PrimrecRel R → Primrec f → Primrec g → PrimrecPred fun (a : α) => R (f a) (g a)
theorem
PrimrecRel.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 : α → β → δ}
:
PrimrecRel R → Primrec₂ f → Primrec₂ g → PrimrecRel fun (a : α) (b : β) => R (f a b) (g a b)
theorem
PrimrecPred.of_eq
{α : Type u_1}
[Primcodable α]
{p q : α → Prop}
[DecidablePred p]
[DecidablePred q]
(hp : PrimrecPred p)
(H : ∀ (a : α), p a ↔ q a)
:
theorem
PrimrecRel.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 : PrimrecRel 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 fun (m n : ℕ) =>
Encodable.encode ((Encodable.decode m).bind fun (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₂ fun (m n : ℕ) => (Encodable.decode m).bind fun (a : α) => Option.map (f a) (Encodable.decode n)
theorem
Primrec.to₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α × β → σ}
(hf : Primrec f)
:
theorem
Primrec.nat_casesOn'
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → β}
{g : α → ℕ → β}
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec₂ fun (a : α) (n : ℕ) => Nat.casesOn n (f a) (g a)
theorem
Primrec.nat_casesOn
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → ℕ}
{g : α → β}
{h : α → ℕ → β}
(hf : Primrec f)
(hg : Primrec g)
(hh : Primrec₂ h)
:
Primrec fun (a : α) => Nat.casesOn (f a) (g a) (h a)
theorem
Primrec.nat_casesOn₁
{α : Type u_1}
[Primcodable α]
{f : ℕ → α}
(a : α)
(hf : Primrec f)
:
Primrec fun (n : ℕ) => Nat.casesOn n a 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)
:
theorem
Primrec.option_casesOn
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{o : α → Option β}
{f : α → σ}
{g : α → β → σ}
(ho : Primrec o)
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec fun (a : α) => Option.casesOn (o a) (f a) (g a)
theorem
Primrec.option_bind
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → Option β}
{g : α → β → Option σ}
(hf : Primrec f)
(hg : Primrec₂ g)
:
theorem
Primrec.option_bind₁
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → Option σ}
(hf : Primrec f)
:
theorem
Primrec.option_map
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → Option β}
{g : α → β → σ}
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec fun (a : α) => Option.map (g a) (f a)
theorem
Primrec.option_map₁
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
(hf : Primrec f)
:
Primrec (Option.map f)
theorem
Primrec.bind_decode_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → Option σ}
:
theorem
Primrec.map_decode_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
theorem
Primrec.cond
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{c : α → Bool}
{f g : α → σ}
(hc : Primrec c)
(hf : Primrec f)
(hg : Primrec g)
:
Primrec fun (a : α) => bif c a then f a else g a
theorem
Primrec.ite
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{c : α → Prop}
[DecidablePred c]
{f g : α → σ}
(hc : PrimrecPred c)
(hf : Primrec f)
(hg : Primrec g)
:
theorem
PrimrecPred.not
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
(hp : PrimrecPred p)
:
PrimrecPred fun (a : α) => ¬p a
theorem
PrimrecPred.and
{α : Type u_1}
[Primcodable α]
{p q : α → Prop}
[DecidablePred p]
[DecidablePred q]
(hp : PrimrecPred p)
(hq : PrimrecPred q)
:
PrimrecPred fun (a : α) => p a ∧ q a
theorem
PrimrecPred.or
{α : Type u_1}
[Primcodable α]
{p q : α → Prop}
[DecidablePred p]
[DecidablePred q]
(hp : PrimrecPred p)
(hq : PrimrecPred q)
:
PrimrecPred fun (a : α) => p a ∨ q a
theorem
Primrec.option_guard
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : α → β → Prop}
[(a : α) → (b : β) → Decidable (p a b)]
(hp : PrimrecRel p)
{f : α → β}
(hf : Primrec f)
:
Primrec fun (a : α) => Option.guard (fun (b : β) => decide (p a b)) (f a)
theorem
Primrec.list_findIdx₁
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : α → β → Bool}
(hp : Primrec₂ p)
(l : List β)
:
Primrec fun (a : α) => List.findIdx (p a) l
theorem
Primrec.list_idxOf₁
{α : Type u_1}
[Primcodable α]
[DecidableEq α]
(l : List α)
:
Primrec fun (a : α) => List.idxOf a l
@[deprecated Primrec.list_idxOf₁ (since := "2025-01-30")]
theorem
Primrec.list_indexOf₁
{α : Type u_1}
[Primcodable α]
[DecidableEq α]
(l : List α)
:
Primrec fun (a : α) => List.idxOf a l
Alias of Primrec.list_idxOf₁.
theorem
Primrec.dom_fintype
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
[Finite α]
(f : α → σ)
:
Primrec f
def
Primrec.PrimrecBounded
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
(f : α → β)
:
A function is PrimrecBounded if its size is bounded by a primitive recursive function
Equations
- Primrec.PrimrecBounded f = ∃ (g : α → ℕ), Primrec g ∧ ∀ (x : α), Encodable.encode (f x) ≤ g x
Instances For
theorem
Primrec.nat_findGreatest
{α : Type u_1}
[Primcodable α]
{f : α → ℕ}
{p : α → ℕ → Prop}
[(x : α) → (n : ℕ) → Decidable (p x n)]
(hf : Primrec f)
(hp : PrimrecRel p)
:
Primrec fun (x : α) => Nat.findGreatest (p x) (f x)
theorem
Primrec.of_graph
{α : Type u_1}
[Primcodable α]
{f : α → ℕ}
(h₁ : PrimrecBounded f)
(h₂ : PrimrecRel fun (a : α) (b : ℕ) => f a = b)
:
Primrec f
To show a function f : α → ℕ is primitive recursive, it is enough to show that the function
is bounded by a primitive recursive function and that its graph is primitive recursive
instance
Primcodable.sum
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primcodable (α ⊕ β)
Equations
- Primcodable.sum = { toEncodable := Sum.encodable, prim := ⋯ }
Equations
- Primcodable.list = { toEncodable := List.encodable, prim := ⋯ }
@[deprecated Primrec.sumInl (since := "2025-02-21")]
Alias of Primrec.sumInl.
@[deprecated Primrec.sumInr (since := "2025-02-21")]
Alias of Primrec.sumInr.
theorem
Primrec.sumCasesOn
{α : 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 fun (a : α) => Sum.casesOn (f a) (g a) (h a)
@[deprecated Primrec.sumCasesOn (since := "2025-02-21")]
theorem
Primrec.sum_casesOn
{α : 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 fun (a : α) => Sum.casesOn (f a) (g a) (h a)
Alias of Primrec.sumCasesOn.
theorem
Primrec.list_casesOn
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → List β}
{g : α → σ}
{h : α → β × List β → σ}
:
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 fun (a : α) => List.foldr (fun (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)
:
@[deprecated Primrec.list_getElem? (since := "2025-02-14")]
Alias of Primrec.list_getElem?.
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_flatMap
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → List β}
{g : α → β → List σ}
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec fun (a : α) => List.flatMap (g a) (f a)
theorem
Primrec.listFilterMap
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → List β}
{g : α → β → Option σ}
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec fun (a : α) => List.filterMap (g a) (f a)
theorem
Primrec.list_findIdx
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → List β}
{p : α → β → Bool}
(hf : Primrec f)
(hp : Primrec₂ p)
:
Primrec fun (a : α) => List.findIdx (p a) (f a)
@[deprecated Primrec.list_idxOf (since := "2025-01-30")]
Alias of Primrec.list_idxOf.
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)) = some (f a n))
:
Primrec₂ f
theorem
Primrec.listLookup
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
[DecidableEq α]
:
theorem
Primrec.nat_omega_rec'
{β : Type u_2}
{σ : Type u_4}
[Primcodable β]
[Primcodable σ]
(f : β → σ)
{m : β → ℕ}
{l : β → List β}
{g : β → List σ → Option σ}
(hm : Primrec m)
(hl : Primrec l)
(hg : Primrec₂ g)
(Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b)
(H : ∀ (b : β), g b (List.map f (l b)) = some (f b))
:
Primrec f
theorem
Primrec.nat_omega_rec
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
(f : α → β → σ)
{m : α → β → ℕ}
{l : α → β → List β}
{g : α → β × List σ → Option σ}
(hm : Primrec₂ m)
(hl : Primrec₂ l)
(hg : Primrec₂ g)
(Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b)
(H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b))
:
Primrec₂ f
def
Primcodable.subtype
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
(hp : PrimrecPred p)
:
Primcodable (Subtype p)
A subtype of a primitive recursive predicate is Primcodable.
Equations
- Primcodable.subtype hp = { toEncodable := Subtype.encodable, prim := ⋯ }
Instances For
Equations
- Primcodable.fin = Primcodable.ofEquiv { a : ℕ // id a < n } Fin.equivSubtype
Equations
Equations
theorem
Primcodable.mem_range_encode
{α : Type u_1}
[Primcodable α]
:
PrimrecPred fun (n : ℕ) => n ∈ Set.range Encodable.encode
Equations
theorem
Primrec.subtype_val
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
{hp : PrimrecPred p}
:
theorem
Primrec.subtype_val_iff
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : β → Prop}
[DecidablePred p]
{hp : PrimrecPred p}
{f : α → Subtype p}
:
theorem
Primrec.subtype_mk
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{p : β → Prop}
[DecidablePred p]
{hp : PrimrecPred 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).isSome = true}
:
theorem
Primrec.vector_toList_iff
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{n : ℕ}
{f : α → List.Vector β n}
:
theorem
Primrec.list_ofFn
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α → σ}
:
theorem
Primrec.vector_ofFn
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α → σ}
(hf : ∀ (i : Fin n), Primrec (f i))
:
Primrec fun (a : α) => List.Vector.ofFn fun (i : Fin n) => f i a
theorem
Primrec.fin_curry₁
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α → σ}
:
theorem
Primrec.fin_curry
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : α → Fin n → σ}
:
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.
- zero : Primrec' fun (x : List.Vector ℕ 0) => 0
- succ : Primrec' fun (v : List.Vector ℕ 1) => v.head.succ
- get {n : ℕ} (i : Fin n) : Primrec' fun (v : List.Vector ℕ n) => v.get i
- comp {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ) : Primrec' f → (∀ (i : Fin n), Primrec' (g i)) → Primrec' fun (a : List.Vector ℕ m) => f (List.Vector.ofFn fun (i : Fin n) => g i a)
- prec {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ} : Primrec' f → Primrec' g → Primrec' fun (v : List.Vector ℕ (n + 1)) => Nat.rec (f v.tail) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Instances For
theorem
Nat.Primrec'.of_eq
{n : ℕ}
{f g : List.Vector ℕ n → ℕ}
(hf : Primrec' f)
(H : ∀ (i : List.Vector ℕ n), f i = g i)
:
Primrec' g
theorem
Nat.Primrec'.tail
{n : ℕ}
{f : List.Vector ℕ n → ℕ}
(hf : Primrec' f)
:
Primrec' fun (v : List.Vector ℕ n.succ) => f v.tail
A function from vectors to vectors is primitive recursive when all of its projections are.
Equations
- Nat.Primrec'.Vec f = ∀ (i : Fin m), Nat.Primrec' fun (v : List.Vector ℕ n) => (f v).get i
Instances For
theorem
Nat.Primrec'.cons
{n m : ℕ}
{f : List.Vector ℕ n → ℕ}
{g : List.Vector ℕ n → List.Vector ℕ m}
(hf : Primrec' f)
(hg : Vec g)
:
Vec fun (v : List.Vector ℕ n) => f v ::ᵥ g v
theorem
Nat.Primrec'.comp'
{n m : ℕ}
{f : List.Vector ℕ m → ℕ}
{g : List.Vector ℕ n → List.Vector ℕ m}
(hf : Primrec' f)
(hg : Vec g)
:
Primrec' fun (v : List.Vector ℕ n) => f (g v)
theorem
Nat.Primrec'.comp₁
(f : ℕ → ℕ)
(hf : Primrec' fun (v : List.Vector ℕ 1) => f v.head)
{n : ℕ}
{g : List.Vector ℕ n → ℕ}
(hg : Primrec' g)
:
Primrec' fun (v : List.Vector ℕ n) => f (g v)
theorem
Nat.Primrec'.comp₂
(f : ℕ → ℕ → ℕ)
(hf : Primrec' fun (v : List.Vector ℕ 2) => f v.head v.tail.head)
{n : ℕ}
{g h : List.Vector ℕ n → ℕ}
(hg : Primrec' g)
(hh : Primrec' h)
:
Primrec' fun (v : List.Vector ℕ n) => f (g v) (h v)
theorem
Nat.Primrec'.prec'
{n : ℕ}
{f g : List.Vector ℕ n → ℕ}
{h : List.Vector ℕ (n + 2) → ℕ}
(hf : Primrec' f)
(hg : Primrec' g)
(hh : Primrec' h)
:
theorem
Nat.Primrec'.unpair₁
{n : ℕ}
{f : List.Vector ℕ n → ℕ}
(hf : Primrec' f)
:
Primrec' fun (v : List.Vector ℕ n) => (unpair (f v)).1
theorem
Nat.Primrec'.unpair₂
{n : ℕ}
{f : List.Vector ℕ n → ℕ}
(hf : Primrec' f)
:
Primrec' fun (v : List.Vector ℕ n) => (unpair (f v)).2