diff options
| -rw-r--r-- | backends/lean/Base.lean | 1 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives.lean (renamed from backends/lean/Primitives.lean) | 47 | ||||
| -rw-r--r-- | backends/lean/lake-manifest.json | 8 | ||||
| -rw-r--r-- | backends/lean/lakefile.lean | 2 |
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» {} |