feat(computability/halting): halting problem

data/computability/halting.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+
+More partial recursive functions using a universal program;
+Rice's theorem and the halting problem.
+-/
+import data.computability.partrec_code
+
+open encodable denumerable
+
+namespace nat.partrec
+open computable roption
+
+theorem merge' {f g}
+  (hf : nat.partrec f) (hg : nat.partrec g) :
+  ∃ h, nat.partrec h ∧ ∀ a,
+    (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧
+    ((h a).dom ↔ (f a).dom ∨ (g a).dom) :=
+begin
+  rcases code.exists_code.1 hf with ⟨cf, rfl⟩,
+  rcases code.exists_code.1 hg with ⟨cg, rfl⟩,
+  have : nat.partrec (λ n,
+    (nat.rfind_opt (λ k, cf.evaln k n <|> cg.evaln k n))) :=
+  partrec.nat_iff.1 (partrec.rfind_opt $
+    primrec.option_orelse.to_comp.comp
+      (code.evaln_prim.to_comp.comp $ (snd.pair (const cf)).pair fst)
+      (code.evaln_prim.to_comp.comp $ (snd.pair (const cg)).pair fst)),
+  refine ⟨_, this, λ n, _⟩,
+  suffices, refine ⟨this,
+    ⟨λ h, (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, _⟩⟩,
+  { intro h, rw nat.rfind_opt_dom,
+    simp [dom_iff_mem, code.evaln_complete] at h,
+    rcases h with ⟨x, k, e⟩ | ⟨x, k, e⟩,
+    { refine ⟨k, x, _⟩, simp [e] },
+    { refine ⟨k, _⟩,
+      cases cf.evaln k n with y,
+      { exact ⟨x, by simp [e]⟩ },
+      { exact ⟨y, by simp⟩ } } },
+  { intros x h,
+    rcases nat.rfind_opt_spec h with ⟨k, e⟩,
+    revert e,
+    simp; cases e' : cf.evaln k n with y; simp; intro,
+    { exact or.inr (code.evaln_sound e) },
+    { subst y,
+        exact or.inl (code.evaln_sound e') } }
+end
+
+end nat.partrec
+
+namespace partrec
+variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
+variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
+
+open computable roption nat.partrec (code) nat.partrec.code
+
+theorem merge' {f g : α →. σ}
+  (hf : partrec f) (hg : partrec g) :
+  ∃ k : α →. σ, partrec k ∧ ∀ a,
+    (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧
+    ((k a).dom ↔ (f a).dom ∨ (g a).dom) :=
+let ⟨k, hk, H⟩ :=
+  nat.partrec.merge' (bind_decode2_iff.1 hf) (bind_decode2_iff.1 hg) in
+begin
+  let k' := λ a, (k (encode a)).bind (λ n, decode σ n),
+  refine ⟨k', ((nat_iff.2 hk).comp computable.encode).bind
+    (computable.decode.of_option.comp snd).to₂, λ a, _⟩,
+  suffices, refine ⟨this,
+    ⟨λ h, (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, _⟩⟩,
+  { intro h, simp [k'],
+    have hk : (k (encode a)).dom :=
+      (H _).2.2 (by simpa [encodek2] using h),
+    existsi hk,
+    cases (H _).1 _ ⟨hk, rfl⟩ with h h;
+    { simp at h,
+      rcases h with ⟨a', ha', y, hy, e⟩,
+      simp [e.symm, encodek] } },
+  { intros x h', simp [k'] at h',
+    rcases h' with ⟨n, hn, hx⟩,
+    have := (H _).1 _ hn, simp [mem_decode2] at this,
+    cases this with h h;
+    { rcases h with ⟨a', ⟨ha₁, ha₂⟩, y, hy, rfl⟩,
+      rw encodek at hx ha₁, simp at hx ha₁, substs y a',
+      simp [hy] } },
+end
+
+theorem merge {f g : α →. σ}
+  (hf : partrec f) (hg : partrec g)
+  (H : ∀ a (x ∈ f a) (y ∈ g a), x = y) :
+  ∃ k : α →. σ, partrec k ∧ ∀ a x, x ∈ k a ↔ x ∈ f a ∨ x ∈ g a :=
+let ⟨k, hk, K⟩ := merge' hf hg in
+⟨k, hk, λ a x, ⟨(K _).1 _, λ h, begin
+  have : (k a).dom := (K _).2.2 (h.imp Exists.fst Exists.fst),
+  refine ⟨this, _⟩,
+  cases h with h h; cases (K _).1 _ ⟨this, rfl⟩ with h' h',
+  { exact mem_unique h' h },
+  { exact (H _ _ h _ h').symm },
+  { exact H _ _ h' _ h },
+  { exact mem_unique h' h }
+end⟩⟩
+
+theorem cond {c : α → bool} {f : α →. σ} {g : α →. σ}
+  (hc : computable c) (hf : partrec f) (hg : partrec g) :
+  partrec (λ a, cond (c a) (f a) (g a)) :=
+let ⟨cf, ef⟩ := exists_code.1 hf,
+    ⟨cg, eg⟩ := exists_code.1 hg in
+((eval_part.comp
+    (computable.cond hc (const cf) (const cg)) computable.id).bind
+  ((@computable.decode σ _).comp snd).of_option.to₂).of_eq $
+λ a, by cases c a; simp [ef, eg, encodek]
+
+theorem sum_cases
+  {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ →. σ}
+  (hf : computable f) (hg : partrec₂ g) (hh : partrec₂ h) :
+  @partrec _ σ _ _ (λ a, sum.cases_on (f a) (g a) (h a)) :=
+option_some_iff.1 $ (cond
+  (sum_cases hf (const tt).to₂ (const ff).to₂)
+  (sum_cases_left hf (option_some_iff.2 hg).to₂ (const option.none).to₂)
+  (sum_cases_right hf (const option.none).to₂ (option_some_iff.2 hh).to₂))
+.of_eq $ λ a, by cases f a; simp
+
+end partrec
+
+def computable_pred {α} [primcodable α] (p : α → Prop) :=
+∃ [D : decidable_pred p],
+by exactI computable (λ a, to_bool (p a))
+
+/- recursively enumerable predicate -/
+def re_pred {α} [primcodable α] (p : α → Prop) :=
+partrec (λ a, roption.assert (p a) (λ _, roption.some ()))
+
+theorem computable_pred.of_eq {α} [primcodable α]
+  {p q : α → Prop}
+  (hp : computable_pred p) (H : ∀ a, p a ↔ q a) : computable_pred q :=
+(funext (λ a, propext (H a)) : p = q) ▸ hp
+
+namespace computable_pred
+variables {α : Type*} {σ : Type*}
+variables [primcodable α] [primcodable σ]
+open nat.partrec (code) nat.partrec.code computable
+
+theorem rice (C : set (ℕ →. ℕ))
+  (h : computable_pred (λ c, eval c ∈ C))
+  {f g} (hf : nat.partrec f) (hg : nat.partrec g)
+  (fC : f ∈ C) : g ∈ C :=
+begin
+  cases h with _ h, resetI,
+  rcases fixed_point₂ (partrec.cond (h.comp fst)
+    ((partrec.nat_iff.2 hg).comp snd).to₂
+    ((partrec.nat_iff.2 hf).comp snd).to₂).to₂ with ⟨c, e⟩,
+  simp at e,
+  by_cases eval c ∈ C,
+  { simp [h] at e, rwa ← e },
+  { simp at h, simp [h] at e,
+    rw e at h, contradiction }
+end
+
+theorem rice₂ (C : set code)
+  (H : ∀ cf cg, eval cf = eval cg → (cf ∈ C ↔ cg ∈ C)) :
+  computable_pred (λ c, c ∈ C) ↔ C = ∅ ∨ C = set.univ :=
+by haveI := classical.dec; exact
+have hC : ∀ f, f ∈ C ↔ eval f ∈ eval '' C,
+from λ f, ⟨set.mem_image_of_mem _, λ ⟨g, hg, e⟩, (H _ _ e).1 hg⟩,
+⟨λ h, or_iff_not_imp_left.2 $ λ C0,
+  set.eq_univ_of_forall $ λ cg,
+  let ⟨cf, fC⟩ := set.ne_empty_iff_exists_mem.1 C0 in
+  (hC _).2 $ rice (eval '' C) (h.of_eq hC)
+    (partrec.nat_iff.1 $ eval_part.comp (const cf) computable.id)
+    (partrec.nat_iff.1 $ eval_part.comp (const cg) computable.id)
+    ((hC _).1 fC),
+λ h, by rcases h with rfl | rfl; simp [computable_pred];
+  exact ⟨by apply_instance, computable.const _⟩⟩
+
+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

data/computability/partrec.lean

@@ -100,6 +100,40 @@ eq_none_iff.2 $ λ a h,
 let ⟨n, h₁, h₂⟩ := rfind_dom'.1 h.fst in
 (p0 ▸ h₂ (zero_le _) : (@roption.none bool).dom)
 
+def rfind_opt {α} (f : ℕ → option α) : roption α :=
+(rfind (λ n, (f n).is_some)).bind (λ n, f n)
+
+theorem rfind_opt_spec {α} {f : ℕ → option α} {a}
+ (h : a ∈ rfind_opt f) : ∃ n, a ∈ f n :=
+let ⟨n, h₁, h₂⟩ := mem_bind_iff.1 h in ⟨n, mem_coe.1 h₂⟩
+
+theorem rfind_opt_dom {α} {f : ℕ → option α} :
+  (rfind_opt f).dom ↔ ∃ n a, a ∈ f n :=
+⟨λ h, (rfind_opt_spec ⟨h, rfl⟩).imp (λ n h, ⟨_, h⟩),
+ λ h, begin
+  have h' : ∃ n, (f n).is_some :=
+    h.imp (λ n, option.is_some_iff_exists.2),
+  have s := nat.find_spec h',
+  have fd : (rfind (λ n, (f n).is_some)).dom :=
+    ⟨nat.find h', by simpa using s.symm, λ _ _, trivial⟩,
+  refine ⟨fd, _⟩,
+  have := rfind_spec (get_mem fd),
+  simp at this ⊢,
+  cases option.is_some_iff_exists.1 this.symm with a e,
+  rw e, trivial
+end⟩
+
+theorem rfind_opt_mono {α} {f : ℕ → option α}
+  (H : ∀ {a m n}, m ≤ n → a ∈ f m → a ∈ f n)
+  {a} : a ∈ rfind_opt f ↔ ∃ n, a ∈ f n :=
+⟨rfind_opt_spec, λ ⟨n, h⟩, begin
+  have h' := rfind_opt_dom.2 ⟨_, _, h⟩,
+  cases rfind_opt_spec ⟨h', rfl⟩ with k hk,
+  have := (H (le_max_left _ _) h).symm.trans
+          (H (le_max_right _ _) hk),
+  simp at this, simp [this, get_mem]
+end⟩
+
 inductive partrec : (ℕ →. ℕ) → Prop
 | zero : partrec (pure 0)
 | succ : partrec succ
@@ -193,6 +227,9 @@ theorem primrec.to_comp {α σ} [primcodable α] [primcodable σ]
 (nat.partrec.ppred.comp (nat.partrec.of_primrec hf)).of_eq $
 λ n, by simp; cases decode α n; simp [option.map, option.bind]
 
+theorem primrec₂.to_comp {α β σ} [primcodable α] [primcodable β] [primcodable σ]
+  {f : α → β → σ} (hf : primrec₂ f) : computable₂ f := hf.to_comp
+
 theorem computable.part {α σ} [primcodable α] [primcodable σ]
   {f : α → σ} (hf : computable f) : partrec (f : α →. σ) := hf
 
@@ -247,6 +284,21 @@ 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
 
+protected theorem encode : computable (@encode α _) :=
+primrec.encode.to_comp
+
+protected theorem decode : computable (decode α) :=
+primrec.decode.to_comp
+
+protected theorem of_nat (α) [denumerable α] : computable (of_nat α) :=
+(primrec.of_nat _).to_comp
+
+theorem encode_iff {f : α → σ} : computable (λ a, encode (f a)) ↔ computable f :=
+iff.rfl
+
+theorem option_some : computable (@option.some α) :=
+primrec.option_some.to_comp
+
 end computable
 
 namespace partrec
@@ -306,6 +358,9 @@ theorem comp {f : β →. σ} {g : α → β}
 theorem nat_iff {f : ℕ →. ℕ} : partrec f ↔ nat.partrec f :=
 by simp [partrec, map_id']
 
+theorem map_encode_iff {f : α →. σ} : partrec (λ a, (f a).map encode) ↔ partrec f :=
+iff.rfl
+
 end partrec
 
 namespace partrec₂
@@ -381,6 +436,11 @@ theorem rfind {p : α → ℕ →. bool} (hp : partrec₂ p) :
   cases b; refl
 end
 
+theorem rfind_opt {f : α → ℕ → option σ} (hf : computable₂ f) :
+  partrec (λ a, nat.rfind_opt (f a)) :=
+(rfind (primrec.option_is_some.to_comp.comp hf).part.to₂).bind
+  (of_option hf)
+
 theorem nat_cases_right
   {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ}
   (hf : computable f) (hg : computable g) (hh : partrec₂ h) :
@@ -396,51 +456,19 @@ theorem nat_cases_right
     exact ⟨⟨this n, H.fst⟩, H.snd⟩ }
 end
 
-/-
-theorem cond {c : α → bool} {f : α →. σ} {g : α →. σ}
-  (hc : computable c) (hf : partrec f) (hg : partrec g) :
-  partrec (λ a, cond (c a) (f a) (g a)) :=
-(nat_cases (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq $
-λ a, by cases c a; refl
-
-theorem sum_cases
-  {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ →. σ}
-  (hf : computable f) (hg : partrec₂ g) (hh : partrec₂ h) :
-  @partrec _ σ _ _ (λ a, sum.cases_on (f a) (g a) (h a)) :=
-(cond (nat_bodd.comp $ encode_iff.2 hf)
-  (option_map (primrec.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hh)
-  (option_map (primrec.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hg)).of_eq $
-λ a, by cases f a with b c;
-  simp [nat.div2_bit, nat.bodd_bit, encodek]; refl
-
-theorem fix {α σ} [primcodable α] [primcodable σ]
-  {f : α →. σ ⊕ α} (hf : partrec f) : partrec (pfun.fix f) :=
-begin
-  have := nat_elim snd fst _,
-end
--/
+theorem bind_decode2_iff {f : α →. σ} : partrec f ↔
+  nat.partrec (λ n, roption.bind (decode2 α n) (λ a, (f a).map encode)) :=
+⟨λ hf, nat_iff.1 $ (of_option primrec.decode2.to_comp).bind $
+  (map hf (computable.encode.comp snd).to₂).comp snd,
+λ h, map_encode_iff.1 $ by simpa [encodek2]
+  using (nat_iff.2 h).comp (@computable.encode α _)⟩
 
 end partrec
 
 namespace computable
 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
 
-protected theorem encode : computable (@encode α _) :=
-primrec.encode.to_comp
-
-protected theorem decode : computable (decode α) :=
-primrec.decode.to_comp
-
-protected theorem of_nat (α) [denumerable α] : computable (of_nat α) :=
-(primrec.of_nat _).to_comp
-
-theorem encode_iff {f : α → σ} : computable (λ a, encode (f a)) ↔ computable f :=
-iff.rfl
-
-theorem option_some : computable (@option.some α) :=
-primrec.option_some.to_comp
-
 theorem option_some_iff {f : α → σ} : computable (λ a, some (f a)) ↔ computable f :=
 ⟨λ h, encode_iff.1 $ primrec.pred.to_comp.comp $ encode_iff.2 h,
  option_some.comp⟩