chore(data/pfun): rename roption to part, split data.part off `…

…data.pfun` (#8544)

src/computability/halting.lean

@@ -18,7 +18,7 @@ A universal partial recursive function, Rice's theorem, and the halting problem.
 open encodable denumerable
 
 namespace nat.partrec
-open computable roption
+open computable part
 
 theorem merge' {f g}
   (hf : nat.partrec f) (hg : nat.partrec g) :
@@ -60,7 +60,7 @@ namespace partrec
 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
 
-open computable roption nat.partrec (code) nat.partrec.code
+open computable part nat.partrec (code) nat.partrec.code
 
 theorem merge' {f g : α →. σ}
   (hf : partrec f) (hg : partrec g) :
@@ -137,7 +137,7 @@ by exactI computable (λ a, to_bool (p a))
 /-- A recursively enumerable predicate is one which is the domain of a computable partial function.
  -/
 def re_pred {α} [primcodable α] (p : α → Prop) :=
-partrec (λ a, roption.assert (p a) (λ _, roption.some ()))
+partrec (λ a, part.assert (p a) (λ _, part.some ()))
 
 theorem computable_pred.of_eq {α} [primcodable α]
   {p q : α → Prop}
@@ -165,8 +165,8 @@ theorem to_re {p : α → Prop} (hp : computable_pred p) : re_pred p :=
 begin
   obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp,
   unfold re_pred,
-  refine (partrec.cond hf (decidable.partrec.const' (roption.some ())) partrec.none).of_eq
-    (λ n, roption.ext $ λ a, _),
+  refine (partrec.cond hf (decidable.partrec.const' (part.some ())) partrec.none).of_eq
+    (λ n, part.ext $ λ a, _),
   cases a, cases f n; simp
 end
 
@@ -215,15 +215,15 @@ theorem computable_iff_re_compl_re {p : α → Prop} [decidable_pred p] :
   obtain ⟨k, pk, hk⟩ := partrec.merge
     (h₁.map (computable.const tt).to₂)
     (h₂.map (computable.const ff).to₂) _,
-  { refine partrec.of_eq pk (λ n, roption.eq_some_iff.2 _),
+  { refine partrec.of_eq pk (λ n, part.eq_some_iff.2 _),
     rw hk, simp, apply decidable.em },
   { intros a x hx y hy, simp at hx hy, cases hy.1 hx.1 }
 end⟩⟩
 
 end computable_pred
 
 namespace nat
-open vector roption
+open vector part
 
 /-- A simplified basis for `partrec`. -/
 inductive partrec' : ∀ {n}, (vector ℕ n →. ℕ) → Prop
@@ -247,7 +247,7 @@ begin
     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,
+      (hf.comp (vector_cons.comp snd fst))).to₂.partrec₂,
     exact this.rfind },
 end
 
@@ -274,12 +274,12 @@ protected theorem bind {n f g}
     refine fin.cases _ (λ i, _) i; simp *,
     exact prim (nat.primrec'.nth _)
   end)).of_eq $
-λ v, by simp [m_of_fn, roption.bind_assoc, pure]
+λ v, by simp [m_of_fn, part.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];
+by simp [(part.bind_some_eq_map _ _).symm];
    exact hf.bind hg
 
 /-- Analogous to `nat.partrec'` for `ℕ`-valued functions, a predicate for partial recursive
@@ -312,9 +312,9 @@ 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)
+   .comp₁ (λ n, part.some (1 - n)) hf)
    .bind ((prim nat.primrec'.pred).comp₁ nat.pred hf)).of_eq $
-λ v, roption.ext $ λ b, begin
+λ v, part.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, _))),
@@ -332,7 +332,7 @@ 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 only [g]; simp [encodek, roption.map_id']),
+    (λ i, by dsimp only [g]; simp [encodek, part.map_id']),
 end,
 λ f hf, begin
   obtain ⟨c, rfl⟩ := exists_code.1 hf,

src/computability/partrec.lean

@@ -12,15 +12,15 @@ import data.pfun
 
 The partial recursive functions are defined similarly to the primitive
 recursive functions, but now all functions are partial, implemented
-using the `roption` monad, and there is an additional operation, called
+using the `part` monad, and there is an additional operation, called
 μ-recursion, which performs unbounded minimization.
 
 ## References
 
 * [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019]
 -/
 
-open encodable denumerable roption
+open encodable denumerable part
 
 local attribute [-simp] not_forall
 
@@ -66,7 +66,7 @@ end
 
 end rfind
 
-def rfind (p : ℕ →. bool) : roption ℕ :=
+def rfind (p : ℕ →. bool) : part ℕ :=
 ⟨_, λ h, (rfind_x p h).1⟩
 
 theorem rfind_spec {p : ℕ →. bool} {n : ℕ} (h : n ∈ rfind p) : tt ∈ p n :=
@@ -110,9 +110,9 @@ theorem rfind_zero_none
   (p : ℕ →. bool) (p0 : p 0 = none) : rfind p = none :=
 eq_none_iff.2 $ λ a h,
 let ⟨n, h₁, h₂⟩ := rfind_dom'.1 h.fst in
-(p0 ▸ h₂ (zero_le _) : (@roption.none bool).dom)
+(p0 ▸ h₂ (zero_le _) : (@part.none bool).dom)
 
-def rfind_opt {α} (f : ℕ → option α) : roption α :=
+def rfind_opt {α} (f : ℕ → option α) : part α :=
 (rfind (λ n, (f n).is_some)).bind (λ n, f n)
 
 theorem rfind_opt_spec {α} {f : ℕ → option α} {a}
@@ -224,7 +224,7 @@ end nat
 
 def partrec {α σ} [primcodable α] [primcodable σ]
   (f : α →. σ) := nat.partrec (λ n,
-  roption.bind (decode α n) (λ a, (f a).map encode))
+  part.bind (decode α n) (λ a, (f a).map encode))
 
 def partrec₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
   (f : α → β →. σ) := partrec (λ p : α × β, f p.1 p.2)
@@ -242,10 +242,10 @@ theorem primrec.to_comp {α σ} [primcodable α] [primcodable σ]
 theorem primrec₂.to_comp {α β σ} [primcodable α] [primcodable β] [primcodable σ]
   {f : α → β → σ} (hf : primrec₂ f) : computable₂ f := hf.to_comp
 
-theorem computable.part {α σ} [primcodable α] [primcodable σ]
+protected theorem computable.partrec {α σ} [primcodable α] [primcodable σ]
   {f : α → σ} (hf : computable f) : partrec (f : α →. σ) := hf
 
-theorem computable₂.part {α β σ} [primcodable α] [primcodable β] [primcodable σ]
+protected theorem computable₂.partrec₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
   {f : α → β → σ} (hf : computable₂ f) : partrec₂ (λ a, (f a : β →. σ)) := hf
 
 namespace computable
@@ -258,8 +258,8 @@ theorem of_eq {f g : α → σ} (hf : computable f) (H : ∀ n, f n = g n) : com
 theorem const (s : σ) : computable (λ a : α, s) :=
 (primrec.const _).to_comp
 
-theorem of_option {f : α → option β}
-  (hf : computable f) : partrec (λ a, (f a : roption β)) :=
+theorem of_option {f : α → option β} (hf : computable f) :
+  partrec (λ a, (f a : part β)) :=
 (nat.partrec.ppred.comp hf).of_eq $ λ n, begin
   cases decode α n with a; simp,
   cases f a with b; simp
@@ -337,15 +337,15 @@ theorem of_eq_tot {f : α →. σ} {g : α → σ}
   (hf : partrec f) (H : ∀ n, g n ∈ f n) : computable g :=
 hf.of_eq (λ a, eq_some_iff.2 (H a))
 
-theorem none : partrec (λ a : α, @roption.none σ) :=
+theorem none : partrec (λ a : α, @part.none σ) :=
 nat.partrec.none.of_eq $ λ n, by cases decode α n; simp
 
-protected theorem some : partrec (@roption.some α) := computable.id
+protected theorem some : partrec (@part.some α) := computable.id
 
-theorem _root_.decidable.partrec.const' (s : roption σ) [decidable s.dom] : partrec (λ a : α, s) :=
+theorem _root_.decidable.partrec.const' (s : part σ) [decidable s.dom] : partrec (λ a : α, s) :=
 (of_option (const (to_option s))).of_eq (λ a, of_to_option s)
 
-theorem const' (s : roption σ) : partrec (λ a : α, s) :=
+theorem const' (s : part σ) : partrec (λ a : α, s) :=
 by haveI := classical.dec s.dom; exact decidable.partrec.const' s
 
 protected theorem bind {f : α →. β} {g : α → β →. σ}
@@ -357,7 +357,7 @@ protected theorem bind {f : α →. β} {g : α → β →. σ}
 theorem map {f : α →. β} {g : α → β → σ}
   (hf : partrec f) (hg : computable₂ g) : partrec (λ a, (f a).map (g a)) :=
 by simpa [bind_some_eq_map] using
-   @@partrec.bind _ _ _ (λ a b, roption.some (g a b)) hf hg
+   @@partrec.bind _ _ _ (λ a b, part.some (g a b)) hf hg
 
 theorem to₂ {f : α × β →. σ} (hf : partrec f) : partrec₂ (λ a b, f (a, b)) :=
 hf.of_eq $ λ ⟨a, b⟩, rfl
@@ -456,14 +456,14 @@ theorem rfind {p : α → ℕ →. bool} (hp : partrec₂ p) :
   cases e : decode α n with a;
     simp [e, nat.rfind_zero_none, map_id'],
   congr, funext n,
-  simp [roption.map_map, (∘)],
+  simp [part.map_map, (∘)],
   apply map_id' (λ b, _),
   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
+(rfind (primrec.option_is_some.to_comp.comp hf).partrec.to₂).bind
   (of_option hf)
 
 theorem nat_cases_right
@@ -475,14 +475,14 @@ theorem nat_cases_right
   simp, cases f a; simp,
   refine ext (λ b, ⟨λ H, _, λ H, _⟩),
   { rcases mem_bind_iff.1 H with ⟨c, h₁, h₂⟩, exact h₂ },
-  { have : ∀ m, (nat.elim (roption.some (g a))
+  { have : ∀ m, (nat.elim (part.some (g a))
       (λ y IH, IH.bind (λ _, h a n)) m).dom,
     { intro, induction m; simp [*, H.fst] },
     exact ⟨⟨this n, H.fst⟩, H.snd⟩ }
 end
 
 theorem bind_decode₂_iff {f : α →. σ} : partrec f ↔
-  nat.partrec (λ n, roption.bind (decode₂ α n) (λ a, (f a).map encode)) :=
+  nat.partrec (λ n, part.bind (decode₂ α n) (λ a, (f a).map encode)) :=
 ⟨λ hf, nat_iff.1 $ (of_option primrec.decode₂.to_comp).bind $
   (map hf (computable.encode.comp snd).to₂).comp snd,
 λ h, map_encode_iff.1 $ by simpa [encodek₂]
@@ -497,8 +497,8 @@ theorem vector_m_of_fn : ∀ {n} {f : fin n → α →. σ}, (∀ i, partrec (f
 
 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) :=
+@[simp] theorem vector.m_of_fn_part_some {α n} : ∀ (f : fin n → α),
+  vector.m_of_fn (λ i, part.some (f i)) = part.some (vector.of_fn f) :=
 vector.m_of_fn_pure
 
 namespace computable
@@ -514,13 +514,13 @@ theorem bind_decode_iff {f : α → β → option σ} : computable₂ (λ a n,
 ⟨λ hf, nat.partrec.of_eq
     (((partrec.nat_iff.2 (nat.partrec.ppred.comp $
         nat.partrec.of_primrec $ primcodable.prim β)).comp snd).bind
-      (computable.comp hf fst).to₂.part) $
+      (computable.comp hf fst).to₂.partrec₂) $
   λ n, by simp;
     cases decode α n.unpair.1; simp;
     cases decode β n.unpair.2; simp,
 λ hf, begin
   have : partrec (λ a : α × ℕ, (encode (decode β a.2)).cases
-    (some option.none) (λ n, roption.map (f a.1) (decode β n))) :=
+    (some option.none) (λ n, part.map (f a.1) (decode β n))) :=
   partrec.nat_cases_right (primrec.encdec.to_comp.comp snd)
     (const none) ((of_option (computable.decode.comp snd)).map
       (hf.comp (fst.comp $ fst.comp fst) snd).to₂),
@@ -536,7 +536,7 @@ theorem nat_elim
   {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ}
   (hf : computable f) (hg : computable g) (hh : computable₂ h) :
   computable (λ a, (f a).elim (g a) (λ y IH, h a (y, IH))) :=
-(partrec.nat_elim hf hg hh.part).of_eq $
+(partrec.nat_elim hf hg hh.partrec₂).of_eq $
 λ a, by simp; induction f a; simp *
 
 theorem nat_cases {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ}
@@ -629,15 +629,15 @@ open computable
 theorem option_some_iff {f : α →. σ} :
   partrec (λ a, (f a).map option.some) ↔ partrec f :=
 ⟨λ h, (nat.partrec.ppred.comp h).of_eq $
-   λ n, by simp [roption.bind_assoc, bind_some_eq_map],
+   λ n, by simp [part.bind_assoc, bind_some_eq_map],
  λ hf, hf.map (option_some.comp snd).to₂⟩
 
 theorem option_cases_right {o : α → option β} {f : α → σ} {g : α → β →. σ}
   (ho : computable o) (hf : computable f) (hg : partrec₂ g) :
   @partrec _ σ _ _ (λ a, option.cases_on (o a) (some (f a)) (g a)) :=
-have partrec (λ (a : α), nat.cases (roption.some (f a))
-  (λ n, roption.bind (decode β n) (g a)) (encode (o a))) :=
-nat_cases_right (encode_iff.2 ho) hf.part $
+have partrec (λ (a : α), nat.cases (part.some (f a))
+  (λ n, part.bind (decode β n) (g a)) (encode (o a))) :=
+nat_cases_right (encode_iff.2 ho) hf.partrec $
   ((@computable.decode β _).comp snd).of_option.bind
     (hg.comp (fst.comp fst) snd).to₂,
 this.of_eq $ λ a, by cases o a with b; simp [encodek]
@@ -649,7 +649,7 @@ have partrec (λ a, (option.cases_on
   (sum.cases_on (f a) (λ b, option.none) option.some : option γ)
   (some (sum.cases_on (f a) (λ b, some (g a b))
      (λ c, option.none)))
-  (λ c, (h a c).map option.some) : roption (option σ))) :=
+  (λ c, (h a c).map option.some) : part (option σ))) :=
 option_cases_right
   (sum_cases hf (const option.none).to₂ (option_some.comp snd).to₂)
   (sum_cases hf (option_some.comp hg) (const option.none).to₂)
@@ -666,7 +666,7 @@ theorem sum_cases_left {f : α → β ⊕ γ} {g : α → β →. σ} {h : α 
 lemma fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) :
   let F : α → ℕ →. σ ⊕ α := λ a n,
     n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
-    sum.cases_on s (λ _, roption.some s) f in
+    sum.cases_on s (λ _, part.some s) f in
   (∃ (n : ℕ), ((∃ (b' : σ), sum.inl b' ∈ F a n) ∧
         ∀ {m : ℕ}, m < n → (∃ (b : α), sum.inr b ∈ F a m)) ∧
       sum.inl b ∈ F a n) ↔ b ∈ pfun.fix f a :=
@@ -707,13 +707,13 @@ end
 theorem fix {f : α →. σ ⊕ α} (hf : partrec f) : partrec (pfun.fix f) :=
 let F : α → ℕ →. σ ⊕ α := λ a n,
   n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
-  sum.cases_on s (λ _, roption.some s) f in
+  sum.cases_on s (λ _, part.some s) f in
 have hF : partrec₂ F :=
-partrec.nat_elim snd (sum_inr.comp fst).part
+partrec.nat_elim snd (sum_inr.comp fst).partrec
   (sum_cases_right (snd.comp snd)
     (snd.comp $ snd.comp fst).to₂
     (hf.comp snd).to₂).to₂,
-let p := λ a n, @roption.map _ bool
+let p := λ a n, @part.map _ bool
   (λ s, sum.cases_on s (λ_, tt) (λ _, ff)) (F a n) in
 have hp : partrec₂ p := hF.map ((sum_cases computable.id
   (const tt).to₂ (const ff).to₂).comp snd).to₂,

src/computability/partrec_code.lean

@@ -494,11 +494,11 @@ def eval : code → ℕ →. ℕ
 
 instance : has_mem (ℕ →. ℕ) code := ⟨λ f c, eval c = f⟩
 
-@[simp] theorem eval_const : ∀ n m, eval (code.const n) m = roption.some n
+@[simp] theorem eval_const : ∀ n m, eval (code.const n) m = part.some n
 | 0     m := rfl
 | (n+1) m := by simp! *
 
-@[simp] theorem eval_id (n) : eval code.id n = roption.some n := by simp! [(<*>)]
+@[simp] theorem eval_id (n) : eval code.id n = part.some n := by simp! [(<*>)]
 
 @[simp] theorem eval_curry (c n x) : eval (curry c n) x = eval c (mkpair n x) :=
 by simp! [(<*>)]
@@ -541,7 +541,7 @@ theorem exists_code {f : ℕ →. ℕ} : nat.partrec f ↔ ∃ c : code, eval c
   case nat.partrec.rfind : f pf hf {
     rcases hf with ⟨cf, rfl⟩,
     refine ⟨comp (rfind' cf) (pair code.id zero), _⟩,
-    simp [eval, (<*>), pure, pfun.pure, roption.map_id'] },
+    simp [eval, (<*>), pure, pfun.pure, part.map_id'] },
 end, λ h, begin
   rcases h with ⟨c, rfl⟩, induction c,
   case nat.partrec.code.zero { exact nat.partrec.zero },
@@ -893,7 +893,7 @@ 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
+part.ext $ λ x, begin
   refine evaln_complete.trans (nat.rfind_opt_mono _).symm,
   intros a m n hl, apply evaln_mono hl,
 end
@@ -905,30 +905,30 @@ theorem eval_part : partrec₂ eval :=
 
 theorem fixed_point
   {f : code → code} (hf : computable f) : ∃ c : code, eval (f c) = eval c :=
-let g (x y : ℕ) : roption ℕ :=
+let g (x y : ℕ) : part ℕ :=
   eval (of_nat code x) x >>= λ b, eval (of_nat code b) y in
 have partrec₂ g :=
   (eval_part.comp ((computable.of_nat _).comp fst) fst).bind
   (eval_part.comp ((computable.of_nat _).comp snd) (snd.comp fst)).to₂,
 let ⟨cg, eg⟩ := exists_code.1 this in
-have eg' : ∀ a n, eval cg (mkpair a n) = roption.map encode (g a n) :=
+have eg' : ∀ a n, eval cg (mkpair a n) = part.map encode (g a n) :=
   by simp [eg],
 let F (x : ℕ) : code := f (curry cg x) in
 have computable F :=
   hf.comp (curry_prim.comp (primrec.const cg) primrec.id).to_comp,
 let ⟨cF, eF⟩ := exists_code.1 this in
-have eF' : eval cF (encode cF) = roption.some (encode (F (encode cF))),
+have eF' : eval cF (encode cF) = part.some (encode (F (encode cF))),
   by simp [eF],
 ⟨curry cg (encode cF), funext (λ n,
   show eval (f (curry cg (encode cF))) n = eval (curry cg (encode cF)) n,
-  by simp [eg', eF', roption.map_id', g])⟩
+  by simp [eg', eF', part.map_id', g])⟩
 
 theorem fixed_point₂
   {f : code → ℕ →. ℕ} (hf : partrec₂ f) : ∃ c : code, eval c = f c :=
 let ⟨cf, ef⟩ := exists_code.1 hf in
 (fixed_point (curry_prim.comp
   (primrec.const cf) primrec.encode).to_comp).imp $
-λ c e, funext $ λ n, by simp [e.symm, ef, roption.map_id']
+λ c e, funext $ λ n, by simp [e.symm, ef, part.map_id']
 
 end