From 2d1d03dbc60d04c7e9344bdc794bbcdbce843b21 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 22 Jan 2024 15:55:39 +0000 Subject: [PATCH] feat: fix alex's comments --- SSA/Projects/InstCombine/AliveHandwrittenExamples.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean index 42971213a..a1b1ac340 100644 --- a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean +++ b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean @@ -60,12 +60,13 @@ theorem alive_DivRemOfSelect (w : Nat) : LLVM.const?, LLVM.icmp?, HVector.toTuple, List.nthLe, bitvec_minus_one] intro y x c - simp [Option.bind, bind, Monad.toBind] + simp only [List.length_singleton, Fin.zero_eta, List.get_cons_zero, List.map_eq_map, List.map_cons, + List.map_nil, CharP.cast_eq_zero, Ctxt.Valuation.snoc_last, pairBind, bind, Option.bind, Int.ofNat_eq_coe] clear Γv cases c -- | select condition is itself `none`, nothing more to be done. propagate the `none`. - . case none => cases x <;> cases y <;> simp - . case some cond => + case none => cases x <;> cases y <;> simp + case some cond => obtain ⟨vcond, hcond⟩ := cond obtain (h | h) : vcond = 1 ∨ vcond = 0 := by norm_num at hcond