diff options
| author | Son HO | 2024-06-22 13:22:32 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-22 13:22:32 +0200 |
| commit | 8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c (patch) | |
| tree | b3de971e89c369f30de349806c87913edeb17333 /backends/lean/Base/Primitives | |
| parent | 4d30546c809cb2c512e0c3fd8ee540fff1330eab (diff) | |
Improve `scalar_tac` and `scalar_decr_tac` (#256)
* Fix an issue in a proof of the hashmap
* Improve scalar_decr_tac
* Improve the error message of scalar_tac and add the missing Termination.lean
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index e584777a..12789fa9 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -48,10 +48,7 @@ abbrev Vec.len (α : Type u) (v : Vec α) : Usize := theorem Vec.len_val {α : Type u} (v : Vec α) : (Vec.len α v).val = v.length := by rfl --- This shouldn't be used -def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := () - --- This is actually the backward function +@[irreducible] def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α) := let nlen := List.length v.val + 1 @@ -68,7 +65,7 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α) theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.len < Usize.max) : ∃ v1, v.push α x = ok v1 ∧ v1.val = v.val ++ [x] := by - simp [push] + rw [push]; simp split <;> simp_all [List.len_eq_length] scalar_tac |