Merge branch 'master' into YK-card-fiber-eq

.github/workflows/add_ported_warnings.yml

@@ -0,0 +1,29 @@
+name: Add mathlib4 porting warnings
+
+on:
+  pull_request:
+
+jobs:
+  build:
+    name: Check for modifications to ported files
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: install Python
+        uses: actions/setup-python@v3
+        with:
+          python-version: 3.8
+
+      - name: install latest mathlibtools
+        run: |
+          pip install git+https://github.com/leanprover-community/mathlib-tools
+
+      # TODO: is this really faster than just calling git from python?
+      - name: Get changed files
+        id: changed-files
+        uses: tj-actions/changed-files@v34
+
+      - name: run the script
+        run: |
+          python scripts/detect_ported_files.py ${{ steps.changed-files.outputs.all_changed_files }}

archive/100-theorems-list/16_abel_ruffini.lean

@@ -3,11 +3,13 @@ Copyright (c) 2021 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
-import field_theory.abel_ruffini
 import analysis.calculus.local_extr
+import data.nat.prime_norm_num
+import field_theory.abel_ruffini
 import ring_theory.eisenstein_criterion
+
 /-!
-Construction of an algebraic number that is not solvable by radicals.
+# Construction of an algebraic number that is not solvable by radicals.
 
 The main ingredients are:
  * `solvable_by_rad.is_solvable'` in `field_theory/abel_ruffini` :
@@ -131,7 +133,7 @@ begin
   have q_ne_zero : Φ ℚ a b ≠ 0 := (monic_Phi a b).ne_zero,
   obtain ⟨x, y, hxy, hx, hy⟩ := real_roots_Phi_ge_aux a b hab,
   have key : ↑({x, y} : finset ℝ) ⊆ (Φ ℚ a b).root_set ℝ,
-  { simp [set.insert_subset, mem_root_set q_ne_zero, hx, hy] },
+  { simp [set.insert_subset, mem_root_set_of_ne q_ne_zero, hx, hy] },
   convert fintype.card_le_of_embedding (set.embedding_of_subset _ _ key),
   simp only [finset.coe_sort_coe, fintype.card_coe, finset.card_singleton,
              finset.card_insert_of_not_mem (mt finset.mem_singleton.mp hxy)]

archive/100-theorems-list/42_inverse_triangle_sum.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jalex Stark, Yury Kudryashov
 -/
+import algebra.big_operators.basic
 import data.real.basic
 
 /-!

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -3,10 +3,9 @@ Copyright (c) 2019 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import data.fin.tuple
 import data.real.basic
+import data.set.finite
 import data.set.intervals
-import data.set.pairwise
 
 /-!
 Proof that a cube (in dimension n ≥ 3) cannot be cubed:

archive/imo/imo1988_q6.lean

@@ -8,6 +8,7 @@ import data.nat.prime
 import data.rat.defs
 import order.well_founded
 import tactic.linarith
+import tactic.wlog
 
 /-!
 # IMO 1988 Q6 and constant descent Vieta jumping
@@ -111,8 +112,8 @@ begin
       -- And hence we are done by H_zero and H_diag.
       solve_by_elim } },
   -- To finish the main proof, we need to show that the exceptional locus is nonempty.
-  -- So we assume that the exceptional locus is empty, and work towards dering a contradiction.
-  rw ← set.ne_empty_iff_nonempty,
+  -- So we assume that the exceptional locus is empty, and work towards deriving a contradiction.
+  rw set.nonempty_iff_ne_empty,
   assume exceptional_empty,
   -- Observe that S is nonempty.
   have S_nonempty : S.nonempty,

archive/imo/imo1998_q2.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import data.fintype.basic
+import data.fintype.prod
 import data.int.parity
 import algebra.big_operators.order
 import tactic.ring
@@ -138,7 +138,7 @@ lemma norm_bound_of_odd_sum {x y z : ℤ} (h : x + y = 2*z + 1) :
   2*z*z + 2*z + 1 ≤ x*x + y*y :=
 begin
   suffices : 4*z*z + 4*z + 1 + 1 ≤ 2*x*x + 2*y*y,
-  { rw ← mul_le_mul_left (@zero_lt_two _ _ int.nontrivial), convert this; ring, },
+  { rw ← mul_le_mul_left (zero_lt_two' ℤ), convert this; ring, },
   have h' : (x + y) * (x + y) = 4*z*z + 4*z + 1, { rw h, ring, },
   rw [← add_sq_add_sq_sub, h', add_le_add_iff_left],
   suffices : 0 < (x - y) * (x - y), { apply int.add_one_le_of_lt this, },

archive/imo/imo2005_q4.lean

@@ -80,7 +80,7 @@ begin
   have hp : nat.prime p := nat.min_fac_prime hk',
   -- So `3 ≤ p`
   have hp₃ : 3 ≤ p,
-  { have : 2 ≠ p := by rwa nat.coprime_primes (by norm_num : nat.prime 2) hp at hp₂,
+  { have : 2 ≠ p := by rwa nat.coprime_primes nat.prime_two hp at hp₂,
     apply nat.lt_of_le_and_ne hp.two_le this, },
   -- Testing the special property of `k` for the `p - 2`th term of the sequence, we see that `p` is
   -- coprime to `a (p - 2)`.

counterexamples/char_p_zero_ne_char_zero.lean

@@ -18,11 +18,8 @@ This file shows that there are semiring `R` for which `char_p R 0` holds and `ch
 The example is `{0, 1}` with saturating addition.
 -/
 
-local attribute [semireducible] with_zero
-
-@[simp] lemma add_one_eq_one : ∀ (x : with_zero unit), x + 1 = 1
-| 0 := rfl
-| 1 := rfl
+@[simp] lemma add_one_eq_one (x : with_zero unit) : x + 1 = 1 :=
+with_zero.cases_on x (by refl) (λ h, by refl)
 
 lemma with_zero_unit_char_p_zero : char_p (with_zero unit) 0 :=
 ⟨λ x, by cases x; simp⟩

counterexamples/direct_sum_is_internal.lean

@@ -5,6 +5,7 @@ Authors: Eric Wieser, Kevin Buzzard
 -/
 
 import algebra.direct_sum.module
+import algebra.group.conj_finite
 import tactic.fin_cases
 
 /-!

counterexamples/homogeneous_prime_not_prime.lean

@@ -118,14 +118,14 @@ instance : graded_algebra (grading R) :=
 /-- The counterexample is the ideal `I = span {(2, 2)}`. -/
 def I : ideal (R × R) := ideal.span {((2, 2) : (R × R))}.
 
-set_option class.instance_max_depth 33
+set_option class.instance_max_depth 34
 
 lemma I_not_prime : ¬ I.is_prime :=
 begin
   rintro ⟨rid1, rid2⟩,
   apply rid1, clear rid1, revert rid2,
   simp only [I, ideal.mem_span_singleton, ideal.eq_top_iff_one],
-  dec_trivial, -- this is what we change the max instance depth for, it's only 1 above the default
+  dec_trivial, -- this is what we change the max instance depth for, it's only 2 above the default
 end
 
 set_option class.instance_max_depth 32

counterexamples/phillips.lean

@@ -532,7 +532,7 @@ begin
     ⊆ ⋃ y ∈ φ.to_bounded_additive_measure.discrete_support, {x | y ∈ spf Hcont x},
   { assume x hx,
     dsimp at hx,
-    rw [← ne.def, ne_empty_iff_nonempty] at hx,
+    rw [← ne.def, ←nonempty_iff_ne_empty] at hx,
     simp only [exists_prop, mem_Union, mem_set_of_eq],
     exact hx },
   apply countable.mono (subset.trans A B),

scripts/add_port_comments.py

@@ -57,23 +57,30 @@ def add_port_status(fcontent: str, fstatus: FileStatus) -> str:
     module_comment_end = module_comment.end(1)
     module_comment = module_comment.group(1)
 
-    # remove any existing comment
-    comment_re = re.compile(
+    # replace any markers that appear at the start of the docstring
+    module_comment = re.compile(
+        r"\A\n((?:> )?)THIS FILE IS SYNCHRONIZED WITH MATHLIB4\."
+        r"(?:\n\1[^\n]+)*\n?",
+        re.MULTILINE
+    ).sub('', module_comment)
+
+    # markers which appear with two blank lines before
+    module_comment = re.compile(
         r"\n{,2}((?:> )?)THIS FILE IS SYNCHRONIZED WITH MATHLIB4\."
         r"(?:\n\1[^\n]+)*",
         re.MULTILINE
-    )
-    module_comment = comment_re.sub('', module_comment)
+    ).sub('', module_comment)
 
     # find the header
     header_re = re.compile('(#[^\n]*)', re.MULTILINE)
     existing_header = header_re.search(module_comment)
-    if not existing_header:
-        raise ValueError(f"No header in {module_comment!r}")
-
-    # insert a comment below the header
-    module_comment = replace_range(module_comment, existing_header.end(1), existing_header.end(1),
-        "\n\n" + make_comment(f_status))
+    if existing_header:
+        # insert a comment below the header
+        module_comment = replace_range(module_comment, existing_header.end(1), existing_header.end(1),
+            "\n\n" + make_comment(f_status))
+    else:
+        # insert the comment at the top
+        module_comment = "\n" + make_comment(f_status) + "\n" + module_comment
 
     # and insert the new module docstring
     fcontent = replace_range(fcontent, module_comment_start, module_comment_end, module_comment)

scripts/detect_ported_files.py

@@ -0,0 +1,28 @@
+# this script is only intended to be run by CI
+import sys
+from pathlib import Path
+
+from mathlibtools.file_status import PortStatus, FileStatus
+
+status = PortStatus.deserialize_old()
+
+src_path = Path(__file__).parent.parent / 'src'
+
+def encode_msg_text_for_github(msg):
+    # even though this is probably url quoting, we match the implementation at
+    # https://github.com/actions/toolkit/blob/af821474235d3c5e1f49cee7c6cf636abb0874c4/packages/core/src/command.ts#L36-L94
+    return msg.replace('%', '%25').replace('\r', '%0D').replace('\n', '%0A')
+
+def fname_for(import_path: str) -> Path:
+    return src_path / Path(*import_path.split('.')).with_suffix('.lean')
+
+if __name__ == '__main__':
+    files = [Path(f) for f in sys.argv[1:]]
+    for iname, f_status in status.file_statuses.items():
+        if f_status.ported:
+            fname = fname_for(iname)
+            if fname in files:
+                msg = ("Changes to this file will need to be ported to mathlib 4!\n"
+                    "Please consider retracting the changes to this file unless you are willing "
+                    "to immediately forward-port them." )
+                print(f"::warning file={fname},line=1,col=1::{encode_msg_text_for_github(msg)}")

scripts/port_status.py

@@ -8,18 +8,20 @@
 from mathlibtools.lib import PortStatus, LeanProject, FileStatus
 from sys import argv
 from pathlib import Path
+import shlex
 
 import_re = re.compile(r"^import ([^ ]*)")
 synchronized_re = re.compile(r".*SYNCHRONIZED WITH MATHLIB4.*")
 hash_re = re.compile(r"[0-9a-f]*")
 
-# not using re.compile as this is passed to git
-comment_git_re = '^' + '|'.join(re.escape(line) for line in [
-    "> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.",
-    "> https://github.com/leanprover-community/mathlib4/pull/.*",
-    "> Any changes to this file require a corresponding PR to mathlib4.",
-    ""
-]) + '$'
+# Not using re.compile as this is passed to git which uses a different regex dialect:
+# https://www.sjoerdlangkemper.nl/2021/08/13/how-does-git-diff-ignore-matching-lines-work/
+comment_git_re = r'\`(' + r'|'.join([
+    re.escape("> THIS FILE IS SYNCHRONIZED WITH MATHLIB4."),
+    re.escape("> https://github.com/leanprover-community/mathlib4/pull/") + r"[0-9]*",
+    re.escape("> Any changes to this file require a corresponding PR to mathlib4."),
+    r"",
+]) + r")" + "\n"
 
 proj = LeanProject.from_path(Path(__file__).parent.parent)
 
@@ -69,12 +71,12 @@ def mk_label(path: Path) -> str:
 for node in graph.nodes:
     if data[node].mathlib3_hash:
         verified[node] = data[node].mathlib3_hash
-        git_command = ['git', 'diff', '--name-only',
+        git_command = ['git', 'diff', '--quiet',
             f'--ignore-matching-lines={comment_git_re}',
-            data[node].mathlib3_hash + "..HEAD", "src" + os.sep + node.replace('.', os.sep) + ".lean"]
-        result = subprocess.run(git_command, stdout=subprocess.PIPE)
-        if result.stdout != b'':
-            del(git_command[2:4])
+            data[node].mathlib3_hash + "..HEAD", "--", "src" + os.sep + node.replace('.', os.sep) + ".lean"]
+        result = subprocess.run(git_command)
+        if result.returncode == 1:
+            git_command.remove('--quiet')
             touched[node] = git_command
     elif data[node].ported:
         print("Bad status for " + node)
@@ -120,4 +122,4 @@ def mk_label(path: Path) -> str:
     print()
     print('# The following files have been modified since the commit at which they were verified.')
     for v in touched.values():
-        print(' '.join(v))
+        print(' '.join(shlex.quote(vi) for vi in v))

src/algebra/add_torsor.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers, Yury Kudryashov
 -/
-import data.set.pointwise.basic
+import data.set.pointwise.smul
 
 /-!
 # Torsors of additive group actions