merge master

src/Init/Data/List/Nat/Count.lean

@@ -103,23 +103,15 @@ theorem Sublist.le_countP (s : l₁ <+ l₂) (p) : countP p l₂ - (l₂.length
     have := s.length_le
     split <;> omega
 
-grind_pattern Sublist.le_countP => l₁ <+ l₂, countP p l₁, countP p l₂
-
 theorem IsPrefix.le_countP (s : l₁ <+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
   s.sublist.le_countP _
 
-grind_pattern IsPrefix.le_countP => l₁ <+: l₂, countP p l₁, countP p l₂
-
 theorem IsSuffix.le_countP (s : l₁ <:+ l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
   s.sublist.le_countP _
 
-grind_pattern IsSuffix.le_countP => l₁ <:+ l₂, countP p l₁, countP p l₂
-
 theorem IsInfix.le_countP (s : l₁ <:+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁ :=
   s.sublist.le_countP _
 
-grind_pattern IsInfix.le_countP => l₁ <:+: l₂, countP p l₁, countP p l₂
-
 /--
 The number of elements satisfying a predicate in the tail of a list is
 at least one less than the number of elements satisfying the predicate in the list.
@@ -136,23 +128,15 @@ variable [BEq α]
 theorem Sublist.le_count (s : l₁ <+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
   s.le_countP _
 
-grind_pattern Sublist.le_count => l₁ <+ l₂, count a l₁, count a l₂
-
 theorem IsPrefix.le_count (s : l₁ <+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
   s.sublist.le_count _
 
-grind_pattern IsPrefix.le_count => l₁ <+: l₂, count a l₁, count a l₂
-
 theorem IsSuffix.le_count (s : l₁ <:+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
   s.sublist.le_count _
 
-grind_pattern IsSuffix.le_count => l₁ <:+ l₂, count a l₁, count a l₂
-
 theorem IsInfix.le_count (s : l₁ <:+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁ :=
   s.sublist.le_count _
 
-grind_pattern IsInfix.le_count => l₁ <:+: l₂, count a l₁, count a l₂
-
 theorem le_count_tail {a : α} {l : List α} : count a l - 1 ≤ count a l.tail :=
   le_countP_tail
 

src/Init/Grind/Tactics.lean

@@ -98,14 +98,14 @@ structure Config where
   /-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
   trace : Bool := false
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
-  splits : Nat := 8
+  splits : Nat := 9
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
   ematch : Nat := 5
   /--
   Maximum term generation.
   The input goal terms have generation 0. When we instantiate a theorem using a term from generation `n`,
   the new terms have generation `n+1`. Thus, this parameter limits the length of an instantiation chain. -/
-  gen : Nat := 5
+  gen : Nat := 8
   /-- Maximum number of theorem instances generated using E-matching in a proof search tree branch. -/
   instances : Nat := 1000
   /-- If `matchEqs` is `true`, `grind` uses `match`-equations as E-matching theorems. -/

src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean

@@ -230,7 +230,7 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d
     let hNot := mkLambda `h .default (mkApp2 lt (← c₁.p.denoteExpr) (← getZero)) (hFalse.abstract #[mkFVar fvarId])
     let h ← mkIntModLinOrdThmPrefix ``Grind.Linarith.diseq_split_resolve
     return mkApp5 h (← mkPolyDecl c₁.p) (← mkPolyDecl c'.p) reflBoolTrue (← c₁.toExprProof) hNot
-  | _ => throwError "NIY"
+  | _ => throwError "not implemented yet"
 
 partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do
   match c'.h with
@@ -253,14 +253,14 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c'
     let h ← mkIntModThmPrefix ``Grind.Linarith.eq_diseq_subst1
     return mkApp7 h (toExpr k) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p) reflBoolTrue
       (← c₁.toExprProof) (← c₂.toExprProof)
-  | .oneNeZero => throwError "NIY"
+  | .oneNeZero => throwError "not implemented yet"
 
 partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
   match c'.h with
   | .core a b lhs rhs =>
     let h ← mkIntModThmPrefix ``Grind.Linarith.eq_norm
     return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue (← mkEqProof a b)
-  | .coreCommRing _a _b _ra _rb _p _lhs' => throwError "NIY"
+  | .coreCommRing .. => throwError "not implemented yet"
   | .neg c =>
     let h ← mkIntModThmPrefix ``Grind.Linarith.eq_neg
     return mkApp4 h (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof)

tests/lean/run/grind_ctor_ematch.lean

@@ -45,7 +45,6 @@ h : ¬Even 16
     [thm] Even.zero: [Even `[0]]
   [limits] Thresholds reached
     [limit] maximum number of E-matching rounds has been reached, threshold: `(ematch := 5)`
-    [limit] maximum term generation has been reached, threshold: `(gen := 5)`
 [grind] Diagnostics
   [thm] E-Matching instances
     [thm] Even.plus_two ↦ 5

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -51,8 +51,20 @@ trace: [grind.ematch.instance] pbind_some': ∀ (h : b = some a), (b.pbind fun a
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + 3 * f b ⋯ + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_2 : b = some (a + 4 * f b ⋯)),
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + 4 * f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 5 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 5 * f b ⋯ + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (2 * a + f b ⋯)),
       (b.pbind fun a h => some (a + f b ⋯)) = some (2 * a + f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 6 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 6 * f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 7 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 7 * f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 5 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 5 * f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 6 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 6 * f b ⋯ + f b ⋯)
+[grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 7 * f b ⋯)),
+      (b.pbind fun a h => some (a + f b ⋯)) = some (a + 7 * f b ⋯ + f b ⋯)
 -/
 #guard_msgs (trace) in
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by
@@ -60,7 +72,7 @@ example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = som
   grind only [pbind_some', f]
 
 
--- `Option.pbing_some` produces an instance with a `cast` that makes the result hard to use
+-- `Option.pbind_some` produces an instance with a `cast` that makes the result hard to use
 /--
 trace: [grind.ematch.instance] Option.pbind_some: (some a).pbind (cast ⋯ fun a h => some (a + f b ⋯)) =
       cast ⋯ (fun a h => some (a + f b ⋯)) a ⋯

tests/lean/run/grind_getLast_dropLast.lean

@@ -6,7 +6,7 @@ theorem length_pos_of_ne_nil {l : List α} (h : l ≠ []) : 0 < l.length := by
 
 theorem getLast?_dropLast {xs : List α} :
     xs.dropLast.getLast? = if xs.length ≤ 1 then none else xs[xs.length - 2]? := by
-  grind (splits := 15) only [List.getElem?_eq_none, List.getElem?_reverse, getLast?_eq_getElem?,
+  grind (splits := 23) only [List.getElem?_eq_none, List.getElem?_reverse, getLast?_eq_getElem?,
     List.head?_eq_getLast?_reverse, getElem?_dropLast, List.getLast?_reverse, List.length_dropLast,
     List.length_reverse, length_nil, List.reverse_reverse, head?_nil, List.getElem?_eq_none,
     length_pos_of_ne_nil, getLast?_nil, List.head?_reverse, List.getLast?_eq_head?_reverse,

tests/lean/run/grind_ite.lean

@@ -154,7 +154,7 @@ theorem normalize_spec (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → ¬ v ∈ assign := by
-  fun_induction normalize with grind (gen := 7) (splits := 9)
+  fun_induction normalize with grind
 
 -- We can also prove other variations, where we spell "`v` is not in `assign`"
 -- different ways, and `grind` doesn't mind.
@@ -163,13 +163,13 @@ example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign.contains v = false := by
-  fun_induction normalize with grind (gen := 7) (splits := 9)
+  fun_induction normalize with grind
 
 example (assign : Std.HashMap Nat Bool) (e : IfExpr) :
     (normalize assign e).normalized
     ∧ (∀ f, (normalize assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize assign e) → assign[v]? = none := by
-  fun_induction normalize with grind (gen := 8) (splits := 9)
+  fun_induction normalize with grind
 
 /--
 We recall the statement of the if-normalization problem.
@@ -205,18 +205,18 @@ theorem normalize'_spec (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → ¬ v ∈ assign := by
-  fun_induction normalize' with grind (gen := 7) (splits := 9)
+  fun_induction normalize' with grind
 
 example (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign.contains v = false := by
-  fun_induction normalize' with grind (gen := 7) (splits := 9)
+  fun_induction normalize' with grind
 
 example (assign : Std.TreeMap Nat Bool) (e : IfExpr) :
     (normalize' assign e).normalized
     ∧ (∀ f, (normalize' assign e).eval f = e.eval fun w => assign[w]?.getD (f w))
     ∧ ∀ (v : Nat), v ∈ vars (normalize' assign e) → assign[v]? = none := by
-  fun_induction normalize' with grind (gen := 8) (splits := 9)
+  fun_induction normalize' with grind
 
 end IfExpr

tests/lean/run/grind_list2.lean

@@ -1010,12 +1010,12 @@ theorem foldr_hom (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ :
 theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} {r : β → β → Prop}
     (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
     r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
-  induction l generalizing a b with grind (ematch := 6)
+  induction l generalizing a b with grind
 
 theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} {r : β → β → Prop}
     (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
     r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
-  induction l generalizing a b with grind (ematch := 6)
+  induction l generalizing a b with grind
 
 /-! #### Further results about `getLast` and `getLast?` -/
 
@@ -1089,11 +1089,7 @@ theorem dropLast_append {l₁ l₂ : List α} :
 theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast (b :: l₂) := by
   grind +extAll
 
--- Failing with:
--- [issue] unexpected metavariable during internalization
---       ?α
---     `grind` is not supposed to be used in goals containing metavariables.
--- theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by grind (gen := 6)
+-- theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by grind
 
 theorem dropLast_replicate {n : Nat} {a : α} : dropLast (replicate n a) = replicate (n - 1) a := by
   grind +extAll

tests/lean/run/grind_list_erase.lean

@@ -28,4 +28,4 @@ theorem getLast_eraseP_mem {xs : List α} {p : α → Bool} (h) : (xs.eraseP p).
 theorem set_getElem_succ_eraseIdx_succ
     {xs : Array α} {i : Nat} (h : i + 1 < xs.size) :
     (xs.eraseIdx (i + 1)).set i xs[i + 1] (by grind) = xs.eraseIdx i := by
-  grind (splits := 12)
+  grind (splits := 10)

tests/lean/run/grind_map.lean

@@ -35,7 +35,7 @@ open scoped HashMap in
 example (m : HashMap Nat Nat) :
     (m.insert 1 2).filter (fun k _ => k > 1000) ~m m.filter fun k _ => k > 1000 := by
   apply HashMap.Equiv.of_forall_getElem?_eq
-  grind (gen := 6)
+  grind
 
 example [BEq α] [LawfulBEq α] [Hashable α] [LawfulHashable α]
   {m : HashMap α β} {f : α → β → γ} {k : α} :

tests/lean/run/grind_mvar.lean

@@ -6,5 +6,5 @@ attribute [grind] Vector.getElem?_append getElem?_dropLast
 #guard_msgs (trace) in -- should not report any issues
 set_option trace.grind.issues true
 theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by
-   fail_if_success grind (gen := 6)
+   fail_if_success grind
    grind -ext only [List.dropLast_append_cons, List.dropLast_singleton, List.append_nil]

tests/lean/run/grind_qsort.lean

@@ -28,8 +28,6 @@ open List Vector
 
 -- These attributes still need to be moved to the standard library.
 
--- attribute [grind =] Vector.getElem_swap_of_ne -- Setting `(splits := 9)` means we don't need this
-
 -- set_option trace.grind.ematch.pattern true in
 -- attribute [grind] Vector.getElem?_eq_getElem -- This one requires some consideration! -- Probably not need, see Vector.Perm.extract' below.
 
@@ -127,7 +125,7 @@ private theorem getElem_qpartition_loop_snd_of_lt_lo
 private theorem getElem_qpartition_snd_of_lt_lo (as : Vector α n)
     (hhi : hi < n) (w : lo ≤ hi)
     (k : Nat) (h : k < lo) : (qpartition as lt lo hi).2[k] = as[k] := by
-  grind (splits := 9) [qpartition, getElem_qpartition_loop_snd_of_lt_lo]
+  grind [qpartition, getElem_qpartition_loop_snd_of_lt_lo]
 
 @[local grind] private theorem getElem_qsort_sort_of_lt_lo
     (as : Vector α n)
@@ -144,7 +142,7 @@ private theorem getElem_qpartition_loop_snd_of_hi_lt
 private theorem getElem_qpartition_snd_of_hi_lt (as : Vector α n)
     (hhi : hi < n) (w : lo ≤ hi)
     (k : Nat) (h : hi < k) (h' : k < n) : (qpartition as lt lo hi).2[k] = as[k] := by
-  grind (splits := 9) [qpartition, getElem_qpartition_loop_snd_of_hi_lt]
+  grind [qpartition, getElem_qpartition_loop_snd_of_hi_lt]
 
 @[local grind] private theorem getElem_qsort_sort_of_hi_lt
     (as : Vector α n) (w : lo ≤ hi)