From 8144c39f4d37aa1fa14a8a061eb7ed60e153fb4c Mon Sep 17 00:00:00 2001
From: Son HO
Date: Sat, 22 Jun 2024 13:22:32 +0200
Subject: 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---
 backends/lean/Base/Primitives/Vec.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'backends/lean/Base/Primitives')

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
 
-- 
cgit v1.2.3