summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Arith/Int.lean1
-rw-r--r--backends/lean/Base/Diverge.lean1
-rw-r--r--backends/lean/Base/Diverge/Base.lean4
-rw-r--r--backends/lean/Base/Diverge/Elab.lean1
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean5
-rw-r--r--backends/lean/Base/Primitives/Range.lean1
-rw-r--r--backends/lean/Base/Primitives/Vec.lean1
-rw-r--r--backends/lean/lake-manifest.json16
-rw-r--r--backends/lean/lean-toolchain2
9 files changed, 12 insertions, 20 deletions
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