565c6f3eb2
This PR fixes an issue in the `grind` tactic when case splitting on if-then-else expressions. It adds a new marker gadget that prevents `grind` for re-normalizing the condition `c` of an if-then-else expression. Without this marker, the negated condition `¬c` might be rewritten into an alternative form `c'`, which `grind` may not recognize as equivalent to `¬c`. As a result, `grind` could fail to propagate that `if c then a else b` simplifies to `b` in the `¬c` branch.
30 lines
587 B
Text
30 lines
587 B
Text
set_option grind.warning false
|
|
|
|
attribute [grind =] Int.min_def Int.max_def
|
|
|
|
example (a b : Int) : min a b = 10 → a ≥ 10 := by
|
|
grind
|
|
|
|
example (a b : Int) : min a b ≤ a := by
|
|
grind
|
|
|
|
example (a b : Int) : min a b ≤ b := by
|
|
grind
|
|
|
|
example (a b : Int) : min a b ≤ min b a := by
|
|
grind
|
|
|
|
example (a b : Int) : max a (min a b) ≥ a := by
|
|
grind
|
|
|
|
example (a b : Int) : max a (min a b) ≥ min b a := by
|
|
grind
|
|
|
|
example (a b : Int) : max a (max a b) ≥ b := by
|
|
grind
|
|
|
|
example (a b : Int) : max a (max a b) ≥ a := by
|
|
grind
|
|
|
|
example (a : Int) : max a a = a := by
|
|
grind
|