From ea4bb706e2136ce9546165c7438afb0f2a558c79 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 11 Sep 2025 09:40:39 +0200 Subject: [PATCH 1/4] initial notes about grind annotation --- Manual/Grind.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Manual/Grind.lean b/Manual/Grind.lean index 1c3a242e..dc465e00 100644 --- a/Manual/Grind.lean +++ b/Manual/Grind.lean @@ -166,6 +166,7 @@ Inspect these lists to spot missing facts or contradictory assumptions. {include 1 Manual.Grind.Linarith} +{include 1 Manual.Grind.Annotation} ```comment # Diagnostics From 68610a5e6d06193d1c3bd7b7f5c3fcc9687ab87f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 12 Sep 2025 05:59:26 +0200 Subject: [PATCH 2/4] fix --- Manual/Grind.lean | 1 + Manual/Grind/Annotation.lean | 74 ++++++++++++++++++++++++++++++++++++ 2 files changed, 75 insertions(+) create mode 100644 Manual/Grind/Annotation.lean diff --git a/Manual/Grind.lean b/Manual/Grind.lean index dc465e00..8adb9c42 100644 --- a/Manual/Grind.lean +++ b/Manual/Grind.lean @@ -18,6 +18,7 @@ import Manual.Grind.EMatching import Manual.Grind.Cutsat import Manual.Grind.Algebra import Manual.Grind.Linarith +import Manual.Grind.Annotation import Manual.Grind.ExtendedExamples -- Needed for the if-then-else normalization example. diff --git a/Manual/Grind/Annotation.lean b/Manual/Grind/Annotation.lean new file mode 100644 index 00000000..5383e639 --- /dev/null +++ b/Manual/Grind/Annotation.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Leo de Moura, Kim Morrison +-/ + +import VersoManual + +import Lean.Parser.Term + +import Manual.Meta + + +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean +open Verso.Doc.Elab (CodeBlockExpander) + +open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode + +#doc (Manual) "Annotating libraries for `grind`" => +%%% +tag := "grind annotation" +%%% + +(work-in-progress, this needs examples) + +Annotations should generally be conservative: only add an attribute or grind pattern when +you expect that {tactic}`grind` should always instantiate the theorem once the patterns are matched. + +Typically, many theorems that are annotated with `@[simp]` will also be need to be annotated with `@[grind =]`. +One significant exception is that typically we avoid having `@[simp]` theorems that introduce an `if` on the right hand side, +instead preferring a pair of theorems with the positive and negative conditions as hypotheses. +Because `grind` is designed to perform case splitting, it is generally better to instead label the single theorem introducting the `if` with `@[grind =]`. + +Besides using `@[grind =]` to encourage {tactic}`grind` to perform rewriting from left to right, +you can also use `@[grind _=_]` to "saturate", allowing bidirectional rewriting whenever either side is encountered. + +Use `@[grind ←]` (which generates patterns from the conclusion of the theorem) for backwards reasoning theorems, +i.e. theorems that should be tried when their conclusion matches a goal. + +Use `@[grind →]` (which generates patterns from the hypotheses) for forwards reasoning theorems, +i.e. where facts should be propagated from existing facts on the whiteboard. + +There are many uses for custom patterns created with the `grind_pattern` command. +One common use is to introduce inequalities about terms, or membership propositions. + +We might have +``` +theorem count_le_size {a : α} {xs : Array α} : count a xs ≤ xs.size := countP_le_size + +grind_pattern count_le_size => count a xs +``` +which will register this inequality as soon as a `count a xs` term is encountered (even if the problem has not previously involved inequalities). + +We can also use multi-patterns to be more restrictive, +e.g. only introducing an inequality about sizes if the whiteboard already contains facts about sizes: +``` +theorem size_pos_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size := sorry + +grind_pattern size_pos_of_mem => a ∈ xs, xs.size +``` +Unlike `@[grind →]` attribute, which would cause this theorem to be instantiated whenever `a ∈ xs` is encountered, +this pattern will only be used when `xs.size` is already on the whiteboard. + +In Mathlib we might want to enable polynomial reasoning about the sine and cosine functions, +and so add a custom grind pattern +``` +theorem sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 := ... + +grind_pattern sin_sq_add_cos_sq => sin x, cos x +``` +which will instantiate the theorem as soon as *both* `sin x` and `cos x` (with the same `x`) are encountered. +This theorem will then automatically enter the Grobner basis module, +and be used to reason about polynomial expressions involving both `sin x` and `cos x`. From b6ea50ada195b5a3dacc27d12f425c546b2e4a0c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 12 Sep 2025 06:03:03 +0200 Subject: [PATCH 3/4] more notes --- Manual/Grind/Annotation.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Manual/Grind/Annotation.lean b/Manual/Grind/Annotation.lean index 5383e639..eefc6336 100644 --- a/Manual/Grind/Annotation.lean +++ b/Manual/Grind/Annotation.lean @@ -30,7 +30,7 @@ you expect that {tactic}`grind` should always instantiate the theorem once the p Typically, many theorems that are annotated with `@[simp]` will also be need to be annotated with `@[grind =]`. One significant exception is that typically we avoid having `@[simp]` theorems that introduce an `if` on the right hand side, instead preferring a pair of theorems with the positive and negative conditions as hypotheses. -Because `grind` is designed to perform case splitting, it is generally better to instead label the single theorem introducting the `if` with `@[grind =]`. +Because `grind` is designed to perform case splitting, it is generally better to instead label the single theorem introducing the `if` with `@[grind =]`. Besides using `@[grind =]` to encourage {tactic}`grind` to perform rewriting from left to right, you can also use `@[grind _=_]` to "saturate", allowing bidirectional rewriting whenever either side is encountered. @@ -61,6 +61,8 @@ grind_pattern size_pos_of_mem => a ∈ xs, xs.size ``` Unlike `@[grind →]` attribute, which would cause this theorem to be instantiated whenever `a ∈ xs` is encountered, this pattern will only be used when `xs.size` is already on the whiteboard. +(Note that this grind pattern could also be produced using the `@[grind <=]` attribute, which looks at the conclusion first, +then backwards through the hypotheses to select patterns. On the other hand `@[grind →]` would select only `a ∈ xs`.) In Mathlib we might want to enable polynomial reasoning about the sine and cosine functions, and so add a custom grind pattern @@ -72,3 +74,4 @@ grind_pattern sin_sq_add_cos_sq => sin x, cos x which will instantiate the theorem as soon as *both* `sin x` and `cos x` (with the same `x`) are encountered. This theorem will then automatically enter the Grobner basis module, and be used to reason about polynomial expressions involving both `sin x` and `cos x`. +One both alternatively, more aggressively, write two separate grind patterns so that this theorem instantiated when either `sin x` or `cos x` is encountered. From 9659196e25375c206e08aced02f35e4b3ac627fe Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 12 Sep 2025 06:14:47 +0200 Subject: [PATCH 4/4] umlaut, sure --- Manual/Grind/Annotation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/Grind/Annotation.lean b/Manual/Grind/Annotation.lean index eefc6336..d7d49c62 100644 --- a/Manual/Grind/Annotation.lean +++ b/Manual/Grind/Annotation.lean @@ -72,6 +72,6 @@ theorem sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 := ... grind_pattern sin_sq_add_cos_sq => sin x, cos x ``` which will instantiate the theorem as soon as *both* `sin x` and `cos x` (with the same `x`) are encountered. -This theorem will then automatically enter the Grobner basis module, +This theorem will then automatically enter the Gröbner basis module, and be used to reason about polynomial expressions involving both `sin x` and `cos x`. One both alternatively, more aggressively, write two separate grind patterns so that this theorem instantiated when either `sin x` or `cos x` is encountered.