From 26a8ffe7fa5c16c826773e520be4a774baba0ee5 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Wed, 2 Oct 2024 10:38:06 +0000 Subject: [PATCH] Update to Lean 4.11.0 The changes to the five files: * `putnam_1965_a5.lean` * `putnam_1985_b1.lean` * `putnam_1994_a6.lean` * `putnam_2011_b6.lean` * `putnam_2016_b2.lean` are fixes to account for the fact that Lean now tries to interpret certain expressions of the form `{ ... }.ncard` using `Finset.ncard` (which does not exist) rather than `Set.ncard`. Similar remarks for `Set.encard`. I have changed these to use `Finset.card`. --- lean4/check_docstrings.lean | 1 - lean4/lake-manifest.json | 16 ++++++++-------- lean4/lakefile.lean | 2 +- lean4/lean-toolchain | 2 +- lean4/src/putnam_1965_a5.lean | 2 +- lean4/src/putnam_1985_b1.lean | 2 +- lean4/src/putnam_1994_a6.lean | 4 ++-- lean4/src/putnam_2011_b6.lean | 2 +- lean4/src/putnam_2016_b2.lean | 4 ++-- 9 files changed, 17 insertions(+), 18 deletions(-) diff --git a/lean4/check_docstrings.lean b/lean4/check_docstrings.lean index dba487fb..3fafca70 100644 --- a/lean4/check_docstrings.lean +++ b/lean4/check_docstrings.lean @@ -1,6 +1,5 @@ import Mathlib.Lean.CoreM import Mathlib.Util.GetAllModules -import Batteries.Lean.Util.Path import Lean.Elab.Frontend import Batteries.Data.String.Matcher diff --git a/lean4/lake-manifest.json b/lean4/lake-manifest.json index f22bba95..be7a964b 100644 --- a/lean4/lake-manifest.json +++ b/lean4/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0", + "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5", + "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "209712c78b16c795453b6da7f7adbda4589a8f21", + "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c87908619cccadda23f71262e6898b9893bffa36", + "rev": "a96aee5245720f588876021b6a0aa73efee49c76", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.40", + "inputRev": "v0.0.41", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "543725b3bfed792097fc134adca628406f6145f5", + "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a719ba5c3115d47b68bf0497a9dd1bcbb21ea663", + "rev": "20c73142afa995ac9c8fb80a9bb585a55ca38308", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.10.0", + "inputRev": "v4.11.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "putnam", diff --git a/lean4/lakefile.lean b/lean4/lakefile.lean index b7f534f8..ed2b66aa 100644 --- a/lean4/lakefile.lean +++ b/lean4/lakefile.lean @@ -6,7 +6,7 @@ package «putnam» where leanOptions := #[ ⟨`autoImplicit, false⟩ ] -require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.10.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.11.0" @[default_target] lean_lib «putnam» where diff --git a/lean4/lean-toolchain b/lean4/lean-toolchain index 7f0ea50a..5a9c76dc 100644 --- a/lean4/lean-toolchain +++ b/lean4/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0 +leanprover/lean4:v4.11.0 diff --git a/lean4/src/putnam_1965_a5.lean b/lean4/src/putnam_1965_a5.lean index 303a9c60..6c99a86c 100644 --- a/lean4/src/putnam_1965_a5.lean +++ b/lean4/src/putnam_1965_a5.lean @@ -9,5 +9,5 @@ abbrev putnam_1965_a5_solution : ℕ → ℕ := sorry How many orderings of the integers from $1$ to $n$ satisfy the condition that, for every integer $i$ except the first, there exists some earlier integer in the ordering which differs from $i$ by $1$? -/ theorem putnam_1965_a5 -: ∀ n > 0, {p ∈ permsOfFinset (Finset.Icc 1 n) | ∀ m ∈ Finset.Icc 2 n, ∃ k ∈ Finset.Ico 1 m, p m = p k + 1 ∨ p m = p k - 1}.ncard = putnam_1965_a5_solution n := +: ∀ n > 0, {p ∈ permsOfFinset (Finset.Icc 1 n) | ∀ m ∈ Finset.Icc 2 n, ∃ k ∈ Finset.Ico 1 m, p m = p k + 1 ∨ p m = p k - 1}.card = putnam_1965_a5_solution n := sorry diff --git a/lean4/src/putnam_1985_b1.lean b/lean4/src/putnam_1985_b1.lean index c3533d52..e23c5a3e 100644 --- a/lean4/src/putnam_1985_b1.lean +++ b/lean4/src/putnam_1985_b1.lean @@ -16,6 +16,6 @@ theorem putnam_1985_b1 (p : (Fin 5 → ℤ) → (Polynomial ℝ)) (hp : p = fun m ↦ ∏ i : Fin 5, ((X : Polynomial ℝ) - m i)) (numnzcoeff : Polynomial ℝ → ℕ) -(hnumnzcoeff : numnzcoeff = fun p ↦ {j ∈ Finset.range (p.natDegree + 1) | coeff p j ≠ 0}.ncard) +(hnumnzcoeff : numnzcoeff = fun p ↦ {j ∈ Finset.range (p.natDegree + 1) | coeff p j ≠ 0}.card) : (Injective putnam_1985_b1_solution ∧ ∀ m : Fin 5 → ℤ, Injective m → numnzcoeff (p putnam_1985_b1_solution) ≤ numnzcoeff (p m)) := sorry diff --git a/lean4/src/putnam_1994_a6.lean b/lean4/src/putnam_1994_a6.lean index 9d34259d..f1982454 100644 --- a/lean4/src/putnam_1994_a6.lean +++ b/lean4/src/putnam_1994_a6.lean @@ -1,7 +1,7 @@ import Mathlib open BigOperators -open Filter Topology +open Classical Filter Topology -- Note: uses (ℕ → Fin 10) instead of (Fin m → Fin 10) /-- @@ -14,5 +14,5 @@ theorem putnam_1994_a6 (hf: ∀ n : ℤ, ∃ m : ℕ, ∃ i : ℕ → Fin 10, m ≥ 1 ∧ (mijcomp m i 0) 0 = n) (hmijcomp : ∀ m ≥ 1, ∀ (i : ℕ → Fin 10) (j : Fin m), mijcomp m i j = if (j = m - 1) then (f (i j) : ℤ → ℤ) else (f (i j) ∘ mijcomp m i (j + 1))) (hF : F = {g : ℤ → ℤ | ∃ e : Fin 10 → Fin 2, g = (f 0)^[e 0] ∘ (f 1)^[e 1] ∘ (f 2)^[e 2] ∘ (f 3)^[e 3] ∘ (f 4)^[e 4] ∘ (f 5)^[e 5] ∘ (f 6)^[e 6] ∘ (f 7)^[e 7] ∘ (f 8)^[e 8] ∘ (f 9)^[e 9]}) -: ∀ A : Finset ℤ, A.Nonempty → {g ∈ F | g '' A = A}.encard ≤ 512 := +: ∀ A : Finset ℤ, A.Nonempty → {g ∈ F | g '' A = A}.card ≤ 512 := sorry diff --git a/lean4/src/putnam_2011_b6.lean b/lean4/src/putnam_2011_b6.lean index 039cee6e..7c79d24d 100644 --- a/lean4/src/putnam_2011_b6.lean +++ b/lean4/src/putnam_2011_b6.lean @@ -12,5 +12,5 @@ Let $p$ be an odd prime. Show that for at least $(p+1)/2$ values of $n$ in $\{0, theorem putnam_2011_b6 (p : ℕ) (hp : Odd p ∧ Nat.Prime p) -: {n ∈ Finset.range p | ¬ p ∣ ∑ k : Finset.range p, Nat.factorial k * n^(k : ℕ)}.ncard ≥ (p + 1)/2 := +: {n ∈ Finset.range p | ¬ p ∣ ∑ k : Finset.range p, Nat.factorial k * n^(k : ℕ)}.card ≥ (p + 1)/2 := sorry diff --git a/lean4/src/putnam_2016_b2.lean b/lean4/src/putnam_2016_b2.lean index eac214c7..7d42b51c 100644 --- a/lean4/src/putnam_2016_b2.lean +++ b/lean4/src/putnam_2016_b2.lean @@ -1,7 +1,7 @@ import Mathlib open BigOperators -open Polynomial Filter Topology Real Set Nat List +open Classical Polynomial Filter Topology Real Set Nat List noncomputable abbrev putnam_2016_b2_solution : ℝ × ℝ := sorry -- (3 / 4, 4 / 3) @@ -19,7 +19,7 @@ theorem putnam_2016_b2 (squarish : ℤ → Prop) (hsquarish : squarish = fun n ↦ IsSquare n ∨ ∃ w : ℤ, IsSquare |n - w ^ 2| ∧ ∀ v : ℕ, |n - w ^ 2| ≤ |n - v ^ 2|) (S : ℤ → ℕ) -(hS : S = fun n ↦ {i ∈ Finset.Icc 1 n | squarish i}.ncard) +(hS : S = fun n ↦ {i ∈ Finset.Icc 1 n | squarish i}.card) (p : ℝ → ℝ → Prop) (hp : p = fun α ↦ fun β ↦ α > 0 ∧ β > 0 ∧ Tendsto (fun N ↦ S N / (N : ℝ) ^ α) atTop (𝓝 β)) : ((∀ α β : ℝ, ((α, β) = putnam_2016_b2_solution ↔ p α β)) ∨ ¬∃ α β : ℝ, p α β) :=