summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base')
-rw-r--r--backends/lean/Base/Core.lean17
-rw-r--r--backends/lean/Base/IList/IList.lean18
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean8
-rw-r--r--backends/lean/Base/Primitives/Base.lean22
-rw-r--r--backends/lean/Base/Primitives/Core.lean13
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean9
-rw-r--r--backends/lean/Base/Primitives/Vec.lean4
7 files changed, 69 insertions, 22 deletions
diff --git a/backends/lean/Base/Core.lean b/backends/lean/Base/Core.lean
new file mode 100644
index 00000000..89dd199b
--- /dev/null
+++ b/backends/lean/Base/Core.lean
@@ -0,0 +1,17 @@
+
+import Lean
+
+/- This lemma is generally useful. It often happens that (because we
+ make a split on a condition for instance) we have `x ≠ y` in the context
+ and need to simplify `y ≠ x` somewhere. -/
+@[simp]
+theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
+
+/- This is generally useful, and doing without is actually quite cumbersome.
+
+ Note that the following theorem does not seem to be necessary (we invert `x`
+ and `y` in the conclusion), probably because of `neq_imp`:
+ `¬ x = y → ¬ y == x`
+ -/
+@[simp]
+theorem neq_imp_nbeq [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ x == y := by simp [*]
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index c77f075f..1b103bb3 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -3,13 +3,7 @@
import Base.Arith
import Base.Utils
-
--- TODO: move?
--- This lemma is generally useful. It often happens that (because we
--- make a split on a condition for instance) we have `x ≠ y` in the context
--- and need to simplify `y ≠ x` somewhere.
-@[simp]
-theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
+import Base.Core
namespace List
@@ -134,7 +128,7 @@ def pairwise_rel
| [] => True
| hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl
-section Lemmas
+section
variable {α : Type u}
@@ -578,6 +572,12 @@ theorem pairwise_rel_cons {α : Type u} (rel : α → α → Prop) (hd: α) (tl:
pairwise_rel rel (hd :: tl) ↔ allP tl (rel hd) ∧ pairwise_rel rel tl
:= by simp [pairwise_rel]
-end Lemmas
+theorem lookup_not_none_imp_len_pos [BEq α] (l : List (α × β)) (key : α)
+ (hLookup : l.lookup key ≠ none) :
+ 0 < l.len := by
+ induction l <;> simp_all
+ scalar_tac
+
+end
end List
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 899871af..3cc0f9c1 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -16,6 +16,10 @@ open Result Error core.ops.range
def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
+instance [BEq α] : BEq (Array α n) := SubtypeBEq _
+
+instance [BEq α] [LawfulBEq α] : LawfulBEq (Array α n) := SubtypeLawfulBEq _
+
instance (a : Type u) (n : Usize) : Arith.HasIntProp (Array a n) where
prop_ty := λ v => v.val.len = n.val
prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
@@ -109,6 +113,10 @@ theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v:
def Slice (α : Type u) := { l : List α // l.length ≤ Usize.max }
+instance [BEq α] : BEq (Slice α) := SubtypeBEq _
+
+instance [BEq α] [LawfulBEq α] : LawfulBEq (Slice α) := SubtypeLawfulBEq _
+
instance (a : Type u) : Arith.HasIntProp (Slice a) where
prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index c9237e65..63fbd8c0 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -134,18 +134,16 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } :=
-- MISC --
----------
--- This acts like a swap effectively in a functional pure world.
--- We return the old value of `dst`, i.e. `dst` itself.
--- The new value of `dst` is `src`.
-@[simp] def core.mem.replace (a : Type) (dst : a) (src : a) : a × a := (dst, src)
-/- [core::option::Option::take] -/
-@[simp] def Option.take (T: Type) (self: Option T): Option T × Option T := (self, .none)
-/- [core::mem::swap] -/
-@[simp] def core.mem.swap (T: Type) (a b: T): T × T := (b, a)
-
-/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
- Use with `simp [ aeneas ]` -/
-register_simp_attr aeneas
+instance SubtypeBEq [BEq α] (p : α → Prop) : BEq (Subtype p) where
+ beq v0 v1 := v0.val == v1.val
+
+instance SubtypeLawfulBEq [BEq α] (p : α → Prop) [LawfulBEq α] : LawfulBEq (Subtype p) where
+ eq_of_beq {a b} h := by cases a; cases b; simp_all [BEq.beq]
+ rfl := by intro a; cases a; simp [BEq.beq]
+
+------------------------------
+---- Misc Primitives Types ---
+------------------------------
-- We don't really use raw pointers for now
structure MutRawPtr (T : Type) where
diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean
index 14a51bc1..aa4a7f28 100644
--- a/backends/lean/Base/Primitives/Core.lean
+++ b/backends/lean/Base/Primitives/Core.lean
@@ -59,4 +59,17 @@ def Option.unwrap (T : Type) (x : Option T) : Result T :=
end option -- core.option
+/- [core::option::Option::take] -/
+@[simp] def Option.take (T: Type) (self: Option T): Option T × Option T := (self, .none)
+
+/- [core::mem::replace]
+
+ This acts like a swap effectively in a functional pure world.
+ We return the old value of `dst`, i.e. `dst` itself.
+ The new value of `dst` is `src`. -/
+@[simp] def mem.replace (a : Type) (dst : a) (src : a) : a × a := (dst, src)
+
+/- [core::mem::swap] -/
+@[simp] def mem.swap (T: Type) (a b: T): T × T := (b, a)
+
end core
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 31038e0d..2359c140 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -299,7 +299,14 @@ structure Scalar (ty : ScalarTy) where
val : Int
hmin : Scalar.min ty ≤ val
hmax : val ≤ Scalar.max ty
-deriving Repr
+deriving Repr, BEq, DecidableEq
+
+instance {ty} : BEq (Scalar ty) where
+ beq a b := a.val = b.val
+
+instance {ty} : LawfulBEq (Scalar ty) where
+ eq_of_beq {a b} := by cases a; cases b; simp[BEq.beq]
+ rfl {a} := by cases a; simp [BEq.beq]
instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
coe := λ v => v.val
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 12789fa9..82ecb8ed 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -16,6 +16,10 @@ namespace alloc.vec
def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
+instance [BEq α] : BEq (Vec α) := SubtypeBEq _
+
+instance [BEq α] [LawfulBEq α] : LawfulBEq (Vec α) := SubtypeLawfulBEq _
+
instance (a : Type u) : Arith.HasIntProp (Vec a) where
prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]