chore(data/equiv): add docstrings (#7704)

- add module docstrings
- add def docstrings
- rename `decode2` to `decode₂`
- squash some simps

scripts/nolints.txt

@@ -1169,4 +1169,4 @@ apply_nolint uniform_space.completion.map₂ doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame

src/computability/halting.lean

@@ -26,8 +26,8 @@ theorem merge' {f g}
     (∀ 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⟩,
+  obtain ⟨cf, rfl⟩ := code.exists_code.1 hf,
+  obtain ⟨cg, rfl⟩ := code.exists_code.1 hg,
   have : nat.partrec (λ n,
     (nat.rfind_opt (λ k, cf.evaln k n <|> cg.evaln k n))) :=
   partrec.nat_iff.1 (partrec.rfind_opt $
@@ -38,20 +38,20 @@ begin
   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] },
+    simp only [dom_iff_mem, code.evaln_complete, option.mem_def] at h,
+    obtain ⟨x, k, e⟩ | ⟨x, k, e⟩ := h,
+    { refine ⟨k, x, _⟩, simp only [e, option.some_orelse, option.mem_def] },
     { 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') } }
+      { exact ⟨x, by simp only [e, option.mem_def, option.none_orelse]⟩ },
+      { exact ⟨y, by simp only [option.some_orelse, option.mem_def]⟩ } } },
+  intros x h,
+  obtain ⟨k, e⟩ := nat.rfind_opt_spec h,
+  revert e,
+  simp only [option.mem_def]; 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
@@ -68,29 +68,28 @@ theorem merge' {f g : α →. σ}
     (∀ 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
+  nat.partrec.merge' (bind_decode₂_iff.1 hf) (bind_decode₂_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'],
+  { intro h,
+    rw bind_dom,
     have hk : (k (encode a)).dom :=
-      (H _).2.2 (by simpa [encodek2] using h),
+      (H _).2.2 (by simpa only [encodek₂, bind_some, coe_some] 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, encode_injective.eq_iff] at this,
-    cases this with h h;
-    { rcases h with ⟨a', ha, rfl⟩,
-      simp [encodek] at hx, subst a',
-      simp [ha] } },
+    simp only [exists_prop, mem_map_iff, mem_coe, mem_bind_iff, option.mem_def] at H,
+    obtain ⟨a', ha', y, hy, e⟩ | ⟨a', ha', y, hy, e⟩ := (H _).1 _ ⟨hk, rfl⟩;
+    { simp only [e.symm, encodek] } },
+  intros x h', simp only [k', exists_prop, mem_coe, mem_bind_iff, option.mem_def] at h',
+  obtain ⟨n, hn, hx⟩ := h',
+  have := (H _).1 _ hn,
+  simp [mem_decode₂, encode_injective.eq_iff] at this,
+  obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this; simp only [encodek] at hx; rw hx at ha,
+  { exact or.inl ha },
+  exact or.inr ha
 end
 
 theorem merge {f g : α →. σ}
@@ -126,7 +125,7 @@ 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
+.of_eq $ λ a, by cases f a; simp only [bool.cond_tt, bool.cond_ff]
 
 end partrec
 
@@ -157,14 +156,14 @@ theorem computable_iff {p : α → Prop} :
 
 protected theorem not {p : α → Prop}
   (hp : computable_pred p) : computable_pred (λ a, ¬ p a) :=
-by rcases computable_iff.1 hp with ⟨f, hf, rfl⟩; exact
+by obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp; exact
   ⟨by apply_instance,
     (cond hf (const ff) (const tt)).of_eq
       (λ n, by {dsimp, cases f n; refl})⟩
 
 theorem to_re {p : α → Prop} (hp : computable_pred p) : re_pred p :=
 begin
-  rcases computable_iff.1 hp with ⟨f, hf, rfl⟩,
+  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, _),
@@ -177,14 +176,14 @@ theorem rice (C : set (ℕ →. ℕ))
   (fC : f ∈ C) : g ∈ C :=
 begin
   cases h with _ h, resetI,
-  rcases fixed_point₂ (partrec.cond (h.comp fst)
+  obtain ⟨c, e⟩ := 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⟩,
+    ((partrec.nat_iff.2 hf).comp snd).to₂).to₂,
   simp at e,
-  by_cases eval c ∈ C,
-  { simp [h] at e, rwa ← e },
-  { simp [h] at e,
-    rw e at h, contradiction }
+  by_cases H : eval c ∈ C,
+  { simp only [H, if_true] at e, rwa ← e },
+  { simp only [H, if_false] at e,
+    rw e at H, contradiction }
 end
 
 theorem rice₂ (C : set code)
@@ -200,7 +199,7 @@ from λ f, ⟨set.mem_image_of_mem _, λ ⟨g, hg, e⟩, (H _ _ e).1 hg⟩,
     (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];
+λ h, by obtain rfl | rfl := h; simp [computable_pred, set.mem_empty_eq];
   exact ⟨by apply_instance, computable.const _⟩⟩
 
 theorem halting_problem (n) : ¬ computable_pred (λ c, (eval c n).dom)
@@ -213,9 +212,9 @@ theorem halting_problem (n) : ¬ computable_pred (λ c, (eval c n).dom)
 theorem computable_iff_re_compl_re {p : α → Prop} [decidable_pred p] :
   computable_pred p ↔ re_pred p ∧ re_pred (λ a, ¬ p a) :=
 ⟨λ h, ⟨h.to_re, h.not.to_re⟩, λ ⟨h₁, h₂⟩, ⟨‹_›, begin
-  rcases partrec.merge
+  obtain ⟨k, pk, hk⟩ := partrec.merge
     (h₁.map (computable.const tt).to₂)
-    (h₂.map (computable.const ff).to₂) _ with ⟨k, pk, hk⟩,
+    (h₂.map (computable.const ff).to₂) _,
   { refine partrec.of_eq pk (λ n, roption.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 }
@@ -296,7 +295,7 @@ 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
+λ i, fin.cases (by simp *) (λ i, by simp only [hg i, nth_cons_succ]) i
 
 theorem idv {n} : @vec n n id := vec.prim nat.primrec'.idv
 
@@ -333,10 +332,10 @@ 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']),
+    (λ i, by dsimp only [g]; simp [encodek, roption.map_id']),
 end,
 λ f hf, begin
-  rcases exists_code.1 hf with ⟨c, rfl⟩,
+  obtain ⟨c, rfl⟩ := exists_code.1 hf,
   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 $
@@ -349,18 +348,18 @@ 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),
+    λ i, primrec.id).to_comp).of_eq (λ v, by simp only [id.def, head_of_fn]),
   λ 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),
+    vector_cons.comp snd (const nil)).of_eq (λ v, by simp only [cons_head, cons_tail]),
   λ 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, by simpa only [of_fn_nth] using vector_of_fn (λ i, to_part (h i)),
  λ h i, of_part $ vector_nth.comp h (const i)⟩
 
 end nat.partrec'

src/computability/partrec.lean

@@ -36,7 +36,7 @@ parameter (H : ∃ n, tt ∈ p n ∧ ∀ k < n, (p k).dom)
 private def wf_lbp : well_founded lbp :=
 ⟨let ⟨n, pn⟩ := H in begin
   suffices : ∀m k, n ≤ k + m → acc (lbp p) k,
-  { from λa, this _ _ (nat.le_add_left _ _) },
+  { from λ a, this _ _ (nat.le_add_left _ _) },
   intros m k kn,
   induction m with m IH generalizing k;
     refine ⟨_, λ y r, _⟩; rcases r with ⟨rfl, a⟩,
@@ -481,11 +481,11 @@ theorem nat_cases_right
     exact ⟨⟨this n, H.fst⟩, H.snd⟩ }
 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 $
+theorem bind_decode₂_iff {f : α →. σ} : partrec f ↔
+  nat.partrec (λ n, roption.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 [encodek2]
+λ h, map_encode_iff.1 $ by simpa [encodek₂]
   using (nat_iff.2 h).comp (@computable.encode α _)⟩
 
 theorem vector_m_of_fn : ∀ {n} {f : fin n → α →. σ}, (∀ i, partrec (f i)) →

src/computability/primrec.lean

@@ -631,7 +631,7 @@ theorem option_orelse :
 (option_cases fst snd (fst.comp fst).to₂).of_eq $
 λ ⟨o₁, o₂⟩, by cases o₁; cases o₂; refl
 
-protected theorem decode2 : primrec (decode2 α) :=
+protected theorem decode₂ : primrec (decode₂ α) :=
 option_bind primrec.decode $
 option_guard ((@primrec.eq _ _ nat.decidable_eq).comp
   (encode_iff.2 snd) (fst.comp fst)) snd
@@ -1041,13 +1041,12 @@ local attribute [instance, priority 100]
   encodable.decidable_range_encode encodable.decidable_eq_of_encodable
 
 instance ulower : primcodable (ulower α) :=
-have primrec_pred (λ n, encodable.decode2 α n ≠ none),
+have primrec_pred (λ n, encodable.decode₂ α n ≠ none),
 from primrec.not (primrec.eq.comp (primrec.option_bind primrec.decode
   (primrec.ite (primrec.eq.comp (primrec.encode.comp primrec.snd) primrec.fst)
     (primrec.option_some.comp primrec.snd) (primrec.const _))) (primrec.const _)),
 primcodable.subtype $
-  primrec_pred.of_eq this $
-  by simp [set.range, option.eq_none_iff_forall_not_mem, encodable.mem_decode2]
+  primrec_pred.of_eq this (λ n, decode₂_ne_none_iff)
 
 end ulower
 
@@ -1100,7 +1099,7 @@ subtype_mk primrec.encode
 
 theorem ulower_up : primrec (ulower.up : ulower α → α) :=
 by letI : ∀ a, decidable (a ∈ set.range (encode : α → ℕ)) := decidable_range_encode _; exact
-option_get (primrec.decode2.comp subtype_val)
+option_get (primrec.decode₂.comp subtype_val)
 
 theorem fin_val_iff {n} {f : α → fin n} :
   primrec (λ a, (f a).1) ↔ primrec f :=