Primitive recursive functions on Lists #
The primitive recursive functions are defined in Mathlib.Computability.Primrec.Basic.
This file contains definitions and theorems about primitive recursive functions that
relate to operation on lists.
References #
Equations
- Primcodable.list = { toEncodable := List.encodable, prim := ⋯ }
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)
:
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.listFilter
{α : Type u_1}
[Primcodable α]
{p : α → Prop}
[DecidablePred p]
(hf : PrimrecPred p)
:
Primrec fun (L : List α) => List.filter (fun (x : α) => decide (p x)) L
Filtering a list for elements that satisfy a decidable predicate is primitive recursive.
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 α]
:
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
theorem
PrimrecPred.exists_mem_list
{α : Type u_1}
{p : α → Prop}
[Primcodable α]
(hf : PrimrecPred p)
:
PrimrecPred fun (L : List α) => ∃ a ∈ L, p a
Checking if any element of a list satisfies a decidable predicate is primitive recursive.
theorem
PrimrecPred.forall_mem_list
{α : Type u_1}
{p : α → Prop}
[Primcodable α]
(hf : PrimrecPred p)
:
PrimrecPred fun (L : List α) => ∀ a ∈ L, p a
Checking if every element of a list satisfies a decidable predicate is primitive recursive.
theorem
PrimrecPred.exists_lt
{p : ℕ → Prop}
(hf : PrimrecPred p)
:
PrimrecPred fun (n : ℕ) => ∃ x < n, p x
Bounded existential quantifiers are primitive recursive.
theorem
PrimrecPred.forall_lt
{p : ℕ → Prop}
(hf : PrimrecPred p)
:
PrimrecPred fun (n : ℕ) => ∀ x < n, p x
Bounded universal quantifiers are primitive recursive.
theorem
PrimrecPred.listFilter_listRange
{R : ℕ → ℕ → Prop}
(s : ℕ)
[DecidableRel R]
(hf : PrimrecRel R)
:
Primrec fun (n : ℕ) => List.filter (fun (y : ℕ) => decide (R y n)) (List.range s)
A helper lemma for proofs about bounded quantifiers on decidable relations.
theorem
PrimrecRel.listFilter
{α : Type u_1}
{β : Type u_2}
{R : α → β → Prop}
[Primcodable α]
[Primcodable β]
(hf : PrimrecRel R)
[DecidableRel R]
:
Primrec₂ fun (L : List α) (b : β) => List.filter (fun (a : α) => decide (R a b)) L
If R a b is decidable, then given L : List α and b : β, it is primitive recursive
to filter L for elements a with R a b
theorem
PrimrecRel.exists_mem_list
{α : Type u_1}
{β : Type u_2}
{R : α → β → Prop}
[Primcodable α]
[Primcodable β]
(hf : PrimrecRel R)
:
PrimrecRel fun (L : List α) (b : β) => ∃ a ∈ L, R a b
If R a b is decidable, then given L : List α and b : β, g L b ↔ ∃ a L, R a b
is a primitive recursive relation.
theorem
PrimrecRel.forall_mem_list
{α : Type u_1}
{β : Type u_2}
{R : α → β → Prop}
[Primcodable α]
[Primcodable β]
(hf : PrimrecRel R)
:
PrimrecRel fun (L : List α) (b : β) => ∀ a ∈ L, R a b
If R a b is decidable, then given L : List α and b : β, g L b ↔ ∀ a L, R a b
is a primitive recursive relation.
theorem
PrimrecRel.exists_lt
{R : ℕ → ℕ → Prop}
(hf : PrimrecRel R)
:
PrimrecRel fun (n y : ℕ) => ∃ x < n, R x y
If R a b is decidable, then for any fixed n and y, g n y ↔ ∃ x < n, R x y is a
primitive recursive relation.
theorem
PrimrecRel.forall_lt
{R : ℕ → ℕ → Prop}
(hf : PrimrecRel R)
:
PrimrecRel fun (n y : ℕ) => ∀ x < n, R x y
If R a b is decidable, then for any fixed n and y, g n y ↔ ∀ x < n, R x y is a
primitive recursive relation.
Equations
Equations
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