chore: bump toolchain to v4.24.0

.github/workflows/lean_lint_suggest.yml

@@ -8,6 +8,6 @@ jobs:
     if: github.repository == 'leanprover/cslib' && github.event.pull_request.draft == false
     runs-on: ubuntu-latest
     steps:
-      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22 (taken from mathlib)
+      - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
         with:
-          mode: suggest
+          mode: suggest

Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean

@@ -19,29 +19,6 @@ universe u v
 
 variable {α : Type u} {β : Type v}
 
--- TODO: These are pieces of API that cannot be directly automated by adding `grind` attributes to
--- `Mathlib.Data.List.Sigma`. We should consider upstreaming them to Mathlib.
-namespace List
-
-variable {β : α → Type v} {l₁ l₂ : List (Sigma β)}
-
-/-- Keys distribute with appending. -/
-theorem keys_append : (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys := by
-  simp [keys]
-
-variable [DecidableEq α] in
-/-- Sublists without duplicate keys preserve lookups. -/
-theorem sublist_dlookup (nd₂ : l₂.NodupKeys) (s : l₁ <+ l₂) (mem : b ∈ l₁.dlookup a) : 
-    b ∈ l₂.dlookup a := by
-  grind [Option.mem_def, → perm_nodupKeys, dlookup_append, => perm_dlookup,
-    → Sublist.exists_perm_append]
-
-@[grind =]
-lemma nodupKeys_middle : (l₁ ++ s :: l₂).NodupKeys ↔ (s :: (l₁ ++ l₂)).NodupKeys := by
-  simp_all [NodupKeys, keys, nodup_middle]
-
-end List
-
 namespace LambdaCalculus.LocallyNameless
 
 variable [DecidableEq α]
@@ -57,7 +34,6 @@ open List
 attribute [scoped grind =] Option.mem_def
 attribute [scoped grind _=_] List.append_eq
 attribute [scoped grind =] List.Nodup
-attribute [scoped grind =] List.NodupKeys
 attribute [scoped grind _=_] List.singleton_append
 
 -- a few grinds on Option:
@@ -68,11 +44,7 @@ attribute [scoped grind =] Option.or_eq_none_iff
 attribute [scoped grind _=_] List.mem_toFinset
 
 -- otherwise, we mostly reuse existing API in `Mathlib.Data.List.Sigma`
-attribute [scoped grind =] List.keys_cons
-attribute [scoped grind =] List.dlookup_cons_eq
-attribute [scoped grind =] List.dlookup_cons_ne
-attribute [scoped grind =] List.dlookup_nil
-attribute [scoped grind _=_] List.dlookup_isSome
+attribute [scoped grind =] List.nodupKeys_middle
 attribute [scoped grind →] List.perm_nodupKeys
 
 /-- The domain of a context is the finite set of free variables it uses. -/
@@ -88,12 +60,6 @@ theorem haswellformed_def (Γ : Context α β) : Γ✓ = Γ.NodupKeys := by rfl
 
 variable {Γ Δ : Context α β}
 
-omit [DecidableEq α] in
-/-- Context well-formedness is preserved on removing an element. -/
-@[scoped grind →]
-theorem wf_strengthen (ok : (Δ ++ ⟨x, σ⟩ :: Γ)✓) : (Δ ++ Γ)✓ := by
-  grind [keys_append]
-
 /-- A mapping of values within a context. -/
 @[simp, scoped grind]
 def map_val (f : β → β) (Γ : Context α β) : Context α β := 
@@ -102,8 +68,8 @@ def map_val (f : β → β) (Γ : Context α β) : Context α β :=
 omit [DecidableEq α] in
 /-- A mapping of values preserves keys. -/
 @[scoped grind]
-lemma map_val_keys (f) : Γ.keys = (Γ.map_val f).keys := by
-  induction Γ <;> grind
+lemma map_val_keys (f) : (Γ.map_val f).keys = Γ.keys :=
+  map₂_keys (f := fun _ => f) Γ
 
 /-- A mapping of values maps lookups. -/
 lemma map_val_mem (mem : σ ∈ Γ.dlookup x) (f) : f σ ∈ (Γ.map_val f).dlookup x := by

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean

@@ -76,7 +76,9 @@ lemma openRec_neq_eq {σ τ γ : Ty Var} (neq : X ≠ Y) (h : σ⟦Y ↝ τ⟧
 
 /-- A locally closed type is unchanged by opening. -/
 lemma openRec_lc {σ τ : Ty Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ᵞ := by
-  induction lc generalizing X <;> (have := fresh_exists <| free_union Var; grind [openRec_neq_eq])
+  induction lc generalizing X with
+  | all => have := fresh_exists <| free_union Var; grind [openRec_neq_eq]
+  | _ => grind
 
 omit [HasFresh Var] in
 @[scoped grind _=_]

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean

@@ -66,7 +66,7 @@ lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ
   induction sub generalizing Γ 
   case all => 
     subst eq
-    apply all (free_union [Context.dom] Var) <;> grind [keys_append]
+    apply all (free_union [Context.dom] Var) <;> grind
   all_goals grind [Ty.Wf.weaken, <= sublist_dlookup]
 
 lemma weaken_head (sub : Sub Δ σ σ') (wf : (Γ ++ Δ).Wf) : Sub (Γ ++ Δ) σ σ' := by
@@ -80,11 +80,10 @@ lemma narrow_aux
   generalize eq : Γ ++ ⟨X, Binding.sub δ⟩ :: Δ = Θ at sub₁ 
   induction sub₁ generalizing Γ δ
   case trans_tvar σ _ σ' X' mem sub ih => 
+    subst eq
     have p : ∀ δ, Γ ++ ⟨X, Binding.sub δ⟩ :: Δ ~ ⟨X, Binding.sub δ⟩ :: (Γ ++ Δ) := 
       by grind [perm_middle]
-    have := perm_dlookup (p := p δ')
-    have := perm_dlookup (p := p δ)
-    grind [Sub.weaken, sublist_append_of_sublist_right]
+    by_cases X = X' <;> grind [Sub.weaken, sublist_append_of_sublist_right]
   case all => apply Sub.all (free_union Var) <;> grind
   all_goals grind [Env.Wf.narrow, Ty.Wf.narrow]
 
@@ -141,17 +140,17 @@ lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub
     have : .sub σ ∈ dlookup X' (⟨X, .sub δ'⟩ :: (Γ ++ Δ)) := by grind [perm_dlookup]
     have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var))
     by_cases X = X'
-    · trans δ' <;> grind [→ mem_dlookup, Ty.subst_fresh, Ty.Wf.nmem_fv, weaken_head, keys_append]
-    · grind [keys_append]
+    · trans δ' <;> grind [→ mem_dlookup, Ty.subst_fresh, Ty.Wf.nmem_fv, weaken_head]
+    · grind
   all_goals
-    grind [Env.Wf.to_ok, keys_append, Sub.refl, Env.Wf.map_subst, Ty.Wf.map_subst]
+    grind [Env.Wf.to_ok, Sub.refl, Env.Wf.map_subst, Ty.Wf.map_subst]
 
 /-- Strengthening of subtypes. -/
 lemma strengthen (sub : Sub (Γ ++ ⟨X, Binding.ty δ⟩ :: Δ) σ τ) :  Sub (Γ ++ Δ) σ τ := by
   generalize eq : Γ ++ ⟨X, Binding.ty δ⟩ :: Δ = Θ at sub
   induction sub generalizing Γ 
   case all => apply Sub.all (free_union Var) <;> grind
-  all_goals grind [to_ok, Wf.strengthen, Env.Wf.strengthen, dlookup_append]
+  all_goals grind [to_ok, Wf.strengthen, Env.Wf.strengthen]
 
 end Sub
 

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean

@@ -135,7 +135,7 @@ lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub :
     have : Γ ++ ⟨X, .sub δ'⟩ :: Δ ~ ⟨X, .sub δ'⟩ :: (Γ ++ Δ) := perm_middle
     have : .ty σ ∈ dlookup X' (⟨X, .sub δ'⟩ :: (Γ ++ Δ)) := by grind [perm_dlookup]
     have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var))
-    grind [Env.Wf.map_subst, keys_append, → notMem_keys_of_nodupKeys_cons]
+    grind [Env.Wf.map_subst, → notMem_keys_of_nodupKeys_cons]
   case abs => 
     apply abs (free_union [Ty.fv] Var)
     grind [Ty.subst_fresh, open_tm_subst_ty_var]

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean

@@ -76,7 +76,7 @@ theorem perm_env (wf : σ.Wf Γ) (perm : Γ ~ Δ) (ok_Γ : Γ✓) (ok_Δ : Δ✓
 theorem weaken (wf_ΓΘ : σ.Wf (Γ ++ Θ)) (ok_ΓΔΘ : (Γ ++ Δ ++ Θ)✓) : σ.Wf (Γ ++ Δ ++ Θ) := by
   generalize eq : Γ ++ Θ = ΓΔ at wf_ΓΘ
   induction wf_ΓΘ generalizing Γ
-  case all => apply all ((Γ ++ Δ ++ Θ).dom ∪ free_union Var) <;> grind
+  case all => apply all ((Γ ++ Δ ++ Θ).dom ∪ free_union Var) <;> grind [-keys_append]
   all_goals grind [NodupKeys.sublist, <= sublist_dlookup]
 
 /-- A type remains well-formed under context weakening (at the front). -/
@@ -92,8 +92,8 @@ lemma narrow (wf : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (ok : (Γ ++ ⟨
     σ.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by
   generalize eq : (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ) = Θ at wf
   induction wf generalizing Γ with
-  | all => apply all (free_union [dom] Var) <;> grind [nodupKeys_cons, keys_append]
-  | _ => grind [sublist_dlookup, dlookup_append]
+  | all => apply all (free_union [dom] Var) <;> grind [nodupKeys_cons]
+  | _ => grind [sublist_dlookup]
 
 lemma narrow_cons (wf : σ.Wf (⟨X, Binding.sub τ⟩ :: Δ)) (ok : (⟨X, Binding.sub τ'⟩ :: Δ)✓) :
     σ.Wf (⟨X, Binding.sub τ'⟩ :: Δ) := by
@@ -105,7 +105,7 @@ lemma strengthen (wf : σ.Wf (Γ ++ ⟨X, Binding.ty τ⟩ :: Δ)) : σ.Wf (Γ +
   generalize eq : Γ ++ ⟨X, Binding.ty τ⟩ :: Δ = Θ at wf
   induction wf generalizing Γ with
   | all => apply all (free_union [Context.dom] Var) <;> grind
-  | _ => grind [dlookup_append]
+  | _ => grind
 
 variable [HasFresh Var] in
 /-- A type remains well-formed under context substitution (of a well-formed type). -/
@@ -119,9 +119,9 @@ lemma map_subst (wf_σ : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' :
     apply all (free_union [dom] Var)
     · grind
     · intro X' _
-      have : (map_val (·[X:=τ']) (⟨X', Binding.sub γ⟩ :: Γ) ++ Δ)✓ := by grind [keys_append]
+      have : (map_val (·[X:=τ']) (⟨X', Binding.sub γ⟩ :: Γ) ++ Δ)✓ := by grind
       grind [open_subst_var]
-  all_goals grind [weaken_head, dlookup_append]
+  all_goals grind [weaken_head]
 
 variable [HasFresh Var] in
 /-- A type remains well-formed under opening (to a well-formed type). -/
@@ -150,7 +150,7 @@ variable [HasFresh Var] in
 lemma nmem_fv {σ : Ty Var} (wf : σ.Wf Γ) (nmem : X ∉ Γ.dom) : X ∉ σ.fv := by
   induction wf with
   | all => have := fresh_exists <| free_union [dom] Var; grind [nmem_fv_open, openRec_lc]
-  | _ => grind
+  | _ => grind [dlookup_isSome]
 
 end Ty.Wf
 
@@ -162,19 +162,19 @@ open Context List Binding
 lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) : 
     Env.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by
   induction Γ <;> cases wf_env <;> 
-  grind [Ty.Wf.narrow, keys_append, eq_nil_of_append_eq_nil, cases Env.Wf]
+  grind [Ty.Wf.narrow, eq_nil_of_append_eq_nil, cases Env.Wf]
 
 /-- A context remains well-formed under strengthening. -/
 lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by
-  induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen, keys_append]
+  induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen]
 
 variable [HasFresh Var] in
 /-- A context remains well-formed under substitution (of a well-formed type). -/
 lemma map_subst (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) :
     Env.Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by
   induction Γ generalizing wf_τ' Δ τ' <;> cases wf_env
   case nil => grind
-  case cons.sub | cons.ty => constructor <;> grind [Ty.Wf.map_subst, keys_append]
+  case cons.sub | cons.ty => constructor <;> grind [Ty.Wf.map_subst]
 
 variable [HasFresh Var]
 

Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean

@@ -159,7 +159,7 @@ initialize_simps_projections Fact (carrier → coe)
 
 lemma Fact.eq (G : Fact P) : G = (G : Set P)⫠⫠ := G.property
 
-@[scoped grind =, simp] lemma mem_dual {G : Fact P} : p ∈ G⫠ ↔ ∀ q ∈ G, p * q ∈ PhaseSpace.bot := 
+@[scoped grind =, simp] lemma mem_dual {G : Fact P} : p ∈ G⫠ ↔ ∀ q ∈ G, p * q ∈ PhaseSpace.bot :=
   Iff.rfl
 
 @[scoped grind =>]

docs/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0-rc1
+leanprover/lean4:v4.24.0

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eed770a434957369c6262aa3fb1d6426419016d4",
+   "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.24.0-rc1",
+   "inputRev": "v4.24.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c205f530395b57b520d3d78d975293f0c69b65ce",
+   "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,37 +35,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a564b9c2252afef6e0d40613d4ec086b54ffe7df",
+   "rev": "d768126816be17600904726ca7976b185786e6b9",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "557f2069977de1c95e68de09e693bc4d1eee7842",
+   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.72-pre",
+   "inputRev": "v0.0.74",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fc97e592e3e150370f17a12e3613e96252c4d3d0",
+   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "345a958916d27982d4ecb4500fba0ebb21096651",
+   "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,17 +75,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b3a8bc5f8b72102ebbe4da3302432b196e215522",
+   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386",
+   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -6,11 +6,16 @@ testDriver = "CslibTests"
 [leanOptions]
 weak.linter.mathlibStandardSet = true
 weak.linter.flexible = true
+# The next three linters are provided by Mathlib, but don't work here.
+# This should be fixed, see discussion at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weak.2Elinter.2EmathlibStandardSet.20and.20lint-style-action/with/544726745
+weak.linter.pythonStyle = false
+weak.linter.checkInitImports = false
+weak.linter.allScriptsDocumented = false
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.24.0-rc1"
+rev = "v4.24.0"
 
 [[lean_lib]]
 name = "Cslib"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0-rc1
+leanprover/lean4:v4.24.0