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.)
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
The primitive recursive functions ℕ → ℕ.
- zero: Nat.Primrec fun (x : ℕ) => 0
- succ: Nat.Primrec Nat.succ
- left: Nat.Primrec fun (n : ℕ) => (Nat.unpair n).1
- right: Nat.Primrec fun (n : ℕ) => (Nat.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 (Nat.unpaired fun (z n : ℕ) => Nat.rec (f z) (fun (y IH : ℕ) => g (Nat.pair z (Nat.pair y IH))) n)
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 (Nat.unpaired fun (z n : ℕ) => Nat.casesOn n (f z) fun (y : ℕ) => g (Nat.pair z y))
A Primcodable type is an Encodable type for which
the encode/decode functions are primitive recursive.
- encode : α → ℕ
- encodek : ∀ (a : α), Encodable.decode (Encodable.encode a) = some a
- prim : Nat.Primrec fun (n : ℕ) => Encodable.encode (Encodable.decode n)
Instances
- LO.FirstOrder.Language.ORing.instPrimcodableFuncORing
- LO.FirstOrder.Language.ORing.instPrimcodableRelORing
- Primcodable.bool
- Primcodable.empty
- Primcodable.fin
- Primcodable.finArrow
- Primcodable.list
- Primcodable.ofDenumerable
- Primcodable.option
- Primcodable.prod
- Primcodable.sum
- Primcodable.ulower
- Primcodable.unit
- Primcodable.vector
theorem
Primcodable.prim
{α : Type u_1}
[self : Primcodable α]
:
Nat.Primrec fun (n : ℕ) => Encodable.encode (Encodable.decode n)
@[instance 10]
Equations
Builds a Primcodable instance from an equivalence to a Primcodable type.
Equations
- Primcodable.ofEquiv α e = let __spread.0 := Encodable.ofEquiv α e; Primcodable.mk ⋯
Equations
Equations
- Primcodable.option = Primcodable.mk ⋯
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))
theorem
Primrec.dom_denumerable
{α : Type u_4}
{β : Type u_5}
[Denumerable α]
[Primcodable β]
{f : α → β}
:
Primrec f ↔ Nat.Primrec fun (n : ℕ) => Encodable.encode (f (Denumerable.ofNat α n))
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 : α → σ}
:
(Primrec fun (a : α) => Encodable.encode (f a)) ↔ Primrec f
theorem
Primrec.ofNat_iff
{α : Type u_4}
{β : Type u_5}
[Denumerable α]
[Primcodable β]
{f : α → β}
:
Primrec f ↔ Primrec fun (n : ℕ) => f (Denumerable.ofNat α n)
theorem
Primrec.option_some_iff
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
:
theorem
Primrec.of_equiv_symm
{α : Type u_1}
[Primcodable α]
{β : Type u_4}
{e : β ≃ α}
:
Primrec ⇑e.symm
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 = Primcodable.mk ⋯
theorem
Primrec.pair
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{f : α → β}
{g : α → γ}
(hf : Primrec f)
(hg : Primrec g)
:
Primrec fun (a : α) => (f a, g a)
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.
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)
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)
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₂.pair
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primrec₂ Prod.mk
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₂.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₂ fun (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 : α → β → σ}
:
theorem
Primrec₂.ofNat_iff
{α : Type u_4}
{β : Type u_5}
{σ : Type u_6}
[Denumerable α]
[Denumerable β]
[Primcodable σ]
{f : α → β → σ}
:
Primrec₂ f ↔ Primrec₂ fun (m n : ℕ) => f (Denumerable.ofNat α m) (Denumerable.ofNat β 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₂ 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 : α → Prop}
{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 : α → β → Prop}
{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_5}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α × β → σ}
(hf : Primrec f)
:
Primrec₂ fun (a : α) (b : β) => f (a, b)
theorem
Primrec.nat_rec
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → β}
{g : α → ℕ × β → β}
(hf : Primrec f)
(hg : Primrec₂ g)
:
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_5}
[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_5}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → Option β}
{g : α → β → Option σ}
(hf : Primrec f)
(hg : Primrec₂ g)
:
Primrec fun (a : α) => (f a).bind (g a)
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 fun (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 σ}
:
(Primrec₂ fun (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₂ fun (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 fun (a : α) => bif c a then f a else g a
theorem
Primrec.ite
{α : Type u_1}
{σ : Type u_5}
[Primcodable α]
[Primcodable σ]
{c : α → Prop}
[DecidablePred c]
{f : α → σ}
{g : α → σ}
(hc : PrimrecPred c)
(hf : Primrec f)
(hg : Primrec g)
:
Primrec fun (a : α) => if c a then f a else g a
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 : α → Prop}
{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 : α → Prop}
{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 (p a) (f a)
theorem
Primrec.option_orElse
{α : Type u_1}
[Primcodable α]
:
Primrec₂ fun (x x_1 : Option α) => HOrElse.hOrElse x fun (x : Unit) => x_1
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_indexOf₁
{α : Type u_1}
[Primcodable α]
[DecidableEq α]
(l : List α)
:
Primrec fun (a : α) => List.indexOf a l
theorem
Primrec.dom_fintype
{α : Type u_1}
{σ : Type u_5}
[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
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₁ : Primrec.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 = Primcodable.mk ⋯
Equations
- Primcodable.list = Primcodable.mk ⋯
theorem
Primrec.sum_inl
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primrec Sum.inl
theorem
Primrec.sum_inr
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Primrec Sum.inr
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)
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 : α → σ × β → σ}
:
Primrec f → Primrec g → Primrec₂ h → Primrec fun (a : α) => List.foldl (fun (s : σ) (b : β) => h a (s, b)) (g a) (f a)
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)
:
Primrec fun (a : α) => List.recOn (f a) (g a) fun (b : β) (l : List β) (IH : σ) => h a (b, l, IH)
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_bind
{α : 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 : α) => (f a).bind (g 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)
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 α]
:
Primrec₂ List.lookup
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
Equations
- Primcodable.fin = Primcodable.ofEquiv { a : ℕ // id a < n } Fin.equivSubtype
instance
Primcodable.vector
{α : Type u_1}
[Primcodable α]
{n : ℕ}
:
Primcodable (Mathlib.Vector α n)
Equations
- Primcodable.vector = Primcodable.subtype ⋯
Equations
- Primcodable.finArrow = Primcodable.ofEquiv (Mathlib.Vector α n) (Equiv.vectorEquivFin α n).symm
theorem
Primcodable.mem_range_encode
{α : Type u_1}
[Primcodable α]
:
PrimrecPred fun (n : ℕ) => n ∈ Set.range Encodable.encode
Equations
- Primcodable.ulower = Primcodable.subtype ⋯
theorem
Primrec.subtype_val
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
{hp : PrimrecPred p}
:
Primrec Subtype.val
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)
:
Primrec fun (a : α) => ⟨f a, ⋯⟩
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 : α → Mathlib.Vector β n}
:
theorem
Primrec.list_ofFn
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α → σ}
:
theorem
Primrec.vector_ofFn
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α → σ}
(hf : ∀ (i : Fin n), Primrec (f i))
:
Primrec fun (a : α) => Mathlib.Vector.ofFn fun (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 → σ}
:
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: Nat.Primrec' fun (x : Mathlib.Vector ℕ 0) => 0
- succ: Nat.Primrec' fun (v : Mathlib.Vector ℕ 1) => v.head.succ
- get: ∀ {n : ℕ} (i : Fin n), Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => v.get i
- comp: ∀ {m n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} (g : Fin n → Mathlib.Vector ℕ m → ℕ), Nat.Primrec' f → (∀ (i : Fin n), Nat.Primrec' (g i)) → Nat.Primrec' fun (a : Mathlib.Vector ℕ m) => f (Mathlib.Vector.ofFn fun (i : Fin n) => g i a)
- prec: ∀ {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} {g : Mathlib.Vector ℕ (n + 2) → ℕ}, Nat.Primrec' f → Nat.Primrec' g → Nat.Primrec' fun (v : Mathlib.Vector ℕ (n + 1)) => Nat.rec (f v.tail) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
theorem
Nat.Primrec'.of_eq
{n : ℕ}
{f : Mathlib.Vector ℕ n → ℕ}
{g : Mathlib.Vector ℕ n → ℕ}
(hf : Nat.Primrec' f)
(H : ∀ (i : Mathlib.Vector ℕ n), f i = g i)
:
theorem
Nat.Primrec'.tail
{n : ℕ}
{f : Mathlib.Vector ℕ n → ℕ}
(hf : Nat.Primrec' f)
:
Nat.Primrec' fun (v : Mathlib.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 : Mathlib.Vector ℕ n) => (f v).get i
theorem
Nat.Primrec'.nil
{n : ℕ}
:
Nat.Primrec'.Vec fun (x : Mathlib.Vector ℕ n) => Mathlib.Vector.nil
theorem
Nat.Primrec'.cons
{n : ℕ}
{m : ℕ}
{f : Mathlib.Vector ℕ n → ℕ}
{g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m}
(hf : Nat.Primrec' f)
(hg : Nat.Primrec'.Vec g)
:
Nat.Primrec'.Vec fun (v : Mathlib.Vector ℕ n) => f v ::ᵥ g v
theorem
Nat.Primrec'.comp'
{n : ℕ}
{m : ℕ}
{f : Mathlib.Vector ℕ m → ℕ}
{g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m}
(hf : Nat.Primrec' f)
(hg : Nat.Primrec'.Vec g)
:
Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => f (g v)
theorem
Nat.Primrec'.comp₁
(f : ℕ → ℕ)
(hf : Nat.Primrec' fun (v : Mathlib.Vector ℕ 1) => f v.head)
{n : ℕ}
{g : Mathlib.Vector ℕ n → ℕ}
(hg : Nat.Primrec' g)
:
Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => f (g v)
theorem
Nat.Primrec'.comp₂
(f : ℕ → ℕ → ℕ)
(hf : Nat.Primrec' fun (v : Mathlib.Vector ℕ 2) => f v.head v.tail.head)
{n : ℕ}
{g : Mathlib.Vector ℕ n → ℕ}
{h : Mathlib.Vector ℕ n → ℕ}
(hg : Nat.Primrec' g)
(hh : Nat.Primrec' h)
:
Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => f (g v) (h v)
theorem
Nat.Primrec'.prec'
{n : ℕ}
{f : Mathlib.Vector ℕ n → ℕ}
{g : Mathlib.Vector ℕ n → ℕ}
{h : Mathlib.Vector ℕ (n + 2) → ℕ}
(hf : Nat.Primrec' f)
(hg : Nat.Primrec' g)
(hh : Nat.Primrec' h)
:
Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => Nat.rec (g v) (fun (y IH : ℕ) => h (y ::ᵥ IH ::ᵥ v)) (f v)
theorem
Nat.Primrec'.if_lt
{n : ℕ}
{a : Mathlib.Vector ℕ n → ℕ}
{b : Mathlib.Vector ℕ n → ℕ}
{f : Mathlib.Vector ℕ n → ℕ}
{g : Mathlib.Vector ℕ n → ℕ}
(ha : Nat.Primrec' a)
(hb : Nat.Primrec' b)
(hf : Nat.Primrec' f)
(hg : Nat.Primrec' g)
:
Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => if a v < b v then f v else g v
theorem
Nat.Primrec'.natPair :
Nat.Primrec' fun (v : Mathlib.Vector ℕ 2) => Nat.pair v.head v.tail.head
theorem
Nat.Primrec'.unpair₁
{n : ℕ}
{f : Mathlib.Vector ℕ n → ℕ}
(hf : Nat.Primrec' f)
:
Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => (Nat.unpair (f v)).1
theorem
Nat.Primrec'.unpair₂
{n : ℕ}
{f : Mathlib.Vector ℕ n → ℕ}
(hf : Nat.Primrec' f)
:
Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => (Nat.unpair (f v)).2
theorem
Nat.Primrec'.prim_iff₁
{f : ℕ → ℕ}
:
(Nat.Primrec' fun (v : Mathlib.Vector ℕ 1) => f v.head) ↔ Primrec f
theorem
Nat.Primrec'.prim_iff₂
{f : ℕ → ℕ → ℕ}
:
(Nat.Primrec' fun (v : Mathlib.Vector ℕ 2) => f v.head v.tail.head) ↔ Primrec₂ f
theorem
Nat.Primrec'.vec_iff
{m : ℕ}
{n : ℕ}
{f : Mathlib.Vector ℕ m → Mathlib.Vector ℕ n}
:
Nat.Primrec'.Vec f ↔ Primrec f