diff --git a/src/Init/Data/List/Nat/Count.lean b/src/Init/Data/List/Nat/Count.lean index 09e898959a..c6d4b19172 100644 --- a/src/Init/Data/List/Nat/Count.lean +++ b/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 diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index 14a69f67e6..0dabeb1141 100644 --- a/src/Init/Grind/Tactics.lean +++ b/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. -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean index 00bd24236a..2c2120e375 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean +++ b/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) diff --git a/tests/lean/run/grind_ctor_ematch.lean b/tests/lean/run/grind_ctor_ematch.lean index 8b935ffb03..880def6887 100644 --- a/tests/lean/run/grind_ctor_ematch.lean +++ b/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 diff --git a/tests/lean/run/grind_ematch_gen_pattern.lean b/tests/lean/run/grind_ematch_gen_pattern.lean index 29e6ecba50..fdab6a3eb4 100644 --- a/tests/lean/run/grind_ematch_gen_pattern.lean +++ b/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 ⋯ diff --git a/tests/lean/run/grind_getLast_dropLast.lean b/tests/lean/run/grind_getLast_dropLast.lean index 2c5611bde8..8f16e654ee 100644 --- a/tests/lean/run/grind_getLast_dropLast.lean +++ b/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, diff --git a/tests/lean/run/grind_ite.lean b/tests/lean/run/grind_ite.lean index a95860dd56..4df23b0402 100644 --- a/tests/lean/run/grind_ite.lean +++ b/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 diff --git a/tests/lean/run/grind_list2.lean b/tests/lean/run/grind_list2.lean index 290c2b825b..47ea0cd484 100644 --- a/tests/lean/run/grind_list2.lean +++ b/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 diff --git a/tests/lean/run/grind_list_erase.lean b/tests/lean/run/grind_list_erase.lean index e7c2e7a2fd..bed9926518 100644 --- a/tests/lean/run/grind_list_erase.lean +++ b/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) diff --git a/tests/lean/run/grind_map.lean b/tests/lean/run/grind_map.lean index 2f53b899a1..fa2c569af0 100644 --- a/tests/lean/run/grind_map.lean +++ b/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 : α} : diff --git a/tests/lean/run/grind_mvar.lean b/tests/lean/run/grind_mvar.lean index 79d25cc21d..c09b476791 100644 --- a/tests/lean/run/grind_mvar.lean +++ b/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] diff --git a/tests/lean/run/grind_qsort.lean b/tests/lean/run/grind_qsort.lean index 98356eaec7..bb11a35306 100644 --- a/tests/lean/run/grind_qsort.lean +++ b/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)