inductive Partrec : ℕ → Type

• const {n : ℕ} : ℕ → Partrec n
• succ : Partrec 1
• proj {n : ℕ} : Fin n → Partrec n
• comp {n m : ℕ} : Partrec n → (Fin n → Partrec m) → Partrec m
• prec {n : ℕ} : Partrec n → Partrec (n + 2) → Partrec (n + 1)
• mu {n : ℕ} : Partrec (n + 1) → Partrec n

@[reducible, inline]

abbrev Partrec.comp₁ {n : ℕ} (f : Partrec 1) (g : Partrec n) : Partrec n

Equations

• f.comp₁ g = f.comp [g]ᵥ

@[reducible, inline]

abbrev Partrec.comp₂ {n : ℕ} (f : Partrec 2) (g₁ g₂ : Partrec n) : Partrec n

Equations

• f.comp₂ g₁ g₂ = f.comp [g₁, g₂]ᵥ

@[reducible, inline]

abbrev Partrec.comp₃ {n : ℕ} (f : Partrec 3) (g₁ g₂ g₃ : Partrec n) : Partrec n

Equations

• f.comp₃ g₁ g₂ g₃ = f.comp [g₁, g₂, g₃]ᵥ

def Partrec.eval {n : ℕ} : Partrec n → Vec ℕ n →. ℕ

Equations

• (Partrec.const n_3).eval x✝ = Part.some n_3
• Partrec.succ.eval v = Part.some v.head.succ
• (Partrec.proj i).eval x✝ = Part.some (x✝ i)
• (f.comp g).eval x✝ = (Part.bindVec fun (i : Fin n_3) => (g i).eval x✝) >>= f.eval
• (f.prec g).eval v = (f.eval v.tail).natrec (fun (n ih : ℕ) => do let m ← ↑(some ih) g.eval (n ∷ᵥ m ∷ᵥ v.tail)) v.head
• f.mu.eval x✝ = Part.find fun (n_1 : ℕ) => f.eval (n_1 ∷ᵥ x✝)

instance Partrec.instCoeFunPFunVecNat {n : ℕ} : CoeFun (Partrec n) fun (x : Partrec n) => Vec ℕ n →. ℕ

Equations

• Partrec.instCoeFunPFunVecNat = { coe := Partrec.eval }

@[simp]

theorem Partrec.zero_eval {n n✝ : ℕ} {v : Vec ℕ n✝} : (const n).eval v = Part.some n

@[simp]

theorem Partrec.succ_eval {v : Vec ℕ 1} : succ.eval v = Part.some v.head.succ

@[simp]

theorem Partrec.proj_eval {n✝ : ℕ} {i : Fin n✝} {v : Vec ℕ n✝} : (proj i).eval v = Part.some (v i)

@[simp]

theorem Partrec.comp_eval {a✝ : ℕ} {f : Partrec a✝} {a✝¹ : ℕ} {g : Fin a✝ → Partrec a✝¹} {v : Vec ℕ a✝¹} : (f.comp g).eval v = (Part.bindVec fun (i : Fin a✝) => (g i).eval v) >>= f.eval

theorem Partrec.prec_eval {a✝ : ℕ} {f : Partrec a✝} {g : Partrec (a✝ + 2)} {v : Vec ℕ (a✝ + 1)} : (f.prec g).eval v = (f.eval v.tail).natrec (fun (n ih : ℕ) => do let m ← ↑(some ih) g.eval (n ∷ᵥ m ∷ᵥ v.tail)) v.head

theorem Partrec.prec_eval_zero {a✝ : ℕ} {f : Partrec a✝} {g : Partrec (a✝ + 2)} {v : Vec ℕ a✝} : (f.prec g).eval (0 ∷ᵥ v) = f.eval v

theorem Partrec.prec_eval_succ {a✝ : ℕ} {f : Partrec a✝} {g : Partrec (a✝ + 2)} {v : Vec ℕ a✝} {n : ℕ} : (f.prec g).eval (n.succ ∷ᵥ v) = do let m ← (f.prec g).eval (n ∷ᵥ v) g.eval (n ∷ᵥ m ∷ᵥ v)

@[simp]

theorem Partrec.mu_eval {a✝ : ℕ} {f : Partrec (a✝ + 1)} {v : Vec ℕ a✝} : f.mu.eval v = Part.find fun (n : ℕ) => f.eval (n ∷ᵥ v)

def Partrec.Total {n : ℕ} (f : Partrec n) : Prop

Equations

• f.Total = ∀ (v : Vec ℕ n), (f.eval v).Dom

def Partrec.ofPrim {n : ℕ} : Primrec n → Partrec n

Equations

• Partrec.ofPrim (Primrec.const n_3) = Partrec.const n_3
• Partrec.ofPrim Primrec.succ = Partrec.succ
• Partrec.ofPrim (Primrec.proj i) = Partrec.proj i
• Partrec.ofPrim (f.comp g) = (Partrec.ofPrim f).comp fun (i : Fin n_3) => Partrec.ofPrim (g i)
• Partrec.ofPrim (f.prec g) = (Partrec.ofPrim f).prec (Partrec.ofPrim g)

@[simp]

theorem Partrec.ofPrim_eval {a✝ : ℕ} {f : Primrec a✝} {v : Vec ℕ a✝} : (ofPrim f).eval v = Part.some (f.eval v)

theorem Partrec.ofPrim_total {a✝ : ℕ} {f : Primrec a✝} : (ofPrim f).Total

@[reducible, inline]

abbrev Primrec.toPart {n : ℕ} : Primrec n → Partrec n

Equations

• Primrec.toPart = Partrec.ofPrim

def Partrec.loop {n : ℕ} : Partrec n

Equations

• Partrec.loop = (Partrec.ofPrim (Primrec.const 0)).mu

@[simp]

theorem Partrec.loop_eval {n✝ : ℕ} {v : Vec ℕ n✝} : loop.eval v = Part.none

def Partrec.cov {n : ℕ} (f : Partrec (n + 2)) : Partrec (n + 1)

Equations

• f.cov = (Partrec.const 0).prec ((Partrec.ofPrim Primrec.rcons).comp₃ (Partrec.proj 0) (Partrec.proj 1) f)

theorem Partrec.cov_dom {n : ℕ} {v : Vec ℕ n} {f : Partrec (n + 2)} (hf : ∀ (a b : ℕ), (f.eval (a ∷ᵥ b ∷ᵥ v)).Dom) (m : ℕ) : (f.cov.eval (m ∷ᵥ v)).Dom

theorem Partrec.cov_eval {n : ℕ} {v : Vec ℕ n} {m : ℕ} {f : Partrec (n + 2)} (hf : ∀ (a b : ℕ), (f.eval (a ∷ᵥ b ∷ᵥ v)).Dom) : f.cov.eval (m ∷ᵥ v) = Part.some (Vec.paired fun (i : Fin m) => (f.eval (↑i ∷ᵥ (f.cov.eval (↑i ∷ᵥ v)).get ⋯ ∷ᵥ v)).get ⋯)

def Partrec.covrec {n : ℕ} (f : Partrec (n + 2)) : Partrec (n + 1)

Course-of-values recursion. For simplicity we assume the totality of f on the first two arguments.

Equations

• f.covrec = (Partrec.ofPrim Primrec.vget).comp₂ (f.cov.comp (Partrec.succ.comp₁ (Partrec.proj 0) ∷ᵥ fun (x : Fin n) => Partrec.proj x.succ)) (Partrec.proj 0)

theorem Partrec.covrec_dom {n : ℕ} {v : Vec ℕ n} {f : Partrec (n + 2)} (hf : ∀ (a b : ℕ), (f.eval (a ∷ᵥ b ∷ᵥ v)).Dom) (m : ℕ) : (f.covrec.eval (m ∷ᵥ v)).Dom

theorem Partrec.covrec_eval {n : ℕ} {v : Vec ℕ n} {m : ℕ} {f : Partrec (n + 2)} (hf : ∀ (a b : ℕ), (f.eval (a ∷ᵥ b ∷ᵥ v)).Dom) : f.covrec.eval (m ∷ᵥ v) = f.eval (m ∷ᵥ (Vec.paired fun (i : Fin m) => (f.covrec.eval (↑i ∷ᵥ v)).get ⋯) ∷ᵥ v)

def Partrec.bd {n : ℕ} : Partrec n → Primrec (n + 1)

bd f (k ∷ᵥ v) replaces all unbounded mu in f v with a Primrec.bdMu bounded by k; it returns 0 for Part.none, and x + 1 for Part.some x.

bd is similar to Nat.Partrec.Code.evaln in mathlib, although bd itself is not primitive recursive (since bd f is equivalent to f + 1 when f is primitive recursive).

Equations

• One or more equations did not get rendered due to their size.
• (Partrec.const n_3).bd = Primrec.const (n_3 + 1)
• Partrec.succ.bd = Primrec.succ.comp₁ (Primrec.succ.comp₁ (Primrec.proj 1))
• (Partrec.proj i).bd = Primrec.succ.comp₁ (Primrec.proj i.succ)
• (f.comp g).bd = (Primrec.andv fun (i : Fin n_3) => (g i).bd).ite (f.bd.comp (Primrec.proj 0 ∷ᵥ fun (i : Fin n_3) => Primrec.pred.comp₁ (g i).bd)) Primrec.zero

theorem Partrec.bd_mono {a✝ : ℕ} {f : Partrec a✝} {k : ℕ} {v : Vec ℕ a✝} {m k' : ℕ} : f.bd.eval (k ∷ᵥ v) = m + 1 → k' ≥ k → f.bd.eval (k' ∷ᵥ v) = m + 1

theorem Partrec.bd_sound {a✝ : ℕ} {f : Partrec a✝} {k : ℕ} {v : Vec ℕ a✝} {m : ℕ} : f.bd.eval (k ∷ᵥ v) = m + 1 → m ∈ f.eval v

theorem Partrec.bd_zero_of_not_dom {a✝ : ℕ} {f : Partrec a✝} {v : Vec ℕ a✝} : ¬(f.eval v).Dom → ∀ (k : ℕ), f.bd.eval (k ∷ᵥ v) = 0

theorem Partrec.bd_pos_of_mem {a✝ : ℕ} {f : Partrec a✝} {m : ℕ} {v : Vec ℕ a✝} : m ∈ f.eval v → ∃ (k : ℕ), f.bd.eval (k ∷ᵥ v) = m + 1

theorem Partrec.bd_of_mem {a✝ : ℕ} {f : Partrec a✝} {m : ℕ} {v : Vec ℕ a✝} : m ∈ f.eval v → ∃ (k : ℕ), ∀ (k' : ℕ), f.bd.eval (k' ∷ᵥ v) = if k' < k then 0 else m + 1

theorem Partrec.bd_ofPrim {n k : ℕ} {v : Vec ℕ n} {f : Primrec n} : (ofPrim f).bd.eval (k ∷ᵥ v) = f.eval v + 1

theorem Partrec.dom_iff_exists_bd_pos {a✝ : ℕ} {f : Partrec a✝} {v : Vec ℕ a✝} : (f.eval v).Dom ↔ ∃ (k : ℕ), 0 < f.bd.eval (k ∷ᵥ v)

def Partrec.site {n : ℕ} (f g h : Partrec n) : Partrec n

Short-circuit if-then-else. site f g h is equivalent to g when f is positive, and equivalent to h when f is zero.

Equations

• One or more equations did not get rendered due to their size.

theorem Partrec.mem_site_eval_iff {a✝ : ℕ} {f g h : Partrec a✝} {v : Vec ℕ a✝} {m : ℕ} : m ∈ (f.site g h).eval v ↔ 0 < f.eval v ∧ m ∈ g.eval v ∨ 0 ∈ f.eval v ∧ m ∈ h.eval v

theorem Partrec.site_dom {a✝ : ℕ} {f g h : Partrec a✝} {v : Vec ℕ a✝} : ((f.site g h).eval v).Dom ↔ 0 < f.eval v ∧ (g.eval v).Dom ∨ 0 ∈ f.eval v ∧ (h.eval v).Dom

def Partrec.sand {n : ℕ} (f g : Partrec n) : Partrec n

Short-circuit and.

Equations

• f.sand g = f.site g (Partrec.const 0)

theorem Partrec.sand_dom {a✝ : ℕ} {f g : Partrec a✝} {v : Vec ℕ a✝} : ((f.sand g).eval v).Dom ↔ 0 < f.eval v ∧ (g.eval v).Dom ∨ 0 ∈ f.eval v

theorem Partrec.sand_eval_pos_iff {a✝ : ℕ} {f g : Partrec a✝} {v : Vec ℕ a✝} : 0 < (f.sand g).eval v ↔ 0 < f.eval v ∧ 0 < g.eval v

theorem Partrec.sand_eval_zero_iff {a✝ : ℕ} {f g : Partrec a✝} {v : Vec ℕ a✝} : 0 ∈ (f.sand g).eval v ↔ 0 < f.eval v ∧ 0 ∈ g.eval v ∨ 0 ∈ f.eval v

def Partrec.par {n : ℕ} (f g : Partrec n) : Partrec n

Parallel execution of f and g.

Equations

• One or more equations did not get rendered due to their size.

theorem Partrec.par_dom {a✝ : ℕ} {f g : Partrec a✝} {v : Vec ℕ a✝} : ((f.par g).eval v).Dom ↔ (f.eval v).Dom ∨ (g.eval v).Dom

theorem Partrec.mem_par_eval_left {a✝ : ℕ} {f : Partrec a✝} {m : ℕ} {g : Partrec a✝} {v : Vec ℕ a✝} : m ∈ f.eval v → ¬(g.eval v).Dom → m ∈ (f.par g).eval v

theorem Partrec.mem_par_eval_right {a✝ : ℕ} {f g : Partrec a✝} {m : ℕ} {v : Vec ℕ a✝} : ¬(f.eval v).Dom → m ∈ g.eval v → m ∈ (f.par g).eval v

theorem Partrec.mem_par_eval {a✝ : ℕ} {f g : Partrec a✝} {v : Vec ℕ a✝} {m : ℕ} : m ∈ (f.par g).eval v → m ∈ f.eval v ∨ m ∈ g.eval v

def Partrec.repr {n : ℕ} : Partrec n → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• (Partrec.const n_3).repr x✝ = Std.Format.text "const " ++ Std.Format.text n_3.repr
• Partrec.succ.repr x✝ = Std.Format.text "succ"
• (Partrec.proj i).repr x✝ = Repr.addAppParen (Std.Format.text "proj " ++ reprPrec i Lean.Parser.maxPrec) x✝
• (f.prec g).repr x✝ = Repr.addAppParen (Std.Format.text "prec " ++ f.repr Lean.Parser.maxPrec ++ Std.Format.text " " ++ g.repr Lean.Parser.maxPrec) x✝
• f.mu.repr x✝ = Repr.addAppParen (Std.Format.text "mu " ++ f.repr Lean.Parser.maxPrec) x✝

instance Partrec.instRepr {n : ℕ} : Repr (Partrec n)

Equations

• Partrec.instRepr = { reprPrec := Partrec.repr }

class Recursive {α : Type u} [Encodable α] (s : Set α) : Type

A set is recursive if it can be decided by a recursive function f.

Note: for flexibility, we only require f's totality on the image of Encodable.encode, instead of the whole ℕ.

• char : Partrec 1
• char_dom (x : α) : ((char s).eval [Encodable.encode x]ᵥ).Dom
• mem_iff (x : α) : x ∈ s ↔ 0 < (char s).eval [Encodable.encode x]ᵥ

theorem Recursive.not_mem_iff {α : Type u} [Encodable α] {s : Set α} [Recursive s] (x : α) : x ∉ s ↔ 0 ∈ (char s).eval [Encodable.encode x]ᵥ

def Recursive.compl {α : Type u} [Encodable α] {s : Set α} [Recursive s] : Recursive sᶜ

Equations

• Recursive.compl = { char := Primrec.nsign.toPart.comp₁ (Recursive.char s), char_dom := ⋯, mem_iff := ⋯ }

instance Recursive.dec {α : Type u} [Encodable α] (s : Set α) [Recursive s] (x : α) : Decidable (x ∈ s)

Equations

• Recursive.dec s x = ⋯.mpr (⋯.mpr (⋯.mpr inferInstance))

def IsRecursive {α : Type u} [Encodable α] (s : Set α) : Prop

Prop version of Recursive.

Equations

• IsRecursive s = Nonempty (Recursive s)

theorem IsRecursive.def {α : Type u} [Encodable α] {s : Set α} : IsRecursive s ↔ ∃ (f : Partrec 1), (∀ (x : α), (f.eval [Encodable.encode x]ᵥ).Dom) ∧ ∀ (x : α), x ∈ s ↔ 0 < f.eval [Encodable.encode x]ᵥ

theorem IsRecursive.compl_iff {α : Type u} [Encodable α] {s : Set α} : IsRecursive s ↔ IsRecursive sᶜ

class Enumerable {α : Type u} [Encodable α] (s : Set α) : Type

A set is enumerable (also called recursively enumerable, or RE) if it can be decided through a "μ-operator search" over a recursive function. The equivalent definitions are IsEnumerable.iff_range_partrec and IsEnumerable.iff_semi_decidable.

• enum : Partrec 2
• enum_dom (n : ℕ) (x : α) : ((enum s).eval [n, Encodable.encode x]ᵥ).Dom
• mem_iff (x : α) : x ∈ s ↔ ∃ (n : ℕ), 0 < (enum s).eval [n, Encodable.encode x]ᵥ

theorem Enumerable.not_mem_iff {α : Type u} [Encodable α] {s : Set α} [Enumerable s] (x : α) : x ∉ s ↔ ∀ (n : ℕ), 0 ∈ (enum s).eval [n, Encodable.encode x]ᵥ

instance Recursive.enumerable {α : Type u} [Encodable α] {s : Set α} [Recursive s] : Enumerable s

Equations

• Recursive.enumerable = { enum := (Recursive.char s).comp₁ (Partrec.proj 1), enum_dom := ⋯, mem_iff := ⋯ }

def IsEnumerable {α : Type u} [Encodable α] (s : Set α) : Prop

Prop version of Enumerable.

Equations

• IsEnumerable s = Nonempty (Enumerable s)

theorem IsRecursive.enumerable {α : Type u} [Encodable α] {s : Set α} : IsRecursive s → IsEnumerable s

theorem IsEnumerable.def {α : Type u} [Encodable α] {s : Set α} : IsEnumerable s ↔ ∃ (f : Partrec 2), (∀ (n : ℕ) (x : α), (f.eval [n, Encodable.encode x]ᵥ).Dom) ∧ ∀ (x : α), x ∈ s ↔ ∃ (n : ℕ), 0 < f.eval [n, Encodable.encode x]ᵥ

theorem IsEnumerable.iff_range_partrec {α : Type u} [Encodable α] {s : Set α} : IsEnumerable s ↔ ∃ (f : Partrec 1), ∀ (x : α), x ∈ s ↔ ∃ (n : ℕ), Encodable.encode x ∈ f.eval [n]ᵥ

A set is enumerable if and only if it is the range of some partial recursive function f.

theorem IsEnumerable.iff_semi_decidable {α : Type u} [Encodable α] {s : Set α} : IsEnumerable s ↔ ∃ (f : Partrec 1), ∀ (x : α), x ∈ s ↔ (f.eval [Encodable.encode x]ᵥ).Dom

A set is enumerable if and only if it can be semi-decided.

theorem IsRecursive.iff_re_compl_re {α : Type u} [Encodable α] {s : Set α} : IsRecursive s ↔ IsEnumerable s ∧ IsEnumerable sᶜ

A set is recursive if and only if it and its complement are both enumerable.