From 65a77968d0abc2d01da92aa8982256855e7519a6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 5 Apr 2024 14:04:25 +0200
Subject: Update the lean toolchain and fix the proofs

---
 backends/lean/Base/Arith/Int.lean             |  1 -
 backends/lean/Base/Diverge.lean               |  1 -
 backends/lean/Base/Diverge/Base.lean          |  4 +---
 backends/lean/Base/Diverge/Elab.lean          |  1 -
 backends/lean/Base/Primitives/ArraySlice.lean |  5 ++---
 backends/lean/Base/Primitives/Range.lean      |  1 -
 backends/lean/Base/Primitives/Vec.lean        |  1 -
 backends/lean/lake-manifest.json              | 16 ++++++++--------
 backends/lean/lean-toolchain                  |  2 +-
 9 files changed, 12 insertions(+), 20 deletions(-)

(limited to 'backends/lean')

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index a57f8bb1..5a85dff0 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -3,7 +3,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 -- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet
 --import Mathlib.Tactic.Omega
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index c9a2eec2..92ffd3cd 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.Diverge.Base
 import Base.Diverge.Elab
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index e40432bd..7521eecc 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
 import Base.Arith.Base
@@ -39,8 +38,7 @@ namespace Lemmas
     case zero =>
       simp_all
       intro m h1 h2
-      have h: n = m := by
-        linarith
+      have h: n = m := by omega
       unfold for_all_fin_aux; simp_all
       simp_all
       -- There is no i s.t. m ≤ i
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index f30148dc..71eaba10 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Base.Utils
 import Base.Diverge.Base
 import Base.Diverge.ElabBase
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index e1a39d40..3bd2aebb 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
@@ -269,7 +268,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
       . scalar_tac
       . scalar_tac
     let na := s_beg.append (s.val.append s_end)
-    have : na.len = a.val.len := by simp [*]
+    have : na.len = a.val.len := by simp [na, *]
     ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
@@ -343,7 +342,7 @@ def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : S
       . scalar_tac
       . scalar_tac
     let ns := s_beg.append (ss.val.append s_end)
-    have : ns.len = s.val.len := by simp [*]
+    have : ns.len = s.val.len := by simp [ns, *]
     ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
diff --git a/backends/lean/Base/Primitives/Range.lean b/backends/lean/Base/Primitives/Range.lean
index a268bcba..416cd201 100644
--- a/backends/lean/Base/Primitives/Range.lean
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 65249c12..2b8425d8 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 3a18466f..99ec856e 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.27",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "056cc4b21e25e8d1daaeef3a6e3416872c9fc12c",
+   "rev": "3e99b48baf21ffdd202d5c2e39990fc23f4c6d32",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index f96d662e..9ad30404 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0
-- 
cgit v1.2.3