|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Floris van Doorn. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Floris van Doorn |
| 5 | +-/ |
| 6 | + |
| 7 | +module |
| 8 | + |
| 9 | +public import Lean.Meta.Tactic.Grind.RegisterCommand |
| 10 | +public import Mathlib.Init |
| 11 | + |
| 12 | +/-! |
| 13 | +# Custom grind-sets |
| 14 | +
|
| 15 | +In this file we declare custom grind attributes and tactics that call grind using only these grind |
| 16 | +attributes. These grind sets are helpful because they can contain a lot of specialized ways to |
| 17 | +prove a particular problem. |
| 18 | +
|
| 19 | +Currently, this implements the `compactness` and `closedness` grind attribute and tactic. |
| 20 | +
|
| 21 | +## Usage Notes |
| 22 | +
|
| 23 | +These tactics can be useful for various purposes: |
| 24 | +* directly as a tactic: `by compactness` |
| 25 | +* as auto-params for lemmas: `(h : IsCompact K := by compactness)` |
| 26 | +* as discharger for other tactics, e.g. `fun_prop (disch := compactness)` |
| 27 | +* You can also use the grind sets directly: `grind only [compactness, closedness]`. |
| 28 | + This is especially useful if you want to combine multiple grind sets. |
| 29 | +
|
| 30 | +## Implementation Notes |
| 31 | +
|
| 32 | +We define these grind sets so that we can aggressively tag lemmas in one particular topic as |
| 33 | +grind lemmas for a particular grind set. For the default grind set we should be a lot |
| 34 | +more careful with tagging lemmas, to avoid slowing down `grind`, but since these specialized grind |
| 35 | +attributes don't have any tagged lemmas outside its specialized domain, it should still be |
| 36 | +performant. |
| 37 | +
|
| 38 | +These tactics will not use the full power of grind, and could disable some of the grind engines if |
| 39 | +these would slow down these tactics. We could have alternatively used a tactic similar to |
| 40 | +`apply_rules` here, but we think that the efficient implementation of `grind` is helpful even for |
| 41 | +these simpler tactics. For example, we can safely tag both the following lemmas, and `grind` will |
| 42 | +add both pairs of hypotheses to the whiteboard without having to backtrack. |
| 43 | +``` |
| 44 | +IsCompact.inter_left : IsClosed s → IsCompact t → IsCompact (s ∩ t) |
| 45 | +IsCompact.inter_right : IsCompact s → IsClosed t → IsCompact (s ∩ t) |
| 46 | +``` |
| 47 | +
|
| 48 | +We will tag transition theorems, e.g. `Set.Finite.isCompact : Finite s → IsCompact s` should be |
| 49 | +tagged `@[compactness .]`, even if `compactness` won't contain lemmas about finite sets. |
| 50 | +The advantages of this are that we can use local finiteness hypotheses, and this will ensure that |
| 51 | +the different grind sets will interact well with each other. For the same reason we tag lemmas |
| 52 | +that involve other properties, e.g. `IsCompact.inter_left` |
| 53 | +
|
| 54 | +## To do |
| 55 | +
|
| 56 | +* Implement other grind sets, e.g. `boundedness`, `countability`, `connectedness`, ... |
| 57 | +
|
| 58 | +-/ |
| 59 | + |
| 60 | +open Lean Parser Tactic |
| 61 | + |
| 62 | +/-- A hash set of the grind attributes in Mathlib. |
| 63 | +
|
| 64 | +When adding a new grind attribute, manually add it to this hash set as well. -/ |
| 65 | +def Mathlib.grindAttrs : Std.HashSet Name := |
| 66 | + {`compactness, `closedness} |
| 67 | + |
| 68 | +/-- The `compactness` attribute is a custom grind-set specialized to prove that sets are compact. |
| 69 | +It is called by the `compactness` tactic. -/ |
| 70 | +register_grind_attr compactness |
| 71 | + |
| 72 | +/-- |
| 73 | +`compactness` is a simple tactic that tries various lemmas to prove that a set is compact. |
| 74 | +It is implemented using `grind`, and has the same configuration options as `grind`. |
| 75 | +
|
| 76 | +Use `grind only [compactness, closedness]` instead if you want to prove that the closure of sets are |
| 77 | +compact. |
| 78 | +
|
| 79 | +It also exists as a grind attribute, and can be combined with other grind attributes using |
| 80 | +`grind only [compactness, ...]`. |
| 81 | +-/ |
| 82 | +macro (name := compactnessTac) "compactness" config:optConfig : tactic => |
| 83 | + -- note: directly giving `compactness` as argument in the syntax quotation below is treated |
| 84 | + -- as an unknown identifier by the hygiene system. |
| 85 | + `(tactic|grind $config only [$(mkIdent `compactness):term]) |
| 86 | + |
| 87 | +@[inherit_doc compactnessTac] |
| 88 | +macro "compactness?" config:optConfig : tactic => |
| 89 | + `(tactic|grind? $config only [$(mkIdent `compactness):term]) |
| 90 | + |
| 91 | +/-- The `closedness` attribute is a custom grind-set specialized to prove that sets are closed. |
| 92 | +It is called by the `closedness` tactic. -/ |
| 93 | +register_grind_attr closedness |
| 94 | + |
| 95 | +/-- |
| 96 | +`closedness` is a simple tactic that tries various lemmas to prove that a set is closed, |
| 97 | +and reasoning about the closure of sets. |
| 98 | +It is implemented using `grind`, and has the same configuration options as `grind`. |
| 99 | +
|
| 100 | +It also exists as a grind attribute, and can be combined with other grind attributes using |
| 101 | +`grind only [closedness, ...]`. |
| 102 | +-/ |
| 103 | +macro (name := closednessTac) "closedness" config:optConfig : tactic => |
| 104 | + -- note: directly giving `closedness` as argument in the syntax quotation below is treated |
| 105 | + -- as an unknown identifier by the hygiene system. |
| 106 | + `(tactic|grind $config only [$(mkIdent `closedness):term]) |
| 107 | + |
| 108 | +@[inherit_doc closednessTac] |
| 109 | +macro "closedness?" config:optConfig : tactic => |
| 110 | + `(tactic|grind? $config only [$(mkIdent `closedness):term]) |
0 commit comments