chore(data/seq/*): cases_on → rec_on (#15843)

We rename recursion principles on `Sort` from `cases_on` to `rec_on`.



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

scripts/nolints.txt

@@ -933,4 +933,4 @@ apply_nolint transfer.compute_transfer doc_blame
 apply_nolint tactic.wlog doc_blame
 
 -- topology/algebra/group.lean
-apply_nolint topological_space.positive_compacts.locally_compact_space_of_group to_additive_doc
+apply_nolint topological_space.positive_compacts.locally_compact_space_of_group to_additive_doc

src/data/seq/computation.lean

@@ -128,7 +128,8 @@ by cases s with f al; apply subtype.eq; dsimp [tail, think]; rw [stream.tail_con
 theorem think_empty : empty α = think (empty α) :=
 destruct_eq_think destruct_empty
 
-def cases_on {C : computation α → Sort v} (s : computation α)
+/-- Recursion principle for computations, compare with `list.rec_on`. -/
+def rec_on {C : computation α → Sort v} (s : computation α)
   (h1 : ∀ a, C (return a)) (h2 : ∀ s, C (think s)) : C s := begin
   induction H : destruct s with v v,
   { rw destruct_eq_ret H, apply h1 },
@@ -212,7 +213,7 @@ section bisim
         by cases s; refl, by cases s'; refl, r⟩) this,
       begin
         have := bisim r, revert r this,
-        apply cases_on s _ _; intros; apply cases_on s' _ _; intros; intros r this,
+        apply rec_on s _ _; intros; apply rec_on s' _ _; intros; intros r this,
         { constructor, dsimp at this, rw this, assumption },
         { rw [destruct_ret, destruct_think] at this,
           exact false.elim this },
@@ -441,7 +442,7 @@ theorem eq_thinkN {s : computation α} {a n} (h : results s a n) :
 begin
   revert s,
   induction n with n IH; intro s;
-  apply cases_on s (λ a', _) (λ s, _); intro h,
+  apply rec_on s (λ a', _) (λ s, _); intro h,
   { rw ←eq_of_ret_mem h.mem, refl },
   { cases of_results_think h with n h, cases h, contradiction },
   { have := h.len_unique (results_ret _), contradiction },
@@ -506,7 +507,7 @@ def join (c : computation (computation α)) : computation α := c >>= id
 
 @[simp]
 theorem destruct_map (f : α → β) (s) : destruct (map f s) = lmap f (rmap (map f) (destruct s)) :=
-by apply s.cases_on; intro; simp
+by apply s.rec_on; intro; simp
 
 @[simp] theorem map_id : ∀ (s : computation α), map id s = s
 | ⟨f, al⟩ := begin
@@ -556,7 +557,7 @@ begin
     exact match c₁, c₂, h with
     | _, _, or.inl (eq.refl c) := begin cases destruct c with b cb; simp end
     | _, _, or.inr ⟨s, rfl, rfl⟩ := begin
-      apply cases_on s; intros s; simp,
+      apply rec_on s; intros s; simp,
       exact or.inr ⟨s, rfl, rfl⟩
     end end },
   { exact or.inr ⟨s, rfl, rfl⟩ }
@@ -574,9 +575,9 @@ begin
     exact match c₁, c₂, h with
     | _, _, or.inl (eq.refl c) := by cases destruct c with b cb; simp
     | ._, ._, or.inr ⟨s, rfl, rfl⟩ := begin
-      apply cases_on s; intros s; simp,
+      apply rec_on s; intros s; simp,
       { generalize : f s = fs,
-        apply cases_on fs; intros t; simp,
+        apply rec_on fs; intros t; simp,
         { cases destruct (g t) with b cb; simp } },
       { exact or.inr ⟨s, rfl, rfl⟩ }
     end end },
@@ -619,7 +620,7 @@ theorem of_results_bind {s : computation α} {f : α → computation β} {b k} :
   ∃ a m n, results s a m ∧ results (f a) b n ∧ k = n + m :=
 begin
   induction k with n IH generalizing s;
-  apply cases_on s (λ a, _) (λ s', _); intro e,
+  apply rec_on s (λ a, _) (λ s', _); intro e,
   { simp [thinkN] at e, refine ⟨a, _, _, results_ret _, e, rfl⟩ },
   { have := congr_arg head (eq_thinkN e), contradiction },
   { simp at e, refine ⟨a, _, n+1, results_ret _, e, rfl⟩ },
@@ -705,15 +706,15 @@ destruct_eq_think $ by unfold has_orelse.orelse; simp [orelse]
 begin
   apply eq_of_bisim (λ c₁ c₂, (empty α <|> c₂) = c₁) _ rfl,
   intros s' s h, rw ←h,
-  apply cases_on s; intros s; rw think_empty; simp,
+  apply rec_on s; intros s; rw think_empty; simp,
   rw ←think_empty,
 end
 
 @[simp] theorem orelse_empty (c : computation α) : (c <|> empty α) = c :=
 begin
   apply eq_of_bisim (λ c₁ c₂, (c₂ <|> empty α) = c₁) _ rfl,
   intros s' s h, rw ←h,
-  apply cases_on s; intros s; rw think_empty; simp,
+  apply rec_on s; intros s; rw think_empty; simp,
   rw←think_empty,
 end
 
@@ -920,7 +921,7 @@ attribute [simp] lift_rel_aux
   (C : computation α → computation β → Prop) (a cb) :
   lift_rel_aux R C (sum.inl a) (destruct cb) ↔ ∃ {b}, b ∈ cb ∧ R a b :=
 begin
-  apply cb.cases_on (λ b, _) (λ cb, _),
+  apply cb.rec_on (λ b, _) (λ cb, _),
   { exact ⟨λ h, ⟨_, ret_mem _, h⟩, λ ⟨b', mb, h⟩,
     by rw [mem_unique (ret_mem _) mb]; exact h⟩ },
   { rw [destruct_think],
@@ -944,7 +945,7 @@ begin
   revert cb, refine mem_rec_on ha _ (λ ca' IH, _);
   intros cb Hc; have h := H Hc,
   { simp at h, simp [h] },
-  { have h := H Hc, simp, revert h, apply cb.cases_on (λ b, _) (λ cb', _);
+  { have h := H Hc, simp, revert h, apply cb.rec_on (λ b, _) (λ cb', _);
     intro h; simp at h; simp [h], exact IH _ h }
 end
 

src/data/seq/parallel.lean

@@ -187,7 +187,7 @@ begin
       cases list.foldr parallel.aux2._match_1 (sum.inr list.nil) l; simp [parallel.aux2],
       cases destruct c; simp },
     simp [parallel.aux1], rw this, cases parallel.aux2 l with a l'; simp,
-    apply S.cases_on _ (λ c S, _) (λ S, _); simp; simp [parallel.aux1];
+    apply S.rec_on _ (λ c S, _) (λ S, _); simp; simp [parallel.aux1];
     exact ⟨_, _, rfl, rfl⟩
   end end
 end

src/data/seq/seq.lean

@@ -183,7 +183,8 @@ by cases s with f al; apply subtype.eq; dsimp [tail, cons]; rw [stream.tail_cons
 
 @[simp] theorem nth_tail (s : seq α) (n) : nth (tail s) n = nth s (n + 1) := rfl
 
-def cases_on {C : seq α → Sort v} (s : seq α)
+/-- Recursion principle for sequences, compare with `list.rec_on`. -/
+def rec_on {C : seq α → Sort v} (s : seq α)
   (h1 : C nil) (h2 : ∀ x s, C (cons x s)) : C s := begin
   induction H : destruct s with v v,
   { rw destruct_eq_nil H, apply h1 },
@@ -199,7 +200,7 @@ begin
     { apply destruct_eq_cons,
       unfold destruct nth functor.map, rw ←e, refl },
     rw TH, apply h1 _ _ (or.inl rfl) },
-  revert e, apply s.cases_on _ (λ b s', _); intro e,
+  revert e, apply s.rec_on _ (λ b s', _); intro e,
   { injection e },
   { have h_eq : (cons b s').val (nat.succ k) = s'.val k, { cases s'; refl },
     rw [h_eq] at e,
@@ -270,7 +271,7 @@ section bisim
         by cases s; refl, by cases s'; refl, r⟩) this,
       begin
         have := bisim r, revert r this,
-        apply cases_on s _ _; intros; apply cases_on s' _ _; intros; intros r this,
+        apply rec_on s _ _; intros; apply rec_on s' _ _; intros; intros r this,
         { constructor, refl, assumption },
         { rw [destruct_nil, destruct_cons] at this,
           exact false.elim this },
@@ -483,7 +484,7 @@ else sum.inr (to_stream s h)
 begin
   apply coinduction2, intro s,
   dsimp [append], rw [corec_eq],
-  dsimp [append], apply cases_on s _ _,
+  dsimp [append], apply rec_on s _ _,
   { trivial },
   { intros x s,
     rw [destruct_cons], dsimp,
@@ -500,7 +501,7 @@ end
 @[simp] theorem append_nil (s : seq α) : append s nil = s :=
 begin
   apply coinduction2 s, intro s,
-  apply cases_on s _ _,
+  apply rec_on s _ _,
   { trivial },
   { intros x s,
     rw [cons_append, destruct_cons, destruct_cons], dsimp,
@@ -513,9 +514,9 @@ begin
   apply eq_of_bisim (λ s1 s2, ∃ s t u,
     s1 = append (append s t) u ∧ s2 = append s (append t u)),
   { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, t, u, rfl, rfl⟩ := begin
-      apply cases_on s; simp,
-      { apply cases_on t; simp,
-        { apply cases_on u; simp,
+      apply rec_on s; simp,
+      { apply rec_on t; simp,
+        { apply rec_on u; simp,
           { intros x u, refine ⟨nil, nil, u, _, _⟩; simp } },
         { intros x t, refine ⟨nil, t, u, _, _⟩; simp } },
       { intros x s, exact ⟨s, t, u, rfl, rfl⟩ }
@@ -550,8 +551,8 @@ begin
   apply eq_of_bisim (λ s1 s2, ∃ s t,
     s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _ ⟨s, t, rfl, rfl⟩,
   intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, t, rfl, rfl⟩ := begin
-    apply cases_on s; simp,
-    { apply cases_on t; simp,
+    apply rec_on s; simp,
+    { apply rec_on t; simp,
       { intros x t, refine ⟨nil, t, _, _⟩; simp } },
     { intros x s, refine ⟨s, t, rfl, rfl⟩ }
   end end
@@ -584,11 +585,11 @@ begin
   intros s1 s2 h,
   exact match s1, s2, h with
   | _, _, (or.inl $ eq.refl s) := begin
-      apply cases_on s, { trivial },
+      apply rec_on s, { trivial },
       { intros x s, rw [destruct_cons], exact ⟨rfl, or.inl rfl⟩ }
     end
   | ._, ._, (or.inr ⟨a, s, S, rfl, rfl⟩) := begin
-      apply cases_on s,
+      apply rec_on s,
       { simp },
       { intros x s, simp, refine or.inr ⟨x, s, S, rfl, rfl⟩ }
     end
@@ -602,9 +603,9 @@ begin
     s1 = append s (join (append S T)) ∧
     s2 = append s (append (join S) (join T))),
   { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, S, T, rfl, rfl⟩ := begin
-      apply cases_on s; simp,
-      { apply cases_on S; simp,
-        { apply cases_on T, { simp },
+      apply rec_on s; simp,
+      { apply rec_on S; simp,
+        { apply rec_on T, { simp },
           { intros s T, cases s with a s; simp,
             refine ⟨s, nil, T, _, _⟩; simp } },
         { intros s S, cases s with a s; simp,
@@ -662,7 +663,7 @@ begin
   generalize e : append s₁ s₂ = ss, intro h, revert s₁,
   apply mem_rec_on h _,
   intros b s' o s₁,
-  apply s₁.cases_on _ (λ c t₁, _); intros m e;
+  apply s₁.rec_on _ (λ c t₁, _); intros m e;
   have := congr_arg destruct e,
   { apply or.inr, simpa using m },
   { cases (show a = c ∨ a ∈ append t₁ s₂, by simpa using m) with e' m,
@@ -721,7 +722,7 @@ def bind (s : seq1 α) (f : α → seq1 β) : seq1 β :=
 join (map f s)
 
 @[simp] theorem join_map_ret (s : seq α) : seq.join (seq.map ret s) = s :=
-by apply coinduction2 s; intro s; apply cases_on s; simp [ret]
+by apply coinduction2 s; intro s; apply rec_on s; simp [ret]
 
 @[simp] theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
 | ⟨a, s⟩ := begin
@@ -733,7 +734,7 @@ end
 begin
   simp [ret, bind, map],
   cases f a with a s,
-  apply cases_on s; intros; simp
+  apply rec_on s; intros; simp
 end
 
 @[simp] theorem map_join' (f : α → β) (S) :
@@ -743,8 +744,8 @@ begin
     ∃ s S, s1 = append s (seq.map f (seq.join S)) ∧
       s2 = append s (seq.join (seq.map (map f) S))),
   { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, S, rfl, rfl⟩ := begin
-      apply cases_on s; simp,
-      { apply cases_on S; simp,
+      apply rec_on s; simp,
+      { apply rec_on S; simp,
         { intros x S, cases x with a s; simp [map],
           exact ⟨_, _, rfl, rfl⟩ } },
       { intros x s, refine ⟨s, S, rfl, rfl⟩ }
@@ -753,7 +754,7 @@ begin
 end
 
 @[simp] theorem map_join (f : α → β) : ∀ S, map f (join S) = join (map (map f) S)
-| ((a, s), S) := by apply cases_on s; intros; simp [map]
+| ((a, s), S) := by apply rec_on s; intros; simp [map]
 
 @[simp] theorem join_join (SS : seq (seq1 (seq1 α))) :
   seq.join (seq.join SS) = seq.join (seq.map join SS) :=
@@ -762,10 +763,10 @@ begin
     ∃ s SS, s1 = seq.append s (seq.join (seq.join SS)) ∧
       s2 = seq.append s (seq.join (seq.map join SS))),
   { intros s1 s2 h, exact match s1, s2, h with ._, ._, ⟨s, SS, rfl, rfl⟩ := begin
-      apply cases_on s; simp,
-      { apply cases_on SS; simp,
+      apply rec_on s; simp,
+      { apply rec_on SS; simp,
         { intros S SS, cases S with s S; cases s with x s; simp [map],
-          apply cases_on s; simp,
+          apply rec_on s; simp,
           { exact ⟨_, _, rfl, rfl⟩ },
           { intros x s,
             refine ⟨cons x (append s (seq.join S)), SS, _, _⟩; simp } } },
@@ -784,8 +785,8 @@ begin
   rw [map_comp _ join],
   generalize : seq.map (map g ∘ f) s = SS,
   rcases map g (f a) with ⟨⟨a, s⟩, S⟩,
-  apply cases_on s; intros; apply cases_on S; intros; simp,
-  { cases x with x t, apply cases_on t; intros; simp },
+  apply rec_on s; intros; apply rec_on S; intros; simp,
+  { cases x with x t, apply rec_on t; intros; simp },
   { cases x_1 with y t; simp }
 end