chore(data/seq/*): trivial spacing fixes (#15847)

We do `λx` → `λ x` and a single instance of `{ x }` → `{x}`.

Author: vihdzp

src/data/seq/computation.lean

@@ -22,21 +22,21 @@ coinductive computation (α : Type u) : Type u
   An element of `computation α` is an infinite sequence of `option α` such
   that if `f n = some a` for some `n` then it is constantly `some a` after that. -/
 def computation (α : Type u) : Type u :=
-{ f : stream (option α) // ∀ {n a}, f n = some a → f (n+1) = some a }
+{f : stream (option α) // ∀ {n a}, f n = some a → f (n + 1) = some a}
 
 namespace computation
 variables {α : Type u} {β : Type v} {γ : Type w}
 
 -- constructors
 /-- `return a` is the computation that immediately terminates with result `a`. -/
-def return (a : α) : computation α := ⟨stream.const (some a), λn a', id⟩
+def return (a : α) : computation α := ⟨stream.const (some a), λ n a', id⟩
 
 instance : has_coe_t α (computation α) := ⟨return⟩ -- note [use has_coe_t]
 
 /-- `think c` is the computation that delays for one "tick" and then performs
   computation `c`. -/
 def think (c : computation α) : computation α :=
-⟨none :: c.1, λn a h, by {cases n with n, contradiction, exact c.2 h}⟩
+⟨none :: c.1, λ n a h, by {cases n with n, contradiction, exact c.2 h}⟩
 
 /-- `thinkN c n` is the computation that delays for `n` ticks and then performs
   computation `c`. -/
@@ -57,7 +57,7 @@ def tail (c : computation α) : computation α :=
 
 /-- `empty α` is the computation that never returns, an infinite sequence of
   `think`s. -/
-def empty (α) : computation α := ⟨stream.const none, λn a', id⟩
+def empty (α) : computation α := ⟨stream.const none, λ n a', id⟩
 
 instance : inhabited (computation α) := ⟨empty _⟩
 
@@ -147,7 +147,7 @@ def corec.F (f : β → α ⊕ β) : α ⊕ β → option α × (α ⊕ β)
   `corec f b = think (corec f b')`. -/
 def corec (f : β → α ⊕ β) (b : β) : computation α :=
 begin
-  refine ⟨stream.corec' (corec.F f) (sum.inr b), λn a' h, _⟩,
+  refine ⟨stream.corec' (corec.F f) (sum.inr b), λ n a' h, _⟩,
   rw stream.corec'_eq,
   change stream.corec' (corec.F f) (corec.F f (sum.inr b)).2 n = some a',
   revert h, generalize : sum.inr b = o, revert o,
@@ -203,12 +203,12 @@ section bisim
   theorem eq_of_bisim (bisim : is_bisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂ :=
   begin
     apply subtype.eq,
-    apply stream.eq_of_bisim (λx y, ∃ s s' : computation α, s.1 = x ∧ s'.1 = y ∧ R s s'),
+    apply stream.eq_of_bisim (λ x y, ∃ s s' : computation α, s.1 = x ∧ s'.1 = y ∧ R s s'),
     dsimp [stream.is_bisimulation],
     intros t₁ t₂ e,
     exact match t₁, t₂, e with ._, ._, ⟨s, s', rfl, rfl, r⟩ :=
       suffices head s = head s' ∧ R (tail s) (tail s'), from
-      and.imp id (λr, ⟨tail s, tail s',
+      and.imp id (λ r, ⟨tail s, tail s',
         by cases s; refl, by cases s'; refl, r⟩) this,
       begin
         have := bisim r, revert r this,
@@ -467,8 +467,8 @@ mem_rec_on (get_mem s) (h1 _) h2
 
 /-- Map a function on the result of a computation. -/
 def map (f : α → β) : computation α → computation β
-| ⟨s, al⟩ := ⟨s.map (λo, option.cases_on o none (some ∘ f)),
-λn b, begin
+| ⟨s, al⟩ := ⟨s.map (λ o, option.cases_on o none (some ∘ f)),
+λ n b, begin
   dsimp [stream.map, stream.nth],
   induction e : s n with a; intro h,
   { contradiction }, { rw [al e, ←h] }
@@ -511,7 +511,7 @@ by apply s.cases_on; intro; simp
 @[simp] theorem map_id : ∀ (s : computation α), map id s = s
 | ⟨f, al⟩ := begin
   apply subtype.eq; simp [map, function.comp],
-  have e : (@option.rec α (λ_, option α) none some) = id,
+  have e : (@option.rec α (λ _, option α) none some) = id,
   { ext ⟨⟩; refl },
   simp [e, stream.map_id]
 end
@@ -528,7 +528,7 @@ end
 @[simp] theorem ret_bind (a) (f : α → computation β) :
   bind (return a) f = f a :=
 begin
-  apply eq_of_bisim (λc₁ c₂,
+  apply eq_of_bisim (λ c₁ c₂,
          c₁ = bind (return a) f ∧ c₂ = f a ∨
          c₁ = corec (bind.F f) (sum.inr c₂)),
   { intros c₁ c₂ h,
@@ -550,7 +550,7 @@ destruct_eq_think $ by simp [bind, bind.F]
 
 @[simp] theorem bind_ret (f : α → β) (s) : bind s (return ∘ f) = map f s :=
 begin
-  apply eq_of_bisim (λc₁ c₂, c₁ = c₂ ∨
+  apply eq_of_bisim (λ c₁ c₂, c₁ = c₂ ∨
          ∃ s, c₁ = bind s (return ∘ f) ∧ c₂ = map f s),
   { intros c₁ c₂ h,
     exact match c₁, c₂, h with
@@ -568,7 +568,7 @@ by rw bind_ret; change (λ x : α, x) with @id α; rw map_id
 @[simp] theorem bind_assoc (s : computation α) (f : α → computation β) (g : β → computation γ) :
   bind (bind s f) g = bind s (λ (x : α), bind (f x) g) :=
 begin
-  apply eq_of_bisim (λc₁ c₂, c₁ = c₂ ∨
+  apply eq_of_bisim (λ c₁ c₂, c₁ = c₂ ∨
          ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s (λ (x : α), bind (f x) g)),
   { intros c₁ c₂ h,
     exact match c₁, c₂, h with
@@ -678,7 +678,7 @@ theorem terminates_map_iff (f : α → β) (s : computation α) :
   the first one that gives a result. -/
 def orelse (c₁ c₂ : computation α) : computation α :=
 @computation.corec α (computation α × computation α)
-  (λ⟨c₁, c₂⟩, match destruct c₁ with
+  (λ ⟨c₁, c₂⟩, match destruct c₁ with
   | sum.inl a := sum.inl a
   | sum.inr c₁' := match destruct c₂ with
     | sum.inl a := sum.inl a
@@ -703,15 +703,15 @@ destruct_eq_think $ by unfold has_orelse.orelse; simp [orelse]
 
 @[simp] theorem empty_orelse (c) : (empty α <|> c) = c :=
 begin
-  apply eq_of_bisim (λc₁ c₂, (empty α <|> c₂) = c₁) _ rfl,
+  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,
   rw ←think_empty,
 end
 
 @[simp] theorem orelse_empty (c : computation α) : (c <|> empty α) = c :=
 begin
-  apply eq_of_bisim (λc₁ c₂, (c₂ <|> empty α) = c₁) _ rfl,
+  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,
   rw←think_empty,
@@ -723,28 +723,28 @@ def equiv (c₁ c₂ : computation α) : Prop := ∀ a, a ∈ c₁ ↔ a ∈ c
 
 infix ` ~ `:50 := equiv
 
-@[refl] theorem equiv.refl (s : computation α) : s ~ s := λ_, iff.rfl
+@[refl] theorem equiv.refl (s : computation α) : s ~ s := λ _, iff.rfl
 
 @[symm] theorem equiv.symm {s t : computation α} : s ~ t → t ~ s :=
-λh a, (h a).symm
+λ h a, (h a).symm
 
 @[trans] theorem equiv.trans {s t u : computation α} : s ~ t → t ~ u → s ~ u :=
-λh1 h2 a, (h1 a).trans (h2 a)
+λ h1 h2 a, (h1 a).trans (h2 a)
 
 theorem equiv.equivalence : equivalence (@equiv α) :=
 ⟨@equiv.refl _, @equiv.symm _, @equiv.trans _⟩
 
 theorem equiv_of_mem {s t : computation α} {a} (h1 : a ∈ s) (h2 : a ∈ t) : s ~ t :=
-λa', ⟨λma, by rw mem_unique ma h1; exact h2,
-      λma, by rw mem_unique ma h2; exact h1⟩
+λ a', ⟨λ ma, by rw mem_unique ma h1; exact h2,
+      λ ma, by rw mem_unique ma h2; exact h1⟩
 
 theorem terminates_congr {c₁ c₂ : computation α}
   (h : c₁ ~ c₂) : terminates c₁ ↔ terminates c₂ :=
 by simp only [terminates_iff, exists_congr h]
 
 theorem promises_congr {c₁ c₂ : computation α}
   (h : c₁ ~ c₂) (a) : c₁ ~> a ↔ c₂ ~> a :=
-forall_congr (λa', imp_congr (h a') iff.rfl)
+forall_congr (λ a', imp_congr (h a') iff.rfl)
 
 theorem get_equiv {c₁ c₂ : computation α} (h : c₁ ~ c₂)
   [terminates c₁] [terminates c₂] : get c₁ = get c₂ :=
@@ -758,9 +758,9 @@ theorem thinkN_equiv (s : computation α) (n) : thinkN s n ~ s :=
 
 theorem bind_congr {s1 s2 : computation α} {f1 f2 : α → computation β}
   (h1 : s1 ~ s2) (h2 : ∀ a, f1 a ~ f2 a) : bind s1 f1 ~ bind s2 f2 :=
-λ b, ⟨λh, let ⟨a, ha, hb⟩ := exists_of_mem_bind h in
+λ b, ⟨λ h, let ⟨a, ha, hb⟩ := exists_of_mem_bind h in
         mem_bind ((h1 a).1 ha) ((h2 a b).1 hb),
-      λh, let ⟨a, ha, hb⟩ := exists_of_mem_bind h in
+      λ h, let ⟨a, ha, hb⟩ := exists_of_mem_bind h in
         mem_bind ((h1 a).2 ha) ((h2 a b).2 hb)⟩
 
 theorem equiv_ret_of_mem {s : computation α} {a} (h : a ∈ s) : s ~ return a :=
@@ -779,10 +779,10 @@ theorem lift_rel.swap (R : α → β → Prop) (ca : computation α) (cb : compu
 and_comm _ _
 
 theorem lift_eq_iff_equiv (c₁ c₂ : computation α) : lift_rel (=) c₁ c₂ ↔ c₁ ~ c₂ :=
-⟨λ⟨h1, h2⟩ a,
+⟨λ ⟨h1, h2⟩ a,
   ⟨λ a1, let ⟨b, b2, ab⟩ := h1 a1 in by rwa ab,
    λ a2, let ⟨b, b1, ab⟩ := h2 a2 in by rwa ←ab⟩,
-λe, ⟨λ a a1, ⟨a, (e _).1 a1, rfl⟩, λ a a2, ⟨a, (e _).2 a2, rfl⟩⟩⟩
+λ e, ⟨λ a a1, ⟨a, (e _).1 a1, rfl⟩, λ a a2, ⟨a, (e _).2 a2, rfl⟩⟩⟩
 
 theorem lift_rel.refl (R : α → α → Prop) (H : reflexive R) : reflexive (lift_rel R) :=
 λ s, ⟨λ a as, ⟨a, as, H a⟩, λ b bs, ⟨b, bs, H b⟩⟩
@@ -831,9 +831,9 @@ H.right h
 
 theorem lift_rel_def {R : α → β → Prop} {ca cb} : lift_rel R ca cb ↔
   (terminates ca ↔ terminates cb) ∧ ∀ {a b}, a ∈ ca → b ∈ cb → R a b :=
-⟨λh, ⟨terminates_of_lift_rel h, λ a b ma mb,
+⟨λ h, ⟨terminates_of_lift_rel h, λ a b ma mb,
   let ⟨b', mb', ab⟩ := h.left ma in by rwa mem_unique mb mb'⟩,
-λ⟨l, r⟩,
+λ ⟨l, r⟩,
  ⟨λ a ma, let ⟨⟨b, mb⟩⟩ := l.1 ⟨⟨_, ma⟩⟩ in ⟨b, mb, r ma mb⟩,
   λ b mb, let ⟨⟨a, ma⟩⟩ := l.2 ⟨⟨_, mb⟩⟩ in ⟨a, ma, r ma mb⟩⟩⟩
 
@@ -858,8 +858,8 @@ let ⟨l1, r1⟩ := h1 in
 
 @[simp] theorem lift_rel_return_left (R : α → β → Prop) (a : α) (cb : computation β) :
   lift_rel R (return a) cb ↔ ∃ {b}, b ∈ cb ∧ R a b :=
-⟨λ⟨l, r⟩, l (ret_mem _),
- λ⟨b, mb, ab⟩,
+⟨λ ⟨l, r⟩, l (ret_mem _),
+ λ ⟨b, mb, ab⟩,
   ⟨λ a' ma', by rw eq_of_ret_mem ma'; exact ⟨b, mb, ab⟩,
    λ b' mb', ⟨_, ret_mem _, by rw mem_unique mb' mb; exact ab⟩⟩⟩
 
@@ -870,13 +870,13 @@ by rw [lift_rel.swap, lift_rel_return_left]
 @[simp] theorem lift_rel_return (R : α → β → Prop) (a : α) (b : β) :
   lift_rel R (return a) (return b) ↔ R a b :=
 by rw [lift_rel_return_left]; exact
-⟨λ⟨b', mb', ab'⟩, by rwa eq_of_ret_mem mb' at ab',
- λab, ⟨_, ret_mem _, ab⟩⟩
+⟨λ ⟨b', mb', ab'⟩, by rwa eq_of_ret_mem mb' at ab',
+ λ ab, ⟨_, ret_mem _, ab⟩⟩
 
 @[simp] theorem lift_rel_think_left (R : α → β → Prop) (ca : computation α) (cb : computation β) :
   lift_rel R (think ca) cb ↔ lift_rel R ca cb :=
-and_congr (forall_congr $ λb, imp_congr ⟨of_think_mem, think_mem⟩ iff.rfl)
- (forall_congr $ λb, imp_congr iff.rfl $
+and_congr (forall_congr $ λ b, imp_congr ⟨of_think_mem, think_mem⟩ iff.rfl)
+ (forall_congr $ λ b, imp_congr iff.rfl $
     exists_congr $ λ b, and_congr ⟨of_think_mem, think_mem⟩ iff.rfl)
 
 @[simp] theorem lift_rel_think_right (R : α → β → Prop) (ca : computation α) (cb : computation β) :

src/data/seq/parallel.lean

@@ -18,7 +18,7 @@ open wseq
 variables {α : Type u} {β : Type v}
 
 def parallel.aux2 : list (computation α) → α ⊕ list (computation α) :=
-list.foldr (λc o, match o with
+list.foldr (λ c o, match o with
 | sum.inl a  := sum.inl a
 | sum.inr ls := rmap (λ c', c' :: ls) (destruct c)
 end) (sum.inr [])
@@ -204,7 +204,7 @@ def parallel_rec {S : wseq (computation α)} (C : α → Sort v)
   (H : ∀ s ∈ S, ∀ a ∈ s, C a) {a} (h : a ∈ parallel S) : C a :=
 begin
   let T : wseq (computation (α × computation α)) :=
-    S.map (λc, c.map (λ a, (a, c))),
+    S.map (λ c, c.map (λ a, (a, c))),
   have : S = T.map (map (λ c, c.1)),
   { rw [←wseq.map_comp], refine (wseq.map_id _).symm.trans (congr_arg (λ f, wseq.map f S) _),
     funext c, dsimp [id, function.comp], rw [←map_comp], exact (map_id _).symm },
@@ -243,11 +243,11 @@ theorem parallel_congr_lem {S T : wseq (computation α)} {a}
 theorem parallel_congr_left {S T : wseq (computation α)} {a}
   (h1 : ∀ s ∈ S, s ~> a) (H : S.lift_rel equiv T) : parallel S ~ parallel T :=
 let h2 := (parallel_congr_lem H).1 h1 in
-λ a', ⟨λh, by have aa := parallel_promises h1 h; rw ←aa; rw ←aa at h; exact
+λ a', ⟨λ h, by have aa := parallel_promises h1 h; rw ←aa; rw ←aa at h; exact
   let ⟨s, sS, as⟩ := exists_of_mem_parallel h,
       ⟨t, tT, st⟩ := wseq.exists_of_lift_rel_left H sS,
       aT := (st _).1 as in mem_parallel h2 tT aT,
-λh, by have aa := parallel_promises h2 h; rw ←aa; rw ←aa at h; exact
+λ h, by have aa := parallel_promises h2 h; rw ←aa; rw ←aa at h; exact
   let ⟨s, sS, as⟩ := exists_of_mem_parallel h,
       ⟨t, tT, st⟩ := wseq.exists_of_lift_rel_right H sS,
       aT := (st _).2 as in mem_parallel h1 tT aT⟩