17.12.1. Integrating grind's features.

This example demonstrates how the various submodules of grind are seamlessly integrated. In particular we can

• instantiate theorems from the library, using custom patterns,

• perform case splitting,

• do linear integer arithmetic reasoning, including modularity conditions, and

• do Gröbner basis reasoning all without providing explicit instructions to drive the interactions between these modes of reasoning.

For this example we'll begin with a "mocked up" version of the real numbers, and the sin and cos functions. Of course, this example works without any changes using Mathlib's versions of these!

Our first step is to tell grind to "put the trig identity on the whiteboard" whenever it sees a goal involving sin or cos:

Note here we use two different patterns for the same theorem, so the theorem is instantiated even if grind sees just one of these functions. If we preferred to more conservatively instantiate the theorem only when both sin and cos are present, we could have used a multi-pattern:

For this example, either approach will work.

Because grind immediately notices the trig identity, we can prove goals like this:

Here grind:

• Notices cos x and sin x, so instantiates the trig identity.

• Notices that this is a polynomial in CommRing R, so sends it to the Gröbner basis module. No calculation happens at this point: it's the first polynomial relation in this ring, so the Gröbner basis is updated to [(cos x)^2 + (sin x)^2 - 1].

• Notices that the left and right hand sides of the goal are polynomials in CommRing R, so sends them to the Gröbner basis module for normalization.

• Since their normal forms modulo (cos x)^2 + (sin x)^2 = 1 are equal, their equivalence classes are merged, and the goal is solved.

We can also do this sort of argument when congruence closure is needed:

As before, grind instantiates the trig identity, notices that (cos x + sin x)^2 and 2 * cos x * sin x + 1 are equal modulo (cos x)^2 + (sin x)^2 = 1, puts those algebraic expressions in the same equivalence class, and then puts the function applications f((cos x + sin x)^2) and f(2 * cos x * sin x + 1) in the same equivalence class, and closes the goal.

Notice that we've used arbitrary function f : R → Nat here; let's check that grind can use some linear integer arithmetic reasoning after the Gröbner basis steps:

Here grind first works out that this goal reduces to 4 * x ≠ 2 + x for some x : Nat (i.e. by identifying the two function applications as described above), and then uses modularity to derive a contradiction.

Finally, we can also mix in some case splitting:

example (f : R → Nat) : max 3 (4 * f ((cos x + sin x)^2)) ≠ 2 + f (2 * cos x * sin x + 1) := by
  grind

As before, grind first does the instantiation and Gröbner basis calculations required to identify the two function applications. However the cutsat algorithm by itself can't do anything with max 3 (4 * x) ≠ 2 + x. Next, instantiating Nat.max_def (automatically, because of an annotation in the standard library) which states max n m = if n ≤ m then m else n, we then case split on the inequality. In the branch 3 ≤ 4 * x, cutsat again uses modularity to prove 4 * x ≠ 2 + x. In the branch 4 * x < 3, cutsat quickly determines x = 0, and then notices 4 * 0 ≠ 2 + 0.

This has been, of course, a quite artificial example! In practice this sort of automatic integration of different reasoning modes is very powerful: the central "whiteboard" which tracks instantiated theorems and equivalence classes can hand off relevant terms and equalities to the appropriate modules (here, cutsat and Gröbner bases), which can then return new facts to the whiteboard.

17.12.2. if-then-else normalization

This example is a showcase for the "out of the box" power of grind. Later examples will explore adding @[grind] annotations as part of the development process, to make grind more effective in a new domain. This example does not rely on any of the algebra extensions to grind, we're just using:

• instantiation of annotated theorems from the library,

• congruence closure, and

• case splitting.

The solution here builds on an earlier formalization by Chris Hughes, but with some notable improvements:

• the verification is separate from the code,

• the proof is now a one-liner combining fun_induction and grind,

• the proof is robust to changes in the code (e.g. swapping out HashMap for TreeMap) as well as changes to the precise verification conditions.

fail to show termination for
  IfExpr.normalize
with errors
failed to infer structural recursion:
Cannot use parameter assign:
  the type HashMap Nat Bool does not have a `.brecOn` recursor
Cannot use parameter #2:
  failed to eliminate recursive application
    normalize assign (a.ite (b.ite t e) (c.ite t e))


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
              #1 x2
1) 1296:27-45  =  <
2) 1297:27-45  =  <
3) 1299:4-52   =  ?
4) 1303:16-50  ?  _
5) 1304:16-51  _  _
6) 1306:16-50  _  _

#1: assign

Please use `termination_by` to specify a decreasing measure.

17.12.3. IndexMap

In this section we'll build an example of a new data structure and basic API for it, illustrating the use of grind.

The example will be derived from Rust's indexmap data structure.

IndexMap is intended as a replacement for HashMap (in particular, it has fast hash-based lookup), but allowing the user to maintain control of the order of the elements. We won't give a complete API, just set up some basic functions and theorems about them.

The two main functions we'll implement for now are insert and eraseSwap:

• insert k v checks if k is already in the map. If so, it replaces the value with v, keeping k in the same position in the ordering. If it is not already in the map, insert adds (k, v) to the end of the map.

• eraseSwap k removes the element with key k from the map, and swaps it with the last element of the map (or does nothing if k is not in the map). (This semantics is maybe slightly surprising: this function exists because it is an efficient way to erase element, when you don't care about the order of the remaining elements. Another function, not implemented here, would preserve the order of the remaining elements, but at the cost of running in time proportional to the number of elements after the erased element.)

Our goals will be:

• complete encapsulation: the implementation of IndexMap is hidden from the users, and the theorems about the implementation details are private.

• to use grind as much as possible: we'll preferring adding a private theorem and annotating it with @[grind] over writing a longer proof whenever practical.

• to use auto-parameters as much as possible, so that we don't even see the proofs, as they're mostly handled invisibly by grind.

To begin with, we'll write out a skeleton of what we want to achieve, liberally using sorry as a placeholder for all proofs. In particular, this version makes no use of grind.

Let's get started. We'll aspire to never writing a proof by hand, and the first step of that is to install auto-parameters for the size_keys and WF field, so we can omit these fields whenever grind can prove them. While we're modifying the definition of IndexMap itself, lets make all the fields private, since we're planning on having complete encapsulation.

Let's give grind access to the definition of size, and size_keys private field:

Our first sorrys in the draft version are the size_keys and WF fields in our construction of def emptyWithCapacity. Surely these are trivial, and solvable by grind, so we simply delete those fields:

Our next task is to deal with the sorry in our construction of the GetElem? instance:

The goal at this sorry is

m : IndexMap α β
a : α
h : a ∈ m
⊢ m.indices[a] < m.values.size

Let's try proving this as a stand-alone theorem, via grind, and see where grind gets stuck. Because we've added grind annotations for size and size_keys already, we can safely reformulate the goal as:

This fails, and looking at the message from grind we see that it hasn't done much:

[grind] Goal diagnostics ▼
  [facts] Asserted facts ▼
    [prop] a ∈ m
    [prop] m.size ≤ (indices m)[a]
    [prop] m.size = (values m).size
  [eqc] True propositions ▼
    [prop] m.size ≤ (indices m)[a]
    [prop] a ∈ m
  [eqc] Equivalence classes ▼
    [] {Membership.mem, fun m a => a ∈ m}
    [] {m.size, (values m).size}
  [ematch] E-matching patterns ▼
    [thm] size.eq_1: [@size #4 #3 #2 #1 #0]
    [thm] HashMap.contains_iff_mem: [@Membership.mem #5 (HashMap _ #4 #3 #2) _ #1 #0]
  [cutsat] Assignment satisfying linear constraints ▼
    [assign] m.size := 0
    [assign] (indices m)[a] := 0
    [assign] (values m).size := 0

An immediate problem we can see here is that grind does not yet know that a ∈ m is the same as a ∈ m.indices. Let's add this fact:

However this proof is going to work, we know the following:

• It must use the well-formedness condition of the map.

• It can't do so without relating m.indices[a] and m.indices[a]? (because the later is what appears in the well-formedness condition).

• The expected relationship there doesn't even hold unless the map m.indices satisfies LawfulGetElem, for which we need [LawfulBEq α] and [LawfulHashable α].

Let's configure things so that those are available:

and then give grind one manual hint, to relate m.indices[a] and m.indices[a]?: