The grind tactic can be extended to a new domain by defining a mapping from the new domain to one for which there already exists a dedicated solver.
This extension consists of a homomorphism: a structure-preserving translation from the new domain to the existing domain.
In other words, grind can be made to reason about some new type T using an existing solver for U by defining a mapping T.toU from T to U that satisfies certain properties.
Lean includes homomorphism rewrite rules for Fin, BitVec, UInt8–UInt64, USize, Int8–Int64, and ISize that rewrite them to the lia solver's domain.
Additionally, the inequality relations and byte-index bounds of String.Pos are mapped, allowing grind to reason about string positions.
Homomorphism rewriting is controlled by the hom flag to grind, and it is enabled by default.
To use the feature at all, the mapping should be injective with respect to equality.
That is, given x and y of type T, it should be the case that x=y is logically equivalent to x.toU=y.toU.
Adding the grind hom attribute to a suitable injectivity theorem activates the mapping feature.
To be useful, the mapping should translate operations of interest on T into operations in U that are supported by grind's solvers.
The grind hom attribute can be added to the following kinds of theorems:
To translate f into g, it should be the case that (fxy).toU=gx.toUy.toU.
Ordering relations can be translated by showing that x≤y↔x.toU≤y.toU and x<y↔x.toU<y.toU.
Numeric literals can be translated by providing a theorem that translates them into a function into U.
This is done by adding the grind hom attribute to a theorem of the form (OfNat.ofNatn:T).toU=hn.
Conditionals can be translated by providing a theorem that shows that (ifpthenxelsey).toU=ifpthenx.toUelsey.toU.
As a last resort, fallback rules can be provided that are applied after other rules have failed to rewrite a term.
These are typically used for rules that would otherwise overlap others.
Additional facts about the range of the mapping can be provided by tagging lemmas with grind hom_pred.
This is typically used to restrict the range, such as by asserting that the target of Fin.val is less than the Fin's bound.
These lemmas are instantiated when the constants that they mention are used in terms that are not themselves rewritten by grind hom rules.
Homomorphism lemmas are applied prior to adding statements to the shared “whiteboard,” rather than repeatedly while the solvers run.
This can be much more efficient.
Because the mapping is injective, disequality of terms in the new type implies disequality in the solver's domain, so grind's strategy of negating statements to derive a contradiction can be applied directly even without having a bijection.
Because they run only very early in the process, homomorphism lemmas are applied without a discharger.
This means that they do not permit conditional rewrites that require further proving (though rewrites can still be made conditional on an instance-implicit hypothesis, and propositional hypotheses are permitted when they are fully determined by the left-hand side).
Homomorphism rules are declared using three attributes: grind hom, grind hom fallback, and grind hom_pred.
These attributes respectively register homomorphism rules, fallback rules to be tried when the other grind hom rules don't apply, and facts about the range of the mapping.
attributeHomomorphism Rules
attr::= ...
|Marks a theorem or definition for use by the `grind` tactic.
An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
controls how `grind` uses the declaration:
* whether it is applied forwards, backwards, or both,
* whether equalities are used on the left, right, or both sides,
* whether case-splits, constructors, extensionality, or injectivity are applied,
* or whether custom instantiation patterns are used.
See the individual modifier docstrings for details.grindThe `hom` modifier marks a theorem as a homomorphism rule for `grind`.
Homomorphism rules translate terms from a source domain into a target domain that has a
dedicated solver. A collection of homomorphism rules encodes an algebra homomorphism
`h : A → B`: each rule states how `h` commutes with a source-domain operation, as in
`h (f x y) = g (h x) (h y)`. Example: injecting bitvector operations into integer
arithmetic using `BitVec.toNat`:
```
@[grind hom] theorem toNat_add (x y : BitVec w) :
(x + y).toNat = (x.toNat + y.toNat) % 2^w
```
The rules must be unconditional equations (or `Iff`s). They are applied to fixpoint
outside the E-graph, and only the final result is internalized.hom
The hom modifier marks a theorem as a homomorphism rule for grind.
Homomorphism rules translate terms from a source domain into a target domain that has a
dedicated solver. A collection of homomorphism rules encodes an algebra homomorphism
h:A→B: each rule states how h commutes with a source-domain operation, as in
h(fxy)=g(hx)(hy). Example: injecting bitvector operations into integer
arithmetic using BitVec.toNat:
The rules must be unconditional equations (or Iffs). They are applied to fixpoint
outside the E-graph, and only the final result is internalized.
attributeFallback Homomorphism Rules
attr::= ...
|Marks a theorem or definition for use by the `grind` tactic.
An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
controls how `grind` uses the declaration:
* whether it is applied forwards, backwards, or both,
* whether equalities are used on the left, right, or both sides,
* whether case-splits, constructors, extensionality, or injectivity are applied,
* or whether custom instantiation patterns are used.
See the individual modifier docstrings for details.grindThe `hom fallback` modifier marks a homomorphism rule that is tried only when no other
`[grind hom]` rule applies to the term. It is meant for rules whose left-hand side matches
every application of an injection, such as the bridge `x.toInt = x.toBitVec.toInt` between
the two images of `Int64`: as an ordinary rule it would take precedence over the direct
rules like `Int64.toInt_add`, since the rewriter applies the first matching rule.homfallback
The homfallback modifier marks a homomorphism rule that is tried only when no other
[grindhom] rule applies to the term. It is meant for rules whose left-hand side matches
every application of an injection, such as the bridge x.toInt=x.toBitVec.toInt between
the two images of Int64: as an ordinary rule it would take precedence over the direct
rules like Int64.toInt_add, since the rewriter applies the first matching rule.
attributeHomomorphism Predicates
attr::= ...
|Marks a theorem or definition for use by the `grind` tactic.
An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
controls how `grind` uses the declaration:
* whether it is applied forwards, backwards, or both,
* whether equalities are used on the left, right, or both sides,
* whether case-splits, constructors, extensionality, or injectivity are applied,
* or whether custom instantiation patterns are used.
See the individual modifier docstrings for details.grindThe `hom_pred` modifier marks a theorem as a homomorphism predicate for `grind`.
Homomorphism predicates are facts that `grind` instantiates eagerly for the terms it
internalizes. The conclusion of the theorem must contain an application `f a₁ … aₙ`
whose trailing arguments are exactly the theorem's explicit parameters; the head
symbol `f` becomes the trigger. Whenever `grind` internalizes a term with head `f`,
the theorem is instantiated with the term's trailing arguments, and the resulting
fact is asserted. Typical uses are range facts for injection functions, and
translations of relations into a target domain. Examples:
```
@[grind hom_pred] theorem BitVec.toNat_range (x : BitVec w) : x.toNat < 2^w
@[grind hom_pred] theorem UInt8.le_iff (a b : UInt8) : a ≤ b ↔ a.toBitVec ≤ b.toBitVec
```
The first theorem is triggered by terms of the form `BitVec.toNat x`, and the second
one by `a ≤ b` applications. `grind` uses the types of `a` and `b` to discard
irrelevant instantiations.hom_pred
The hom_pred modifier marks a theorem as a homomorphism predicate for grind.
Homomorphism predicates are facts that grind instantiates eagerly for the terms it
internalizes. The conclusion of the theorem must contain an application f a₁ … aₙ
whose trailing arguments are exactly the theorem's explicit parameters; the head
symbol f becomes the trigger. Whenever grind internalizes a term with head f,
the theorem is instantiated with the term's trailing arguments, and the resulting
fact is asserted. Typical uses are range facts for injection functions, and
translations of relations into a target domain. Examples:
@[grind hom_pred] theorem BitVec.toNat_range (x : BitVec w) : x.toNat < 2^w
@[grind hom_pred] theorem UInt8.le_iff (a b : UInt8) : a ≤ b ↔ a.toBitVec ≤ b.toBitVec
The first theorem is triggered by terms of the form BitVec.toNatx, and the second
one by a≤b applications. grind uses the types of a and b to discard
irrelevant instantiations.
Whenever a Tiny number is converted to a Nat, the resulting number is less than four.
Adding a grind hom_pred attribute to the proof causes grind to include this knowledge when Tiny.toNat is used in a term that is added to the “whiteboard” but not rewritten by a grind hom rule:
A finite type like Tiny must decide the meaning of operations that go outside its bounds.
In this case, Tiny.succ and the addition operator are defined such that they truncate; modular arithmetic would be another valid implementation.
Natural numbers do not exhibit truncating addition, so it seems natural to require that the result of the addition does not truncate prior to mapping it to natural number addition.
However, this results in an error:
invalid `[grind hom]` theorem, `toNat_add_lt_4_eq_add` is conditional: hypothesisx.toNat+y.toNat<4is not determined by the left-hand side and would have to be discharged when the rule is applied. Homomorphism rules must be unconditional; use E-matching attributes such as `[grind =]` or `[grind →]` for conditional theorems
This is because conditional rewrites are disallowed; the homomorphism feature is used too early in grind to support them.
Instead, addition of tiny numbers can be mapped to truncating addition of natural numbers:
Examining grind's output, the problem is that it does not successfully register the contradiction that arises from the fact that (2:Tiny)+(1:Tiny)=(3:Tiny) is negated.
This is because the rewriting process does not rewrite literals like 2 (that is, OfNat.ofNat(α:=Tiny)2), which are left alone:
Difference lists, in which lists are represented as functions, provide an associative append operator.
Reasoning about them as lists using grind hom is very appealing; however, the default representation as a function doesn't have the right injectivity property:
In other words, Lean's function type includes functions that aren't really difference lists.
To use grind hom with difference lists, they need more structure to rule out these counterexamples:
Each time can be represented as the number of minutes since midnight.
This representation is not unique, because more than a day's worth of minutes wrap around to a time in the next day.
However, there is no rule that relates facts about the fields of Time to minute counts.
This leads to failures when using grind to reason about the fields:
One way around this is to use the defining equation of toMinutes as a grind hom rule.
Using this rule causes all applications of toMinutes to be rewritten in terms of the time's field values.
Unfortunately, this rule is applied in situations where one of the more specific rules would have been better.
It's a useful fallback, but it is not the best choice when the other rules could have been used.
In particular, it takes precedence over toMinutes_addMinutes, which causes this proof to fail:
