b0a12cb49f
This PR marks `Nat` power and divisibility theorems for `grind`. We use
the new `grind_pattern` constraints to control theorem instantiation.
Examples:
```lean
example {x m n : Nat} (h : x = 4 ^ (m + 1) * n) : x % 4 = 0 := by
grind
example (a m n o p : Nat) : a ∣ n → a ∣ m * n * o * p := by
grind
example {a b x m n : Nat}
: n > 0 → x = b * 4^m * a → a = 9^n → m > 0 → x % 6 = 0 := by
grind
example {a n : Nat}
: m > 4 → a = 2^(m^n) → a % 2 = 0 := by
grind
```
Closes #11515
Remark: We are adding support for installing extra theorems to `lia`
(aka `cutsat`). The example at #11515 can already be solved by `grind`
with this PR, but we still need to add the new theorems to the set for
`lia`.
cc @kim-em
|
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||