chore: add HVector.cons_nil_get (#909)

opencompl · Dec 25, 2024 · 97e03a5 · 97e03a5
1 parent 3bbfc4e
commit 97e03a5
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/SSA/Core/HVector.lean b/SSA/Core/HVector.lean
@@ -115,6 +115,9 @@ theorem eq_of_type_eq_nil {A : α → Type*} {l : List α}
   cases h; cases t₁; cases t₂; rfl
 syntax "[" withoutPosition(term,*) "]ₕ"  : term
 
+@[simp]
+theorem cons_nil_get : (HVector.cons x .nil).get (0 : Fin 1) = x := rfl
+
 -- Copied from core for List
 macro_rules
   | `([ $elems,* ]ₕ) => do

diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
@@ -70,7 +70,7 @@ macro "simp_alive_ssa" : tactic =>
 
         simp (config := {failIfUnchanged := false}) only [
             InstCombine.Op.denote, HVector.getN, HVector.get,
-            beq_self_eq_true, Option.isSome_some
+            beq_self_eq_true, Option.isSome_some, HVector.cons_nil_get
           ]
 
         -- Fold integers into their canonical form.