chore: update

src/Init/Grind/Norm.lean

@@ -130,6 +130,21 @@ theorem forall_forall_or {α : Sort u} {β : α → Sort v} (p : α → Prop) (q
 theorem forall_and {α} {p q : α → Prop} : (∀ x, p x ∧ q x) = ((∀ x, p x) ∧ (∀ x, q x)) := by
   apply propext; apply _root_.forall_and
 
+theorem exists_const (α : Sort u) [i : Nonempty α] {b : Prop} : (∃ _ : α, b) = b := by
+  apply propext; apply _root_.exists_const
+
+theorem exists_or {α : Sort u} {p q : α → Prop} : (∃ x, p x ∨ q x) = ((∃ x, p x) ∨ ∃ x, q x) := by
+  apply propext; apply _root_.exists_or
+
+theorem exists_prop {a b : Prop} : (∃ _h : a, b) = (a ∧ b) := by
+  apply propext; apply _root_.exists_prop
+
+theorem exists_and_left {α : Sort u} {p : α → Prop} {b : Prop} : (∃ x, b ∧ p x) = (b ∧ (∃ x, p x)) := by
+  apply propext; apply _root_.exists_and_left
+
+theorem exists_and_right {α : Sort u} {p : α → Prop} {b : Prop} : (∃ x, p x ∧ b) = ((∃ x, p x) ∧ b) := by
+  apply propext; apply _root_.exists_and_right
+
 init_grind_norm
   /- Pre theorems -/
   not_and not_or not_ite not_forall not_exists

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

@@ -213,7 +213,55 @@ builtin_simproc_decl simpForall ((a : _) → _) := fun e => do
   -- None of the rules were applicable
   return .continue
 
+/--
+Applies the following rewriting rules:
+- `Grind.exists_or`
+- `Grind.exists_and_left`
+- `Grind.exists_and_right`
+- `Grind.exists_prop`
+- `Grind.exists_const`
+-/
+builtin_simproc_decl simpExists (Exists _) := fun e => do
+  let_expr ex@Exists α fn := e | return .continue
+  let .lam x _ b _ := fn | return .continue
+  if b.isApp && b.getAppNumArgs == 2 then
+    let .const bDeclName _ := b.appFn!.appFn! | return .continue
+    if bDeclName == ``Or then
+      let pRaw := b.appFn!.appArg!
+      let qRaw := b.appArg!
+      let p := mkLambda x .default α pRaw
+      let q := mkLambda x .default α qRaw
+      let u := ex.constLevels!
+      let expr := mkOr (mkApp2 ex α p) (mkApp2 ex α q)
+      return .visit { expr, proof? := mkApp3 (mkConst ``Grind.exists_or u) α p q }
+    else if bDeclName == ``And then
+      let pRaw := b.appFn!.appArg!
+      let qRaw := b.appArg!
+      if !pRaw.hasLooseBVars then
+        let b := pRaw
+        let p := mkLambda x .default α qRaw
+        let expr := mkAnd b (mkApp2 ex α p)
+        let u := ex.constLevels!
+        return .visit { expr, proof? := mkApp3 (mkConst ``Grind.exists_and_left u) α p b }
+      else if !qRaw.hasLooseBVars then
+        let p := mkLambda x .default α pRaw
+        let b := qRaw
+        let expr := mkAnd (mkApp2 ex α p) b
+        let u := ex.constLevels!
+        return .visit { expr, proof? := mkApp3 (mkConst ``Grind.exists_and_right u) α p b }
+  if !b.hasLooseBVars then
+    if (← isProp α) then
+      let expr := mkAnd α b
+      return .visit { expr, proof? := mkApp2 (mkConst ``Grind.exists_prop) α b }
+    else
+      let u := ex.constLevels!
+      let nonempty := mkApp (mkConst ``Nonempty u) α
+      if let .some nonemptyInst ← trySynthInstance nonempty then
+        return .visit { expr := b, proof? := mkApp3 (mkConst ``Grind.exists_const u) α nonemptyInst b }
+  return .continue
+
 def addForallSimproc (s : Simprocs) : CoreM Simprocs := do
-  s.add ``simpForall (post := true)
+  let s ← s.add ``simpForall (post := true)
+  s.add ``simpExists (post := true)
 
 end Lean.Meta.Grind

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {