summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon HO2024-06-13 22:56:37 +0200
committerGitHub2024-06-13 22:56:37 +0200
commit8e3fe11c1b31eafe14806bb513b51530c6eb99ec (patch)
treec101e6bffaf474da394229fa4bda3147409577a0 /backends/lean/Base/Primitives
parent234fa36da87b672397f96098bcf832d869f2cfbb (diff)
parentd5cf75a0f8209298ad85f46249f14d5c3a24faf6 (diff)
Merge pull request #243 from AeneasVerif/son/update-lean
Update Lean to v4.9.0-rc1
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean3
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean24
-rw-r--r--backends/lean/Base/Primitives/Vec.lean3
3 files changed, 14 insertions, 16 deletions
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 17ee626f..be460987 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -325,8 +325,7 @@ theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Ran
have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
simp [*]
-attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing
-set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
+set_option pp.fieldNotation.generalized true
def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
-- TODO: not completely sure here
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index f4264b9b..9f809ead 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1,6 +1,5 @@
import Lean
import Lean.Meta.Tactic.Simp
-import Mathlib.Tactic.Linarith
import Base.Primitives.Base
import Base.Primitives.Core
import Base.Diverge.Base
@@ -9,6 +8,9 @@ import Base.Arith.Int
namespace Primitives
+-- Deactivate the warnings which appear when we use `#assert`
+set_option linter.hashCommand false
+
----------------------
-- MACHINE INTEGERS --
----------------------
@@ -279,11 +281,11 @@ theorem Scalar.cMax_bound ty : Scalar.cMax ty ≤ Scalar.max ty := by
theorem Scalar.cMin_suffices ty (h : Scalar.cMin ty ≤ x) : Scalar.min ty ≤ x := by
have := Scalar.cMin_bound ty
- linarith
+ omega
theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty := by
have := Scalar.cMax_bound ty
- linarith
+ omega
/-- The scalar type.
@@ -310,7 +312,7 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
:=
λ h => by
- apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
+ apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> omega
def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
(h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : Scalar ty :=
@@ -345,7 +347,7 @@ theorem Scalar.check_bounds_imp_in_bounds {ty : ScalarTy} {x : Int}
have ⟨ hmin, hmax ⟩ := h
have hbmin := Scalar.cMin_bound ty
have hbmax := Scalar.cMax_bound ty
- cases hmin <;> cases hmax <;> apply And.intro <;> linarith
+ cases hmin <;> cases hmax <;> apply And.intro <;> omega
theorem Scalar.check_bounds_eq_in_bounds (ty : ScalarTy) (x : Int) :
Scalar.check_bounds ty x ↔ Scalar.in_bounds ty x := by
@@ -730,7 +732,6 @@ theorem Scalar.add_spec {ty} {x y : Scalar ty}
(∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y) := by
have h := @add_equiv ty x y
split at h <;> simp_all
- apply h
theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
(hmax : ↑x + ↑y ≤ Scalar.max ty) :
@@ -738,7 +739,7 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
have hmin : Scalar.min ty ≤ ↑x + ↑y := by
have hx := x.hmin
have hy := y.hmin
- cases ty <;> simp [min, ScalarTy.isSigned] at * <;> linarith
+ cases ty <;> simp [min, ScalarTy.isSigned] at * <;> omega
apply add_spec <;> assumption
/- Fine-grained theorems -/
@@ -825,7 +826,6 @@ theorem Scalar.sub_spec {ty} {x y : Scalar ty}
∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
have h := @sub_equiv ty x y
split at h <;> simp_all
- apply h
theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
{x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) :
@@ -834,7 +834,7 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
have hx := x.hmin
have hxm := x.hmax
have hy := y.hmin
- cases ty <;> simp [min, max, ScalarTy.isSigned] at * <;> linarith
+ cases ty <;> simp [min, max, ScalarTy.isSigned] at * <;> omega
intros
apply sub_spec <;> assumption
@@ -1030,11 +1030,11 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
have hx := x.hmin
have hy := y.hmin
simp [h] at hx hy
- have hmin : 0 ≤ ↑x / ↑y := Int.ediv_nonneg hx hy
+ have hmin : 0 ≤ x.val / y.val := Int.ediv_nonneg hx hy
have hmax : ↑x / ↑y ≤ Scalar.max ty := by
have := Int.ediv_le_self ↑y hx
have := x.hmax
- linarith
+ omega
have hs := @div_spec ty x y hnz
simp [*] at hs
apply hs
@@ -1151,7 +1151,7 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
have h : (0 : Int) < y := by int_tac
have h := Int.emod_lt_of_pos ↑x h
have := y.hmax
- linarith
+ omega
have hs := @rem_spec ty x y hnz
simp [*] at hs
simp [*]
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index d144fcb8..0b010944 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.Linarith
import Base.IList
import Base.Primitives.Scalar
import Base.Primitives.ArraySlice
@@ -59,7 +58,7 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
have h : nlen ≤ Usize.max := by
simp [Usize.max] at *
have hm := Usize.refined_max.property
- cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith
+ cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try omega
ok ⟨ List.concat v.val x, by simp at *; assumption ⟩
else
fail maximumSizeExceeded