Custom grind-sets

In this file we declare custom grind attributes and tactics that call grind using only these grind attributes. These grind sets are helpful because they can contain a lot of specialized ways to prove a particular problem.

Currently, this implements the compactness and closedness grind attribute and tactic.

Usage Notes

These tactics can be useful for various purposes:

• directly as a tactic: by compactness
• as auto-params for lemmas: (h : IsCompact K := by compactness)
• as discharger for other tactics, e.g. fun_prop (disch := compactness)
• You can also use the grind sets directly: grind only [compactness, closedness]. This is especially useful if you want to combine multiple grind sets.

Implementation Notes

We define these grind sets so that we can aggressively tag lemmas in one particular topic as grind lemmas for a particular grind set. For the default grind set we should be a lot more careful with tagging lemmas, to avoid slowing down grind, but since these specialized grind attributes don't have any tagged lemmas outside its specialized domain, it should still be performant.

These tactics will not use the full power of grind, and could disable some of the grind engines if these would slow down these tactics. We could have alternatively used a tactic similar to apply_rules here, but we think that the efficient implementation of grind is helpful even for these simpler tactics. For example, we can safely tag both the following lemmas, and grind will add both pairs of hypotheses to the whiteboard without having to backtrack.

IsCompact.inter_left : IsClosed s → IsCompact t → IsCompact (s ∩ t)
IsCompact.inter_right : IsCompact s → IsClosed t → IsCompact (s ∩ t)

We will tag transition theorems, e.g. Set.Finite.isCompact : Finite s → IsCompact s should be tagged @[compactness .], even if compactness won't contain lemmas about finite sets. The advantages of this are that we can use local finiteness hypotheses, and this will ensure that the different grind sets will interact well with each other. For the same reason we tag lemmas that involve other properties, e.g. IsCompact.inter_left

To do

• Implement other grind sets, e.g. boundedness, countability, connectedness, ...

def Lean.Parser.Attr.compactness? : ParserDescr

The compactness attribute is a custom grind-set specialized to prove that sets are compact. It is called by the compactness tactic.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.compactness!? : ParserDescr

The compactness attribute is a custom grind-set specialized to prove that sets are compact. It is called by the compactness tactic.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.compactness : ParserDescr

The compactness attribute is a custom grind-set specialized to prove that sets are compact. It is called by the compactness tactic.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.compactness! : ParserDescr

The compactness attribute is a custom grind-set specialized to prove that sets are compact. It is called by the compactness tactic.

Equations

• One or more equations did not get rendered due to their size.

def compactnessTac : Lean.ParserDescr

compactness is a simple tactic that tries various lemmas to prove that a set is compact. It is implemented using grind, and has the same configuration options as grind.

Use grind only [compactness, closedness] instead if you want to prove that the closure of sets are compact.

It also exists as a grind attribute, and can be combined with other grind attributes using grind only [compactness, ...].

Equations

• compactnessTac = Lean.ParserDescr.node `compactnessTac 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "compactness" false) Lean.Parser.Tactic.optConfig)

def tacticCompactness?_ : Lean.ParserDescr

compactness is a simple tactic that tries various lemmas to prove that a set is compact. It is implemented using grind, and has the same configuration options as grind.

Use grind only [compactness, closedness] instead if you want to prove that the closure of sets are compact.

It also exists as a grind attribute, and can be combined with other grind attributes using grind only [compactness, ...].

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.closedness? : ParserDescr

The closedness attribute is a custom grind-set specialized to prove that sets are closed. It is called by the closedness tactic.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.closedness : ParserDescr

The closedness attribute is a custom grind-set specialized to prove that sets are closed. It is called by the closedness tactic.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.closedness!? : ParserDescr

The closedness attribute is a custom grind-set specialized to prove that sets are closed. It is called by the closedness tactic.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Attr.closedness! : ParserDescr

The closedness attribute is a custom grind-set specialized to prove that sets are closed. It is called by the closedness tactic.

Equations

• One or more equations did not get rendered due to their size.

def closednessTac : Lean.ParserDescr

closedness is a simple tactic that tries various lemmas to prove that a set is closed, and reasoning about the closure of sets. It is implemented using grind, and has the same configuration options as grind.

It also exists as a grind attribute, and can be combined with other grind attributes using grind only [closedness, ...].

Equations

• closednessTac = Lean.ParserDescr.node `closednessTac 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "closedness" false) Lean.Parser.Tactic.optConfig)

def tacticClosedness?_ : Lean.ParserDescr

closedness is a simple tactic that tries various lemmas to prove that a set is closed, and reasoning about the closure of sets. It is implemented using grind, and has the same configuration options as grind.

It also exists as a grind attribute, and can be combined with other grind attributes using grind only [closedness, ...].

Equations

• One or more equations did not get rendered due to their size.