LawsComplete by proof term generation

Stream: Equational

[Mario Carneiro]

@Joachim Breitner I converted your algorithm to a hybrid proof term generation and refl proof, and it is way faster and cheaper now: equational#784 . In particular this does the proof without any dependency on native_decide.

[Joachim Breitner]

Nice work! I assume a large part of the speedup is that now the findMagmaLaw search happens at elaboration time, and the proof term contains that result already. That’s a notable benefit of term generation over proof by reflection – it’s easier to include such “certificates” in the middle of the computation.

[Joachim Breitner]

This is the part that’s still by refl:

    let h : Q(laws[$i] = $l') := (q(Eq.refl $l') :)

did you benchmark if this was slower than a proof object that shows that $l; is in laws, or was it fast enough and you didn’t bother?

[Mario Carneiro]

the latter

[Joachim Breitner]

In the two examples where I saw you apply this method, you proved custom lemmas like TestLawsBody.mk3 or TestFreeMagmas.succ to build the proof terms from.

Squinting enough, these seem to be a bit similar to the equational lemmas for the functions. So I wonder if one could achieve something similar, with much less manual effort, by using the simplifier (or a variant of it, “simp_cbv” or so, that is only rewriting in an evaluation context) to perform the calculation at elaboration time and produce a suitable proof term.

Would this yield similar performance characteristics (both at elab time and kernel checking time), or is that inherently worse? (Ignoring the “elab-time findMagmaLaw trick for now, although that could probably be done as well, using a simproc or rewrite rules with auto-param or so.)

[Joachim Breitner]

Also, you write

#time says it takes 7 seconds, but because it is checked twice as written (once in the kernel and once in the elaborator)

where is the proof checked in the elaborator in your code? Is there an unnecessary Meta.check in by_elab or in the qq library?

[Mario Carneiro]

I'm not sure exactly where, my general impression is that this happens in any tactic so it must be the tactic / MetaM infrastructure

[Mario Carneiro]

I'm sure it's not in qq

[Joachim Breitner]

Hmm, don’t think it’s general – the decideFin! tactic that I added in the repo does not go through any hoops to avoid the meta-time check. by_elab also looks fine.

[Mario Carneiro]

maybe you could try doing some tests on artificial versions of the example

[Joachim Breitner]

I’ll have a look

[Joachim Breitner]

With set_option debug.skipKernelTC true I can change parts of the proof to bogus values and nothing complains. Looks like the meta-program simply takes its time, but nothing is actually done twice?

[Mario Carneiro]

my experience is that with that option on it takes 3 seconds instead of 6

[Joachim Breitner]

Right – but that could simply mean that the elab code and the kernel checking roughly take the same time; it doesn't necessarily mean that any work is duplicated. (And at least so far I don’t see evidence for that, so all good!)

[Amir Livne Bar-on]

Will it be easy to convert this to also generate a list of laws? That would be useful for proving e.g. the counting lemmas. (In my attempt before I ran into issues with polymorphic induction)

[Mario Carneiro]

The code already produces such a list (or rather, it assembles the list that already exists in the equations files)

[Mario Carneiro]

I'm thinking of making the "canonical" criterion a bit less precise:

/--
Checks whether a magma law is canonical:
* Variables are canonically labeled
* `lhs < rhs` (with the exception of `0 ≃ 0`)
* The symmetric law did not come first
-/
def Law.MagmaLaw.IsCanonical (l : Law.MagmaLaw Nat) : Prop :=
  l.IsCanonicalLabel ∧
  (l.lhs.comp l.rhs = .lt ∨ l.lhs = .Leaf 0) ∧
  l.symm.canonicalize.comp l ≠ .lt

The problem with this criterion is that it's not obvious that either the original or the flipped version of the equation can be made canonical by relabeling, because both the second and third conditions are changed by flipping. Empirically I have observed though that it is impossible to have l.symm.canonicalize > l and yet l.lhs > l.rhs, but my attempts to prove it have failed because canonicalization is a complicated operation with nontrivial effects on the ordering. I can sidestep this issue by just not using this shortcut and considering both l.lhs < l.rhs and l.lhs > l.rhs cases, using only the canonicalization ordering to prune them. Doing this increases the runtime of the check from 7 seconds to 16 seconds.

[Mario Carneiro]

Actually even this isn't enough, because if l.symm.canonicalize = l then we still don't know that l is of the form w = w. In fact this can happen: x * y = x * z is equal to its own symmetric version, but it is not of the form w = w.

[Amir Livne Bar-on]

Mario Carneiro said:

The code already produces such a list (or rather, it assembles the list that already exists in the equations files)

My thought was to generate the list and not base it on the files. If there was code that returned a List or a Finset or an iterator, we could prove theorems about the set of equations (for example, its size) without running it.

[Amir Livne Bar-on]

The way FreeMagma.comp is written looks a bit strange to me. IMO the natural thing is to have a function FreeMagma α → FreeMagma Unit × List α, and compare by lexicographic order on that. Then you're guaranteed that laws with smaller RHS shape are never canonical, and laws with smaller LHS shape are always canonical.

[EDIT: assuming the variables at the leaves are in canonical order]

[Amir Livne Bar-on]

(I've a branch where I used Tree Unit for the shape, since the Enumerative.Catalan module counts that natively, but FreeMagma Unit is equivalent)

[Mario Carneiro]

Yes, that is in the LawsComplete file. It is a prerequisite to stating the theorem that all laws up to a certain size are in "the list", we need "the list" to say this

[Mario Carneiro]

Re: FreeMagma.comp, I think it's equivalent to what you said?

[Mario Carneiro]

the "shape" comparison happens inside Law.MagmaLaw.comp

[Amir Livne Bar-on]

It's equivalent, but this formulation could make it easier to prove that l.symm.canonicalize > l is incompatible with l.lhs > l.rhs

[Mario Carneiro]

can you elaborate?

[Mario Carneiro]

Let's suppose it's defined like that

[Mario Carneiro]

how does it help?

[Mario Carneiro]

I tried to prove that fun l => l.map f is a monotone function if f is, but it doesn't seem to be true

[Amir Livne Bar-on]

If l.symm.canonicalize > l, it is either because l.rhs.forks > l.lhs.forks, or they're equal l.rhs.shape > l.lhs.shape, or they're equal and l.rhs.leaves > l.lhs.leaves. In the first case obviously l.rhs > l.lhs, and the other two cases are exactly phrasing the comparison as lex order on (shape, leaves).

[Mario Carneiro]

oh but l.lhs > l.rhs is using this mixed comparison

[Mario Carneiro]

it's not shape-then-leaves

[Mario Carneiro]

perhaps that was a mistake

[Amir Livne Bar-on]

I can't think of an example where the order as implemented in FreeMagma.comp contradicts this, since we first compare the number of forks

[Mario Carneiro]

is that correct? Doing forks comparison at every node

[Amir Livne Bar-on]

Oh I see, so it would have ((x * x) * x) * (x * x) < (x * (x * (x * x))) * x, which is not the same as the order on shapes

[Amir Livne Bar-on]

(that would mean that once we reach high enough order the set of laws will differ; so really not the same theorem)

[Mario Carneiro]

wait, so which is correct?

[Mario Carneiro]

correct meaning whatever was implemented in the original enumeration

[Amir Livne Bar-on]

I managed to confuse myself. There is only one order on shapes implemented anywhere. (I imagined another one before but it's complicated and not used)

The order on terms is different, in the generating scripts it's based strictly on tree shapes then leaves.

[Amir Livne Bar-on]

For instance y(x(xx)) < x((xx)x)

[Mario Carneiro]

when are forks comparisons involved?

[Mario Carneiro]

is it just once at the top level, once for each side of the equation or once at every node?

[Amir Livne Bar-on]

The (original) generation code doesn't have a comparison function, but there's an implicit order based on what is generated first. Then it checks all $2 \cdot n!$ permutations of variables and orders to eliminate equivalents. (We played around with the order a bit in the first day, so it was useful to have exhaustive equivalence check)

Equations are enumerated by: total order, lhs order, lhs shape, rhs shape, lex order on the leaves.
Enumeration of shapes is by left fork order, left shape, right shape. The implied order is exactly FreeMagma.comp on FreeMagma Unit.

[Amir Livne Bar-on]

A more efficient implementation of the same ordering appears in the newer script
find_equation_id.py, this script also represents an equation as (shape, shape, leaves) which was more efficient than separating to lhs and rhs expressions.

[Mario Carneiro]

Success! equational#789 proves the completeness of the generation code, including the analysis of the canonicalization function and using the original ordering. :tada:

[Joachim Breitner]

Very nice! Glad I didn't give this a more serious attempt, I wouldn't have managed within reasonable time.

I'd say that's the proper theorem, I think the prime should go on the other one (or some other name)

[Floris van Doorn]

equational#789