16.14. Homomorphism Annotations🔗

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 (f x y).toU = g x.toU y.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.ofNat n : T).toU = h n.

• Conditionals can be translated by providing a theorem that shows that (if p then x else y).toU = if p then x.toU else y.toU.

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).

When debugging, homomorphism rewrites can be observed by setting trace.grind.hom or trace.grind.hom.pred to true.

trace.grind.hom

trace.grind.hom.pred

invalid `[grind hom]` theorem, `toNat_add_lt_4_eq_add` is conditional: hypothesis
  x.toNat + y.toNat < 4
is 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

`grind` failed
grind.1h:¬2 + 1 = 3h_1:toNat 1 + toNat 2 ≤ 3⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] ¬2 + 1 = 3
[prop] ¬min (toNat 1 + toNat 2) 3 = toNat 3
[prop] toNat 1 ≤ 3
[prop] toNat 2 ≤ 3
[prop] toNat 3 ≤ 3
[prop] min (toNat 1 + toNat 2) 3 = if toNat 1 + toNat 2 ≤ 3 then toNat 1 + toNat 2 else 3
[prop] toNat 1 + toNat 2 ≤ 3
[eqc] True propositions
[prop] toNat 1 ≤ 3
[prop] toNat 2 ≤ 3
[prop] toNat 3 ≤ 3
[prop] toNat 1 + toNat 2 ≤ 3
[eqc] False propositions
[prop] min (toNat 1 + toNat 2) 3 = toNat 3
[prop] 2 + 1 = 3
[eqc] Equivalence classes
[eqc] {min (toNat 1 + toNat 2) 3, toNat 1 + toNat 2}
[eqc] {if toNat 1 + toNat 2 ≤ 3 then toNat 1 + toNat 2 else 3}
[cases] Case analyses
[cases] [1/2]: if toNat 1 + toNat 2 ≤ 3 then toNat 1 + toNat 2 else 3
[cases] source: E-matching `Nat.min_def`
[ematch] E-matching patterns
[thm] Rat.min_def: [@min `[Rat] `[Rat.instMin] #1 #0]
[thm] Int.min_def: [@min `[Int] `[Int.instMin] #1 #0]
[thm] Nat.min_def: [@min `[Nat] `[instMinNat] #1 #0]
[cutsat] Assignment satisfying linear constraints
[assign] toNat 1 := 0
[assign] toNat 2 := 0
[assign] toNat 3 := 1
[assign] min (toNat 1 + toNat 2) 3 := 0
[assoc] Operator `min`
[basis] Basis
[_] min (toNat 1 + toNat 2) 3 = toNat 1 + toNat 2
[properties] Properties
[_] commutative
[_] idempotent

[grind] Diagnostics
[ematch] E-matching Diagnostics
[thm] Theorem Instance Count
[thm] Nat.min_def ↦ 1