From be7adcdf31254fc726bff71c0be42691278b9ac0 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 27 Dec 2024 16:24:38 +0100 Subject: [PATCH] chore: use `simp -implicitDefEqProofs` (#922) --- SSA/Projects/InstCombine/TacticAuto.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean index 5645d31fc..85cb2ffc7 100644 --- a/SSA/Projects/InstCombine/TacticAuto.lean +++ b/SSA/Projects/InstCombine/TacticAuto.lean @@ -52,7 +52,7 @@ macro_rules -- that occur in the later tactics | intro (v : Option (_)) -- Introduce the variable, rcases v with _|x -- Do the case distinction - <;> simp (config:={failIfUnchanged := false}) only [simp_llvm_case_bash] + <;> simp (config:={failIfUnchanged := false}) -implicitDefEqProofs only [simp_llvm_case_bash] -- ^^^^^^^^^^^^^^^^^^^^^^^^ Simplify, in the hopes that the `none` case is trivially closed <;> simp_alive_case_bash' -- Recurse, to case bash the next variable (if it exists) <;> (try revert x) -- Finally, revert the variable we got in the `some` case, so that @@ -258,15 +258,15 @@ macro "simp_alive_split": tactic => ( all_goals try intros repeat( - all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl, Option.some_bind'', + all_goals try simp -implicitDefEqProofs only [BitVec.Refinement.some_some, BitVec.Refinement.refl, Option.some_bind'', BitVec.Refinement.none_left, Option.some_bind, Option.bind_none, Option.none_bind, Option.some.injEq] - all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl, Option.some_bind'', + all_goals try simp -implicitDefEqProofs only [BitVec.Refinement.some_some, BitVec.Refinement.refl, Option.some_bind'', BitVec.Refinement.none_left, Option, some_bind, Option.bind_none, Option.none_bind, Option.some.injEq] at * any_goals split ) - all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl, Option.some_bind'', + all_goals try simp -implicitDefEqProofs only [BitVec.Refinement.some_some, BitVec.Refinement.refl, Option.some_bind'', BitVec.Refinement.none_left, Option.some_bind, Option.bind_none, Option.none_bind, Option.some.injEq] - all_goals try simp only [BitVec.Refinement.some_some, BitVec.Refinement.refl, Option.some_bind'', + all_goals try simp -implicitDefEqProofs only [BitVec.Refinement.some_some, BitVec.Refinement.refl, Option.some_bind'', BitVec.Refinement.none_left, Option.some_bind, Option.bind_none, Option.none_bind, Option.some.injEq] at * ) )