Primitive recursive list operations
DefinitionBoolean membership test for lists of natural numbers#✓fully proved
For a list \(G\) of natural numbers and a natural number \(j\), the Boolean value that is true exactly when \(j\) is an entry of \(G\).
Used by 51
DefinitionDuplicate removal for lists of natural numbers#✓fully proved
For a list \(l\) of natural numbers, the list obtained from \(l\) by deleting every entry that occurs again later in \(l\): each element of \(l\) is kept once, at its last occurrence, and the kept entries stay in their order in \(l\).
def dedupB (l : List ℕ) : List ℕ :=
l.foldr (fun x acc => cond (memB acc x) acc (x :: acc)) []def memB (G : List ℕ) (j : ℕ) : Bool :=
G.foldr (fun a b => decide (a = j) || b) falseCSLibExt/Computability/Decidability/PrimrecList.lean:40
Uses 1 · Used by 14
TheoremBounded monotone rounds on lists close off#✓fully proved
Let \(f\) map lists of natural numbers to lists of natural numbers and be monotone for list inclusion: \(f(G) \subseteq f(G')\) whenever \(G \subseteq G'\), where \(G \subseteq G'\) means that every entry of \(G\) is an entry of \(G'\). If \(B\) is a list with \(f(G) \subseteq B\) for every list \(G\), and \(n\) is the length of \(B\), then \(f(f^n([\,])) \subseteq f^n([\,])\), where \(f^n\) is the \(n\)-fold iterate of \(f\) and \([\,]\) is the empty list.
TheoremPredicates with a primitive recursive decision procedure are computable#✓fully proved
Let \(\beta\) be a primcodable type, \(p\) a predicate on \(\beta\), and \(f : \beta \to \mathrm{Bool}\) a primitive recursive function such that \(f(b) = \mathrm{true}\) exactly when \(p(b)\) holds, for every \(b \in \beta\). Then \(p\) is a computable predicate.
theorem computablePred_of_primrec_bool {β : Type*} [Primcodable β] {p : β → Prop}
{f : β → Bool} (hf : Primrec f) (h : ∀ b, f b = true ↔ p b) : ComputablePred pUsed by 16
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.