feat(data/computablility): reduced partrec

Author: digama0

data/computability/halting.lean

@@ -176,3 +176,143 @@ theorem halting_problem (n) : ¬ computable_pred (λ c, (eval c n).dom)
 | h := rice {f | (f n).dom} h nat.partrec.zero nat.partrec.none trivial
 
 end computable_pred
+
+namespace nat
+open vector roption
+
+/-- A simplified basis for `partrec`. -/
+inductive partrec' : ∀ {n}, (vector ℕ n →. ℕ) → Prop
+| prim {n f} : @primrec' n f → @partrec' n f
+| comp {m n f} (g : fin n → vector ℕ m →. ℕ) :
+  partrec' f → (∀ i, partrec' (g i)) →
+  partrec' (λ v, m_of_fn (λ i, g i v) >>= f)
+| rfind {n} {f : vector ℕ (n+1) → ℕ} : @partrec' (n+1) f →
+  partrec' (λ v, rfind (λ n, some (f (n :: v) = 0)))
+
+end nat
+
+namespace nat.partrec'
+open vector partrec computable nat (partrec') nat.partrec'
+
+theorem to_part {n f} (pf : @partrec' n f) : partrec f :=
+begin
+  induction pf,
+  case nat.partrec'.prim : n f hf { exact hf.to_prim.to_comp },
+  case nat.partrec'.comp : m n f g _ _ hf hg {
+    exact (vector_m_of_fn (λ i, hg i)).bind (hf.comp snd) },
+  case nat.partrec'.rfind : n f _ hf {
+    have := ((primrec.eq.comp primrec.id (primrec.const 0)).to_comp.comp
+      (hf.comp (vector_cons.comp snd fst))).to₂.part,
+    exact this.rfind },
+end
+
+theorem of_eq {n} {f g : vector ℕ n →. ℕ}
+  (hf : partrec' f) (H : ∀ i, f i = g i) : partrec' g :=
+(funext H : f = g) ▸ hf
+
+theorem of_prim {n} {f : vector ℕ n → ℕ} (hf : primrec f) : @partrec' n f :=
+prim (nat.primrec'.of_prim hf)
+
+theorem head {n : ℕ} : @partrec' n.succ (@head ℕ n) :=
+prim nat.primrec'.head
+
+theorem tail {n f} (hf : @partrec' n f) : @partrec' n.succ (λ v, f v.tail) :=
+(hf.comp _ (λ i, @prim _ _ $ nat.primrec'.nth i.succ)).of_eq $
+λ v, by simp; rw [← of_fn_nth v.tail]; congr; funext i; simp
+
+protected theorem bind {n f g}
+  (hf : @partrec' n f) (hg : @partrec' (n+1) g) :
+  @partrec' n (λ v, (f v).bind (λ a, g (a :: v))) :=
+(@comp n (n+1) g
+  (λ i, fin.cases f (λ i v, some (v.nth i)) i) hg
+  (λ i, begin
+    refine fin.cases _ (λ i, _) i; simp *,
+    exact prim (nat.primrec'.nth _)
+  end)).of_eq $
+λ v, by simp [m_of_fn, roption.bind_assoc, pure]
+
+protected theorem map {n f} {g : vector ℕ (n+1) → ℕ}
+  (hf : @partrec' n f) (hg : @partrec' (n+1) g) :
+  @partrec' n (λ v, (f v).map (λ a, g (a :: v))) :=
+by simp [(roption.bind_some_eq_map _ _).symm];
+   exact hf.bind hg
+
+def vec {n m} (f : vector ℕ n → vector ℕ m) :=
+∀ i, partrec' (λ v, (f v).nth i)
+
+theorem vec.prim {n m f} (hf : @nat.primrec'.vec n m f) : vec f :=
+λ i, prim $ hf i
+
+protected theorem nil {n} : @vec n 0 (λ _, nil) := λ i, i.elim0
+
+protected theorem cons {n m} {f : vector ℕ n → ℕ} {g}
+  (hf : @partrec' n f) (hg : @vec n m g) :
+  vec (λ v, f v :: g v) :=
+λ i, fin.cases (by simp *) (λ i, by simp [hg i]) i
+
+theorem idv {n} : @vec n n id := vec.prim nat.primrec'.idv
+
+theorem comp' {n m f g} (hf : @partrec' m f) (hg : @vec n m g) :
+  partrec' (λ v, f (g v)) :=
+(hf.comp _ hg).of_eq $ λ v, by simp
+
+theorem comp₁ {n} (f : ℕ →. ℕ) {g : vector ℕ n → ℕ}
+  (hf : @partrec' 1 (λ v, f v.head)) (hg : @partrec' n g) :
+  @partrec' n (λ v, f (g v)) :=
+by simpa using hf.comp' (partrec'.cons hg partrec'.nil)
+
+theorem rfind_opt {n} {f : vector ℕ (n+1) → ℕ}
+  (hf : @partrec' (n+1) f) :
+  @partrec' n (λ v, nat.rfind_opt (λ a, of_nat (option ℕ) (f (a :: v)))) :=
+((rfind $ (of_prim (primrec.nat_sub.comp (primrec.const 1) primrec.vector_head))
+   .comp₁ (λ n, roption.some (1 - n)) hf)
+   .bind ((prim nat.primrec'.pred).comp₁ nat.pred hf)).of_eq $
+λ v, roption.ext $ λ b, begin
+  simp [nat.rfind_opt, -nat.mem_rfind],
+  refine exists_congr (λ a,
+    (and_congr (iff_of_eq _) iff.rfl).trans (and_congr_right (λ h, _))),
+  { congr; funext n,
+    simp, cases f (n :: v); simp [nat.succ_ne_zero]; refl },
+  { have := nat.rfind_spec h,
+    simp at this,
+    cases f (a :: v) with c, {cases this},
+    rw [← option.some_inj, eq_comm], refl }
+end
+
+open nat.partrec.code
+theorem of_part : ∀ {n f}, partrec f → @partrec' n f :=
+suffices ∀ f, nat.partrec f → @partrec' 1 (λ v, f v.head), from
+λ n f hf, begin
+  let g, swap,
+  exact (comp₁ g (this g hf) (prim nat.primrec'.encode)).of_eq
+    (λ i, by dsimp [g]; simp [encodek, roption.map_id']),
+end,
+λ f hf, begin
+  rcases exists_code.1 hf with ⟨c, rfl⟩,
+  simpa [eval_eq_rfind_opt] using
+    (rfind_opt $ of_prim $ primrec.encode_iff.2 $ evaln_prim.comp $
+      (primrec.vector_head.pair (primrec.const c)).pair $
+      primrec.vector_head.comp primrec.vector_tail)
+end
+
+theorem part_iff {n f} : @partrec' n f ↔ partrec f := ⟨to_part, of_part⟩
+
+theorem part_iff₁ {f : ℕ →. ℕ} :
+  @partrec' 1 (λ v, f v.head) ↔ partrec f :=
+part_iff.trans ⟨
+  λ h, (h.comp $ (primrec.vector_of_fn $
+    λ i, primrec.id).to_comp).of_eq (λ v, by simp),
+  λ h, h.comp vector_head⟩
+
+theorem part_iff₂ {f : ℕ → ℕ →. ℕ} :
+  @partrec' 2 (λ v, f v.head v.tail.head) ↔ partrec₂ f :=
+part_iff.trans ⟨
+  λ h, (h.comp $ vector_cons.comp fst $
+    vector_cons.comp snd (const nil)).of_eq (λ v, by simp),
+  λ h, h.comp vector_head (vector_head.comp vector_tail)⟩
+
+theorem vec_iff {m n f} : @vec m n f ↔ computable f :=
+⟨λ h, by simpa using vector_of_fn (λ i, to_part (h i)),
+ λ h i, of_prim $ vector_nth.comp h (primrec.const i)⟩
+
+end nat.primrec'

data/computability/partrec.lean

@@ -284,6 +284,17 @@ theorem list_append : computable₂ ((++) : list α → list α → list α) :=
 theorem list_concat : computable₂ (λ l (a:α), l ++ [a]) := primrec.list_concat.to_comp
 theorem list_length : computable (@list.length α) := primrec.list_length.to_comp
 
+theorem vector_cons {n} : computable₂ (@vector.cons α n) := primrec.vector_cons.to_comp
+theorem vector_to_list {n} : computable (@vector.to_list α n) := primrec.vector_to_list.to_comp
+theorem vector_length {n} : computable (@vector.length α n) := primrec.vector_length.to_comp
+theorem vector_head {n} : computable (@vector.head α n) := primrec.vector_head.to_comp
+theorem vector_tail {n} : computable (@vector.tail α n) := primrec.vector_tail.to_comp
+theorem vector_nth {n} : computable₂ (@vector.nth α n) := primrec.vector_nth.to_comp
+theorem vector_nth' {n} : computable (@vector.nth α n) := primrec.vector_nth'.to_comp
+theorem vector_of_fn' {n} : computable (@vector.of_fn α n) := primrec.vector_of_fn'.to_comp
+
+theorem fin_app {n} : computable₂ (@id (fin n → σ)) := primrec.fin_app.to_comp
+
 protected theorem encode : computable (@encode α _) :=
 primrec.encode.to_comp
 
@@ -463,8 +474,19 @@ theorem bind_decode2_iff {f : α →. σ} : partrec f ↔
 λ h, map_encode_iff.1 $ by simpa [encodek2]
   using (nat_iff.2 h).comp (@computable.encode α _)⟩
 
+theorem vector_m_of_fn : ∀ {n} {f : fin n → α →. σ}, (∀ i, partrec (f i)) →
+  partrec (λ (a : α), vector.m_of_fn (λ i, f i a))
+| 0     f hf := const _
+| (n+1) f hf := by simp [vector.m_of_fn]; exact
+  (hf 0).bind (partrec.bind ((vector_m_of_fn (λ i, hf i.succ)).comp fst)
+    (primrec.vector_cons.to_comp.comp (snd.comp fst) snd))
+
 end partrec
 
+@[simp] theorem vector.m_of_fn_roption_some {α n} : ∀ (f : fin n → α),
+  vector.m_of_fn (λ i, roption.some (f i)) = roption.some (vector.of_fn f) :=
+vector.m_of_fn_pure
+
 namespace computable
 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
@@ -561,6 +583,16 @@ option_some_iff.1 $
   simp [IH, H, list.range_concat, option.bind]
 end
 
+theorem list_of_fn : ∀ {n} {f : fin n → α → σ},
+  (∀ i, computable (f i)) → computable (λ a, list.of_fn (λ i, f i a))
+| 0     f hf := const []
+| (n+1) f hf := by simp [list.of_fn_succ]; exact
+  list_cons.comp (hf 0) (list_of_fn (λ i, hf i.succ))
+
+theorem vector_of_fn {n} {f : fin n → α → σ}
+  (hf : ∀ i, computable (f i)) : computable (λ a, vector.of_fn (λ i, f i a)) :=
+(partrec.vector_m_of_fn hf).of_eq $ λ a, by simp
+
 end computable
 
 namespace partrec

data/computability/partrec_code.lean

@@ -877,14 +877,17 @@ end
 section
 open partrec computable
 
+theorem eval_eq_rfind_opt (c n) :
+  eval c n = nat.rfind_opt (λ k, evaln k c n) :=
+roption.ext $ λ x, begin
+  refine evaln_complete.trans (nat.rfind_opt_mono _).symm,
+  intros a m n hl, apply evaln_mono hl,
+end
+
 theorem eval_part : partrec₂ eval :=
 (rfind_opt (evaln_prim.to_comp.comp
   ((snd.pair (fst.comp fst)).pair (snd.comp fst))).to₂).of_eq $
-λ a, roption.ext $ λ x, begin
-  simp,
-  refine (nat.rfind_opt_mono _).trans evaln_complete.symm,
-  intros a m n hl, apply evaln_mono hl,
-end
+λ a, by simp [eval_eq_rfind_opt]
 
 theorem fixed_point
   {f : code → code} (hf : computable f) : ∃ c : code, eval (f c) = eval c :=

data/computability/primrec.lean

@@ -1187,20 +1187,20 @@ theorem tail {n f} (hf : @primrec' n f) : @primrec' n.succ (λ v, f v.tail) :=
 (hf.comp _ (λ i, @nth _ i.succ)).of_eq $
 λ v, by rw [← of_fn_nth v.tail]; congr; funext i; simp
 
-def primvec {n m} (f : vector ℕ n → vector ℕ m) :=
+def vec {n m} (f : vector ℕ n → vector ℕ m) :=
 ∀ i, primrec' (λ v, (f v).nth i)
 
-protected theorem nil {n} : @primvec n 0 (λ _, nil) := λ i, i.elim0
+protected theorem nil {n} : @vec n 0 (λ _, nil) := λ i, i.elim0
 
 protected theorem cons {n m f g}
-  (hf : @primrec' n f) (hg : @primvec n m g) :
-  primvec (λ v, f v :: g v) :=
+  (hf : @primrec' n f) (hg : @vec n m g) :
+  vec (λ v, f v :: g v) :=
 λ i, fin.cases (by simp *) (λ i, by simp [hg i]) i
 
-theorem idv {n} : @primvec n n id := nth
+theorem idv {n} : @vec n n id := nth
 
 theorem comp' {n m f g}
-  (hf : @primrec' m f) (hg : @primvec n m g) :
+  (hf : @primrec' m f) (hg : @vec n m g) :
   primrec' (λ v, f (g v)) :=
 (hf.comp _ hg).of_eq $ λ v, by simp
 
@@ -1337,8 +1337,8 @@ prim_iff.trans ⟨
     vector_cons.comp snd (primrec.const nil)).of_eq (λ v, by simp),
   λ h, h.comp vector_head (vector_head.comp vector_tail)⟩
 
-theorem primvec_iff {m n f} :
-  @primvec m n f ↔ primrec f :=
+theorem vec_iff {m n f} :
+  @vec m n f ↔ primrec f :=
 ⟨λ h, by simpa using vector_of_fn (λ i, to_prim (h i)),
  λ h i, of_prim $ vector_nth.comp h (primrec.const i)⟩
 

data/vector2.lean

@@ -69,4 +69,26 @@ by simp [nth_zero]
   (a : α) (v : vector α n) (i : fin n) : nth (a :: v) i.succ = nth v i :=
 by rw [← nth_tail, tail_cons]
 
+def {u} m_of_fn {m} [monad m] {α : Type u} : ∀ {n}, (fin n → m α) → m (vector α n)
+| 0     f := pure nil
+| (n+1) f := do a ← f 0, v ← m_of_fn (λi, f i.succ), pure (a :: v)
+
+theorem m_of_fn_pure {m} [monad m] [is_lawful_monad m] {α} :
+  ∀ {n} (f : fin n → α), @m_of_fn m _ _ _ (λ i, pure (f i)) = pure (of_fn f)
+| 0     f := rfl
+| (n+1) f := by simp [m_of_fn, @m_of_fn_pure n, of_fn]
+
+def {u} mmap {m} [monad m] {α} {β : Type u} (f : α → m β) :
+  ∀ {n}, vector α n → m (vector β n)
+| _ ⟨[], rfl⟩   := pure nil
+| _ ⟨a::l, rfl⟩ := do h' ← f a, t' ← mmap ⟨l, rfl⟩, pure (h' :: t')
+
+@[simp] theorem mmap_nil {m} [monad m] {α β} (f : α → m β) :
+  mmap f nil = pure nil := rfl
+
+@[simp] theorem mmap_cons {m} [monad m] {α β} (f : α → m β) (a) :
+  ∀ {n} (v : vector α n), mmap f (a::v) =
+  do h' ← f a, t' ← mmap f v, pure (h' :: t')
+| _ ⟨l, rfl⟩ := rfl
+
 end vector