WIP

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -159,6 +159,267 @@ builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofN
       proof? := some proof
   }
 
+-- The following simprocs implement rewrites where we only want to look for exact syntactic
+-- matches instead of unification, example: `x == x` should simplify to true but we don't want to
+-- run unification for all `x == y` pairs.
+
+builtin_simproc [bv_normalize] bool_eq_self ((_ : Bool) = (_ : Bool)) := fun e => do
+  let_expr Eq α lhs rhs := e | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``True
+    proof? := mkApp2 (mkConst ``eq_self [1]) α lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_eq_self ((_ : BitVec _) = (_ : BitVec _)) := fun e => do
+  let_expr Eq α lhs rhs := e | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``True
+    proof? := mkApp2 (mkConst ``eq_self [1]) α lhs
+  }
+
+builtin_simproc [bv_normalize] bool_ite_self (ite _ _ _) := fun e => do
+  let_expr ite α c instDec t e := e | return .continue
+  if t != e then return .continue
+  return .done {
+    expr := t
+    proof? := mkApp4 (mkConst ``ite_self [1]) α c instDec t
+  }
+
+builtin_simproc [bv_normalize] bitvec_ite_self (ite _ _ _) := fun e => do
+  let_expr ite α c instDec t e := e | return .continue
+  if t != e then return .continue
+  return .done {
+    expr := t
+    proof? := mkApp4 (mkConst ``ite_self [1]) α c instDec t
+  }
+
+builtin_simproc [bv_normalize] bool_beq_not_self ((_ : Bool) == !(_ : Bool)) := fun e => do
+  let_expr BEq.beq _ _ lhs rhsExpr := e | return .continue
+  let_expr Bool.not rhs := rhsExpr | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.false,
+    proof? := mkApp (mkConst ``Bool.beq_not_self) lhs
+  }
+
+builtin_simproc [bv_normalize] bool_not_beq_self (!(_ : Bool) == (_ : Bool)) := fun e => do
+  let_expr BEq.beq _ _ lhsExpr rhs := e | return .continue
+  let_expr Bool.not lhs := lhsExpr | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.false,
+    proof? := mkApp (mkConst ``Bool.not_beq_self) lhs
+  }
+
+builtin_simproc [bv_normalize] beq_self_left ((_ : Bool) == ((_ : Bool) == (_ : Bool))) := fun e => do
+  let_expr BEq.beq _ _ fst rhsExpr := e | return .continue
+  let_expr BEq.beq _ _ snd thr := rhsExpr | return .continue
+  if fst != snd then return .continue
+  return .done {
+    expr := thr,
+    proof? := mkApp2 (mkConst ``Bool.beq_self_left) fst thr
+  }
+
+builtin_simproc [bv_normalize] beq_self_right (((_ : Bool) == (_ : Bool)) == (_ : Bool)) := fun e => do
+  let_expr BEq.beq _ _ lhsExpr thr := e | return .continue
+  let_expr BEq.beq _ _ fst snd := lhsExpr | return .continue
+  if snd != thr then return .continue
+  return .done {
+    expr := thr,
+    proof? := mkApp2 (mkConst ``Bool.beq_self_right) fst thr
+  }
+
+builtin_simproc [bv_normalize] and_self_left ((_ : Bool) && ((_ : Bool) && (_ : Bool))) := fun e => do
+  let_expr Bool.and fst rhsExpr := e | return .continue
+  let_expr Bool.and snd thr := rhsExpr | return .continue
+  if fst != snd then return .continue
+  return .done {
+    expr := mkApp2 (mkConst ``Bool.and) fst thr,
+    proof? := mkApp2 (mkConst ``Bool.and_self_left) fst thr
+  }
+
+builtin_simproc [bv_normalize] and_self_right (((_ : Bool) && (_ : Bool)) && (_ : Bool)) := fun e => do
+  let_expr Bool.and lhsExpr thr := e | return .continue
+  let_expr Bool.and fst snd := lhsExpr | return .continue
+  if snd != thr then return .continue
+  return .done {
+    expr := mkApp2 (mkConst ``Bool.and) fst thr,
+    proof? := mkApp2 (mkConst ``Bool.and_self_right) fst thr
+  }
+
+builtin_simproc [bv_normalize] bool_and_self ((_ : Bool) && (_ : Bool)) := fun e => do
+  let_expr Bool.and lhs rhs := e | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.true
+    proof? := mkApp (mkConst ``Bool.and_self) lhs
+  }
+
+builtin_simproc [bv_normalize] bool_xor_self ((_ : Bool) ^^ (_ : Bool)) := fun e => do
+  let_expr Bool.xor lhs rhs := e | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.false
+    proof? := mkApp (mkConst ``Bool.xor_self) lhs
+  }
+
+builtin_simproc [bv_normalize] bool_and_not_self ((_ : Bool) && !(_ : Bool)) := fun e => do
+  let_expr Bool.and lhs rhsExpr := e | return .continue
+  let_expr Bool.not rhs := rhsExpr | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.false
+    proof? := mkApp (mkConst ``Bool.and_not_self) lhs
+  }
+
+builtin_simproc [bv_normalize] bool_not_and_self (!(_ : Bool) && (_ : Bool)) := fun e => do
+  let_expr Bool.and lhsExpr rhs := e | return .continue
+  let_expr Bool.not lhs := lhsExpr | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.false
+    proof? := mkApp (mkConst ``Bool.not_and_self) lhs
+  }
+
+builtin_simproc [bv_normalize] bool_xor_not_self ((_ : Bool) ^^ !(_ : Bool)) := fun e => do
+  let_expr Bool.xor lhs rhsExpr := e | return .continue
+  let_expr Bool.not rhs := rhsExpr | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.true
+    proof? := mkApp (mkConst ``Bool.xor_not_self) lhs
+  }
+
+builtin_simproc [bv_normalize] bool_not_xor_self (!(_ : Bool) ^^ (_ : Bool)) := fun e => do
+  let_expr Bool.and lhsExpr rhs := e | return .continue
+  let_expr Bool.not lhs := lhsExpr | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.true
+    proof? := mkApp (mkConst ``Bool.not_xor_self) lhs
+  }
+
+builtin_simproc [bv_normalize] bool_beq_self ((_ : Bool) == (_ : Bool)) := fun e => do
+  let_expr BEq.beq α _ lhs rhs := e | return .continue
+  if lhs != rhs then return .continue
+  return .done {
+    expr := mkConst ``Bool.true
+    proof? := mkApp3 (mkConst ``beq_self_eq_true' [0]) α (mkConst ``Bool.decEq) lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_beq_self ((_ : BitVec _) == (_ : BitVec _)) := fun e => do
+  let_expr BEq.beq α _ lhs rhs := e | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec w := α | return .continue
+  let decEq := mkApp (mkConst ``BitVec.decEq) w
+  return .done {
+    expr := mkConst ``Bool.true
+    proof? := mkApp3 (mkConst ``beq_self_eq_true' [0]) α decEq lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_and_self ((_ : BitVec _) &&& (_ : BitVec _)) := fun e => do
+  let_expr HAnd.hAnd α _ _ _ lhs rhs := e | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec w := α | return .continue
+  return .done {
+    expr := lhs
+    proof? := mkApp2 (mkConst ``BitVec.and_self) w lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_and_not_self ((_ : BitVec _) &&& ~~~(_ : BitVec _)) := fun e => do
+  let_expr HAnd.hAnd _ _ _ _ lhs rhsExpr := e | return .continue
+  let_expr Complement.complement α _ rhs := rhsExpr | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec wExpr := α | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  return .done {
+    expr := toExpr 0#w
+    proof? := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.and_contra) wExpr lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_not_and_self (~~~(_ : BitVec _) &&& (_ : BitVec _)) := fun e => do
+  let_expr HAnd.hAnd _ _ _ _ lhsExpr rhs := e | return .continue
+  let_expr Complement.complement α _ lhs := lhsExpr | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec wExpr := α | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  return .done {
+    expr := toExpr 0#w
+    proof? := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.and_contra') wExpr lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_add_not_self ((_ : BitVec _) + ~~~(_ : BitVec _)) := fun e => do
+  let_expr HAdd.hAdd _ _ _ _ lhs rhsExpr := e | return .continue
+  let_expr Complement.complement α _ rhs := rhsExpr | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec wExpr := α | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  return .done {
+    expr := toExpr 0#w
+    proof? := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.add_not) wExpr lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_not_add_self (~~~(_ : BitVec _) + (_ : BitVec _)) := fun e => do
+  let_expr HAdd.hAdd _ _ _ _ lhsExpr rhs := e | return .continue
+  let_expr Complement.complement α _ lhs := lhsExpr | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec wExpr := α | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  return .done {
+    expr := toExpr 0#w
+    proof? := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.not_add) wExpr lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_add_neg ((_ : BitVec _) + ~~~((_ : BitVec _) + 1#_)) := fun e => do
+  let_expr HAdd.hAdd _ _ _ _ lhs rhsExpr := e | return .continue
+  let_expr Complement.complement _ _ rhsExpr := rhsExpr | return .continue
+  let_expr HAdd.hAdd α _ _ _ rhs _ := rhsExpr | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec wExpr := α | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  return .done {
+    expr := toExpr 0#w
+    proof? := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.add_neg) wExpr lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_add_neg' ((_ : BitVec _) + ~~~(1#_ + (_ : BitVec _))) := fun e => do
+  let_expr HAdd.hAdd _ _ _ _ lhs rhsExpr := e | return .continue
+  let_expr Complement.complement _ _ rhsExpr := rhsExpr | return .continue
+  let_expr HAdd.hAdd α _ _ _ _ rhs := rhsExpr | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec wExpr := α | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  return .done {
+    expr := toExpr 0#w
+    proof? := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.add_neg') wExpr lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_neg_add (~~~((_ : BitVec _) + 1#_) + (_ : BitVec _)) := fun e => do
+  let_expr HAdd.hAdd _ _ _ _ lhsExpr rhs := e | return .continue
+  let_expr Complement.complement _ _ lhsExpr := lhsExpr | return .continue
+  let_expr HAdd.hAdd α _ _ _ lhs _ := lhsExpr | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec wExpr := α | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  return .done {
+    expr := toExpr 0#w
+    proof? := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.neg_add) wExpr lhs
+  }
+
+builtin_simproc [bv_normalize] bitvec_neg_add' (1#_ + ~~~((_ : BitVec _)) + (_ : BitVec _)) := fun e => do
+  let_expr HAdd.hAdd _ _ _ _ lhsExpr rhs := e | return .continue
+  let_expr Complement.complement _ _ lhsExpr := lhsExpr | return .continue
+  let_expr HAdd.hAdd α _ _ _ _ lhs := lhsExpr | return .continue
+  if lhs != rhs then return .continue
+  let_expr BitVec wExpr := α | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  return .done {
+    expr := toExpr 0#w
+    proof? := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.neg_add') wExpr lhs
+  }
+
 /--
 A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
 the goal fully, indicated by returning `none`.

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -136,7 +136,7 @@ section Constant
 
 attribute [bv_normalize] BitVec.add_zero
 attribute [bv_normalize] BitVec.zero_add
-attribute [bv_normalize] BitVec.setWidth_eq
+--attribute [bv_normalize] BitVec.setWidth_eq
 attribute [bv_normalize] BitVec.setWidth_zero
 attribute [bv_normalize] BitVec.getLsbD_zero
 attribute [bv_normalize] BitVec.getLsbD_zero_length
@@ -154,57 +154,47 @@ end Constant
 attribute [bv_normalize] BitVec.zero_and
 attribute [bv_normalize] BitVec.and_zero
 
--- Used in simproc because of - normalization
+-- A lot of the following are only used in simprocs
+
 theorem BitVec.ones_and (a : BitVec w) : (-1#w) &&& a = a := by
   ext
   simp [BitVec.negOne_eq_allOnes]
 
--- Used in simproc because of - normalization
 theorem BitVec.and_ones (a : BitVec w) : a &&& (-1#w) = a := by
   ext
   simp [BitVec.negOne_eq_allOnes]
 
-attribute [bv_normalize] BitVec.and_self
-
-@[bv_normalize]
 theorem BitVec.and_contra (a : BitVec w) : a &&& ~~~a = 0#w := by
   ext
   simp
 
-@[bv_normalize]
 theorem BitVec.and_contra' (a : BitVec w) : ~~~a &&& a = 0#w := by
   ext
   simp
 
-@[bv_normalize]
 theorem BitVec.add_not (a : BitVec w) : a + ~~~a = (-1#w) := by
   ext
   simp [BitVec.negOne_eq_allOnes]
 
-@[bv_normalize]
 theorem BitVec.not_add (a : BitVec w) : ~~~a + a = (-1#w) := by
   rw [BitVec.add_comm]
   rw [BitVec.add_not]
 
-@[bv_normalize]
 theorem BitVec.add_neg (a : BitVec w) : a + (~~~a + 1#w) = 0#w := by
   rw [← BitVec.neg_eq_not_add]
   rw [← BitVec.sub_toAdd]
   rw [BitVec.sub_self]
 
-@[bv_normalize]
 theorem BitVec.add_neg' (a : BitVec w) : a + (1#w + ~~~a) = 0#w := by
   rw [BitVec.add_comm 1#w (~~~a)]
   rw [BitVec.add_neg]
 
-@[bv_normalize]
 theorem BitVec.neg_add (a : BitVec w) : (~~~a + 1#w) + a = 0#w := by
   rw [← BitVec.neg_eq_not_add]
   rw [BitVec.add_comm]
   rw [← BitVec.sub_toAdd]
   rw [BitVec.sub_self]
 
-@[bv_normalize]
 theorem BitVec.neg_add' (a : BitVec w) : (1#w + ~~~a) + a = 0#w := by
   rw [BitVec.add_comm 1#w (~~~a)]
   rw [BitVec.neg_add]
@@ -230,10 +220,6 @@ theorem BitVec.not_neg''' (x : BitVec w) : ~~~(1#w + x) = ~~~x + -1#w := by
   rw [BitVec.add_comm 1#w x]
   rw [BitVec.not_neg'']
 
-@[bv_normalize]
-theorem BitVec.add_same (a : BitVec w) : a + a = a * 2#w := by
-  rw [BitVec.mul_two]
-
 theorem BitVec.add_const_left (a b c : BitVec w) : a + (b + c) = (a + b) + c := by ac_rfl
 theorem BitVec.add_const_right (a b c : BitVec w) : a + (b + c) = (a + c) + b := by ac_rfl
 theorem BitVec.add_const_left' (a b c : BitVec w) : (a + b) + c = (a + c) + b := by ac_rfl

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -20,28 +20,13 @@ attribute [bv_normalize] Bool.and_true
 attribute [bv_normalize] Bool.true_and
 attribute [bv_normalize] Bool.and_false
 attribute [bv_normalize] Bool.false_and
-attribute [bv_normalize] beq_self_eq_true'
 attribute [bv_normalize] Bool.true_beq
 attribute [bv_normalize] Bool.false_beq
-attribute [bv_normalize] Bool.beq_not_self
-attribute [bv_normalize] Bool.not_beq_self
-attribute [bv_normalize] Bool.beq_self_left
-attribute [bv_normalize] Bool.beq_self_right
-attribute [bv_normalize] Bool.and_self
-attribute [bv_normalize] Bool.and_not_self
-attribute [bv_normalize] Bool.not_and_self
-attribute [bv_normalize] Bool.xor_self
 attribute [bv_normalize] Bool.xor_false
 attribute [bv_normalize] Bool.false_xor
 attribute [bv_normalize] Bool.true_xor
 attribute [bv_normalize] Bool.xor_true
-attribute [bv_normalize] Bool.not_xor_self
-attribute [bv_normalize] Bool.xor_not_self
 attribute [bv_normalize] Bool.not_not
-attribute [bv_normalize] Bool.and_self_left
-attribute [bv_normalize] Bool.and_self_right
-attribute [bv_normalize] eq_self
-attribute [bv_normalize] ite_self
 
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide

src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean

@@ -99,17 +99,5 @@ attribute [bv_normalize] BitVec.mul_eq
 attribute [bv_normalize] BitVec.udiv_eq
 attribute [bv_normalize] BitVec.umod_eq
 
-@[bv_normalize]
-theorem Bool.and_eq_and (x y : Bool) : x.and y = (x && y) := by
-  rfl
-
-@[bv_normalize]
-theorem Bool.or_eq_or (x y : Bool) : x.or y = (x || y) := by
-  rfl
-
-@[bv_normalize]
-theorem Bool.no_eq_not (x : Bool) : x.not = !x := by
-  rfl
-
 end Normalize
 end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Normalize/Equal.lean

@@ -18,8 +18,6 @@ attribute [bv_normalize] beq_true
 attribute [bv_normalize] Bool.true_beq
 attribute [bv_normalize] beq_false
 attribute [bv_normalize] Bool.false_beq
-attribute [bv_normalize] beq_self_eq_true
-attribute [bv_normalize] beq_self_eq_true'
 
 @[bv_normalize]
 theorem Bool.not_beq_not : ∀ (a b : Bool), ((!a) == (!b)) = (a == b) := by