summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/Demo/Properties.lean12
-rw-r--r--tests/lean/Hashmap/Properties.lean14
-rw-r--r--tests/lean/Tutorial.lean22
3 files changed, 24 insertions, 24 deletions
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index e514ac3e..abdc2985 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -9,7 +9,7 @@ namespace demo
-- @[pspec]
theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
- : ∃ y, mul2_add1 x = ret y ∧
+ : ∃ y, mul2_add1 x = ok y ∧
↑y = 2 * ↑x + (1 : Int)
:= by
rw [mul2_add1]
@@ -18,7 +18,7 @@ theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
simp; scalar_tac
theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
- ∃ z, use_mul2_add1 x y = ret z ∧
+ ∃ z, use_mul2_add1 x y = ok z ∧
↑z = 2 * ↑x + (1 : Int) + ↑y := by
rw [use_mul2_add1]
progress with mul2_add1_spec as ⟨ i ⟩
@@ -34,7 +34,7 @@ open CList
theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
(h : ↑i < l.to_list.len) :
- ∃ x, list_nth T l i = ret x ∧
+ ∃ x, list_nth T l i = ok x ∧
x = l.to_list.index ↑i
:= by
rw [list_nth]
@@ -52,7 +52,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
simp_all
theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
- ∃ y, i32_id x = ret y ∧ x.val = y.val := by
+ ∃ y, i32_id x = ok y ∧ x.val = y.val := by
rw [i32_id]
if hx : x = 0#i32 then
simp_all
@@ -66,8 +66,8 @@ termination_by x.val.toNat
decreasing_by scalar_decr_tac
theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) :
- ∃ back, list_tail T l = ret (CList.CNil, back) ∧
- ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
+ ∃ back, list_tail T l = ok (CList.CNil, back) ∧
+ ∀ tl', ∃ l', back tl' = ok l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
rw [list_tail]
match l with
| CNil =>
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 4e0ca509..fcaf5806 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -59,7 +59,7 @@ def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x
def hash_mod_key (k : Usize) (l : Int) : Int :=
match hash_key k with
- | .ret k => k.val % l
+ | .ok k => k.val % l
| _ => 0
@[simp]
@@ -121,7 +121,7 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (
(hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
(hdk : distinct_keys l0.v) :
∃ b l1,
- insert_in_list α key value l0 = ret (b, l1) ∧
+ insert_in_list α key value l0 = ok (b, l1) ∧
-- The boolean is true ↔ we inserted a new binding
(b ↔ (l0.lookup key = none)) ∧
-- We update the binding
@@ -183,7 +183,7 @@ theorem insert_in_list_spec {α : Type} (l : Int) (key: Usize) (value: α) (l0:
(hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
(hdk : distinct_keys l0.v) :
∃ b l1,
- insert_in_list α key value l0 = ret (b, l1) ∧
+ insert_in_list α key value l0 = ok (b, l1) ∧
(b ↔ (l0.lookup key = none)) ∧
-- We update the binding
l1.lookup key = value ∧
@@ -240,7 +240,7 @@ set_option maxHeartbeats 2000000
theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
(hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
- ∃ nhm, hm.insert_no_resize α key value = ret nhm ∧
+ ∃ nhm, hm.insert_no_resize α key value = ok nhm ∧
-- We preserve the invariant
nhm.inv ∧
-- We updated the binding for key
@@ -253,7 +253,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
| some _ => nhm.len_s = hm.len_s) := by
rw [insert_no_resize]
-- Simplify. Note that this also simplifies some function calls, like array index
- simp [hash_key, bind_tc_ret]
+ simp [hash_key, bind_tc_ok]
have _ : (alloc.vec.Vec.len (List α) hm.slots).val ≠ 0 := by
intro
simp_all [inv]
@@ -281,7 +281,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
rw [if_update_eq] -- TODO: necessary because we don't have a join
-- TODO: progress to ...
have hipost :
- ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧
+ ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ok i0 ∧
i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val
:= by
if inserted then
@@ -328,7 +328,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
-- TODO: we want to automate this
simp only [k_hash_mod]
have h := Int.emod_lt_of_pos k.val hvpos
- simp_all only [ret.injEq, exists_eq_left', List.len_update, gt_iff_lt,
+ simp_all only [ok.injEq, exists_eq_left', List.len_update, gt_iff_lt,
List.index_update_eq, ne_eq, not_false_eq_true, neq_imp]
if h_hm : k_hash_mod = hash_mod.val then
simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq,
diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean
index d92b2dd7..94b70991 100644
--- a/tests/lean/Tutorial.lean
+++ b/tests/lean/Tutorial.lean
@@ -18,7 +18,7 @@ namespace Tutorial
def mul2_add1 (x : U32) : Result U32 := do
let x1 ← x + x
let x2 ← x1 + 1#u32
- ret x2
+ ok x2
/- There are several things to note.
@@ -75,9 +75,9 @@ def mul2_add1 (x : U32) : Result U32 := do
-/
def mul2_add1_desugared (x : U32) : Result U32 :=
match Scalar.add x x with
- | ret x1 => -- Success case
+ | ok x1 => -- Success case
match Scalar.add x1 (U32.ofInt 1) with
- | ret x2 => ret x2
+ | ok x2 => ok x2
| error => error
| error => error -- Propagating the errors
@@ -105,7 +105,7 @@ theorem mul2_add1_spec
-/
(h : 2 * ↑x + 1 ≤ U32.max)
/- The postcondition -/
- : ∃ y, mul2_add1 x = ret y ∧ -- The call succeeds
+ : ∃ y, mul2_add1 x = ok y ∧ -- The call succeeds
↑ y = 2 * ↑x + (1 : Int) -- The output has the expected value
:= by
/- The proof -/
@@ -154,7 +154,7 @@ theorem mul2_add1_spec
-/
@[pspec] -- the [pspec] attribute saves the theorem in a database, for [progress] to use it
theorem mul2_add1_spec2 (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
- : ∃ y, mul2_add1 x = ret y ∧
+ : ∃ y, mul2_add1 x = ok y ∧
↑ y = 2 * ↑x + (1 : Int)
:= by
rw [mul2_add1]
@@ -172,7 +172,7 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := do
@[pspec]
theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
- ∃ z, use_mul2_add1 x y = ret z ∧
+ ∃ z, use_mul2_add1 x y = ok z ∧
↑z = 2 * ↑x + (1 : Int) + ↑y := by
rw [use_mul2_add1]
-- Here we use [progress] on [mul2_add1]
@@ -230,7 +230,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
match l with
| CCons x tl =>
if i = 0#u32
- then ret x
+ then ok x
else do
let i1 ← i - 1#u32
list_nth T tl i1
@@ -263,7 +263,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
-- Precondition: the index is in bounds
(h : ↑i < l.to_list.len)
-- Postcondition
- : ∃ x, list_nth T l i = ret x ∧
+ : ∃ x, list_nth T l i = ok x ∧
-- [x] is the ith element of [l] after conversion to [List]
x = l.to_list.index ↑i
:= by
@@ -340,7 +340,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
If in a theorem we state and prove that:
```
- ∃ y, i32_id x = ret x
+ ∃ y, i32_id x = ok x
```
we not only prove that the function doesn't fail, but also that it terminates.
@@ -348,7 +348,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
annotates it with the [divergent] keyword.
-/
divergent def i32_id (x : I32) : Result I32 :=
- if x = 0#i32 then ret 0#i32
+ if x = 0#i32 then ok 0#i32
else do
let x1 ← x - 1#i32
let x2 ← i32_id x1
@@ -356,7 +356,7 @@ divergent def i32_id (x : I32) : Result I32 :=
/- We can easily prove that [i32_id] behaves like the identity on positive inputs -/
theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
- ∃ y, i32_id x = ret y ∧ x.val = y.val := by
+ ∃ y, i32_id x = ok y ∧ x.val = y.val := by
rw [i32_id]
if hx : x = 0#i32 then
simp_all
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 07:08:17 +0000