lint(*): curly braces linter (#10280)

This PR:

1. Adds a style linter for curly braces: a line shall never end with `{` or start with `}` (modulo white space)
2. Adds `scripts/cleanup-braces.{sh,py}` to reflow lines that violate (1)
3. Runs the scripts from (2) to generate a boatload of changes in mathlib
4. Fixes one line that became to long due to (3)

archive/imo/imo1960_q1.lean

@@ -85,8 +85,8 @@ H.2 _ (by linarith [lt_1000 ppn]) ppn
 lemma right_direction {n : ℕ} : problem_predicate n → solution_predicate n :=
 begin
   have := search_up_to_start,
-  iterate 82 {
-    replace := search_up_to_step this (by norm_num1; refl) (by norm_num1; refl)
+  iterate 82
+  { replace := search_up_to_step this (by norm_num1; refl) (by norm_num1; refl)
       (by norm_num1; refl) dec_trivial },
   exact search_up_to_end this
 end

archive/imo/imo1988_q6.lean

@@ -99,8 +99,8 @@ begin
     { rw H_symm at hH, solve_by_elim },
     { solve_by_elim },
     -- The final two cases are very similar.
-    all_goals {
-      -- Consider the quadratic equation that (a,b) satisfies.
+    all_goals
+    { -- Consider the quadratic equation that (a,b) satisfies.
       rw H_quad at hH,
       -- We find the other root of the equation, and Vieta's formulas.
       rcases Vieta_formula_quadratic hH with ⟨c, h_root, hV₁, hV₂⟩,

archive/sensitivity.lean

@@ -190,13 +190,13 @@ begin
     simp },
   { dsimp [ε, e],
     cases hp : p 0 ; cases hq : q 0,
-    all_goals {
-      repeat {rw cond_tt},
+    all_goals
+    { repeat {rw cond_tt},
       repeat {rw cond_ff},
       simp only [linear_map.fst_apply, linear_map.snd_apply, linear_map.comp_apply, IH],
       try { congr' 1, rw Q.succ_n_eq, finish },
-      try {
-        erw (ε _).map_zero,
+      try
+      { erw (ε _).map_zero,
         have : p ≠ q, { intro h, rw p.succ_n_eq q at h, finish },
         simp [this] } } }
 end
@@ -210,8 +210,8 @@ begin
     ext ; change _ = (0 : V n) ; simp only ; apply ih ; intro p ;
     [ let q : Q (n+1) := λ i, if h : i = 0 then tt else p (i.pred h),
       let q : Q (n+1) := λ i, if h : i = 0 then ff else p (i.pred h)],
-    all_goals {
-      specialize h q,
+    all_goals
+    { specialize h q,
       rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|>
         rw [ε, show q 0 = ff, from rfl, cond_ff] at h,
       rwa show p = π q, by { ext, simp [q, fin.succ_ne_zero, π] } } }

scripts/cleanup-braces.py

@@ -0,0 +1,85 @@
+#!/usr/bin/env python3
+
+from pathlib import Path
+import re
+import sys, os
+
+TMP_SUFFIX = ".brace_cleanup"
+
+def fix_brace_o(a, b):
+    """Move any `{`s between the contents of line `a` and line `b` to the start of line `b`.
+    
+    :param a: A line of Lean code, ending with `\n'
+    :param b: A line of Lean code, ending with `\n'
+    
+    :returns: A tuple `(anew, bnew, fix)`, where `anew` and `bnew` are `a` and `b` with corrected brace positions,
+    and `fix` is a boolean indicating whether there was a change, i.e. `fix = ((anew, bnew) != (a, b))`.
+    """
+    astr = a.rstrip()
+    if astr == "":
+        return a, b, False
+    if not astr[-1] == '{':
+        return a, b, False
+    a = astr[:-1].rstrip() + '\n'
+    bstr = b.lstrip()
+    indent = len(b) - len(bstr)
+    indent = max(indent - 2, 0)
+    b = " " * indent + "{ " + bstr
+    return a, b, True
+
+def fix_brace_c(a, b):
+    """Move any `}`s between the contents of line `a` and line `b` to the end of line `a`.
+    
+    :param a: A line of Lean code, ending with `\n'
+    :param b: A line of Lean code, ending with `\n'
+    
+    :returns: A tuple `(anew, bnew, merge)`, where `anew` and `bnew` are `a` and `b` with corrected brace positions,
+    and `merge` is a boolean indicating if the result is a single line, returned in `bnew` (and `anew` can be ignored).
+    """
+    bstr = b.lstrip()
+    if bstr == "":
+        return a, b, False
+    if not bstr[0] == '}':
+        return a, b, False
+    return "", a.rstrip() + " " + bstr, True
+
+def fix_brace_pair(a, b):
+    """Move any `{`s and `}`s between the contents of line `a` and line `b` to the correct position.
+    
+    :param a: A line of Lean code, ending with `\n'
+    :param b: A line of Lean code, ending with `\n'
+    
+    :returns: A tuple `(anew, bnew, merge)`, where `anew` and `bnew` are `a` and `b` with corrected brace positions,
+    and `merge` is a boolean indicating if the result is a single line, returned in `bnew` (and `anew` can be ignored).
+    """
+    anew, bnew, fix = fix_brace_o(a, b)
+    if fix:  # `a` ended with a `{` that got moved to `bnew`, so `fix_brace_c` doesn't have anything to do.
+        return anew, bnew, False
+    else:
+        return fix_brace_c(anew, bnew)
+
+def fix_braces(filename):
+    # open files for reading and writing
+    fi = Path(filename).open(mode="r", encoding="utf-8", newline='\n')
+    fo = Path(filename + TMP_SUFFIX).open(mode="w", encoding="utf-8", newline='\n')
+    merge = False  # indicates when `ao` got merged into `bo`, so we can ignore `ao`.
+    # read the first line
+    ai = fi.readline()
+    bo = ai # if there is only one line, the last output line is the first line
+    while (bi := fi.readline()):
+        ao, bo, merge = fix_brace_pair(ai, bi)
+        # prepare for next iteration
+        ai = bo
+        if not merge:
+            fo.write(ao)
+    # write the last line
+    fo.write(bo)
+    # close the files
+    fi.close()
+    fo.close()
+    # move the output file back to the input
+    os.rename(filename + TMP_SUFFIX, filename)
+
+for filename in sys.argv[1:]:
+    fix_braces(filename)
+

scripts/cleanup-braces.sh

@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+
+set -exo pipefail
+
+find src archive counterexamples -name '*.lean' | xargs ./scripts/cleanup-braces.py

scripts/lint-style.py

@@ -43,6 +43,7 @@
 ERR_OME = 8 # imported tactic.omega
 ERR_TAC = 9 # imported tactic
 WRN_IND = 10 # indentation
+WRN_BRC = 11 # curly braces
 
 exceptions = []
 
@@ -77,6 +78,8 @@
             exceptions += [(ERR_TAC, path)]
         if errno == "WRN_IND":
             exceptions += [(WRN_IND, path)]
+        if errno == "WRN_BRC":
+            exceptions += [(WRN_BRC, path)]
 
 new_exceptions = False
 
@@ -210,6 +213,24 @@ def indent_check(lines, path):
         indent_lvl -= 2 * line.count('}') # there can be multiple closing braces on one line
     return errors
 
+def braces_check(lines, path):
+    """Check that curly braces are placed correctly.
+
+    This linter warns whenever a `{` (resp. `}`) appears at the end (resp. start) of a line.
+    """
+    errors = []
+    for line_nr, line in enumerate(lines, 1):
+        lstr = line.strip()
+        if len(lstr) == 0:
+            continue
+        if lstr[-1] == '{':
+            if "goal" in lstr:
+                continue
+            errors += [(WRN_BRC, line_nr, path)]
+        if lstr[0] == '}':
+            errors += [(WRN_BRC, line_nr, path)]
+    return errors
+
 def import_only_check(lines, path):
     import_only_file = True
     errors = []
@@ -328,6 +349,8 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_TAC", "Files in mathlib cannot import the whole tactic folder")
         if errno == WRN_IND:
             output_message(path, line_nr, "WRN_IND", "Probable indentation mistake in proof")
+        if errno == WRN_BRC:
+            output_message(path, line_nr, "WRN_BRC", "Probable misformatting of curly braces")
 
 def lint(path):
     with path.open(encoding="utf-8") as f:
@@ -350,6 +373,8 @@ def lint(path):
         format_errors(errs)
         errs = indent_check(lines, path)
         format_errors(errs)
+        errs = braces_check(lines, path)
+        format_errors(errs)
 
 for filename in sys.argv[1:]:
     lint(Path(filename))

src/algebra/algebra/basic.lean

@@ -309,8 +309,8 @@ variables (R)
 /-- A `semiring` that is an `algebra` over a commutative ring carries a natural `ring` structure.
 See note [reducible non-instances]. -/
 @[reducible]
-def semiring_to_ring [semiring A] [algebra R A] : ring A := {
-  ..module.add_comm_monoid_to_add_comm_group R,
+def semiring_to_ring [semiring A] [algebra R A] : ring A :=
+{ ..module.add_comm_monoid_to_add_comm_group R,
   ..(infer_instance : semiring A) }
 
 variables {R}

src/algebra/algebra/operations.lean

@@ -329,8 +329,8 @@ which is equivalent to `x • J ⊆ I` (see `mem_div_iff_smul_subset`), but nice
 This is the general form of the ideal quotient, traditionally written $I : J$.
 -/
 instance : has_div (submodule R A) :=
-⟨ λ I J, {
-  carrier   := { x | ∀ y ∈ J, x * y ∈ I },
+⟨ λ I J,
+{ carrier   := { x | ∀ y ∈ J, x * y ∈ I },
   zero_mem' := λ y hy, by { rw zero_mul, apply submodule.zero_mem },
   add_mem'  := λ a b ha hb y hy, by { rw add_mul, exact submodule.add_mem _ (ha _ hy) (hb _ hy) },
   smul_mem' := λ r x hx y hy, by { rw algebra.smul_mul_assoc,

src/algebra/category/CommRing/pushout.lean

@@ -40,22 +40,19 @@ begin
 end
 
 @[simp]
-lemma pushout_cocone_inl : (pushout_cocone f g).inl = (by {
-  letI := f.to_algebra, letI := g.to_algebra,
-  exactI algebra.tensor_product.include_left.to_ring_hom
-}) := rfl
+lemma pushout_cocone_inl : (pushout_cocone f g).inl = (by
+{ letI := f.to_algebra, letI := g.to_algebra,
+  exactI algebra.tensor_product.include_left.to_ring_hom }) := rfl
 
 @[simp]
-lemma pushout_cocone_inr : (pushout_cocone f g).inr = (by {
-  letI := f.to_algebra, letI := g.to_algebra,
-  exactI algebra.tensor_product.include_right.to_ring_hom
-}) := rfl
+lemma pushout_cocone_inr : (pushout_cocone f g).inr = (by
+{ letI := f.to_algebra, letI := g.to_algebra,
+  exactI algebra.tensor_product.include_right.to_ring_hom }) := rfl
 
 @[simp]
-lemma pushout_cocone_X : (pushout_cocone f g).X = (by {
-  letI := f.to_algebra, letI := g.to_algebra,
-  exactI CommRing.of (A ⊗[R] B)
-}) := rfl
+lemma pushout_cocone_X : (pushout_cocone f g).X = (by
+{ letI := f.to_algebra, letI := g.to_algebra,
+  exactI CommRing.of (A ⊗[R] B) }) := rfl
 
 /-- Verify that the `pushout_cocone` is indeed the colimit. -/
 def pushout_cocone_is_colimit : limits.is_colimit (pushout_cocone f g) :=
@@ -64,24 +61,22 @@ begin
   letI := ring_hom.to_algebra f,
   letI := ring_hom.to_algebra g,
   letI := ring_hom.to_algebra (f ≫ s.inl),
-  let f' : A →ₐ[R] s.X := { commutes' := λ r, by {
-        change s.inl.to_fun (f r) = (f ≫ s.inl) r, refl
-      }, ..s.inl },
-  let g' : B →ₐ[R] s.X := { commutes' := λ r, by {
-        change (g ≫ s.inr) r = (f ≫ s.inl) r,
+  let f' : A →ₐ[R] s.X := { commutes' := λ r, by
+      { change s.inl.to_fun (f r) = (f ≫ s.inl) r, refl }, ..s.inl },
+  let g' : B →ₐ[R] s.X := { commutes' := λ r, by
+      { change (g ≫ s.inr) r = (f ≫ s.inl) r,
         congr' 1,
         exact (s.ι.naturality limits.walking_span.hom.snd).trans
-          (s.ι.naturality limits.walking_span.hom.fst).symm
-      }, ..s.inr },
+          (s.ι.naturality limits.walking_span.hom.fst).symm }, ..s.inr },
   /- The factor map is a ⊗ b ↦ f(a) * g(b). -/
   use alg_hom.to_ring_hom (algebra.tensor_product.product_map f' g'),
   simp only [pushout_cocone_inl, pushout_cocone_inr],
   split, { ext x, exact algebra.tensor_product.product_map_left_apply  _ _ x, },
   split, { ext x, exact algebra.tensor_product.product_map_right_apply _ _ x, },
   intros h eq1 eq2,
   let h' : (A ⊗[R] B) →ₐ[R] s.X :=
-    { commutes' := λ r, by {
-      change h ((f r) ⊗ₜ[R] 1) = s.inl (f r),
+    { commutes' := λ r, by
+    { change h ((f r) ⊗ₜ[R] 1) = s.inl (f r),
       rw ← eq1, simp }, ..h },
   suffices : h' = algebra.tensor_product.product_map f' g',
   { ext x,

src/algebra/category/Group/images.lean

@@ -69,8 +69,7 @@ noncomputable def image.lift (F' : mono_factorisation f) : image f ⟶ F'.I :=
     rw (classical.indefinite_description (λ z, f z = _) _).2,
     rw (classical.indefinite_description (λ z, f z = _) _).2,
     refl,
-  end,
- }
+  end, }
 lemma image.lift_fac (F' : mono_factorisation f) : image.lift F' ≫ F'.m = image.ι f :=
 begin
   ext x,

src/algebra/category/Mon/adjunctions.lean

@@ -37,8 +37,7 @@ def adjoin_one : Semigroup.{u} ⥤ Mon.{u} :=
 instance has_forget_to_Semigroup : has_forget₂ Mon Semigroup :=
 { forget₂ :=
   { obj := λ M, Semigroup.of M,
-    map := λ M N, monoid_hom.to_mul_hom },
-}
+    map := λ M N, monoid_hom.to_mul_hom }, }
 
 /-- The adjoin_one-forgetful adjunction from `Semigroup` to `Mon`.-/
 @[to_additive "The adjoin_one-forgetful adjunction from `AddSemigroup` to `AddMon`"]

src/algebra/continued_fractions/convergents_equiv.lean

@@ -361,8 +361,8 @@ begin
           obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.nth m = some gp_m, from
             g.s.ge_stable m.le_succ s_succ_mth_eq,
           -- we then plug them into the recurrence
-          suffices : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b, by {
-            have ot : g'.s.nth m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩, from
+          suffices : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b, by
+          { have ot : g'.s.nth m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩, from
               squash_seq_nth_of_not_terminated mth_s_eq s_succ_mth_eq,
             have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩, by cc,
             rwa this },

src/algebra/direct_sum/ring.lean

@@ -206,8 +206,8 @@ begin
 end
 
 /-- The `semiring` structure derived from `gsemiring A`. -/
-instance semiring : semiring (⨁ i, A i) := {
-  one := 1,
+instance semiring : semiring (⨁ i, A i) :=
+{ one := 1,
   mul := (*),
   zero := 0,
   add := (+),
@@ -241,8 +241,8 @@ begin
 end
 
 /-- The `comm_semiring` structure derived from `gcomm_semiring A`. -/
-instance comm_semiring : comm_semiring (⨁ i, A i) := {
-  one := 1,
+instance comm_semiring : comm_semiring (⨁ i, A i) :=
+{ one := 1,
   mul := (*),
   zero := 0,
   add := (+),
@@ -255,8 +255,8 @@ section ring
 variables [Π i, add_comm_group (A i)] [add_comm_monoid ι] [gsemiring A]
 
 /-- The `ring` derived from `gsemiring A`. -/
-instance ring : ring (⨁ i, A i) := {
-  one := 1,
+instance ring : ring (⨁ i, A i) :=
+{ one := 1,
   mul := (*),
   zero := 0,
   add := (+),
@@ -271,8 +271,8 @@ section comm_ring
 variables [Π i, add_comm_group (A i)] [add_comm_monoid ι] [gcomm_semiring A]
 
 /-- The `comm_ring` derived from `gcomm_semiring A`. -/
-instance comm_ring : comm_ring (⨁ i, A i) := {
-  one := 1,
+instance comm_ring : comm_ring (⨁ i, A i) :=
+{ one := 1,
   mul := (*),
   zero := 0,
   add := (+),