diff options
author | Son HO | 2024-06-13 22:56:37 +0200 |
---|---|---|
committer | GitHub | 2024-06-13 22:56:37 +0200 |
commit | 8e3fe11c1b31eafe14806bb513b51530c6eb99ec (patch) | |
tree | c101e6bffaf474da394229fa4bda3147409577a0 /backends/lean/Base/Primitives | |
parent | 234fa36da87b672397f96098bcf832d869f2cfbb (diff) | |
parent | d5cf75a0f8209298ad85f46249f14d5c3a24faf6 (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.lean | 3 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 24 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 3 |
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 |