diff options
author | Son Ho | 2024-04-11 19:40:08 +0200 |
---|---|---|
committer | Son Ho | 2024-04-11 19:40:08 +0200 |
commit | 86c3680b1f3f50b4c4e6198eebc145cadfff3876 (patch) | |
tree | c79ea2c4a35198d9011287db4767599b0c5c1c42 /backends/lean/Base/Primitives | |
parent | 9c1773530a7056c161e69471b36eaa3603f6ed26 (diff) | |
parent | 4fb9c9f655a9ffc3b4a1a717988311c057c9c599 (diff) |
Merge remote-tracking branch 'origin/main' into son/clean
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 5 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Range.lean | 1 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 17 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 1 |
4 files changed, 16 insertions, 8 deletions
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index ef658e1b..91ca7284 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, *] ok ⟨ 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, *] ok ⟨ 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/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index c298ba92..98d695a4 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 @@ -1117,19 +1128,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 .. diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index dbe5c8dd..8e2d65a8 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 |