feat: overapplied ite and dite applications in grind (#8544)

This PR implements support for over-applied `ite` and `dite`
applications in the `grind` tactic. It adds support for propagation and
case-split.

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

@@ -62,7 +62,7 @@ def isMorallyIff (e : Expr) : Bool :=
 private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
   match h : e with
   | .app .. =>
-    if (← getConfig).splitIte && (e.isIte || e.isDIte) then
+    if (← getConfig).splitIte && (isIte e || isDIte e) then
       addSplitCandidate (.default e)
       return ()
     if isMorallyIff e then

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

@@ -240,35 +240,73 @@ builtin_grind_propagator propagateHEqUp ↑HEq := fun e => do
   if (← isEqv a b) then
     pushEqTrue e <| mkEqTrueCore e (← mkHEqProof a b)
 
+/--
+Helper function for propagating over-applied `ite` and `dite`-applications.
+`h` is a proof for the `e`'s prefix (of size `prefixSize`) that is equal to `rhs`.
+`args` contains all arguments of `e`.
+`prefixSize <= args.size`
+-/
+private def applyCongrFun (e rhs : Expr) (h : Expr) (prefixSize : Nat) (args : Array Expr) : GoalM Unit := do
+  if prefixSize == args.size then
+    internalize rhs (← getGeneration e)
+    pushEq e rhs h
+  else
+    go rhs h prefixSize
+where
+  go (rhs : Expr) (h : Expr) (i : Nat) : GoalM Unit := do
+    if _h : i < args.size then
+      let arg := args[i]
+      let rhs' := mkApp rhs arg
+      let h' ← mkCongrFun h arg
+      go rhs' h' (i+1)
+    else
+      let rhs ← preprocessLight rhs
+      internalize rhs (← getGeneration e)
+      pushEq e rhs h
+
 /-- Propagates `ite` upwards -/
 builtin_grind_propagator propagateIte ↑ite := fun e => do
-  let_expr f@ite α c h a b := e | return ()
+  let numArgs := e.getAppNumArgs
+  if numArgs < 5 then return ()
+  let c := e.getArg! 1 numArgs
   if (← isEqTrue c) then
-    internalize a (← getGeneration e)
-    pushEq e a <| mkApp6 (mkConst ``ite_cond_eq_true f.constLevels!) α c h a b (← mkEqTrueProof c)
+    let f := e.getAppFn
+    let args := e.getAppArgs
+    let rhs := args[3]!
+    let h := mkApp (mkAppRange (mkConst ``ite_cond_eq_true f.constLevels!) 0 5 args) (← mkEqTrueProof c)
+    applyCongrFun e rhs h 5 args
   else if (← isEqFalse c) then
-    internalize b (← getGeneration e)
-    pushEq e b <| mkApp6 (mkConst ``ite_cond_eq_false f.constLevels!) α c h a b (← mkEqFalseProof c)
+    let f := e.getAppFn
+    let args := e.getAppArgs
+    let rhs := args[4]!
+    let h := mkApp (mkAppRange (mkConst ``ite_cond_eq_false f.constLevels!) 0 5 args) (← mkEqFalseProof c)
+    applyCongrFun e rhs h 5 args
 
 /-- Propagates `dite` upwards -/
 builtin_grind_propagator propagateDIte ↑dite := fun e => do
-  let_expr f@dite α c h a b := e | return ()
+  let numArgs := e.getAppNumArgs
+  if numArgs < 5 then return ()
+  let c := e.getArg! 1 numArgs
   if (← isEqTrue c) then
-     let h₁ ← mkEqTrueProof c
-     let ah₁ := mkApp a (mkOfEqTrueCore c h₁)
-     let p ← preprocess ah₁
-     let r := p.expr
-     let h₂ ← p.getProof
-     internalize r (← getGeneration e)
-     pushEq e r <| mkApp8 (mkConst ``Grind.dite_cond_eq_true' f.constLevels!) α c h a b r h₁ h₂
+    let f := e.getAppFn
+    let args := e.getAppArgs
+    let h₁ ← mkEqTrueProof c
+    let ah₁ := mkApp args[3]! (mkOfEqTrueCore c h₁)
+    let p ← preprocess ah₁
+    let r := p.expr
+    let h₂ ← p.getProof
+    let h := mkApp3 (mkAppRange (mkConst ``Grind.dite_cond_eq_true' f.constLevels!) 0 5 args) r h₁ h₂
+    applyCongrFun e r h 5 args
   else if (← isEqFalse c) then
-     let h₁ ← mkEqFalseProof c
-     let bh₁ := mkApp b (mkOfEqFalseCore c h₁)
-     let p ← preprocess bh₁
-     let r := p.expr
-     let h₂ ← p.getProof
-     internalize r (← getGeneration e)
-     pushEq e r <| mkApp8 (mkConst ``Grind.dite_cond_eq_false' f.constLevels!) α c h a b r h₁ h₂
+    let f := e.getAppFn
+    let args := e.getAppArgs
+    let h₁ ← mkEqFalseProof c
+    let bh₁ := mkApp args[4]! (mkOfEqFalseCore c h₁)
+    let p ← preprocess bh₁
+    let r := p.expr
+    let h₂ ← p.getProof
+    let h := mkApp3 (mkAppRange (mkConst ``Grind.dite_cond_eq_false' f.constLevels!) 0 5 args) r h₁ h₂
+    applyCongrFun e r h 5 args
 
 builtin_grind_propagator propagateDecideDown ↓decide := fun e => do
   let root ← getRootENode e

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

@@ -93,9 +93,9 @@ private def checkDefaultSplitStatus (e : Expr) : GoalM SplitStatus := do
       checkIffStatus e a b
     else
       return .ready 2
-  | ite _ c _ _ _ => checkIteCondStatus c
-  | dite _ c _ _ _ => checkIteCondStatus c
   | _ =>
+    if isIte e || isDIte e then
+      return (← checkIteCondStatus (e.getArg! 1))
     if (← isResolvedCaseSplit e) then
       trace_goal[grind.debug.split] "split resolved: {e}"
       return .resolved
@@ -215,8 +215,6 @@ private def mkGrindEM (c : Expr) :=
 private def mkCasesMajor (c : Expr) : GoalM Expr := do
   match_expr c with
   | And a b => return mkApp3 (mkConst ``Grind.or_of_and_eq_false) a b (← mkEqFalseProof c)
-  | ite _ c _ _ _ => return mkGrindEM c
-  | dite _ c _ _ _ => return mkGrindEM c
   | Eq _ a b =>
     if isMorallyIff c then
       if (← isEqTrue c) then
@@ -228,7 +226,9 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
       return mkGrindEM c
   | Not e => return mkGrindEM e
   | _ =>
-    if (← isEqTrue c) then
+    if isIte c || isDIte c then
+      return mkGrindEM (c.getArg! 1)
+    else if (← isEqTrue c) then
       return mkOfEqTrueCore c (← mkEqTrueProof c)
     else
       return c

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

@@ -216,4 +216,10 @@ def replacePreMatchCond (e : Expr) : MetaM Simp.Result := do
     let e' ← Core.transform e (pre := pre)
     return { expr := e', proof? := mkExpectedPropHint (← mkEqRefl e') (← mkEq e e') }
 
+def isIte (e : Expr) :=
+  e.isAppOf ``ite && e.getAppNumArgs >= 5
+
+def isDIte (e : Expr) :=
+  e.isAppOf ``dite && e.getAppNumArgs >= 5
+
 end Lean.Meta.Grind

tests/lean/run/grind_overapplied_ite.lean

@@ -0,0 +1,21 @@
+set_option grind.warning false
+
+example : (if (!false) = true then id else id) false = false := by
+  grind
+
+opaque q (h : ¬ (!false) = true) : Bool → Bool
+
+example : (if h : (!false) = true then id else q h) false = false := by
+  grind
+
+example [Decidable c] : (if c then id else id) false = false := by
+  grind
+
+opaque c : Prop
+opaque r (h : ¬ c) : Bool → Bool
+open Classical
+
+@[grind =] theorem rax : r h x = x := sorry
+
+example : (if h : c then id else r h) false = false := by
+  grind