diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index e43db8caf1548..e808ac75f1a2e 100644 --- a/.github/workflows/bors.yml +++ b/.github/workflows/bors.yml @@ -192,13 +192,26 @@ jobs: - name: install Python dependencies if: ${{ ! 1 }} - run: python3 -m pip install --upgrade pip pyyaml requests + run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools - name: tests run: | set -o pipefail lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py + - name: check archive and counterexample directories have unique identifiers + run: | + pip install mathlibtools + (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean) + (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean) + python -m mathlibtools.leanproject mk-all + echo "import all" >> all_all.lean + echo "import counterexamples_all" >> all_all.lean + echo "import archive_all" >> all_all.lean + echo "path ./archive" >> leanpkg.path + echo "path ./counterexamples" >> leanpkg.path + lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py + - uses: actions/setup-java@v2 if: ${{ ! 1 }} with: diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 8296a49e4e11b..0656b61d919ae 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -200,13 +200,26 @@ jobs: - name: install Python dependencies if: ${{ ! 1 }} - run: python3 -m pip install --upgrade pip pyyaml requests + run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools - name: tests run: | set -o pipefail lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py + - name: check archive and counterexample directories have unique identifiers + run: | + pip install mathlibtools + (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean) + (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean) + python -m mathlibtools.leanproject mk-all + echo "import all" >> all_all.lean + echo "import counterexamples_all" >> all_all.lean + echo "import archive_all" >> all_all.lean + echo "path ./archive" >> leanpkg.path + echo "path ./counterexamples" >> leanpkg.path + lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py + - uses: actions/setup-java@v2 if: ${{ ! 1 }} with: diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in index ffed44267c589..f17250cc6b119 100644 --- a/.github/workflows/build.yml.in +++ b/.github/workflows/build.yml.in @@ -178,13 +178,26 @@ jobs: - name: install Python dependencies if: ${{ ! IS_SELF_HOSTED }} - run: python3 -m pip install --upgrade pip pyyaml requests + run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools - name: tests run: | set -o pipefail lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py + - name: check archive and counterexample directories have unique identifiers + run: | + pip install mathlibtools + (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean) + (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean) + python -m mathlibtools.leanproject mk-all + echo "import all" >> all_all.lean + echo "import counterexamples_all" >> all_all.lean + echo "import archive_all" >> all_all.lean + echo "path ./archive" >> leanpkg.path + echo "path ./counterexamples" >> leanpkg.path + lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py + - uses: actions/setup-java@v2 if: ${{ ! IS_SELF_HOSTED }} with: diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index 3a093a8e654f4..8f12c3bc1f37d 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -198,13 +198,26 @@ jobs: - name: install Python dependencies if: ${{ ! 0 }} - run: python3 -m pip install --upgrade pip pyyaml requests + run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools - name: tests run: | set -o pipefail lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py + - name: check archive and counterexample directories have unique identifiers + run: | + pip install mathlibtools + (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean) + (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean) + python -m mathlibtools.leanproject mk-all + echo "import all" >> all_all.lean + echo "import counterexamples_all" >> all_all.lean + echo "import archive_all" >> all_all.lean + echo "path ./archive" >> leanpkg.path + echo "path ./counterexamples" >> leanpkg.path + lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py + - uses: actions/setup-java@v2 if: ${{ ! 0 }} with: diff --git a/.gitignore b/.gitignore index ed583e63ad380..a7798b842bb80 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,6 @@ *.olean /_target -/leanpkg.path +leanpkg.path _cache __pycache__ all.lean diff --git a/archive/100-theorems-list/82_cubing_a_cube.lean b/archive/100-theorems-list/82_cubing_a_cube.lean index 330a23188f703..ff662f64b69eb 100644 --- a/archive/100-theorems-list/82_cubing_a_cube.lean +++ b/archive/100-theorems-list/82_cubing_a_cube.lean @@ -16,11 +16,12 @@ We follow the proof described here: http://www.alaricstephen.com/main-featured/2017/9/28/cubing-a-cube-proof -/ - open real set function fin noncomputable theory +namespace «82» + variable {n : ℕ} /-- Given three intervals `I, J, K` such that `J ⊂ I`, @@ -517,3 +518,5 @@ begin exact @not_correct n s coe hfin.to_subtype h2.coe_sort ⟨hd.subtype _ _, (Union_subtype _ _).trans hU, hinj.injective, hn⟩ end + +end «82» diff --git a/archive/imo/imo1960_q1.lean b/archive/imo/imo1960_q1.lean index 7caef8294f29b..fa3ee7680092f 100644 --- a/archive/imo/imo1960_q1.lean +++ b/archive/imo/imo1960_q1.lean @@ -22,6 +22,8 @@ The strategy here is roughly brute force, checking the possible multiples of 11. open nat +namespace imo1960_q1 + def sum_of_squares (L : list ℕ) : ℕ := (L.map (λ x, x * x)).sum def problem_predicate (n : ℕ) : Prop := @@ -98,5 +100,9 @@ Now we just need to prove the equivalence, for the precise problem statement. lemma left_direction (n : ℕ) (spn : solution_predicate n) : problem_predicate n := by rcases spn with (rfl | rfl); norm_num [problem_predicate, sum_of_squares] +end imo1960_q1 + +open imo1960_q1 + theorem imo1960_q1 (n : ℕ) : problem_predicate n ↔ solution_predicate n := ⟨right_direction, left_direction n⟩ diff --git a/archive/imo/imo1962_q1.lean b/archive/imo/imo1962_q1.lean index 7bd2c6f015d7c..0afc5e6be6726 100644 --- a/archive/imo/imo1962_q1.lean +++ b/archive/imo/imo1962_q1.lean @@ -21,6 +21,8 @@ we define the problem as a predicate, and then prove a particular number is the of a set satisfying it. -/ +namespace imo1962_q1 + open nat def problem_predicate (n : ℕ) : Prop := @@ -154,5 +156,9 @@ begin exact h5.ge, }, }, end +end imo1962_q1 + +open imo1962_q1 + theorem imo1962_q1 : is_least {n | problem_predicate n} 153846 := ⟨satisfied_by_153846, no_smaller_solutions⟩ diff --git a/archive/imo/imo1964_q1.lean b/archive/imo/imo1964_q1.lean index ac90068a7afb6..fd987ba4f5f10 100644 --- a/archive/imo/imo1964_q1.lean +++ b/archive/imo/imo1964_q1.lean @@ -24,6 +24,8 @@ integers which are a multiple of 3. open nat +namespace imo1964_q1 + lemma two_pow_three_mul_mod_seven (m : ℕ) : 2 ^ (3 * m) ≡ 1 [MOD 7] := begin rw pow_mul, @@ -79,6 +81,10 @@ begin apply two_pow_three_mul_mod_seven } end +end imo1964_q1 + +open imo1964_q1 + theorem imo1964_q1b (n : ℕ) : ¬ (7 ∣ 2 ^ n + 1) := begin let t := n % 3, diff --git a/archive/imo/imo1969_q1.lean b/archive/imo/imo1969_q1.lean index a2ccb8cca33e6..3eee264d353ca 100644 --- a/archive/imo/imo1969_q1.lean +++ b/archive/imo/imo1969_q1.lean @@ -17,6 +17,8 @@ the number $z = n^4 + a$ is not prime for any natural number $n$. open int nat +namespace imo1969_q1 + /-- `good_nats` is the set of natural numbers satisfying the condition in the problem statement, namely the `a : ℕ` such that `n^4 + a` is not prime for any `n : ℕ`. -/ def good_nats : set ℕ := {a : ℕ | ∀ n : ℕ, ¬ nat.prime (n^4 + a)} @@ -67,6 +69,10 @@ in the `strict_mono` namespace. -/ lemma a_choice_strict_mono : strict_mono a_choice := ((strict_mono_id.const_add 2).nat_pow (dec_trivial : 0 < 4)).const_mul (dec_trivial : 0 < 4) +end imo1969_q1 + +open imo1969_q1 + /-- We conclude by using the fact that `a_choice` is an injective function from the natural numbers to the set `good_nats`. -/ theorem imo1969_q1 : set.infinite {a : ℕ | ∀ n : ℕ, ¬ nat.prime (n^4 + a)} := diff --git a/archive/imo/imo1981_q3.lean b/archive/imo/imo1981_q3.lean index ea34d76d03bf2..4b40612e5a873 100644 --- a/archive/imo/imo1981_q3.lean +++ b/archive/imo/imo1981_q3.lean @@ -24,7 +24,7 @@ We first generalize the problem to `{1, 2, ..., N}` and specialize to `N = 1981` -/ open int nat set -section +namespace imo1981_q3 variable (N : ℕ) -- N = 1981 @[mk_iff] structure problem_predicate (m n : ℤ) : Prop := @@ -189,7 +189,9 @@ theorem solution_greatest (H : problem_predicate N (fib K) (fib (K + 1))) : is_greatest (specified_set N) M := ⟨⟨fib K, fib (K+1), by simp [HM], H⟩, λ k h, solution_bound HK HM h⟩ -end +end imo1981_q3 + +open imo1981_q3 /- Now we just have to demonstrate that 987 and 1597 are in fact the largest Fibonacci diff --git a/archive/leanpkg.toml b/archive/leanpkg.toml new file mode 100644 index 0000000000000..a89c0e895b5f7 --- /dev/null +++ b/archive/leanpkg.toml @@ -0,0 +1,7 @@ +[package] +name = "mathlib-archive" +version = "0.1" +path = "." + +[dependencies] +mathlib = {path = ".."} diff --git a/counterexamples/homogeneous_prime_not_prime.lean b/counterexamples/homogeneous_prime_not_prime.lean index 8b9f1a9328952..8692774542313 100644 --- a/counterexamples/homogeneous_prime_not_prime.lean +++ b/counterexamples/homogeneous_prime_not_prime.lean @@ -74,7 +74,7 @@ lemma grading.mul_mem : ∀ ⦃i j : two⦄ {a b : (R × R)} (ha : a ∈ grading end -notation `R` := zmod 4 +local notation `R` := zmod 4 /-- `R² ≅ {(a, a) | a ∈ R} ⨁ {(0, b) | b ∈ R}` by `(x, y) ↦ (x, x) + (0, y - x)`. -/ def grading.decompose : (R × R) →+ direct_sum two (λ i, grading R i) := diff --git a/counterexamples/leanpkg.toml b/counterexamples/leanpkg.toml new file mode 100644 index 0000000000000..814d73c4e45c1 --- /dev/null +++ b/counterexamples/leanpkg.toml @@ -0,0 +1,7 @@ +[package] +name = "mathlib-counterexamples" +version = "0.1" +path = "." + +[dependencies] +mathlib = {path = ".."} diff --git a/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean b/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean index 28298a847d2cc..6e08c5f9f847f 100644 --- a/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean +++ b/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean @@ -32,7 +32,7 @@ instance inhabited : inhabited foo := ⟨zero⟩ instance : has_zero foo := ⟨zero⟩ instance : has_one foo := ⟨one⟩ -notation `ε` := eps +local notation `ε` := eps /-- The order on `foo` is the one induced by the natural order on the image of `aux1`. -/ def aux1 : foo → ℕ diff --git a/counterexamples/map_floor.lean b/counterexamples/map_floor.lean index 8c00769a84eaf..b1c262d6d780c 100644 --- a/counterexamples/map_floor.lean +++ b/counterexamples/map_floor.lean @@ -41,9 +41,9 @@ open_locale polynomial /-- The integers with infinitesimals adjoined. -/ @[derive [comm_ring, nontrivial, inhabited]] def int_with_epsilon := ℤ[X] -notation `ℤ[ε]` := int_with_epsilon +local notation `ℤ[ε]` := int_with_epsilon -notation `ε` := (X : ℤ[ε]) +local notation `ε` := (X : ℤ[ε]) namespace int_with_epsilon