From 4f8c3383f126bcb2611d1f3d4f6eb3e6d7a244d9 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 14 Dec 2023 12:49:31 -0700 Subject: [PATCH] Update to lean v4.3.0 --- .gitignore | 1 + Bookshelf/Apostol/Chapter_1_11.lean | 2 +- Bookshelf/Apostol/Chapter_I_03.lean | 2 +- Bookshelf/Enderton/Logic/Chapter_1.lean | 2 +- Bookshelf/Enderton/Set/Chapter_2.lean | 2 +- Bookshelf/Enderton/Set/Chapter_3.lean | 2 +- Bookshelf/Enderton/Set/Chapter_4.lean | 2 +- Bookshelf/Enderton/Set/Chapter_6.lean | 4 +- Common/List/Basic.lean | 2 +- Common/Nat/Basic.lean | 21 +--- Common/Real/Floor.lean | 5 +- lake-manifest.json | 160 +++++++++++++----------- lakefile.lean | 4 +- lean-toolchain | 2 +- 14 files changed, 101 insertions(+), 110 deletions(-) diff --git a/.gitignore b/.gitignore index 5306c36..7a050e4 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,7 @@ lakefile.olean lake-packages _target leanpkg.path +.lake/ # TeX *.aux diff --git a/Bookshelf/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean index c41d6eb..e86fb08 100644 --- a/Bookshelf/Apostol/Chapter_1_11.lean +++ b/Bookshelf/Apostol/Chapter_1_11.lean @@ -50,7 +50,7 @@ theorem exercise_4c (x y : ℝ) : ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ ∨ ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ + 1 := by have hx : x = Int.floor x + Int.fract x := Eq.symm (add_eq_of_eq_sub' rfl) have hy : y = Int.floor y + Int.fract y := Eq.symm (add_eq_of_eq_sub' rfl) - by_cases Int.fract x + Int.fract y < 1 + by_cases h : Int.fract x + Int.fract y < 1 · refine Or.inl ?_ rw [Int.floor_eq_iff] simp only [Int.cast_add] diff --git a/Bookshelf/Apostol/Chapter_I_03.lean b/Bookshelf/Apostol/Chapter_I_03.lean index 2c8fc46..7df8708 100644 --- a/Bookshelf/Apostol/Chapter_I_03.lean +++ b/Bookshelf/Apostol/Chapter_I_03.lean @@ -1,5 +1,5 @@ import Common.Set -import Mathlib.Data.Real.Basic +import Mathlib.Data.Real.Archimedean /-! # Apostol.Chapter_I_03 diff --git a/Bookshelf/Enderton/Logic/Chapter_1.lean b/Bookshelf/Enderton/Logic/Chapter_1.lean index beb9e81..01ed87f 100644 --- a/Bookshelf/Enderton/Logic/Chapter_1.lean +++ b/Bookshelf/Enderton/Logic/Chapter_1.lean @@ -481,7 +481,7 @@ theorem exercise_1_2_2b_iii {k : ℕ} (h : Odd k) exact absurd hr hk unfold σ rw [hn₁] - simp only [Nat.add_eq, add_zero, not_forall, exists_prop, and_true] + simp only [Nat.add_eq, add_zero, imp_false, not_not] exact exercise_1_2_2b_i False Q hn₂ end Exercise_1_2_2 diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean index 848dbab..90cfaad 100644 --- a/Bookshelf/Enderton/Set/Chapter_2.lean +++ b/Bookshelf/Enderton/Set/Chapter_2.lean @@ -616,7 +616,7 @@ lemma right_diff_eq_insert_one_three : A \ (B \ C) = {1, 3} := by rw [hy] at hz unfold Membership.mem Set.instMembershipSet Set.Mem at hz unfold singleton Set.instSingletonSet Set.singleton setOf at hz - simp only at hz + simp at hz · intro hy refine ⟨Or.inr (Or.inr hy), ?_⟩ intro hz diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 47605f5..352e35d 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -542,7 +542,7 @@ theorem exercise_3_1 {x y z u v w : ℕ} · rw [hx, hy, hz, hu, hv, hw] simp · rw [hy, hv] - simp only + simp /-- ### Exercise 3.2a diff --git a/Bookshelf/Enderton/Set/Chapter_4.lean b/Bookshelf/Enderton/Set/Chapter_4.lean index 4d3c6d6..c8c7c43 100644 --- a/Bookshelf/Enderton/Set/Chapter_4.lean +++ b/Bookshelf/Enderton/Set/Chapter_4.lean @@ -702,7 +702,7 @@ theorem exercise_4_17 (m n p : ℕ) | zero => calc m ^ (n + 0) _ = m ^ n := rfl _ = m ^ n * 1 := by rw [right_mul_id] - _ = m ^ n * m ^ 0 := rfl + _ = m ^ n * m ^ 0 := by rfl | succ p ih => calc m ^ (n + p.succ) _ = m ^ (n + p).succ := rfl _ = m ^ (n + p) * m := rfl diff --git a/Bookshelf/Enderton/Set/Chapter_6.lean b/Bookshelf/Enderton/Set/Chapter_6.lean index 2054d2d..44168cb 100644 --- a/Bookshelf/Enderton/Set/Chapter_6.lean +++ b/Bookshelf/Enderton/Set/Chapter_6.lean @@ -512,7 +512,7 @@ theorem corollary_6d_b ] refine ⟨1, ?_⟩ intro x nx - simp only [mul_eq_one, false_and] at nx + simp only [mul_eq_one, OfNat.ofNat_ne_one, false_and] at nx /-- ### Corollary 6E @@ -992,7 +992,7 @@ lemma sdiff_size_aux [DecidableEq α] [Nonempty α] simp only [Set.diff_empty] exact hA rw [this] - refine ⟨trivial, hB', Set.equinumerous_emptyset_emptyset⟩ + refine ⟨by simp, hB', Set.equinumerous_emptyset_emptyset⟩ | succ m ih => /- > #### (ii) diff --git a/Common/List/Basic.lean b/Common/List/Basic.lean index 1fb476a..09b901b 100644 --- a/Common/List/Basic.lean +++ b/Common/List/Basic.lean @@ -162,7 +162,7 @@ theorem length_zipWith_self_tail_eq_length_sub_one rw [length_zipWith] simp only [length_cons, ge_iff_le, min_eq_right_iff] show length as ≤ length as + 1 - simp only [le_add_iff_nonneg_right] + simp only [le_add_iff_nonneg_right, zero_le] /-- The output `List` of a `zipWith` is nonempty **iff** both of its inputs are diff --git a/Common/Nat/Basic.lean b/Common/Nat/Basic.lean index 393c68b..54c5b28 100644 --- a/Common/Nat/Basic.lean +++ b/Common/Nat/Basic.lean @@ -9,23 +9,4 @@ If `n < m⁺`, then `n < m` or `n = m`. theorem lt_or_eq_of_lt {n m : Nat} (h : n < m.succ) : n < m ∨ n = m := lt_or_eq_of_le (lt_succ.mp h) -/-- -The following cancellation law holds for `m`, `n`, and `p` in `ω`: -``` -m ⬝ p = n ⬝ p ∧ p ≠ 0 → m = n -``` --/ -theorem mul_right_cancel (m n p : ℕ) (hp : 0 < p) : m * p = n * p → m = n := by - intro hmn - match @trichotomous ℕ LT.lt _ m n with - | Or.inl h => - have : m * p < n * p := Nat.mul_lt_mul_of_pos_right h hp - rw [hmn] at this - simp at this - | Or.inr (Or.inl h) => exact h - | Or.inr (Or.inr h) => - have : n * p < m * p := Nat.mul_lt_mul_of_pos_right h hp - rw [hmn] at this - simp at this - -end Nat \ No newline at end of file +end Nat diff --git a/Common/Real/Floor.lean b/Common/Real/Floor.lean index 162a67a..52f4a6e 100644 --- a/Common/Real/Floor.lean +++ b/Common/Real/Floor.lean @@ -1,6 +1,5 @@ import Mathlib.Algebra.BigOperators.Basic -import Mathlib.Data.Real.Basic -import Mathlib.Data.Finset.Basic +import Mathlib.Data.Real.Archimedean /-! # Common.Real.Floor @@ -145,4 +144,4 @@ theorem floor_mul_eq_sum_range_floor_add_index_div (n : ℕ) (x : ℝ) -- Close out goal by showing left- and right-hand side equal a common value. rw [hlhs, hrhs] -end Real.Floor \ No newline at end of file +end Real.Floor diff --git a/lake-manifest.json b/lake-manifest.json index b87adbe..fd3b11e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,76 +1,86 @@ -{"version": 6, - "packagesDir": "lake-packages", +{"version": 7, + "packagesDir": ".lake/packages", "packages": - [{"git": - {"url": "https://github.com/mhuisi/lean4-cli", - "subDir?": null, - "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", - "opts": {}, - "name": "Cli", - "inputRev?": "nightly", - "inherited": false}}, - {"git": - {"url": "https://github.com/xubaiw/CMark.lean", - "subDir?": null, - "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", - "opts": {}, - "name": "CMark", - "inputRev?": "main", - "inherited": false}}, - {"git": - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "subDir?": null, - "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71", - "opts": {}, - "name": "UnicodeBasic", - "inputRev?": "main", - "inherited": false}}, - {"git": - {"url": "https://github.com/hargonix/LeanInk", - "subDir?": null, - "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", - "opts": {}, - "name": "leanInk", - "inputRev?": "doc-gen", - "inherited": false}}, - {"git": - {"url": "https://github.com/leanprover-community/mathlib4.git", - "subDir?": null, - "rev": "c97b9b00802c2ed343d9ac73e59be287428dbcf0", - "opts": {}, - "name": "mathlib", - "inputRev?": "master", - "inherited": false}}, - {"git": - {"url": "https://github.com/leanprover/std4.git", - "subDir?": null, - "rev": "87b0742b01e45c6cc53cd3043fe3c7cdbf87a56f", - "opts": {}, - "name": "std", - "inputRev?": "main", - "inherited": false}}, - {"git": - {"url": "https://github.com/leanprover-community/quote4", - "subDir?": null, - "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39", - "opts": {}, - "name": "Qq", - "inputRev?": "master", - "inherited": true}}, - {"git": - {"url": "https://github.com/leanprover-community/aesop", - "subDir?": null, - "rev": "cb87803274405db79ec578fc07c4730c093efb90", - "opts": {}, - "name": "aesop", - "inputRev?": "master", - "inherited": true}}, - {"git": - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "subDir?": null, - "rev": "f1a5c7808b001305ba07d8626f45ee054282f589", - "opts": {}, - "name": "proofwidgets", - "inputRev?": "v0.0.21", - "inherited": true}}], - "name": "bookshelf"} + [{"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/xubaiw/CMark.lean", + "type": "git", + "subDir": null, + "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", + "name": "CMark", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "rev": "dc62b29a26fcc3da545472ab8ad2c98ef3433634", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/hargonix/LeanInk", + "type": "git", + "subDir": null, + "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", + "name": "leanInk", + "manifestFile": "lake-manifest.json", + "inputRev": "doc-gen", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/std4.git", + "type": "git", + "subDir": null, + "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087", + "name": "std", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.3.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.23", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.3.0", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "bookshelf", + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index e1a0b1b..2c2cad2 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -22,10 +22,10 @@ require leanInk from git "doc-gen" require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ - "master" + "v4.3.0" require std from git "https://github.com/leanprover/std4.git" @ - "main" + "v4.3.0" -- ======================================== -- Documentation Generator diff --git a/lean-toolchain b/lean-toolchain index 734efdd..5cadc9d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.3.0-rc1 \ No newline at end of file +leanprover/lean4:v4.3.0