From 8cb83fd3bd1585f2a68a47580a55dfeee01d9f0a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 11 Apr 2024 20:10:21 +0200
Subject: Update some Lean proofs

---
 tests/lean/Demo/Properties.lean    | 12 ++++++------
 tests/lean/Hashmap/Properties.lean | 14 +++++++-------
 tests/lean/Tutorial.lean           | 22 +++++++++++-----------
 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
-- 
cgit v1.2.3