summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-06-09 10:06:43 +0200
committerSon Ho2023-06-09 10:06:43 +0200
commite2fef1a5c986aff4c9975b1376bcc0fc0bb87940 (patch)
treed1bd1ee2170544d9ad878e708ac3c46558851dcc
parentacc09d5c69690f2c46cb1bacf290da5dcc268b24 (diff)
Reorganize a bit the Lean library
Diffstat (limited to '')
-rw-r--r--backends/lean/Base.lean1
-rw-r--r--backends/lean/Base/Primitives.lean (renamed from backends/lean/Primitives.lean)47
-rw-r--r--backends/lean/lake-manifest.json8
-rw-r--r--backends/lean/lakefile.lean2
4 files changed, 36 insertions, 22 deletions
diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
new file mode 100644
index 00000000..960b2bb5
--- /dev/null
+++ b/backends/lean/Base.lean
@@ -0,0 +1 @@
+import Base.Primitives
diff --git a/backends/lean/Primitives.lean b/backends/lean/Base/Primitives.lean
index e7826fbf..d3de1d10 100644
--- a/backends/lean/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -282,6 +282,7 @@ structure Scalar (ty : ScalarTy) where
val : Int
hmin : Scalar.min ty ≤ val
hmax : val ≤ Scalar.max ty
+deriving Repr
theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty ->
@@ -296,8 +297,24 @@ def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
def Scalar.ofInt {ty : ScalarTy} (x : Int)
(h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : Scalar ty :=
- let ⟨ hmin, hmax ⟩ := h
- Scalar.ofIntCore x hmin hmax
+ -- Remark: we initially wrote:
+ -- let ⟨ hmin, hmax ⟩ := h
+ -- Scalar.ofIntCore x hmin hmax
+ -- We updated to the line below because a similar pattern in `Scalar.tryMk`
+ -- made reduction block. Both versions seem to work for `Scalar.ofInt`, though.
+ -- TODO: investigate
+ Scalar.ofIntCore x h.left h.right
+
+@[simp] def Scalar.check_bounds (ty : ScalarTy) (x : Int) : Bool :=
+ (Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) ∧ (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty)
+
+theorem Scalar.check_bounds_prop {ty : ScalarTy} {x : Int} (h: Scalar.check_bounds ty x) :
+ Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by
+ simp at *
+ have ⟨ hmin, hmax ⟩ := h
+ have hbmin := Scalar.cMin_bound ty
+ have hbmax := Scalar.cMax_bound ty
+ cases hmin <;> cases hmax <;> apply And.intro <;> linarith
-- Further thoughts: look at what has been done here:
-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean
@@ -305,16 +322,15 @@ def Scalar.ofInt {ty : ScalarTy} (x : Int)
-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean
-- which both contain a fair amount of reasoning already!
def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
- -- TODO: write this with only one if then else
- if h: (Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) && (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty) then
- let h: Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by
- simp at *
- have ⟨ hmin, hmax ⟩ := h
- have hbmin := Scalar.cMin_bound ty
- have hbmax := Scalar.cMax_bound ty
- cases hmin <;> cases hmax <;> apply And.intro <;> linarith
- let ⟨ hmin, hmax ⟩ := h
- return Scalar.ofIntCore x hmin hmax
+ if h:Scalar.check_bounds ty x then
+ -- If we do:
+ -- ```
+ -- let ⟨ hmin, hmax ⟩ := (Scalar.check_bounds_prop h)
+ -- Scalar.ofIntCore x hmin hmax
+ -- ```
+ -- then normalization blocks (for instance, some proofs which use reflexivity fail).
+ -- However, the version below doesn't block reduction (TODO: investigate):
+ return Scalar.ofInt x (Scalar.check_bounds_prop h)
else fail integerOverflow
def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val)
@@ -626,11 +642,8 @@ def vec_index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec
-- MISC --
----------
-def mem_replace_fwd (a : Type) (x : a) (_ : a) : a :=
- x
-
-def mem_replace_back (a : Type) (_ : a) (y : a) : a :=
- y
+@[simp] def mem_replace_fwd (a : Type) (x : a) (_ : a) : a := x
+@[simp] def mem_replace_back (a : Type) (_ : a) (y : a) : a := y
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
Use with `simp [ aeneas ]` -/
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 7b23fc19..e5d362fc 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -4,24 +4,24 @@
[{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
- "rev": "f89ee53085b8aad0bacd3bc94d7ef4b8d9aba643",
+ "rev": "cdb1b898e4317567699181f27533182046ebc544",
"name": "mathlib",
"inputRev?": null}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
- "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+ "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
"name": "Qq",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/JLimperg/aesop",
"subDir?": null,
- "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+ "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
"name": "aesop",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
- "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+ "rev": "6932c4ea52914dc6b0488944e367459ddc4d01a6",
"name": "std",
"inputRev?": "main"}}]}
diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean
index c5e27d1c..21a4a332 100644
--- a/backends/lean/lakefile.lean
+++ b/backends/lean/lakefile.lean
@@ -8,4 +8,4 @@ require mathlib from git
package «base» {}
@[default_target]
-lean_lib «Primitives» {}
+lean_lib «Base» {}