6f2c04b6a2
This PR implements `grind_pattern` constraints. They are useful for
controlling theorem instantiation in `grind`. As an example, consider
the following two theorems:
```lean
theorem extract_empty {start stop : Nat} :
(#[] : Array α).extract start stop = #[] := …
theorem extract_extract {as : Array α} {i j k l : Nat} :
(as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := …
```
If both are used for theorem instantiation, an unbounded number of
instances is generated as soon as we add the term `#[].extract i j` to
the `grind` context.
We can now prevent this by adding a `grind_pattern` constraint to
`extract_extract`:
```lean
grind_pattern extract_extract => (as.extract i j).extract k l where
as =/= #[]
```
With this constraint, only one instance is generated, as expected:
```lean
/-- trace: [grind.ematch.instance] extract_empty: #[].extract i j = #[] -/
#guard_msgs (drop error, trace) in
set_option trace.grind.ematch.instance true in
example (as : Array Nat) (h : #[].extract i j = as) : False := by
grind only [= extract_empty, usr extract_extract]
```
35 lines
1.3 KiB
Text
35 lines
1.3 KiB
Text
def map (f : α → Option β) (as : List α) : List β :=
|
||
Id.run <| as.filterMapM (pure <| f ·)
|
||
|
||
theorem map_some {xs : List α} : map some xs = xs := by
|
||
sorry
|
||
|
||
theorem map_map {f : α → Option β} {g : β → Option γ} {xs : List α} :
|
||
map g (map f xs) = map (fun x => (f x).bind g) xs := by
|
||
sorry
|
||
|
||
grind_pattern map_map => map g (map f xs) where
|
||
f =/= some
|
||
g =/= some
|
||
|
||
/-- trace: [grind.ematch.instance] map_some: map some xs = xs -/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example (xs : List Nat) (h : map some xs = ys) : False := by
|
||
grind only [= map_some, usr map_map]
|
||
|
||
theorem extract_empty {start stop : Nat} : (#[] : Array α).extract start stop = #[] :=
|
||
Array.extract_empty_of_size_le_start (Nat.zero_le _)
|
||
|
||
theorem extract_extract {as : Array α} {i j k l : Nat} :
|
||
(as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := by
|
||
apply Array.extract_extract
|
||
|
||
grind_pattern extract_extract => (as.extract i j).extract k l where
|
||
as =/= #[]
|
||
|
||
/-- trace: [grind.ematch.instance] extract_empty: #[].extract i j = #[] -/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example (as : Array Nat) (h : #[].extract i j = as) : False := by
|
||
grind only [= extract_empty, usr extract_extract]
|