From fc0b39c4fe48fdbab06d5fd32e0a2b7dcae674e6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 15:29:11 +0200
Subject: Fix the coerce notation for scalars and update some lemmas

---
 backends/lean/Base/Primitives/Scalar.lean | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'backends/lean')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 3d90f1a5..7668bc59 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -265,6 +265,14 @@ theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty
   have := Scalar.cMax_bound ty
   linarith
 
+/-- The scalar type.
+
+    We could use a subtype, but it using a custom structure type allows us
+    to have more control over the coercions and the simplifications (we tried
+    using a subtype and it caused issues especially as we had to make the Scalar
+    type non-reducible, so that we could have more control, but leading to
+    some natural equalities not being obvious to the simplifier anymore).
+ -/
 structure Scalar (ty : ScalarTy) where
   val : Int
   hmin : Scalar.min ty ≤ val
@@ -274,6 +282,9 @@ deriving Repr
 instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
   coe := λ v => v.val
 
+/- Activate the ↑ notation -/
+attribute [coe] Scalar.val
+
 theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty ->
   Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
@@ -1119,19 +1130,19 @@ theorem Scalar.eq_equiv {ty : ScalarTy} (x y : Scalar ty) :
 
 -- This is sometimes useful when rewriting the goal with the local assumptions
 @[simp] theorem Scalar.eq_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x = y → (↑x : Int) = ↑y := (eq_equiv x y).mp
+  (↑x : Int) = ↑y → x = y := (eq_equiv x y).mpr
 
 theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x < y ↔ (↑x : Int) < ↑y := by simp [LT.lt]
 
 @[simp] theorem Scalar.lt_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x < y → (↑x : Int) < ↑y := (lt_equiv x y).mp
+  (↑x : Int) < (↑y) → x < y := (lt_equiv x y).mpr
 
 theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x ≤ y ↔ (↑x : Int) ≤ ↑y := by simp [LE.le]
 
 @[simp] theorem Scalar.le_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x ≤ y → (↑x : Int) ≤ ↑y := (le_equiv x y).mp
+  (↑x : Int) ≤ ↑y → x ≤ y := (le_equiv x y).mpr
 
 instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt ..
 instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe ..
@@ -1152,6 +1163,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
     | isFalse h => isFalse (Scalar.ne_of_val_ne h)
 
 @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by
-  intro i j; cases i; cases j; simp
+  simp [eq_equiv]
 
 end Primitives
-- 
cgit v1.2.3


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