chore: Bump to v4.18.0-rc1

2025-03-20 12:56:28 -04:00 · 2025-03-20 12:56:28 -04:00 · 812440c812
commit 812440c812
parent a662754b34
8 changed files with 35 additions and 34 deletions
--- a/PhysLean/Mathematics/List.lean
+++ b/PhysLean/Mathematics/List.lean
@ -63,10 +63,10 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
  | [], _, h => by
    simp
  | a :: [], 0, h => by
-    simp only [List.dropWhile, nonpos_iff_eq_zero, List.length_eq_zero, List.takeWhile_eq_nil_iff,
-      List.length_singleton, zero_lt_one, Fin.zero_eta, Fin.isValue, List.get_eq_getElem,
-      Fin.val_eq_zero, List.getElem_cons_zero, decide_eq_true_eq, forall_const, zero_le,
-      Nat.sub_eq_zero_of_le, List.eraseIdx_zero, ite_not, List.nil_eq]
+    simp only [List.eraseIdx_zero, nonpos_iff_eq_zero, List.length_eq_zero_iff,
+      List.takeWhile_eq_nil_iff, List.length_singleton, zero_lt_one, Fin.zero_eta, Fin.isValue,
+      List.get_eq_getElem, Fin.val_eq_zero, List.getElem_cons_zero, decide_eq_true_eq, forall_const,
+      List.dropWhile, zero_le, Nat.sub_eq_zero_of_le, ite_not]
    simp_all only [List.length_cons, List.length_nil, List.get_eq_getElem, Fin.val_eq_zero,
      List.getElem_cons_zero, implies_true, List.tail_cons, List.dropWhile_nil, decide_true,
      decide_false, ite_self]
@ -86,17 +86,17 @@ lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
        zero_le, ↓reduceIte, tsub_zero, List.eraseIdx_cons_succ, List.eraseIdx_nil]
    exact Nat.le_add_left [a].length n
  | a :: b :: l, 0, h => by
-    simp only [List.dropWhile, List.takeWhile, nonpos_iff_eq_zero, List.length_eq_zero, zero_le,
+    simp only [List.dropWhile, List.takeWhile, nonpos_iff_eq_zero, List.length_eq_zero_iff, zero_le,
      Nat.sub_eq_zero_of_le, List.eraseIdx_zero]
    by_cases hPb : P b
    · have hPa : P a := by
        simpa using h ⟨0, by simp⟩ ⟨1, by simp⟩ (by simp [Fin.lt_def]) (by simpa using hPb)
      simp [hPb, hPa]
-    · simp only [hPb, decide_false, nonpos_iff_eq_zero, List.length_eq_zero]
+    · simp only [hPb, decide_false, nonpos_iff_eq_zero, List.length_eq_zero_iff]
      simp_all only [List.length_cons, List.get_eq_getElem]
      simp_rw [decide_false]
      simp_all only [List.tail_cons, decide_false, Bool.false_eq_true, not_false_eq_true,
-        List.dropWhile_cons_of_neg, nonpos_iff_eq_zero, List.length_eq_zero]
+        List.dropWhile_cons_of_neg, nonpos_iff_eq_zero, List.length_eq_zero_iff]
      split
      next x heq =>
        simp_all only [decide_eq_true_eq, List.length_singleton, nonpos_iff_eq_zero, one_ne_zero,
@ -579,7 +579,7 @@ lemma orderedInsert_eq_insertIdx_orderedInsertPos {I : Type} (le1 : I → I →
      erw [List.getElem_insertIdx_of_lt]
      exact hn'
    · simp only [hn', ↓reduceIte]
-      rw [List.getElem_insertIdx_of_ge]
+      rw [List.getElem_insertIdx_of_gt]
      · rfl
      · omega

--- a/PhysLean/Mathematics/List/InsertionSort.lean
+++ b/PhysLean/Mathematics/List/InsertionSort.lean
@ -196,7 +196,7 @@ lemma takeWhile_orderedInsert' {α : Type} (r : α → α → Prop) [DecidableRe
    (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a l)).length =
    (List.takeWhile (fun c => !decide (r b c)) l).length
  | [] => by
-    simp only [List.orderedInsert, List.takeWhile_nil, List.length_nil, List.length_eq_zero,
+    simp only [List.orderedInsert, List.takeWhile_nil, List.length_nil, List.length_eq_zero_iff,
      List.takeWhile_eq_nil_iff, List.length_singleton, zero_lt_one, Fin.zero_eta, Fin.isValue,
      List.get_eq_getElem, Fin.val_eq_zero, List.getElem_cons_zero, Bool.not_eq_eq_eq_not,
      Bool.not_true, decide_eq_false_iff_not, Decidable.not_not, forall_const]
@ -209,7 +209,8 @@ lemma takeWhile_orderedInsert' {α : Type} (r : α → α → Prop) [DecidableRe
    simp only [List.orderedInsert]
    by_cases h : r b c
    · simp only [h, decide_true, Bool.not_true, Bool.false_eq_true, not_false_eq_true,
-      List.takeWhile_cons_of_neg, List.length_nil, List.length_eq_zero, List.takeWhile_eq_nil_iff,
+      List.takeWhile_cons_of_neg, List.length_nil, List.length_eq_zero_iff,
+      List.takeWhile_eq_nil_iff,
      List.get_eq_getElem, Bool.not_eq_eq_eq_not, decide_eq_false_iff_not, Decidable.not_not]
      by_cases hac : r a c
      · simp [hac, hrba]
--- a/PhysLean/Meta/TransverseTactics.lean
+++ b/PhysLean/Meta/TransverseTactics.lean
@ -81,7 +81,7 @@ open transverseTactics in
 /-- Applies `visitTacticInfo` to each tactic in a file. -/
 unsafe def transverseTactics (file : FilePath)
  (visitTacticInfo : FilePath → ContextInfo → TacticInfo → MetaM Unit) : IO Unit := do
-  searchPathRef.set compile_time_search_path%
+  initSearchPath (← findSysroot)
  /- This is equivalent to `(IO.FS.readFile file).bind (fun fileContent => do ...)`. -/
  let fileContent ← IO.FS.readFile file
  enableInitializersExecution
--- a/PhysLean/QFT/PerturbationTheory/FieldSpecification/TimeOrder.lean
+++ b/PhysLean/QFT/PerturbationTheory/FieldSpecification/TimeOrder.lean
@ -293,7 +293,7 @@ lemma orderedInsert_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp}
    List.takeWhile_cons_of_neg, List.append_nil, List.append_cancel_left_eq, List.cons.injEq,
    true_and]
  rw [List.dropWhile_append]
-  simp only [List.isEmpty_eq_true, List.dropWhile_eq_nil_iff, Bool.not_eq_eq_eq_not, Bool.not_true,
+  simp only [List.isEmpty_iff, List.dropWhile_eq_nil_iff, Bool.not_eq_eq_eq_not, Bool.not_true,
    decide_eq_false_iff_not, crAnTimeOrderRel_refl, decide_true, Bool.false_eq_true,
    not_false_eq_true, List.dropWhile_cons_of_neg, ite_eq_left_iff, not_forall, Classical.not_imp,
    Decidable.not_not, List.append_left_eq_self, forall_exists_index, and_imp]
--- a/README.md
+++ b/README.md
@ -7,7 +7,7 @@
 [![](https://img.shields.io/badge/Informal_dependencies-Graph-green)](https://heplean.com/InformalGraph)

 [![](https://img.shields.io/badge/View_The-Stats-blue)](https://heplean.com/Stats)
-[![](https://img.shields.io/badge/Lean-v4.17.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.17.0)
+[![](https://img.shields.io/badge/Lean-v4.18.0--rc1-blue)](https://github.com/leanprover/lean4/releases/tag/v4.18.0)
 [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/HEPLean/HepLean)

 A project to digitalize physics.
@ -60,8 +60,8 @@ How HepLean was used: *Theorems from the space-time files of HepLean were includ

 ## Contributing

-We would love to have you involved! See the [Get Involved](https://heplean.com/GetInvolved.html) page to see how you can get involved. 
-Any contributions are welcome! If you have any questions or want permission  permission to create a pull-request for this 
+We would love to have you involved! See the [Get Involved](https://heplean.com/GetInvolved.html) page to see how you can get involved.
+Any contributions are welcome! If you have any questions or want permission  permission to create a pull-request for this
 repository contact Joseph Tooby-Smith on the [Lean Zulip](https://leanprover.zulipchat.com), or email.

 ## Installation
--- a/lake-manifest.json
+++ b/lake-manifest.json
@ -5,47 +5,47 @@
   "type": "git",
   "subDir": null,
   "scope": "",
-   "rev": "b031cb6aa39c6db80532975c43594f247b8d4b51",
+   "rev": "1b489cdbe4bc57a6acdddb9a5dc5699acacdecdd",
   "name": "«doc-gen4»",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.17.0",
+   "inputRev": "v4.18.0-rc1",
   "inherited": false,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/mathlib4.git",
   "type": "git",
   "subDir": null,
   "scope": "",
-   "rev": "5269898d6a51d047931107c8d72d934d8d5d3753",
+   "rev": "6cecf71a82a22ea7c01598800e12f3e8eb66894b",
   "name": "mathlib",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.17.0",
+   "inputRev": "v4.18.0-rc1",
   "inherited": false,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/mhuisi/lean4-cli",
   "type": "git",
   "subDir": null,
   "scope": "",
-   "rev": "c53b3371dd0fe5f3dd75a2df543c3550e246465a",
+   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
   "name": "Cli",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+  {"url": "https://github.com/jcommelin/lean4-unicode-basic",
   "type": "git",
   "subDir": null,
   "scope": "",
-   "rev": "d890360c960358a42965bdc15defa3fd09feba38",
+   "rev": "458e2d3feda3999490987eabee57b8bb88b1949c",
   "name": "UnicodeBasic",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "bump_to_v4.18.0-rc1",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/dupuisf/BibtexQuery",
   "type": "git",
   "subDir": null,
   "scope": "",
-   "rev": "63a4bd4ffa4b67dbd8cf5489a0f01bfdc084602c",
+   "rev": "c07de335d35ed6b118e084ec48cffc39b40d29d2",
   "name": "BibtexQuery",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
@ -65,7 +65,7 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "c708be04267e3e995a14ac0d08b1530579c1525a",
+   "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
   "name": "plausible",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
@ -85,7 +85,7 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30",
+   "rev": "08372f1ec11df288ff76621ead7b0b575cb29355",
   "name": "importGraph",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
@ -95,17 +95,17 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd",
+   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
   "name": "proofwidgets",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.52",
+   "inputRev": "v0.0.53",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/aesop",
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0",
+   "rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
   "name": "aesop",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
@ -115,7 +115,7 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03",
+   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
   "name": "Qq",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
@ -125,7 +125,7 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover-community",
-   "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
+   "rev": "092b30de8e7ee78e96b24c235d99e26f2942d77e",
   "name": "batteries",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
--- a/lakefile.toml
+++ b/lakefile.toml
@ -6,12 +6,12 @@ defaultTargets = ["PhysLean"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.17.0"
+rev = "v4.18.0-rc1"

 [[require]]
 name = "«doc-gen4»"
 git = "https://github.com/leanprover/doc-gen4"
-rev = "v4.17.0"
+rev = "v4.18.0-rc1"

 [[lean_lib]]
 name = "PhysLean"
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0-rc1