mathlib documentation

computability.partrec_code

source
theorem nat.partrec.rfind' {f : ℕ →. ℕ} (hf : nat.partrec f) :
nat.partrec (nat.unpaired (λ (a m : ℕ), roption.map (λ (_x : ℕ), _x + m) (nat.rfind (λ (n : ℕ), (λ (m : ℕ), to_bool (m = 0)) <$> f (a.mkpair (n + m))))))

source
inductive nat.partrec.code  :
Type

source
@[instance]
def nat.partrec.code.inhabited  :
inhabited nat.partrec.code

Equations
source
def nat.partrec.code.const (a : ℕ) :
nat.partrec.code

Equations
source
theorem nat.partrec.code.const_inj {n₁ n₂ : ℕ} (a : nat.partrec.code.const n₁ = nat.partrec.code.const n₂) :
n₁ = n₂

source
def nat.partrec.code.id  :
nat.partrec.code

Equations
source
def nat.partrec.code.curry (c : nat.partrec.code) (n : ℕ) :
nat.partrec.code

Equations
source
def nat.partrec.code.encode_code (a : nat.partrec.code) :
ℕ

Equations
source
def nat.partrec.code.of_nat_code (a : ℕ) :
nat.partrec.code

Equations
source
@[instance]
def nat.partrec.code.denumerable  :
denumerable nat.partrec.code

Equations
source
theorem nat.partrec.code.encode_code_eq  :
encodable.encode = nat.partrec.code.encode_code

source
theorem nat.partrec.code.of_nat_code_eq  :
denumerable.of_nat nat.partrec.code = nat.partrec.code.of_nat_code

source
theorem nat.partrec.code.encode_lt_pair (cf cg : nat.partrec.code) :
encodable.encode cf < encodable.encode (cf.pair cg) ∧ encodable.encode cg < encodable.encode (cf.pair cg)

source
theorem nat.partrec.code.encode_lt_comp (cf cg : nat.partrec.code) :
encodable.encode cf < encodable.encode (cf.comp cg) ∧ encodable.encode cg < encodable.encode (cf.comp cg)

source
theorem nat.partrec.code.encode_lt_prec (cf cg : nat.partrec.code) :
encodable.encode cf < encodable.encode (cf.prec cg) ∧ encodable.encode cg < encodable.encode (cf.prec cg)

source
theorem nat.partrec.code.encode_lt_rfind' (cf : nat.partrec.code) :
encodable.encode cf < encodable.encode cf.rfind'

source
theorem nat.partrec.code.pair_prim  :
primrec₂ nat.partrec.code.pair

source
theorem nat.partrec.code.comp_prim  :
primrec₂ nat.partrec.code.comp

source
theorem nat.partrec.code.prec_prim  :
primrec₂ nat.partrec.code.prec

source
theorem nat.partrec.code.rfind_prim  :
primrec nat.partrec.code.rfind'

source
theorem nat.partrec.code.rec_prim' {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {c : α → nat.partrec.code} (hc : primrec c) {z : α → σ} (hz : primrec z) {s : α → σ} (hs : primrec s) {l : α → σ} (hl : primrec l) {r : α → σ} (hr : primrec r) {pr : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hpr : primrec₂ pr) {co : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hco : primrec₂ co) {pc : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hpc : primrec₂ pc) {rf : α → nat.partrec.code × σ → σ} (hrf : primrec₂ rf) :
let PR : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), pr a (cf, cg, hf, hg), CO : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), co a (cf, cg, hf, hg), PC : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), pc a (cf, cg, hf, hg), RF : α → nat.partrec.code → σ → σ := λ (a : α) (cf : nat.partrec.code) (hf : σ), rf a (cf, hf), F : α → nat.partrec.code → σ := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in primrec (λ (a : α), F a (c a))

source
theorem nat.partrec.code.rec_prim {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {c : α → nat.partrec.code} (hc : primrec c) {z : α → σ} (hz : primrec z) {s : α → σ} (hs : primrec s) {l : α → σ} (hl : primrec l) {r : α → σ} (hr : primrec r) {pr : α → nat.partrec.code → nat.partrec.code → σ → σ → σ} (hpr : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × σ × σ), pr a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {co : α → nat.partrec.code → nat.partrec.code → σ → σ → σ} (hco : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × σ × σ), co a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {pc : α → nat.partrec.code → nat.partrec.code → σ → σ → σ} (hpc : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × σ × σ), pc a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {rf : α → nat.partrec.code → σ → σ} (hrf : primrec (λ (a : α × nat.partrec.code × σ), rf a.fst a.snd.fst a.snd.snd)) :
let F : α → nat.partrec.code → σ := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a) in primrec (λ (a : α), F a (c a))

source
theorem nat.partrec.code.rec_computable {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {c : α → nat.partrec.code} (hc : computable c) {z : α → σ} (hz : computable z) {s : α → σ} (hs : computable s) {l : α → σ} (hl : computable l) {r : α → σ} (hr : computable r) {pr : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hpr : computable₂ pr) {co : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hco : computable₂ co) {pc : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hpc : computable₂ pc) {rf : α → nat.partrec.code × σ → σ} (hrf : computable₂ rf) :
let PR : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), pr a (cf, cg, hf, hg), CO : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), co a (cf, cg, hf, hg), PC : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), pc a (cf, cg, hf, hg), RF : α → nat.partrec.code → σ → σ := λ (a : α) (cf : nat.partrec.code) (hf : σ), rf a (cf, hf), F : α → nat.partrec.code → σ := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in computable (λ (a : α), F a (c a))

source
def nat.partrec.code.eval (a : nat.partrec.code) :
ℕ →. ℕ

Equations
source
@[instance]
def nat.partrec.code.has_mem  :
has_mem (ℕ →. ℕ) nat.partrec.code

Equations
source
@[simp]
theorem nat.partrec.code.eval_const (n m : ℕ) :
(nat.partrec.code.const n).eval m = roption.some n

source
@[simp]
theorem nat.partrec.code.eval_id (n : ℕ) :
nat.partrec.code.id.eval n = roption.some n

source
@[simp]
theorem nat.partrec.code.eval_curry (c : nat.partrec.code) (n x : ℕ) :
(c.curry n).eval x = c.eval (n.mkpair x)

source
theorem nat.partrec.code.const_prim  :
primrec nat.partrec.code.const

source
theorem nat.partrec.code.curry_prim  :
primrec₂ nat.partrec.code.curry

source
theorem nat.partrec.code.curry_inj {c₁ c₂ : nat.partrec.code} {n₁ n₂ : ℕ} (h : c₁.curry n₁ = c₂.curry n₂) :
c₁ = c₂ ∧ n₁ = n₂

source
theorem nat.partrec.code.smn  :
∃ (f : nat.partrec.code → ℕ → nat.partrec.code), computable₂ f ∧ ∀ (c : nat.partrec.code) (n x : ℕ), (f c n).eval x = c.eval (n.mkpair x)

source
theorem nat.partrec.code.exists_code {f : ℕ →. ℕ} :
nat.partrec f ↔ ∃ (c : nat.partrec.code), c.eval = f

source
def nat.partrec.code.evaln (k : ℕ) (a : nat.partrec.code) (a_1 : ℕ) :
option ℕ

Equations
source
theorem nat.partrec.code.evaln_bound {k : ℕ} {c : nat.partrec.code} {n x : ℕ} (a : x ∈ nat.partrec.code.evaln k c n) :
n < k

source
theorem nat.partrec.code.evaln_mono {k₁ k₂ : ℕ} {c : nat.partrec.code} {n x : ℕ} (a : k₁ ≤ k₂) (a_1 : x ∈ nat.partrec.code.evaln k₁ c n) :
x ∈ nat.partrec.code.evaln k₂ c n

source
theorem nat.partrec.code.evaln_sound {k : ℕ} {c : nat.partrec.code} {n x : ℕ} (a : x ∈ nat.partrec.code.evaln k c n) :
x ∈ c.eval n

source
theorem nat.partrec.code.evaln_complete {c : nat.partrec.code} {n x : ℕ} :
x ∈ c.eval n ↔ ∃ (k : ℕ), x ∈ nat.partrec.code.evaln k c n

source
theorem nat.partrec.code.evaln_prim  :
primrec (λ (a : (ℕ × nat.partrec.code) × ℕ), nat.partrec.code.evaln a.fst.fst a.fst.snd a.snd)

source
theorem nat.partrec.code.eval_eq_rfind_opt (c : nat.partrec.code) (n : ℕ) :
c.eval n = nat.rfind_opt (λ (k : ℕ), nat.partrec.code.evaln k c n)

source
theorem nat.partrec.code.eval_part  :
partrec₂ nat.partrec.code.eval

source
theorem nat.partrec.code.fixed_point {f : nat.partrec.code → nat.partrec.code} (hf : computable f) :
∃ (c : nat.partrec.code), (f c).eval = c.eval

source
theorem nat.partrec.code.fixed_point₂ {f : nat.partrec.code → ℕ →. ℕ} (hf : partrec₂ f) :
∃ (c : nat.partrec.code), c.eval = f c