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

feat: improve case split heuristic used in grind (#6613)

Browse source 
This PR improves the case split heuristic used in the `grind` tactic,
ensuring it now avoids unnecessary case-splits on `Iff`.
This commit is contained in:
Leonardo de Moura 2025-01-12 07:40:36 -08:00 • committed by GitHub
parent 8b1aabbb1e
commit 541902564b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 88 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

97
src/Lean/Meta/Tactic/Grind/Split.lean
View file

@ -17,43 +17,70 @@ inductive CaseSplitStatus where
| ready (numCases : Nat) (isRec := false)
deriving Inhabited, BEq
/-- Given `c`, the condition of an `if-then-else`, check whether we need to case-split on the `if-then-else` or not -/
private def checkIteCondStatus (c : Expr) : GoalM CaseSplitStatus := do
if (← isEqTrue c <||> isEqFalse c) then
return .resolved
else
return .ready 2
/--
Given `e` of the form `a ∨ b`, check whether we are ready to case-split on `e`.
That is, `e` is `True`, but neither `a` nor `b` is `True`."
-/
private def checkDisjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
if (← isEqTrue e) then
if (← isEqTrue a <||> isEqTrue b) then
return .resolved
else
return .ready 2
else if (← isEqFalse e) then
return .resolved
else
return .notReady
/--
Given `e` of the form `a ∧ b`, check whether we are ready to case-split on `e`.
That is, `e` is `False`, but neither `a` nor `b` is `False`.
-/
private def checkConjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
if (← isEqTrue e) then
return .resolved
else if (← isEqFalse e) then
if (← isEqFalse a <||> isEqFalse b) then
return .resolved
else
return .ready 2
else
return .notReady
/--
Given `e` of the form `@Eq Prop a b`, check whether we are ready to case-split on `e`.
There are two cases:
1- `e` is `True`, but neither both `a` and `b` are `True`, nor both `a` and `b` are `False`.
2- `e` is `False`, but neither `a` is `True` and `b` is `False`, nor `a` is `False` and `b` is `True`.
-/
private def checkIffStatus (e a b : Expr) : GoalM CaseSplitStatus := do
if (← isEqTrue e) then
if (← (isEqTrue a <&&> isEqTrue b) <||> (isEqFalse a <&&> isEqFalse b)) then
return .resolved
else
return .ready 2
else if (← isEqFalse e) then
if (← (isEqTrue a <&&> isEqFalse b) <||> (isEqFalse a <&&> isEqTrue b)) then
return .resolved
else
return .ready 2
else
return .notReady
private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
match_expr e with
| Or a b =>
if (← isEqTrue e) then
if (← isEqTrue a <||> isEqTrue b) then
return .resolved
else
return .ready 2
else if (← isEqFalse e) then
return .resolved
else
return .notReady
| And a b =>
if (← isEqTrue e) then
return .resolved
else if (← isEqFalse e) then
if (← isEqFalse a <||> isEqFalse b) then
return .resolved
else
return .ready 2
else
return .notReady
| Eq _ _ _ =>
if (← isEqTrue e <||> isEqFalse e) then
return .ready 2
else
return .notReady
| ite _ c _ _ _ =>
if (← isEqTrue c <||> isEqFalse c) then
return .resolved
else
return .ready 2
| dite _ c _ _ _ =>
if (← isEqTrue c <||> isEqFalse c) then
return .resolved
else
return .ready 2
| Or a b => checkDisjunctStatus e a b
| And a b => checkConjunctStatus e a b
| Eq _ a b => checkIffStatus e a b
| ite _ c _ _ _ => checkIteCondStatus c
| dite _ c _ _ _ => checkIteCondStatus c
| _ =>
if (← isResolvedCaseSplit e) then
trace[grind.debug.split] "split resolved: {e}"

26
tests/lean/run/grind_t1.lean
View file

@ -237,3 +237,29 @@ example {α} (a b c : α) [LE α] :
example (x y : Bool) : ¬(x = true ↔ y = true) ↔ (¬(x = true) ↔ y = true) := by
grind
/--
error: `grind` failed
case grind
p q : Prop
a✝¹ : p = q
a✝ : p
⊢ False
-/
#guard_msgs (error) in
set_option trace.grind.split true in
example (p q : Prop) : (p ↔ q) → p → False := by
grind -- should not split on (p ↔ q)
/--
error: `grind` failed
case grind
p q : Prop
a✝¹ : p = ¬q
a✝ : p
⊢ False
-/
#guard_msgs (error) in
set_option trace.grind.split true in
example (p q : Prop) : ¬(p ↔ q) → p → False := by
grind -- should not split on (p ↔ q)