perf: grind normalizer (#9271)

This PR improves the performance of the formula normalizer used in
`grind`.

src/Init/Grind/Norm.lean

@@ -45,11 +45,19 @@ theorem imp_true_eq (p : Prop) : (p → True) = True := by simp
 theorem imp_false_eq (p : Prop) : (p → False) = ¬p := by simp
 theorem imp_self_eq (p : Prop) : (p → p) = True := by simp
 
-theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
-  by_cases p <;> by_cases q <;> simp [*]
+theorem not_true : (¬True) = False := by simp
+theorem not_false : (¬False) = True := by simp
+theorem not_not (p : Prop) : (¬¬p) = p := by by_cases p <;> simp [*]
+theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by by_cases p <;> by_cases q <;> simp [*]
+theorem not_or (p q : Prop) : (¬(p ∨ q)) = (¬p ∧ ¬q) := by by_cases p <;> by_cases q <;> simp [*]
+theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by by_cases p <;> simp [*]
+theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
+theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
+theorem not_implies (p q : Prop) : (¬(p → q)) = (p ∧ ¬q) := by simp
 
-theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
-  by_cases p <;> simp [*]
+theorem or_assoc (p q r : Prop) : ((p ∨ q) ∨ r) = (p ∨ (q ∨ r)) := by by_cases p <;> simp [*]
+theorem or_swap12 (p q r : Prop) : (p ∨ q ∨ r) = (q ∨ p ∨ r) := by by_cases p <;> simp [*]
+theorem or_swap13 (p q r : Prop) : (p ∨ q ∨ r) = (r ∨ q ∨ p) := by by_cases p <;> by_cases q <;> simp [*]
 
 theorem ite_true_false {_ : Decidable p} : (ite p True False) = p := by
   by_cases p <;> simp
@@ -57,10 +65,6 @@ theorem ite_true_false {_ : Decidable p} : (ite p True False) = p := by
 theorem ite_false_true {_ : Decidable p} : (ite p False True) = ¬p := by
   by_cases p <;> simp
 
-theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
-
-theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
-
 theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
   cases c <;> simp [*]
 
@@ -141,42 +145,28 @@ theorem exists_and_right {α : Sort u} {p : α → Prop} {b : Prop} : (∃ x, p
 theorem zero_sub (a : Nat) : 0 - a = 0 := by
   simp
 
+-- Remark: for additional `grind` simprocs, check `Lean/Meta/Tactic/Grind`
 init_grind_norm
   /- Pre theorems -/
-  not_and not_or not_ite not_forall not_exists
-  /- Nat relational ops neg -/
-  Nat.not_ge_eq Nat.not_le_eq
   |
   /- Post theorems -/
-  Classical.not_not
   iff_eq heq_eq_eq
-  -- Prop equality
-  not_eq_prop
-  -- True
-  not_true
-  -- False
-  not_false_eq_true
   -- And
   and_true true_and and_false false_and and_assoc
-  -- Or
-  or_true true_or or_false false_or or_assoc
   -- ite
   ite_true ite_false ite_true_false ite_false_true
-  dite_eq_ite
   -- Bool cond
   cond_eq_ite
   -- Bool or
-  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
+  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true
   -- Bool and
-  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
+  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true
   -- Bool not
   Bool.not_not
   -- beq
   beq_iff_eq beq_eq_decide_eq beq_self_eq_true
   -- bne
   bne_iff_ne bne_eq_decide_not_eq
-  -- Bool not eq true/false
-  Bool.not_eq_true Bool.not_eq_false
   -- decide
   decide_eq_true_eq decide_not not_decide_eq_true
   -- Nat
@@ -204,6 +194,6 @@ init_grind_norm
   Function.const_apply Function.comp_apply Function.const_comp
   Function.comp_const Function.true_comp Function.false_comp
   -- Field
-  Field.div_eq_mul_inv Field.inv_zero Field.inv_inv Field.inv_one Field.inv_neg
+  Field.inv_zero Field.inv_inv Field.inv_one Field.inv_neg
 
 end Lean.Grind

src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean

@@ -48,7 +48,28 @@ builtin_simproc_decl expandPowAdd (_ ^ _) := fun e => do
     let r ← mkMul (mkApp2 pwFn a m) (mkApp2 pwFn a n)
     return .visit { expr := r, proof? := some (mkApp3 h a m n) }
 
+private def notField : Std.HashSet Name :=
+  [``Nat, ``Int, ``BitVec, ``UInt8, ``UInt16, ``UInt32, ``Int64, ``Int8, ``Int16, ``Int32, ``Int64].foldl (init := {}) (·.insert ·)
+
+private def isNotFieldQuick (type : Expr) : Bool := Id.run do
+  let .const declName _ := type.getAppFn | return false
+  return notField.contains declName
+
+builtin_simproc_decl expandDiv (_ / _) := fun e => do
+  let_expr f@HDiv.hDiv α β γ _ a b ← e | return .continue
+  if isNotFieldQuick α then return .continue
+  unless (← isDefEq α β <&&> isDefEq α γ) do return .continue
+  let us := f.constLevels!
+  let [u, _, _] := us | return .continue
+  let field := mkApp (mkConst ``Grind.Field [u]) α
+  let some fieldInst ← synthInstanceMeta? field | return .continue
+  let some mulInst ← synthInstanceMeta? (mkApp3 (mkConst ``HMul us) α α α) | return .continue
+  let some invInst ← synthInstanceMeta? (mkApp (mkConst ``Inv [u]) α) | return .continue
+  let expr := mkApp6 (mkConst ``HMul.hMul us) α α α mulInst a (mkApp3 (mkConst ``Inv.inv [u]) α invInst b)
+  return .visit { expr, proof? := some <| mkApp4 (mkConst ``Grind.Field.div_eq_mul_inv [u]) α fieldInst a b }
+
 def addSimproc (s : Simprocs) : CoreM Simprocs := do
-  s.add ``expandPowAdd (post := true)
+  let s ← s.add ``expandPowAdd (post := true)
+  s.add ``expandDiv (post := true)
 
 end Lean.Meta.Grind.Arith

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -60,6 +60,71 @@ builtin_simproc_decl simpEq (@Eq _ _ _) := fun e => do
       return .visit { expr := mkNot lhs, proof? := mkApp (mkConst ``Grind.eq_false_eq) lhs }
   return .continue
 
+builtin_simproc_decl simpDIte (@dite _ _ _ _ _) := fun e => do
+ let_expr f@dite α c inst a b ← e | return .continue
+ let .lam _ _ aBody _ := a | return .continue
+ if aBody.hasLooseBVars then return .continue
+ let .lam _ _ bBody _ := b | return .continue
+ if bBody.hasLooseBVars then return .continue
+ let us := f.constLevels!
+ let expr := mkApp5 (mkConst ``ite us) α c inst aBody bBody
+ return .visit { expr, proof? := some (mkApp5 (mkConst ``dite_eq_ite us) c α aBody bBody inst) }
+
+builtin_simproc_decl pushNot (Not _) := fun e => do
+ let_expr Not p ← e | return .continue
+ match_expr p with
+ | True => return .visit { expr := mkConst ``False, proof? := some <| mkConst ``Grind.not_true  }
+ | False => return .visit { expr := mkConst ``True, proof? := some <| mkConst ``Grind.not_false  }
+ | And q r => return .visit { expr := mkApp2 (mkConst ``Or) (mkNot q) (mkNot r), proof? := some <| mkApp2 (mkConst ``Grind.not_and) q r }
+ | Or q r => return .visit { expr := mkApp2 (mkConst ``And) (mkNot q) (mkNot r), proof? := some <| mkApp2 (mkConst ``Grind.not_or) q r }
+ | Not q => return .visit { expr := q, proof? := some <| mkApp (mkConst ``Grind.not_not) q }
+ | f@Eq α a b =>
+   if α.isProp then
+     return .visit { expr := mkApp3 f α a (mkNot b), proof? := some <| mkApp2 (mkConst ``Grind.not_eq_prop) a b }
+   else match_expr b with
+     | Bool.true => return .visit { expr := mkApp3 f α a (mkConst ``Bool.false), proof? := some <| mkApp (mkConst ``Bool.not_eq_true) a }
+     | Bool.false => return .visit { expr := mkApp3 f α a (mkConst ``Bool.true), proof? := some <| mkApp (mkConst ``Bool.not_eq_false) a }
+     | _ => return .continue
+ | f@ite α c inst a b => return .visit { expr := mkApp5 f α c inst (mkNot a) (mkNot b), proof? := some <| mkApp4 (mkConst ``Grind.not_ite) c inst a b }
+ | Exists α p =>
+   let expr := mkForall `a .default α (mkNot (mkApp p (mkBVar 0)))
+   let u ← getLevel α
+   return .visit { expr, proof? := mkApp2 (mkConst ``Grind.not_exists [u]) α p }
+ | LE.le α _ a b =>
+   match_expr α with
+   | Int => return .visit { expr := mkIntLE (mkIntAdd b (mkIntLit 1)) a, proof? := some <| mkApp2 (mkConst ``Int.not_le_eq) a b }
+   | Nat => return .visit { expr := mkNatLE (mkNatAdd b (mkNatLit 1)) a, proof? := some <| mkApp2 (mkConst ``Nat.not_le_eq) a b }
+   | _ => return .continue
+ | _ =>
+  if let .forallE n α b info := e then
+    if α.isProp && !b.hasLooseBVars then
+      return .visit { expr := mkAnd α (mkNot b), proof? := some <| mkApp2 (mkConst ``Grind.not_implies) α b }
+    else
+      let p    := mkLambda n info α b
+      let notP := mkLambda n info α (mkNot b)
+      let u ← getLevel α
+      let expr := mkApp2 (mkConst ``Exists [u]) α notP
+      return .visit { expr, proof? := some <| mkApp2 (mkConst ``Grind.not_forall [u]) α p }
+  else
+    return .continue
+
+builtin_simproc_decl simpOr (Or _ _) := fun e => do
+  let_expr Or p q ← e | return .continue
+  match_expr p with
+  | True => return .visit { expr := p, proof? := some <| mkApp (mkConst ``true_or) q }
+  | False => return .visit { expr := q, proof? := some <| mkApp (mkConst ``false_or) q }
+  | Or p₁ p₂ => return .visit { expr := mkOr p₁ (mkOr p₂ q), proof? := some <| mkApp3 (mkConst ``Grind.or_assoc) p₁ p₂ q }
+  | _ =>
+  match_expr q with
+  | Or q r =>
+    if p.isForall then return .continue
+    if q.isForall then return .visit { expr := mkOr q (mkOr p r), proof? := some <| mkApp3 (mkConst ``Grind.or_swap12) p q r }
+    if r.isForall then return .visit { expr := mkOr r (mkOr q p), proof? := some <| mkApp3 (mkConst ``Grind.or_swap13) p q r }
+    return .continue
+  | True => return .visit { expr := q, proof? := some <| mkApp (mkConst ``or_true) p }
+  | False => return .visit { expr := p, proof? := some <| mkApp (mkConst ``or_false) p }
+  | _ => return .continue
+
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← Simp.getSEvalSimprocs
@@ -81,7 +146,10 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← addPreMatchCondSimproc s
   let s ← Arith.addSimproc s
   let s ← addForallSimproc s
-  let s ← s.add ``simpEq (post := false)
+  let s ← s.add ``simpEq (post := true)
+  let s ← s.add ``simpOr (post := true)
+  let s ← s.add ``simpDIte (post := true)
+  let s ← s.add ``pushNot (post := false)
   return #[s]
 
 private def addDeclToUnfold (s : SimpTheorems) (declName : Name) : MetaM SimpTheorems := do

tests/lean/run/grind_offset_cnstr.lean

@@ -267,7 +267,7 @@ fun {a4} p a1 a2 a3 =>
     fun h h_1 h_2 =>
     intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun h_3 =>
       Classical.byContradiction
-        (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_ge_eq a4 a1) fun h_4 =>
+        (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun h_4 =>
           Eq.mp
             (Eq.trans (Eq.symm (eq_true h_4))
               (Nat.lo_eq_false_of_lo a1 a4 7 1 rfl_true

tests/lean/run/grind_pre.lean

@@ -11,7 +11,7 @@ left : a = true
 right : b = true ∨ c = true
 left_1 : p
 right_1 : q
-h_1 : b = false ∨ a = false
+h_1 : (b && a) = false
 ⊢ False
 [grind] Goal diagnostics
   [facts] Asserted facts
@@ -19,20 +19,17 @@ h_1 : b = false ∨ a = false
     [prop] b = true ∨ c = true
     [prop] p
     [prop] q
-    [prop] b = false ∨ a = false
+    [prop] (b && a) = false
   [eqc] True propositions
     [prop] p
     [prop] q
-    [prop] b = false ∨ a = false
     [prop] b = true ∨ c = true
-    [prop] b = false
     [prop] c = true
   [eqc] False propositions
-    [prop] a = false
     [prop] b = true
   [eqc] Equivalence classes
     [eqc] {a, c, true}
-    [eqc] {b, false}
+    [eqc] {b, false, b && a}
 -/
 #guard_msgs (error) in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@@ -43,14 +40,14 @@ attribute [local grind cases eager] Or
 
 /--
 error: `grind` failed
-case grind.2.1
+case grind.2
 a b c : Bool
 p q : Prop
 left : a = true
 h_1 : c = true
 left_1 : p
 right_1 : q
-h_3 : b = false
+h_2 : (b && a) = false
 ⊢ False
 [grind] Goal diagnostics
   [facts] Asserted facts
@@ -58,16 +55,16 @@ h_3 : b = false
     [prop] c = true
     [prop] p
     [prop] q
-    [prop] b = false
+    [prop] (b && a) = false
   [eqc] True propositions
     [prop] p
     [prop] q
   [eqc] Equivalence classes
     [eqc] {a, c, true}
-    [eqc] {b, false}
+    [eqc] {b, false, b && a}
 [grind] Diagnostics
   [cases] Cases instances
-    [cases] Or ↦ 3
+    [cases] Or ↦ 1
 -/
 #guard_msgs (error) in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by