summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon Ho2024-04-04 16:08:32 +0200
committerSon Ho2024-04-04 16:08:32 +0200
commit4828b77847ee981f5c6a1bbad7f8e6ed0e58eb0f (patch)
tree89f6a530a6c251d62156d7c84307c4d316d8ceb3 /backends/lean/Base/Primitives
parent7f7387c5519da00133ad557450695e6d6838f93c (diff)
Rename Result.ret as Result.ok in the backends
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Alloc.lean4
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean54
-rw-r--r--backends/lean/Base/Primitives/Base.lean30
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean144
-rw-r--r--backends/lean/Base/Primitives/Vec.lean26
5 files changed, 128 insertions, 130 deletions
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 1f470fe1..15fe1ff9 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -11,8 +11,8 @@ namespace boxed -- alloc.boxed
namespace Box -- alloc.boxed.Box
-def deref (T : Type) (x : T) : Result T := ret x
-def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ret (x, λ x => ret x)
+def deref (T : Type) (x : T) : Result T := ok x
+def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ok (x, λ x => ok x)
/-- Trait instance -/
def coreopsDerefInst (Self : Type) :
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index e1a39d40..ef658e1b 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -50,7 +50,7 @@ abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i
def Array.index_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
- | some x => ret x
+ | some x => ok x
-- For initialization
def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n :=
@@ -69,7 +69,7 @@ theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
@[pspec]
theorem Array.index_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x, v.index_usize α n i = ret x ∧ x = v.val.index i.val := by
+ ∃ x, v.index_usize α n i = ok x ∧ x = v.val.index i.val := by
simp only [index_usize]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -79,12 +79,12 @@ def Array.update_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x:
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some _ =>
- .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+ ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
@[pspec]
theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
(hbound : i.val < v.length) :
- ∃ nv, v.update_usize α n i x = ret nv ∧
+ ∃ nv, v.update_usize α n i x = ok nv ∧
nv.val = v.val.update i.val x
:= by
simp only [update_usize]
@@ -96,12 +96,12 @@ theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Us
def Array.index_mut_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) :
Result (α × (α -> Result (Array α n))) := do
let x ← index_usize α n v i
- ret (x, update_usize α n v i)
+ ok (x, update_usize α n v i)
@[pspec]
theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x back, v.index_mut_usize α n i = ret (x, back) ∧
+ ∃ x back, v.index_mut_usize α n i = ok (x, back) ∧
x = v.val.index i.val ∧
back = update_usize α n v i := by
simp only [index_mut_usize, Bind.bind, bind]
@@ -148,7 +148,7 @@ abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : Lis
def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
- | some x => ret x
+ | some x => ok x
/- In the theorems below: we don't always need the `∃ ..`, but we use one
so that `progress` introduces an opaque variable and an equality. This
@@ -158,7 +158,7 @@ def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
@[pspec]
theorem Slice.index_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+ ∃ x, v.index_usize α i = ok x ∧ x = v.val.index i.val := by
simp only [index_usize]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -168,12 +168,12 @@ def Slice.update_usize (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some _ =>
- .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+ ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
@[pspec]
theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
(hbound : i.val < v.length) :
- ∃ nv, v.update_usize α i x = ret nv ∧
+ ∃ nv, v.update_usize α i x = ok nv ∧
nv.val = v.val.update i.val x
:= by
simp only [update_usize]
@@ -185,12 +185,12 @@ theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
def Slice.index_mut_usize (α : Type u) (v: Slice α) (i: Usize) :
Result (α × (α → Result (Slice α))) := do
let x ← Slice.index_usize α v i
- ret (x, Slice.update_usize α v i)
+ ok (x, Slice.update_usize α v i)
@[pspec]
theorem Slice.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x back, v.index_mut_usize α i = ret (x, back) ∧
+ ∃ x back, v.index_mut_usize α i = ok (x, back) ∧
x = v.val.index i.val ∧
back = Slice.update_usize α v i := by
simp only [index_mut_usize, Bind.bind, bind]
@@ -204,30 +204,30 @@ theorem Slice.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i
`progress` tactic), meaning `Array.to_slice` should be considered as opaque.
All what the spec theorem reveals is that the "representative" lists are the same. -/
def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
- ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
+ ok ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
@[pspec]
theorem Array.to_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
- ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice]
+ ∃ s, to_slice α n v = ok s ∧ v.val = s.val := by simp [to_slice]
def Array.from_slice (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
if h: s.val.len = n.val then
- ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
+ ok ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
else fail panic
@[pspec]
theorem Array.from_slice_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
- ∃ na, from_slice α n a ns = ret na ∧ na.val = ns.val
+ ∃ na, from_slice α n a ns = ok na ∧ na.val = ns.val
:= by simp [from_slice, *]
def Array.to_slice_mut (α : Type u) (n : Usize) (a : Array α n) :
Result (Slice α × (Slice α → Result (Array α n))) := do
let s ← Array.to_slice α n a
- ret (s, Array.from_slice α n a)
+ ok (s, Array.from_slice α n a)
@[pspec]
theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
- ∃ s back, to_slice_mut α n v = ret (s, back) ∧
+ ∃ s back, to_slice_mut α n v = ok (s, back) ∧
v.val = s.val ∧
back = Array.from_slice α n v
:= by simp [to_slice_mut, to_slice]
@@ -235,7 +235,7 @@ theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
-- TODO: not completely sure here
if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then
- ret ⟨ a.val.slice r.start.val r.end_.val,
+ ok ⟨ a.val.slice r.start.val r.end_.val,
by
simp [← List.len_eq_length]
have := a.val.slice_len_le r.start.val r.end_.val
@@ -246,7 +246,7 @@ def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize)
@[pspec]
theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
(h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
- ∃ s, subslice α n a r = ret s ∧
+ ∃ s, subslice α n a r = ok s ∧
s.val = a.val.slice r.start.val r.end_.val ∧
(∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
:= by
@@ -270,7 +270,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
. scalar_tac
let na := s_beg.append (s.val.append s_end)
have : na.len = a.val.len := by simp [*]
- ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+ ok ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
else
fail panic
@@ -282,7 +282,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
@[pspec]
theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
(_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) :
- ∃ na, update_subslice α n a r s = ret na ∧
+ ∃ na, update_subslice α n a r s = ok na ∧
(∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
(∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = s.index_s (i - r.start.val)) ∧
(∀ i, r.end_.val ≤ i → i < n.val → na.index_s i = a.index_s i) := by
@@ -306,7 +306,7 @@ theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a :
def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
-- TODO: not completely sure here
if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then
- ret ⟨ s.val.slice r.start.val r.end_.val,
+ ok ⟨ s.val.slice r.start.val r.end_.val,
by
simp [← List.len_eq_length]
have := s.val.slice_len_le r.start.val r.end_.val
@@ -317,7 +317,7 @@ def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slic
@[pspec]
theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
(h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
- ∃ ns, subslice α s r = ret ns ∧
+ ∃ ns, subslice α s r = ok ns ∧
ns.val = s.slice r.start.val r.end_.val ∧
(∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index_s i = s.index_s (r.start.val + i))
:= by
@@ -344,14 +344,14 @@ def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : S
. scalar_tac
let ns := s_beg.append (ss.val.append s_end)
have : ns.len = s.val.len := by simp [*]
- ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+ ok ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
else
fail panic
@[pspec]
theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
(_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) :
- ∃ na, update_subslice α a r ss = ret na ∧
+ ∃ na, update_subslice α a r ss = ok na ∧
(∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
(∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = ss.index_s (i - r.start.val)) ∧
(∀ i, r.end_.val ≤ i → i < a.length → na.index_s i = a.index_s i) := by
@@ -393,7 +393,7 @@ def core.slice.index.Slice.index
let x ← inst.get i slice
match x with
| none => fail panic
- | some x => ret x
+ | some x => ok x
/- [core::slice::index::Range:::get]: forward function -/
def core.slice.index.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice T) :
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 0c64eca1..4c5b2795 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -41,7 +41,7 @@ deriving Repr, BEq
open Error
inductive Result (α : Type u) where
- | ret (v: α): Result α
+ | ok (v: α): Result α
| fail (e: Error): Result α
| div
deriving Repr, BEq
@@ -56,31 +56,31 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
/- HELPERS -/
-def ret? {α: Type u} (r: Result α): Bool :=
+def ok? {α: Type u} (r: Result α): Bool :=
match r with
- | ret _ => true
+ | ok _ => true
| fail _ | div => false
def div? {α: Type u} (r: Result α): Bool :=
match r with
| div => true
- | ret _ | fail _ => false
+ | ok _ | fail _ => false
def massert (b:Bool) : Result Unit :=
- if b then ret () else fail assertionFailure
+ if b then ok () else fail assertionFailure
macro "prove_eval_global" : tactic => `(tactic| first | apply Eq.refl | decide)
-def eval_global {α: Type u} (x: Result α) (_: ret? x := by prove_eval_global) : α :=
+def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) : α :=
match x with
| fail _ | div => by contradiction
- | ret x => x
+ | ok x => x
/- DO-DSL SUPPORT -/
def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
match x with
- | ret v => f v
+ | ok v => f v
| fail v => fail v
| div => div
@@ -88,11 +88,11 @@ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Resu
instance : Bind Result where
bind := bind
--- Allows using return x in do-blocks
+-- Allows using pure x in do-blocks
instance : Pure Result where
- pure := fun x => ret x
+ pure := fun x => ok x
-@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
+@[simp] theorem bind_ok (x : α) (f : α → Result β) : bind (.ok x) f = f x := by simp [bind]
@[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
@[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
@@ -103,14 +103,14 @@ instance : Pure Result where
-- rely on subtype, and a custom let-binding operator, in effect recreating our
-- own variant of the do-dsl
-def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
+def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } :=
match o with
- | ret x => ret ⟨x, rfl⟩
+ | ok x => ok ⟨x, rfl⟩
| fail e => fail e
| div => div
-@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
- (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]
+@[simp] theorem bind_tc_ok (x : α) (f : α → Result β) :
+ (do let y ← .ok x; f y) = f x := by simp [Bind.bind, bind]
@[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
(do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 3d90f1a5..c298ba92 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -339,7 +339,7 @@ def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
-- ```
-- then normalization blocks (for instance, some proofs which use reflexivity fail).
-- However, the version below doesn't block reduction (TODO: investigate):
- return Scalar.ofIntCore x (Scalar.check_bounds_prop h)
+ ok (Scalar.ofIntCore 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)
@@ -573,7 +573,7 @@ instance {ty} : HAnd (Scalar ty) (Scalar ty) (Scalar ty) where
theorem Scalar.add_spec {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ ↑x + y.val)
(hmax : ↑x + ↑y ≤ Scalar.max ty) :
- (∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y) := by
+ (∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y) := by
-- Applying the unfoldings only on the left
conv => congr; ext; lhs; unfold HAdd.hAdd instHAddScalarResult; simp [add, tryMk]
split
@@ -582,7 +582,7 @@ theorem Scalar.add_spec {ty} {x y : Scalar ty}
theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
(hmax : ↑x + ↑y ≤ Scalar.max ty) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
have hmin : Scalar.min ty ≤ ↑x + ↑y := by
have hx := x.hmin
have hy := y.hmin
@@ -591,57 +591,57 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
/- Fine-grained theorems -/
@[pspec] theorem Usize.add_spec {x y : Usize} (hmax : ↑x + ↑y ≤ Usize.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
@[pspec] theorem U8.add_spec {x y : U8} (hmax : ↑x + ↑y ≤ U8.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
@[pspec] theorem U16.add_spec {x y : U16} (hmax : ↑x + ↑y ≤ U16.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
@[pspec] theorem U32.add_spec {x y : U32} (hmax : ↑x + ↑y ≤ U32.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
@[pspec] theorem U64.add_spec {x y : U64} (hmax : ↑x + ↑y ≤ U64.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
@[pspec] theorem U128.add_spec {x y : U128} (hmax : ↑x + ↑y ≤ U128.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
@[pspec] theorem Isize.add_spec {x y : Isize}
(hmin : Isize.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ Isize.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] theorem I8.add_spec {x y : I8}
(hmin : I8.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I8.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] theorem I16.add_spec {x y : I16}
(hmin : I16.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I16.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] theorem I32.add_spec {x y : I32}
(hmin : I32.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I32.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] theorem I64.add_spec {x y : I64}
(hmin : I64.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I64.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] theorem I128.add_spec {x y : I128}
(hmin : I128.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I128.max) :
- ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+ ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
-- Generic theorem - shouldn't be used much
@@ -649,7 +649,7 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
theorem Scalar.sub_spec {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ ↑x - ↑y)
(hmax : ↑x - ↑y ≤ Scalar.max ty) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
conv => congr; ext; lhs; simp [HSub.hSub, sub, tryMk, Sub.sub]
split
. simp [pure]
@@ -658,7 +658,7 @@ theorem Scalar.sub_spec {ty} {x y : Scalar ty}
theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
{x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
have : ↑x - ↑y ≤ Scalar.max ty := by
have hx := x.hmin
have hxm := x.hmax
@@ -669,64 +669,64 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
/- Fine-grained theorems -/
@[pspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ ↑x - ↑y) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
@[pspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ ↑x - ↑y) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
@[pspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ ↑x - ↑y) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
@[pspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ ↑x - ↑y) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
@[pspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ ↑x - ↑y) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
@[pspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ ↑x - ↑y) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
@[pspec] theorem Isize.sub_spec {x y : Isize} (hmin : Isize.min ≤ ↑x - ↑y)
(hmax : ↑x - ↑y ≤ Isize.max) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
@[pspec] theorem I8.sub_spec {x y : I8} (hmin : I8.min ≤ ↑x - ↑y)
(hmax : ↑x - ↑y ≤ I8.max) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
@[pspec] theorem I16.sub_spec {x y : I16} (hmin : I16.min ≤ ↑x - ↑y)
(hmax : ↑x - ↑y ≤ I16.max) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
@[pspec] theorem I32.sub_spec {x y : I32} (hmin : I32.min ≤ ↑x - ↑y)
(hmax : ↑x - ↑y ≤ I32.max) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
@[pspec] theorem I64.sub_spec {x y : I64} (hmin : I64.min ≤ ↑x - ↑y)
(hmax : ↑x - ↑y ≤ I64.max) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
@[pspec] theorem I128.sub_spec {x y : I128} (hmin : I128.min ≤ ↑x - ↑y)
(hmax : ↑x - ↑y ≤ I128.max) :
- ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+ ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
-- Generic theorem - shouldn't be used much
theorem Scalar.mul_spec {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ ↑x * ↑y)
(hmax : ↑x * ↑y ≤ Scalar.max ty) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
conv => congr; ext; lhs; simp [HMul.hMul]
simp [mul, tryMk]
split
@@ -736,7 +736,7 @@ theorem Scalar.mul_spec {ty} {x y : Scalar ty}
theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
(hmax : ↑x * ↑y ≤ Scalar.max ty) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
have : Scalar.min ty ≤ ↑x * ↑y := by
have hx := x.hmin
have hy := y.hmin
@@ -745,57 +745,57 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
/- Fine-grained theorems -/
@[pspec] theorem Usize.mul_spec {x y : Usize} (hmax : ↑x * ↑y ≤ Usize.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
@[pspec] theorem U8.mul_spec {x y : U8} (hmax : ↑x * ↑y ≤ U8.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
@[pspec] theorem U16.mul_spec {x y : U16} (hmax : ↑x * ↑y ≤ U16.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
@[pspec] theorem U32.mul_spec {x y : U32} (hmax : ↑x * ↑y ≤ U32.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
@[pspec] theorem U64.mul_spec {x y : U64} (hmax : ↑x * ↑y ≤ U64.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
@[pspec] theorem U128.mul_spec {x y : U128} (hmax : ↑x * ↑y ≤ U128.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
@[pspec] theorem Isize.mul_spec {x y : Isize} (hmin : Isize.min ≤ ↑x * ↑y)
(hmax : ↑x * ↑y ≤ Isize.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
@[pspec] theorem I8.mul_spec {x y : I8} (hmin : I8.min ≤ ↑x * ↑y)
(hmax : ↑x * ↑y ≤ I8.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
@[pspec] theorem I16.mul_spec {x y : I16} (hmin : I16.min ≤ ↑x * ↑y)
(hmax : ↑x * ↑y ≤ I16.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
@[pspec] theorem I32.mul_spec {x y : I32} (hmin : I32.min ≤ ↑x * ↑y)
(hmax : ↑x * ↑y ≤ I32.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
@[pspec] theorem I64.mul_spec {x y : I64} (hmin : I64.min ≤ ↑x * ↑y)
(hmax : ↑x * ↑y ≤ I64.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
@[pspec] theorem I128.mul_spec {x y : I128} (hmin : I128.min ≤ ↑x * ↑y)
(hmax : ↑x * ↑y ≤ I128.max) :
- ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+ ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
-- Generic theorem - shouldn't be used much
@@ -804,15 +804,14 @@ theorem Scalar.div_spec {ty} {x y : Scalar ty}
(hnz : ↑y ≠ (0 : Int))
(hmin : Scalar.min ty ≤ scalar_div ↑x ↑y)
(hmax : scalar_div ↑x ↑y ≤ Scalar.max ty) :
- ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := by
+ ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := by
simp [HDiv.hDiv, div, Div.div]
simp [tryMk, *]
- simp [pure]
rfl
theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
(hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+ ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at *
have hx := x.hmin
have hy := y.hmin
@@ -828,69 +827,69 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
/- Fine-grained theorems -/
@[pspec] theorem Usize.div_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+ ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U8.div_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+ ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U16.div_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+ ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U32.div_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+ ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U64.div_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+ ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U128.div_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+ ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem Isize.div_spec (x : Isize) {y : Isize}
(hnz : ↑y ≠ (0 : Int))
(hmin : Isize.min ≤ scalar_div ↑x ↑y)
(hmax : scalar_div ↑x ↑y ≤ Isize.max):
- ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+ ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] theorem I8.div_spec (x : I8) {y : I8}
(hnz : ↑y ≠ (0 : Int))
(hmin : I8.min ≤ scalar_div ↑x ↑y)
(hmax : scalar_div ↑x ↑y ≤ I8.max):
- ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+ ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] theorem I16.div_spec (x : I16) {y : I16}
(hnz : ↑y ≠ (0 : Int))
(hmin : I16.min ≤ scalar_div ↑x ↑y)
(hmax : scalar_div ↑x ↑y ≤ I16.max):
- ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+ ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] theorem I32.div_spec (x : I32) {y : I32}
(hnz : ↑y ≠ (0 : Int))
(hmin : I32.min ≤ scalar_div ↑x ↑y)
(hmax : scalar_div ↑x ↑y ≤ I32.max):
- ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+ ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] theorem I64.div_spec (x : I64) {y : I64}
(hnz : ↑y ≠ (0 : Int))
(hmin : I64.min ≤ scalar_div ↑x ↑y)
(hmax : scalar_div ↑x ↑y ≤ I64.max):
- ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+ ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] theorem I128.div_spec (x : I128) {y : I128}
(hnz : ↑y ≠ (0 : Int))
(hmin : I128.min ≤ scalar_div ↑x ↑y)
(hmax : scalar_div ↑x ↑y ≤ I128.max):
- ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+ ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
-- Generic theorem - shouldn't be used much
@@ -899,15 +898,14 @@ theorem Scalar.rem_spec {ty} {x y : Scalar ty}
(hnz : ↑y ≠ (0 : Int))
(hmin : Scalar.min ty ≤ scalar_rem ↑x ↑y)
(hmax : scalar_rem ↑x ↑y ≤ Scalar.max ty) :
- ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by
+ ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by
simp [HMod.hMod, rem]
simp [tryMk, *]
- simp [pure]
rfl
theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
(hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+ ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at *
have hx := x.hmin
have hy := y.hmin
@@ -923,62 +921,62 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
simp [*]
@[pspec] theorem Usize.rem_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+ ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U8.rem_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+ ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U16.rem_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+ ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U32.rem_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+ ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U64.rem_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+ ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem U128.rem_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) :
- ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+ ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] theorem I8.rem_spec (x : I8) {y : I8}
(hnz : ↑y ≠ (0 : Int))
(hmin : I8.min ≤ scalar_rem ↑x ↑y)
(hmax : scalar_rem ↑x ↑y ≤ I8.max):
- ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+ ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
@[pspec] theorem I16.rem_spec (x : I16) {y : I16}
(hnz : ↑y ≠ (0 : Int))
(hmin : I16.min ≤ scalar_rem ↑x ↑y)
(hmax : scalar_rem ↑x ↑y ≤ I16.max):
- ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+ ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
@[pspec] theorem I32.rem_spec (x : I32) {y : I32}
(hnz : ↑y ≠ (0 : Int))
(hmin : I32.min ≤ scalar_rem ↑x ↑y)
(hmax : scalar_rem ↑x ↑y ≤ I32.max):
- ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+ ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
@[pspec] theorem I64.rem_spec (x : I64) {y : I64}
(hnz : ↑y ≠ (0 : Int))
(hmin : I64.min ≤ scalar_rem ↑x ↑y)
(hmax : scalar_rem ↑x ↑y ≤ I64.max):
- ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+ ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
@[pspec] theorem I128.rem_spec (x : I128) {y : I128}
(hnz : ↑y ≠ (0 : Int))
(hmin : I128.min ≤ scalar_rem ↑x ↑y)
(hmax : scalar_rem ↑x ↑y ≤ I128.max):
- ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+ ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
-- ofIntCore
@@ -1152,6 +1150,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
| isFalse h => isFalse (Scalar.ne_of_val_ne h)
@[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by
- intro i j; cases i; cases j; simp
+ simp [eq_equiv]
end Primitives
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 65249c12..dbe5c8dd 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -61,34 +61,34 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
simp [Usize.max] at *
have hm := Usize.refined_max.property
cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith
- return ⟨ List.concat v.val x, by simp at *; assumption ⟩
+ ok ⟨ List.concat v.val x, by simp at *; assumption ⟩
else
fail maximumSizeExceeded
-- This shouldn't be used
def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
if i.val < v.length then
- .ret ()
+ ok ()
else
- .fail arrayOutOfBounds
+ fail arrayOutOfBounds
-- This is actually the backward function
def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
if i.val < v.length then
- .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+ ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
else
- .fail arrayOutOfBounds
+ fail arrayOutOfBounds
@[pspec]
theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
(hbound : i.val < v.length) :
- ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
+ ∃ nv, v.insert α i x = ok nv ∧ nv.val = v.val.update i.val x := by
simp [insert, *]
def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
- | some x => ret x
+ | some x => ok x
/- In the theorems below: we don't always need the `∃ ..`, but we use one
so that `progress` introduces an opaque variable and an equality. This
@@ -98,7 +98,7 @@ def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
@[pspec]
theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x, v.index_usize i = ret x ∧ x = v.val.index i.val := by
+ ∃ x, v.index_usize i = ok x ∧ x = v.val.index i.val := by
simp only [index_usize]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -108,12 +108,12 @@ def Vec.update_usize {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some _ =>
- .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+ ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
@[pspec]
theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
(hbound : i.val < v.length) :
- ∃ nv, v.update_usize i x = ret nv ∧
+ ∃ nv, v.update_usize i x = ok nv ∧
nv.val = v.val.update i.val x
:= by
simp only [update_usize]
@@ -125,15 +125,15 @@ theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
def Vec.index_mut_usize {α : Type u} (v: Vec α) (i: Usize) :
Result (α × (α → Result (Vec α))) :=
match Vec.index_usize v i with
- | ret x =>
- ret (x, Vec.update_usize v i)
+ | ok x =>
+ ok (x, Vec.update_usize v i)
| fail e => fail e
| div => div
@[pspec]
theorem Vec.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x back, v.index_mut_usize i = ret (x, back) ∧
+ ∃ x back, v.index_mut_usize i = ok (x, back) ∧
x = v.val.index i.val ∧
-- Backward function
back = v.update_usize i