Merge pull request #199 from eric-wieser/lean-updates

Update to Lean 4.10.0
trishullab · Aug 17, 2024 · 1681549 · 1681549
2 parents 991ae20 + cf8d5d5
commit 1681549
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 27 deletions.
diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json
@@ -1,19 +1,21 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
+   "scope": "leanprover-community",
+   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "scope": "leanprover-community",
+   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,46 +24,51 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "scope": "leanprover-community",
+   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "scope": "leanprover-community",
+   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.40",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "scope": "leanprover-community",
+   "rev": "543725b3bfed792097fc134adca628406f6145f5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "a45ae63747140c1b2cbad9d46f518015c047047a",
+   "scope": "",
+   "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.10.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "putnam",

diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean
@@ -3,7 +3,7 @@ open Lake DSL
 
 package «putnam» where
   -- add package configuration options here
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.7.0"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.10.0"
 
 @[default_target]
 lean_lib «putnam» where

diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.10.0
diff --git a/lean4/src/putnam_2001_a5.lean b/lean4/src/putnam_2001_a5.lean
@@ -4,5 +4,5 @@ open BigOperators
 open Topology Filter Polynomial Set
 
 theorem putnam_2001_a5
-: ∃! (a : ℤ) (n : ℕ), a > 0 ∧ n > 0 ∧ a^(n+1) - (a+1)^n = 2001 :=
+: ∃! an : ℤ × ℕ, let (a, n) := an; a > 0 ∧ n > 0 ∧ a^(n+1) - (a+1)^n = 2001 :=
 sorry
diff --git a/lean4/src/putnam_2018_b1.lean b/lean4/src/putnam_2018_b1.lean
@@ -1,17 +1,17 @@
 import Mathlib
 open BigOperators
 
-abbrev putnam_2018_b1_solution : Set (Vector ℤ 2) := sorry
--- {v : Vector ℤ 2 | ∃ b : ℤ, 0 ≤ b ∧ b ≤ 100 ∧ Even b ∧ v.toList = [1, b]}
+abbrev putnam_2018_b1_solution : Set (Mathlib.Vector ℤ 2) := sorry
+-- {v : Mathlib.Vector ℤ 2 | ∃ b : ℤ, 0 ≤ b ∧ b ≤ 100 ∧ Even b ∧ v.toList = [1, b]}
 theorem putnam_2018_b1
-(P : Finset (Vector ℤ 2))
-(v : Vector ℤ 2)
+(P : Finset (Mathlib.Vector ℤ 2))
+(v : Mathlib.Vector ℤ 2)
 (vinP : Prop)
-(Pvdiff : Finset (Vector ℤ 2))
+(Pvdiff : Finset (Mathlib.Vector ℤ 2))
 (Pvpart : Prop)
-(hP : P = {v' : Vector ℤ 2 | 0 ≤ v'[0] ∧ v'[0] ≤ 2 ∧ 0 ≤ v'[1] ∧ v'[1] ≤ 100})
+(hP : P = {v' : Mathlib.Vector ℤ 2 | 0 ≤ v'[0] ∧ v'[0] ≤ 2 ∧ 0 ≤ v'[1] ∧ v'[1] ≤ 100})
 (hvinP : vinP = (v ∈ P))
-(hPvdiff : Pvdiff = P \ ({v} : Finset (Vector ℤ 2)))
-(hPvpart : Pvpart = (∃ Q R : Finset (Vector ℤ 2), (Q ∪ R = Pvdiff) ∧ (Q ∩ R = ∅) ∧ (Q.card = R.card) ∧ (∑ q in Q, q[0] = ∑ r in R, r[0]) ∧ (∑ q in Q, q[1] = ∑ r in R, r[1])))
+(hPvdiff : Pvdiff = P \ ({v} : Finset (Mathlib.Vector ℤ 2)))
+(hPvpart : Pvpart = (∃ Q R : Finset (Mathlib.Vector ℤ 2), (Q ∪ R = Pvdiff) ∧ (Q ∩ R = ∅) ∧ (Q.card = R.card) ∧ (∑ q in Q, q[0] = ∑ r in R, r[0]) ∧ (∑ q in Q, q[1] = ∑ r in R, r[1])))
 : (vinP ∧ Pvpart) ↔ v ∈ putnam_2018_b1_solution :=
 sorry