When an operator is associative, grind can efficiently rewrite terms that contain the operator to a normal form, making it easier to prove equalities that involve the operator.
This rewriting can make use of further facts about the operator, such as the fact that it is commutative or idempotent, or that certain values are identities.
Rewriting occurs both when adding terms to the “whiteboard” and in response to facts added by other solvers.
This solver is controlled using the ac flag, and it is on by default.
The acSteps option, which defaults to 1000, controls how many ac rewriting steps are allowed.
The ac solver can reason about strings.
It's common for string-processing code to compute a prefix, and then later append further values.
Using ac, these can be reasoned about more conveniently:
example (dir file p) (h : dir ++ "/" = p) :
dir ++ ("/" ++ file) = p ++ file := dir:Stringfile:Stringp:Stringh:dir ++ "/" = p⊢ dir ++ ("/" ++ file) = p ++ file All goals completed! 🐙
The normal forms used by the ac solver depend on the properties that have been registered for the operator in question.
Associative operators are normalized by reducing nested trees of the operator to lists of operands.
If op is associative, then the normal form of both op (op x y) z and op x (op y z) is [x, y, z].
Operators that are associative and commutative are normalized by sorting the operand lists.
If op is associative and commutative, then the normal form of both op z (op x y) and op (op x z) y is [x, y, z].
In other words, the normal form is a multiset.
If the operator is idempotent, then runs of duplicate elements are collapsed in the operand list.
If op is associative and idempotent, then the normal form of op x (op x y) is [x, y], but the normal form of op (op x y) x is still [x, y, x].
This collapsing occurs after sorting the list if the operator is commutative, so if op is associative, commutative, and idempotent, then the normal form of op (op x y) x is also [x, y].
In other words, the normal form of an associative, commutative, and idempotent operator is a set.
If the operator has a unit, then it is removed from the normal form.
That is, if u is a unit of the associative operator op, then the normal form of op x (op u y) is [x, y].
The ac solver can be extended to support new operators by providing an instance of Std.Associative for the operator.
Instances of Std.Commutative, Std.IdempotentOp, and Std.LawfulIdentity further extend its capabilities by identifying more terms.
Associative op indicates op is an associative operation,
i.e. (a ∘ b) ∘ c = a ∘ (b ∘ c).
Instance Constructor
Std.Associative.mk.{u}
Methods
assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)
An associative operation satisfies (a ∘ b) ∘ c = a ∘ (b ∘ c).
Commutative op says that op is a commutative operation,
i.e. a ∘ b = b ∘ a.
Instance Constructor
Std.Commutative.mk.{u}
Methods
comm : ∀ (a b : α), op a b = op b a
A commutative operation satisfies a ∘ b = b ∘ a.
IdempotentOp op indicates op is an idempotent binary operation.
i.e. a ∘ a = a.
Instance Constructor
Std.IdempotentOp.mk.{u}
Methods
idempotent : ∀ (x : α), op x x = x
An idempotent operation satisfies a ∘ a = a.
LawfulIdentity op o indicates o is a verified left and right
identity of op.
Instance Constructor
Std.LawfulIdentity.mk.{u}
Extends
While extending the ac solver, it can be useful to observe its operation.
The option trace.grind.ac, as well as the more specific options trace.grind.ac.assert, trace.grind.ac.internalize, and trace.grind.ac.basis, can be used to observe its internal behavior.
In particular, trace.grind.ac.assert displays the results of normalization that are added to the “whiteboard.”
trace.grind.ac
Default value: false
enable/disable tracing for the given module and submodules
trace.grind.ac.assert
Default value: false
enable/disable tracing for the given module and submodules
trace.grind.ac.internalize
Default value: false
enable/disable tracing for the given module and submodules
trace.grind.ac.basis
Default value: false
enable/disable tracing for the given module and submodules
Flags tracks a set of Boolean flags, each of which corresponds to a bit position.
Each flag is either set or clear, and all flags are clear when the bit value is 0.
The union of two sets of flags is found by taking the bit-wise OR of their bit representations.
structure Flags where
bits : Nat
namespace Flags
def union (a b : Flags) : Flags := ⟨a.bits ||| b.bits⟩
def none : Flags := ⟨0⟩
The union operation on flags is associative, commutative, and idempotent, and Flags.none is an identity:
instance : Std.Associative union where
assoc x y z := x:Flagsy:Flagsz:Flags⊢ (x.union y).union z = x.union (y.union z) x:Flagsy:Flagsz:Flags⊢ x.bits ||| y.bits ||| z.bits = x.bits ||| (y.bits ||| z.bits); All goals completed! 🐙
instance : Std.Commutative union where
comm x y := x:Flagsy:Flags⊢ x.union y = y.union x x:Flagsy:Flags⊢ x.bits ||| y.bits = y.bits ||| x.bits; All goals completed! 🐙
instance : Std.IdempotentOp union where
idempotent x := x:Flags⊢ x.union x = x All goals completed! 🐙
instance : Std.LawfulIdentity union none where
left_id a := a:Flags⊢ none.union a = a All goals completed! 🐙
right_id a := a:Flags⊢ a.union none = a All goals completed! 🐙
With these instances, the ac solver can dispatch all of the following goals.
In the second example, idempotency can only be used due to commutativity, because the two identical arguments are not adjacent in the original term.
example : union a (union b c) = union (union c a) b := a:Flagsb:Flagsc:Flags⊢ a.union (b.union c) = (c.union a).union b All goals completed! 🐙
example : union (union a b) a = union a b := a:Flagsb:Flags⊢ (a.union b).union a = a.union b All goals completed! 🐙
example : union a none = a := a:Flags⊢ a.union none = a All goals completed! 🐙
example :
union (union a b) (union none (union b c))
= union a (union b c) := a:Flagsb:Flagsc:Flags⊢ (a.union b).union (none.union (b.union c)) = a.union (b.union c)
All goals completed! 🐙
The negated normal-form equality that is added to the context can be seen using trace.grind.ac.assert:
set_option trace.grind.ac.assert true in
example : union (union a b) a = union a (union b none) := a:Flagsb:Flags⊢ (a.union b).union a = a.union (b.union none) All goals completed! 🐙
A difference list is a clever representation of lists as functions that avoids the quadratic overhead of appending to the end of lists.
Because Lean supports efficient arrays, they are typically not useful in day-to-day code, but they effectively demonstrate how to extend the ac solver.
A difference list is a function from lists to lists.
The list xs is represented by a function that, when applied to ys, returns xs ++ ys.
def DList α := List α → List α
The empty list is the identity function. An item is added to the beginning of a list by creating a function that adds the element. Appending two lists is function composition.
def DList.empty : DList α := id
def DList.cons (x : α) (xs : DList α) : DList α :=
fun ys => (x :: xs ys)
instance : Append (DList α) where
append xs ys := xs ∘ ys
The proofs that appending two difference lists is associative and that the empty difference list is a left and right identity of the append operator succeed by reflexivity because definitional equality includes the β and η laws for functions:
instance : Std.Associative (α := DList α) (· ++ ·) where
assoc xs ys zs := α:Type u_1xs:DList αys:DList αzs:DList α⊢ xs ++ ys ++ zs = xs ++ (ys ++ zs) All goals completed! 🐙
instance : Std.LawfulIdentity (α := DList α) (· ++ ·) .empty where
left_id xs := α:Type u_1xs:DList α⊢ DList.empty ++ xs = xs All goals completed! 🐙
right_id xs := α:Type u_1xs:DList α⊢ xs ++ DList.empty = xs All goals completed! 🐙
Given these instances, grind can dispatch many proofs.
variable (a b c d x y : DList Nat)
Because append is associative, terms can be rebracketed and units vanish:
example : ((a ++ b) ++ c) ++ d = a ++ (b ++ (c ++ d)) := a:DList Natb:DList Natc:DList Natd:DList Natx:DList Naty:DList Nat⊢ a ++ b ++ c ++ d = a ++ (b ++ (c ++ d)) All goals completed! 🐙
example : (a ++ .empty) ++ (.empty ++ b) = a ++ b := a:DList Natb:DList Natc:DList Natd:DList Natx:DList Naty:DList Nat⊢ a ++ DList.empty ++ (DList.empty ++ b) = a ++ b All goals completed! 🐙
example : (.empty ++ .empty : DList Nat) = .empty := a:DList Natb:DList Natc:DList Natd:DList Natx:DList Naty:DList Nat⊢ DList.empty ++ DList.empty = DList.empty All goals completed! 🐙
While simplification lemmas could easily solve those problems, grind's ac solver allows a greater degree of flexibility.
To use the hypotheses in these examples, it would not be sufficient to just rewrite goals and hypotheses to a normal form that reassociated an associative operator to the right:
example (h : a ++ b = x) : a ++ (b ++ c) = x ++ c := a:DList Natb:DList Natc:DList Natd:DList Natx:DList Naty:DList Nath:a ++ b = x⊢ a ++ (b ++ c) = x ++ c All goals completed! 🐙
example (h : a ++ b = x) :
(a ++ .empty) ++ (b ++ c) = x ++ c := a:DList Natb:DList Natc:DList Natd:DList Natx:DList Naty:DList Nath:a ++ b = x⊢ a ++ DList.empty ++ (b ++ c) = x ++ c All goals completed! 🐙
example (h₁ : a ++ b = x) (h₂ : x ++ c = y) :
a ++ (b ++ c) = y := a:DList Natb:DList Natc:DList Natd:DList Natx:DList Naty:DList Nath₁:a ++ b = xh₂:x ++ c = y⊢ a ++ (b ++ c) = y All goals completed! 🐙
Because appending difference lists is not commutative, order still matters:
example : a ++ b = b ++ a := a:DList Natb:DList Natc:DList Natd:DList Natx:DList Naty:DList Nat⊢ a ++ b = b ++ a All goals completed! 🐙
The ac solver does not apply to some built-in operators, namely And, Or, and Iff.
They are better served by other grind features.
When the operand type has Lean.Grind.CommRing and/or Lean.Grind.CommSemiring instances, ac omits its rules for certain operators that are usually better solved by the ring solver, namely +, -, *, /, and ^.