max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: implement reduceCond for bv_decide (#6460)

Browse source 
This PR implements the equivalent of `reduceIte` for `cond` in
`bv_decide` as we switched to `bif` for the `if` normal form.
This commit is contained in:
Henrik Böving 2024-12-27 11:12:52 +01:00 • committed by GitHub
parent 6a839796fd
commit c14e5ae7de
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean
View file

@ -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