theorem
nat.partrec.rfind'
{f : ℕ →. ℕ} :
nat.partrec f → nat.partrec (nat.unpaired (λ (a m : ℕ), roption.map (λ (_x : ℕ), _x + m) (nat.rfind (λ (n : ℕ), (λ (m : ℕ), decidable.to_bool (m = 0)) <$> f (a.mkpair (n + m))))))
- zero : nat.partrec.code
- succ : nat.partrec.code
- left : nat.partrec.code
- right : nat.partrec.code
- pair : nat.partrec.code → nat.partrec.code → nat.partrec.code
- comp : nat.partrec.code → nat.partrec.code → nat.partrec.code
- prec : nat.partrec.code → nat.partrec.code → nat.partrec.code
- rfind' : nat.partrec.code → nat.partrec.code
@[instance]
Equations
Equations
theorem
nat.partrec.code.const_inj
{n₁ n₂ : ℕ} :
nat.partrec.code.const n₁ = nat.partrec.code.const n₂ → n₁ = n₂
Equations
- c.curry n = c.comp ((nat.partrec.code.const n).pair nat.partrec.code.id)
Equations
- cf.rfind'.encode_code = bit1 (bit1 cf.encode_code) + 4
- (cf.prec cg).encode_code = bit1 (bit0 (cf.encode_code.mkpair cg.encode_code)) + 4
- (cf.comp cg).encode_code = bit0 (bit1 (cf.encode_code.mkpair cg.encode_code)) + 4
- (cf.pair cg).encode_code = bit0 (bit0 (cf.encode_code.mkpair cg.encode_code)) + 4
- nat.partrec.code.right.encode_code = 3
- nat.partrec.code.left.encode_code = 2
- nat.partrec.code.succ.encode_code = 1
- nat.partrec.code.zero.encode_code = 0
Equations
- nat.partrec.code.of_nat_code (n + 4) = let m : ℕ := n.div2.div2 in have hm : m < n + 4, from _, nat.partrec.code.of_nat_code._match_1 (nat.partrec.code.of_nat_code n.div2.div2.unpair.fst) (nat.partrec.code.of_nat_code n.div2.div2.unpair.snd) (nat.partrec.code.of_nat_code n.div2.div2.unpair.fst) (nat.partrec.code.of_nat_code n.div2.div2.unpair.snd) (nat.partrec.code.of_nat_code n.div2.div2.unpair.fst) (nat.partrec.code.of_nat_code n.div2.div2.unpair.snd) (nat.partrec.code.of_nat_code n.div2.div2) n.bodd n.div2.bodd
- nat.partrec.code.of_nat_code 3 = nat.partrec.code.right
- nat.partrec.code.of_nat_code 2 = nat.partrec.code.left
- nat.partrec.code.of_nat_code 1 = nat.partrec.code.succ
- nat.partrec.code.of_nat_code 0 = nat.partrec.code.zero
- nat.partrec.code.of_nat_code._match_1 _f_1 _f_2 _f_3 _f_4 _f_5 _f_6 _f_7 bool.tt bool.tt = _f_7.rfind'
- nat.partrec.code.of_nat_code._match_1 _f_1 _f_2 _f_3 _f_4 _f_5 _f_6 _f_7 bool.tt bool.ff = _f_5.prec _f_6
- nat.partrec.code.of_nat_code._match_1 _f_1 _f_2 _f_3 _f_4 _f_5 _f_6 _f_7 bool.ff bool.tt = _f_3.comp _f_4
- nat.partrec.code.of_nat_code._match_1 _f_1 _f_2 _f_3 _f_4 _f_5 _f_6 _f_7 bool.ff bool.ff = _f_1.pair _f_2
@[instance]
Equations
- nat.partrec.code.denumerable = denumerable.mk' {to_fun := nat.partrec.code.encode_code, inv_fun := nat.partrec.code.of_nat_code, left_inv := nat.partrec.code.denumerable._proof_1, right_inv := encode_of_nat_code}
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)
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)
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)
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 × σ → σ} :
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)))
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 → σ → σ} :
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)))
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 × σ → σ} :
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)))
Equations
- cf.rfind'.eval = nat.unpaired (λ (a m : ℕ), roption.map (λ (_x : ℕ), _x + m) (nat.rfind (λ (n : ℕ), (λ (m : ℕ), decidable.to_bool (m = 0)) <$> cf.eval (a.mkpair (n + m)))))
- (cf.prec cg).eval = nat.unpaired (λ (a n : ℕ), nat.elim (cf.eval a) (λ (y : ℕ) (IH : roption ℕ), IH >>= λ (i : ℕ), cg.eval (a.mkpair (y.mkpair i))) n)
- (cf.comp cg).eval = λ (n : ℕ), cg.eval n >>= cf.eval
- (cf.pair cg).eval = λ (n : ℕ), nat.mkpair <$> cf.eval n <*> cg.eval n
- nat.partrec.code.right.eval = ↑(λ (n : ℕ), n.unpair.snd)
- nat.partrec.code.left.eval = ↑(λ (n : ℕ), n.unpair.fst)
- nat.partrec.code.succ.eval = ↑nat.succ
- nat.partrec.code.zero.eval = has_pure.pure 0
@[instance]
Equations
- nat.partrec.code.has_mem = {mem := λ (f : ℕ →. ℕ) (c : nat.partrec.code), c.eval = f}
@[simp]
theorem
nat.partrec.code.eval_const
(n m : ℕ) :
(nat.partrec.code.const n).eval m = roption.some n
@[simp]
@[simp]
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)
theorem
nat.partrec.code.exists_code
{f : ℕ →. ℕ} :
nat.partrec f ↔ ∃ (c : nat.partrec.code), c.eval = f
Equations
- nat.partrec.code.evaln (k + 1) cf.rfind' = λ (n : ℕ), guard (n ≤ k) >> nat.unpaired (λ (a m : ℕ), nat.partrec.code.evaln (k + 1) cf (a.mkpair m) >>= λ (x : ℕ), ite (x = 0) (has_pure.pure m) (nat.partrec.code.evaln k cf.rfind' (a.mkpair (m + 1)))) n
- nat.partrec.code.evaln (k + 1) (cf.prec cg) = λ (n : ℕ), guard (n ≤ k) >> nat.unpaired (λ (a n : ℕ), nat.cases (nat.partrec.code.evaln (k + 1) cf a) (λ (y : ℕ), nat.partrec.code.evaln k (cf.prec cg) (a.mkpair y) >>= λ (i : ℕ), nat.partrec.code.evaln (k + 1) cg (a.mkpair (y.mkpair i))) n) n
- nat.partrec.code.evaln (k + 1) (cf.comp cg) = λ (n : ℕ), guard (n ≤ k) >> (nat.partrec.code.evaln (k + 1) cg n >>= λ (x : ℕ), nat.partrec.code.evaln (k + 1) cf x)
- nat.partrec.code.evaln (k + 1) (cf.pair cg) = λ (n : ℕ), guard (n ≤ k) >> nat.mkpair <$> nat.partrec.code.evaln (k + 1) cf n <*> nat.partrec.code.evaln (k + 1) cg n
- nat.partrec.code.evaln (k + 1) nat.partrec.code.right = λ (n : ℕ), guard (n ≤ k) >> has_pure.pure n.unpair.snd
- nat.partrec.code.evaln (k + 1) nat.partrec.code.left = λ (n : ℕ), guard (n ≤ k) >> has_pure.pure n.unpair.fst
- nat.partrec.code.evaln (k + 1) nat.partrec.code.succ = λ (n : ℕ), guard (n ≤ k) >> has_pure.pure n.succ
- nat.partrec.code.evaln (k + 1) nat.partrec.code.zero = λ (n : ℕ), guard (n ≤ k) >> has_pure.pure 0
- nat.partrec.code.evaln 0 _x = λ (m : ℕ), option.none
theorem
nat.partrec.code.evaln_bound
{k : ℕ}
{c : nat.partrec.code}
{n x : ℕ} :
x ∈ nat.partrec.code.evaln k c n → n < k
theorem
nat.partrec.code.evaln_mono
{k₁ k₂ : ℕ}
{c : nat.partrec.code}
{n x : ℕ} :
k₁ ≤ k₂ → x ∈ nat.partrec.code.evaln k₁ c n → x ∈ nat.partrec.code.evaln k₂ c n
theorem
nat.partrec.code.evaln_sound
{k : ℕ}
{c : nat.partrec.code}
{n x : ℕ} :
x ∈ nat.partrec.code.evaln k c n → x ∈ c.eval n
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)
theorem
nat.partrec.code.fixed_point
{f : nat.partrec.code → nat.partrec.code} :
computable f → (∃ (c : nat.partrec.code), (f c).eval = c.eval)
theorem
nat.partrec.code.fixed_point₂
{f : nat.partrec.code → ℕ →. ℕ} :
partrec₂ f → (∃ (c : nat.partrec.code), c.eval = f c)