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') 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