This PR adds support for numerals, lower & upper bounds to the offset
constraint module in the `grind` tactic. `grind` can now solve examples
such as:
```
example (f : Nat → Nat) :
f 2 = a →
b ≤ 1 → b ≥ 1 →
c = b + 1 →
f c = a := by
grind
```
In the example above, the literal `2` and the lower&upper bounds, `b ≤
1` and `b ≥ 1`, are now processed by offset constraint module.
This PR implements support for offset equality constraints in the
`grind` tactic and exhaustive equality propagation for them. The `grind`
tactic can now solve problems such as the following:
```lean
example (f : Nat → Nat) (a b c d e : Nat) :
f (a + 3) = b →
f (c + 1) = d →
c ≤ a + 2 →
a + 1 ≤ e →
e < c →
b = d := by
grind
```
This PR implements exhaustive offset constraint propagation in the
`grind` tactic. This enhancement minimizes the number of case splits
performed by `grind`. For instance, it can solve the following example
without performing any case splits:
```lean
example (p q r s : Prop) (a b : Nat) : (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → a ≤ b → b + 2 ≤ c → p ∧ q ∧ r ∧ s := by
grind (splits := 0)
```
TODO: support for equational offset constraints.
This PR implements support for offset constraints in the `grind` tactic.
Several features are still missing, such as constraint propagation and
support for offset equalities, but `grind` can already solve examples
like the following:
```lean
example (a b c : Nat) : a ≤ b → b + 2 ≤ c → a + 1 ≤ c := by
grind
example (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 2 ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 1 ≤ c := by
grind
example (a b c : Nat) : a + 1 ≤ b → b ≤ c + 2 → a ≤ c + 1 := by
grind
example (a b c : Nat) : a + 2 ≤ b → b ≤ c + 2 → a ≤ c := by
grind
```
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
