summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Base.lean2
-rw-r--r--backends/lean/Base/Primitives/Vec.lean20
2 files changed, 9 insertions, 13 deletions
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index db462c38..7c0fa3bb 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -76,7 +76,7 @@ def eval_global {α: Type u} (x: Result α) (_: ret? x): α :=
/- DO-DSL SUPPORT -/
-def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β :=
+def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
match x with
| ret v => f v
| fail v => fail v
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 5a709566..523372bb 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -75,10 +75,9 @@ def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
.fail arrayOutOfBounds
@[pspec]
-theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) :
- i.val < v.length →
+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
- intro h
simp [insert, *]
def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
@@ -87,10 +86,9 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
| some x => ret x
@[pspec]
-theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
- i.val < v.length →
+theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+ (hbound : i.val < v.length) :
v.index α i = ret (v.val.index i.val) := by
- intro
simp only [index]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -109,10 +107,9 @@ def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
| some x => ret x
@[pspec]
-theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
- i.val < v.length →
+theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+ (hbound : i.val < v.length) :
v.index_mut α i = ret (v.val.index i.val) := by
- intro
simp only [index_mut]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -129,12 +126,11 @@ def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Ve
.ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
@[pspec]
-theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) :
- i.val < v.length →
+theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
+ (hbound : i.val < v.length) :
∃ nv, v.index_mut_back α i x = ret nv ∧
nv.val = v.val.update i.val x
:= by
- intro
simp only [index_mut_back]
have h := List.indexOpt_bounds v.val i.val
split