From c14e5ae7de1eff00c75dcd5675aebb38f7f23cab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 27 Dec 2024 11:12:52 +0100 Subject: [PATCH] chore: implement reduceCond for bv_decide (#6460) This PR implements the equivalent of `reduceIte` for `cond` in `bv_decide` as we switched to `bif` for the `if` normal form. --- .../Elab/Tactic/BVDecide/Frontend/Normalize.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean index 618503b209..8f5e651a13 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean @@ -28,6 +28,18 @@ namespace Frontend.Normalize open Lean.Meta open Std.Tactic.BVDecide.Normalize +builtin_simproc ↓ [bv_normalize] reduceCond (cond _ _ _) := fun e => do + let_expr f@cond α c tb eb := e | return .continue + let r ← Simp.simp c + if r.expr.cleanupAnnotations.isConstOf ``Bool.true then + let pr := mkApp (mkApp4 (mkConst ``Bool.cond_pos f.constLevels!) α c tb eb) (← r.getProof) + return .visit { expr := tb, proof? := pr } + else if r.expr.cleanupAnnotations.isConstOf ``Bool.false then + let pr := mkApp (mkApp4 (mkConst ``Bool.cond_neg f.constLevels!) α c tb eb) (← r.getProof) + return .visit { expr := eb, proof? := pr } + else + return .continue + builtin_simproc [bv_normalize] eqToBEq (((_ : Bool) = (_ : Bool))) := fun e => do let_expr Eq _ lhs rhs := e | return .continue match_expr rhs with