Automatically proving non-implications with invariants

Stream: Equational

[Anand Rao Tadipatri]

I've opened PR equational#526 that formalizes the ideas in Chapter 9 (a generalization of @Hernan Ibarra's original metatheorem) and automatically generates formal proofs for certain non-implications.

Ideas and feedback would be much appreciated.

Currently, the non-implications are of four kinds:

• ones generated by comparing the (ordered) lists of variables appearing on both sides of an equation
• ones generated by comparing the multisets of variables appearing on both sides of an equation
• ones generated by comparing the left-most elements appearing on both sides of an equation (originally suggested by @Daniel Weber in the same thread)
• ones generated by comparing the right-most elements appearing on both sides of an equation

More counter-examples of this kind can be generated by defining new instances of LiftingMagmaFamily in equational_theories/LiftingMagmaFamilies and manually adding them to the liftingMagmaFamilyInstances array in equational_theories/LiftingMagmaFamiliesCounterexamples. Suggestions along this direction would be particularly welcome.

[Anand Rao Tadipatri]

I'd like to add support for translating from FreeMagmaWithLaws (which is nicer to deal with mathematically) to a LiftingMagmaFamily (which is a custom-made definition for this particular use case). I've opened equational#634 and equational#635 towards this.

[Anand Rao Tadipatri]

This PR makes it possible to automatically generate further proofs of non-implications by

• defining a FreeMagmaWithLaws
• proving that the free magma on a set with decidable equality also has decidable equality
• updating the list of lifting magma family instances with the instance derived from this FreeMagmaWithLaws
• running lake exe generate_lifting_magma_family_counterexamples to generate the proofs of non-implications in this directory.

Unfortunately, the third step needs to be done manually at the moment. The obstacle in automating this is that the structure LiftingMagmaFamilyInstance has type Type 1, while the relevant Lean definitions like evalConst and MetaM only deal with objects in the Type universe.

[Terence Tao]

Would resolving equational#186 help with the final step? I vaguely recall @Mario Carneiro had some progress on this front, but I don't recall how far it got.

[Mario Carneiro]

it was merged already

[Mario Carneiro]

https://github.com/teorth/equational_theories/blob/84c00fd62ca990d464c720a6bb86e212ab3a7922/equational_theories/Completeness.lean#L142-L143

[Daniel Weber]

Oh, then I can finish equation_to_law and law_to_equation

[Mario Carneiro]

I would close equational#186 but I don't have the perms

[Mario Carneiro]

the relevant PR is equational#458

[Mario Carneiro]

@Daniel Weber what do you mean by this? I don't see why universe handling should explicitly appear in any other part of the project

[Daniel Weber]

I need to be able to use G ⊧ E for G : Type*

[Mario Carneiro]

Why?

[Terence Tao]

Closed now. Sorry for not noticing this earlier!

[Daniel Weber]

Mario Carneiro said:

Why?

Because we want to convert SomeEquation G to G ⊧ SomeLaw, and G can (and is, in implication theorems) be a Type* there

[Terence Tao]

Our positive implications are spelled using Type*, our negative implications are spelled using Type

[Mario Carneiro]

In both cases, you can go to/from law inequalities without universe munging

[Daniel Weber]

Mario Carneiro said:

In both cases, you can go to/from law inequalities without universe munging

Previously G ⊧ SomeLaw was defined only for G : Type, so it couldn't be used for G : Type*

[Mario Carneiro]

It would help to have a usage example for the tactics in equational#147

[Mario Carneiro]

is the idea that you want to change the theorem statement to a law inequality?

[Mario Carneiro]

(It's still defined that way BTW)

[Daniel Weber]

Mario Carneiro said:

is the idea that you want to change the theorem statement to a law inequality?

Not an equality, just convert the goal SomeEquation G to G ⊧ SomeLaw and vice versa

[Mario Carneiro]

Those are in both cases just unfolding definitions

[Mario Carneiro]

Also, keep in mind that Type* isn't actually a universe, it's syntax for Type u where u is bound somewhere else (and the location of this binding is somewhat relevant). If you write Type* twice you get two different universe variables

[Daniel Weber]

Mario Carneiro said:

(It's still defined that way BTW)

models, yes, but satisfiesPhi now has α G : Type*, while it previously had α G : Type

[Mario Carneiro]

this most likely is not relevant

[Mario Carneiro]

again, I'm not clear on your actual application

[Mario Carneiro]

can you give an example why would you need to do this

[Mario Carneiro]

is there a place in the code today that would use law_to_equation if it existed?

[Mario Carneiro]

This whole project will never involve manipulating a magma in a higher universe. The models_def' theorem is really not there to be used, it is there to check the box saying "yes, this actually is WLOG"

[Daniel Weber]

Mario Carneiro said:

is there a place in the code today that would use law_to_equation if it existed?

The proofs by duality could be something like law_to_equation (implies_iff_dual.1 (equation_to_law some_existing_theorem))

[Daniel Weber]

Mario Carneiro said:

This whole project will never involve manipulating a magma in a higher universe. The models_def' theorem is really not there to be used, it is there to check the box saying "yes, this actually is WLOG"

Not an explicit magmas, but all of the positive implications are on G : Type*

[Mario Carneiro]

that means that they can be instantiated at type 0

[Daniel Weber]

Yes, but for the other direction (from a law implication to a theorem on Type*) you need models_def'

[Mario Carneiro]

only if your counterexample uses a magma in a higher universe, which I assert will never happen in this project

[Daniel Weber]

There's no counterexample involved, it's for positive implications (although perhaps those aren't relevant anymore)

[Mario Carneiro]

For positive implications you have a theorem saying that LawN G -> LawM G for all magmas in all universes, so you specialize that to magmas in the lowest universe and hey presto that's the definition of LawN |= LawM

[Mario Carneiro]

no models_def' needed

[Mario Carneiro]

the only time you need models_def' is if you have a negative implication using a Type 2 magma or something

[Daniel Weber]

Mario Carneiro said:

For positive implications you have a theorem saying that LawN G -> LawM G for all magmas in all universes, so you specialize that to magmas in the lowest universe and hey presto that's the definition of LawN |= LawM

Yes, but for the other direction, where you already have LawN |= LawM (obtained using implies_iff_dual, for instance) and want to get LawN G -> LawM G for all magmas in all universes, don't you need models_def'?

[Mario Carneiro]

Isn't it good enough to have LawN |= LawM?

[Daniel Weber]

All of the theorems are LawN G -> LawM G, not LawN |= LawM, so presumably you'd also want it in that form

[Mario Carneiro]

maybe I'm confused why you want that then

[Mario Carneiro]

you will have to pack it back up in the end anyway

[Mario Carneiro]

My understanding of the discussion around the "final theorem" is that duality will be automatically handled as part of the closure algorithm

[Mario Carneiro]

so I think you should just leave it at having implies_iff_dual itself and not stating dual theorems unless you need them for other reasons

[Terence Tao]

One advantage of the unpacked form LawN G -> LawM G of the implication is that they can be described in a standalone Lean file with only minimal imports, e.g.,

class Magma (α : Type _) where
  op : α → α → α

infix:65 " ◇ " => Magma.op

abbrev Equation3511 (G: Type _) [Magma G] := ∀ x y : G, x ◇ y = x ◇ ((x ◇ y) ◇ x)

abbrev Equation3456 (G: Type _) [Magma G] := ∀ x : G, x ◇ x = x ◇ ((x ◇ x) ◇ x)

theorem Equation3511_implies_Equation3456 (G: Type _) [Magma G] (h: Equation3511 G) : Equation3456 G := by  sorry

In particular if we are to try to perform low-level exports of proofs as per equational#343 then we would presumably spell things in something like this form.

[Mario Carneiro]

I think this is good, for files which are doing direct proofs of implications

[Mario Carneiro]

Daniel seems to be talking about proving implications from other implications though

[Terence Tao]

Right, so for instance suppose we have the above implication 3511=>3456 in the Lean codebase in this unpacked form, and want to then use duality to get the dual implication 3511* => 3456* without having to repeat the proof. Wouldn't we have to convert the above theorem back to a LawN |= LawM statement in order to apply implies_iff_dual?

[Terence Tao]

(in this particular case the proof is just one rw, but let's pretend for sake of argument that the proof is actually dozens of rewrites.)

[Mario Carneiro]

(Assuming you don't fix this issue by just universe generalizing implies_iff_dual, which is certainly a possibility,) you could just have such theorems restrict to type 0

[Mario Carneiro]

since we know that it makes no difference, you should just go with whatever is easiest

[Daniel Weber]

Another alternative is to just write something like otherImplication (op G) as the proof and make sure that this is defeq to what we want (as happens in Mathlib for order dual), although that's defeq abuse

[Mario Carneiro]

Terence Tao said:

One advantage of the unpacked form LawN G -> LawM G of the implication is that they can be described in a standalone Lean file with only minimal imports, e.g.,

class Magma (α : Type _) where
  op : α → α → α

infix:65 " ◇ " => Magma.op

abbrev Equation3511 (G: Type _) [Magma G] := ∀ x y : G, x ◇ y = x ◇ ((x ◇ y) ◇ x)

abbrev Equation3456 (G: Type _) [Magma G] := ∀ x : G, x ◇ x = x ◇ ((x ◇ x) ◇ x)

theorem Equation3511_implies_Equation3456 (G: Type _) [Magma G] (h: Equation3511 G) : Equation3456 G := by  sorry

In particular if we are to try to perform low-level exports of proofs as per equational#343 then we would presumably spell things in something like this form.

Actually, looking at this again I think this is not an okay formulation, because it requires another definition of Magma, so it will clash with all the other definitions of Magma and produce incompatible theorems

[Terence Tao]

Until now we did not expect any higher Type to come into play, but earlier in this thread it was reported that we now have a Type 1 object LiftingMagmaFamilyInstance which may eventually require laws to be applied to higher type objects.

[Terence Tao]

Surely we can enclose the magma inside a namespace if necessary?

[Mario Carneiro]

that would avoid the name conflict but not the incompatibility

[Mario Carneiro]

because now every theorem is proving something about a different class of magma-things

[Terence Tao]

Or have a single very minimal common Magma.lean import containing just the first five lines of that code (This was in fact how the codebase started three weeks ago)

[Mario Carneiro]

yes that's better

[Mario Carneiro]

but you could also put models in that import

[Mario Carneiro]

If you actually want to reduce imports though such that 5 lines is looking like a lot, then you should probably do something about Init, which is massive

[Mario Carneiro]

you can do this by putting prelude at the top of the file and then importing only the files that you need

[Mario Carneiro]

every file implicitly begins with import Init unless you use prelude

[Terence Tao]

Sure but the proofs of the 10,657 forward implications in the codebase are all written using the LawN G -> LawM G spelling. Refactoring them all to LawN |= LawM would be tedious if we did not have an equation_to_law tactic.

[Terence Tao]

Sure, I just gave that code as an example, I'm sure with suitable effort we could find a much lighter version suitable for export purposes.

[Mario Carneiro]

I think the aggregator tool for the "final theorem" should just automatically handle all of the various spellings and convert as needed

[Terence Tao]

OK one could do all this only in the exporter front end, but why not have the capability for conversion in the Lean codebase natively?

[Mario Carneiro]

Daniel Weber said:

Another alternative is to just write something like otherImplication (op G) as the proof and make sure that this is defeq to what we want (as happens in Mathlib for order dual), although that's defeq abuse

It would be nice to have a term elab dually% EquationN_implies_EquationM which does something like this and then cleans up the statement to remove the ops

[Mario Carneiro]

this would also avoid the need to change universes

[Mario Carneiro]

If there are actually higher type objects being used, then I will stand corrected and these will need to use models_def' to squash them back down.

[Mario Carneiro]

But it's a heavy theorem (in the sense of using dependencies which I think will not be involved in most implication proofs) so I think it is better to avoid if possible

[Terence Tao]

I'm not strictly wedded to the tactic-based approach; any other metaprogramming device that allows one to easily pass back and forth between equations and laws would be fine. Duality is the most likely application, but there may be other use cases, for instance through these invariant-based approaches in which an implication between equations is disproven via some syntactic properties of the associated laws.

[Mario Carneiro]

You can pass between equations and laws by definitional unfolding, it just means that the theorem will be restricted to Type instead of Type*, which is actually fine

[Daniel Weber]

Mario Carneiro said:

You can pass between equations and laws by definitional unfolding, it just means that the theorem will be restricted to Type instead of Type*, which is actually fine

From a law to an equation isn't direct unfolding, you need to define an appropriate function

[Terence Tao]

@Anand Rao Tadipatri Will the use of LiftingMagmaFamilyInstance to disprove implications between laws require generating a magma in a Type 1 universe or higher?

[Mario Carneiro]

because if needed we can lift it back up to Type* because that's what models_def' does, but the final theorem needs everything to live in type 0 anyway so it's more a question of lowering all the stuff which isn't at type 0

[Mario Carneiro]

@Daniel Weber ?

[Terence Tao]

Laws are defined as basically a pair of elements of FreeMagma Nat. They aren't defeq to equations.

[Mario Carneiro]

I guess most of the theorems should be done over equations, not laws?

[Mario Carneiro]

There is a metaprogram which converts equations to laws which I wrote as part of the equation command rewrite

[Terence Tao]

All the raw implications are proven this equation-based way. All the metatheorems such as duality theorems are done using laws.

[Daniel Weber]

Mario Carneiro said:

Daniel Weber ?

What?

[Mario Carneiro]

I wanted you to clarify your statement but I think Terence Tao already did

[Mario Carneiro]

Currently the metaprogram is being used to prove some iff statement that equation generates, which should hopefully be the only place you have to interact with it

[Mario Carneiro]

Is there a lean file that enumerates and proves all duality theorems?

[Terence Tao]

in which case the equation_to_law and law_to_equation tactic could essentially be just syntactic sugar for invoking that metaprogram (modulo the issues with different type universes, but the hope was that the tactic would handle all this invisibly).

[Mario Carneiro]

I think you don't want to reuse the metaprogram, you should instead use the iff statements that it added to the environment, which have names like LawN.models_iff

[Mario Carneiro]

I think maybe there is room for another metaprogram which generates duality theorems in both equation and law form

[Mario Carneiro]

I should take a look at how implies_iff_dual works

[Mario Carneiro]

apparently implies_iff_dual is never used?

[Terence Tao]

Yeah precisely because we don't have equation_to_law and law_to_equation yet

[Mario Carneiro]

are there any theorems that want it?

[Terence Tao]

we could cut the number of implications we explicitly prove in the codebase by half once it's implemented

[Mario Carneiro]

okay so it's just being done by copy paste right now?

[Terence Tao]

it's more that the automated code that generate large numbers of implications or antiimplications by brute force don't do any reduction by duality

[Mario Carneiro]

oh but in that case you could just delete dual theorems and still claim them as proved since there is this duality thing

[Terence Tao]

we could in principle do the duality reduction right now because we haven't implemented the transitive completion + duality algorithm in Lean, it's only some external script (ruby, I think?) but for the "final" theorem we'd want to do that in Lean as well and that's where having internal dual metatheorems that link up with the equations and not the laws would be needed.

[Mario Carneiro]

right

[Mario Carneiro]

I think once that last step happens there will be no need to use it via some duality% or equation_to_law tactic, that's an interface meant for humans

[Terence Tao]

So that was one of the motivations for having equation_to_law and law_to_equation tactics. Of course there could be other metaprogramming solutions for this.

[Terence Tao]

Well these tactics could also be useful for pedagogical purposes. If we wanted to give a guided tour of proving various implications or anti-implications in Lean in a human readable fashion, having the ability to dualize in a human-readable way would be nice.

[Mario Carneiro]

The approach I'm currently thinking of is a Equations/Duality.lean file that proves LawN <-> LawM and EquationN G <-> EquationM G for every pair N,M of duals

[Terence Tao]

It's actually EquationN G <-> EquationM G.dual (not sure what the spelling is for the reversed magma of G) [EDIT: I guessed incorrectly, it's actually Op G]

[Mario Carneiro]

ah right, we have to do this on the implication level not the equation level

[Terence Tao]

In particular LawN and LawM need not satisfy any obvious implication between them (a few laws are equivalent to their dual, but those are in the minority).

[Mario Carneiro]

I would like a way to present this which doesn't put .dual in the theorem statement

[Terence Tao]

I think that would be challenging.

[Mario Carneiro]

I guess you can have IsDual LawN LawM and IsDual' EquationN EquationM which is then consumed by other theorems so that dualizing theorems don't have to work out how to actually dualize by recursion

[Mario Carneiro]

I will need to experiment a bit to see if that actually works in practice

[Mario Carneiro]

probably you still want a dually% tactic to hide the details of how to apply that

[Mario Carneiro]

Are there examples that would benefit from such a tactic today? When do we use an implication in a proof of another implication?

[Terence Tao]

This only solves the duality issue. There are other reasons why one would want to convert equations to laws, in particular to invoke the invariant-based metatheorems. For instance we know that LawX cannot imply LawY if LawX has each variable appear the same number of times on both sides of the equation, and LawY does not. In order to get from this to the existence of a magma that obeys EquationX but not EquationY one needs something like a law_to_equation tactic.

[Mario Carneiro]

So my general feeling on that is that in such cases you should have a metaprogram which generates all consequences of a rule like that, i.e. one file that proves a bunch of non-implications

[Mario Carneiro]

and while doing so it's not hard to present the theorem in any desired form, be it via equations or laws

[Terence Tao]

Yeah and that's what we currently do. But for pedagogical purposes I think a tactic that hides all the metaprogramming from view would be more explainable, especially to casual Lean users.

[Mario Carneiro]

Do you have an example?

[Terence Tao]

It allows for more self-contained looking proofs of implications or anti-implications obtained via metatheorems, without having to first run a large metaprogram

[Mario Carneiro]

Hm, it occurs to me that it would be nice to be able to use Facts for this example but it doesn't apply

[Mario Carneiro]

This proof is saying that for all equations A and B where A has the same-variable invariant and B doesn't, A does not imply B, which is exactly the same form as what you get from a Facts application, but there is no single magma G witnessing all of them (or is there?)

[Terence Tao]

https://github.com/teorth/equational_theories/pull/526/files#diff-e246bbd4771fc9a4732cf821dcc7559009178141a90738e7e665ef08231046e2 is an example of a large number of anti-implications generated from a metatheorem . Admittedly no law_to_equation tactic was needed here, but it could conceivably have been deployed to make the proof conceptually more human-readable

[Terence Tao]

In this particular example one can take G to be the free abelian group on countably many generators

[Mario Carneiro]

right, this proof strategy looks about what I would suggest, my only proposals would be to maybe make it a bit more presentable with some specialized syntax

[Terence Tao]

It's an example of a LiftingMagmaFamily which can more generally establish a lot of other anti-implications of this type. It's true that any specific anti-implication of this type can be achieved using a specific magma, but the point is that one can hide these implementation details and work with the more abstract metatheorem

[Mario Carneiro]

I think law_to_equation is actually code for "apply LawN.models_iff, possibly behind some syntax or typeclass to keep it clean"

[Terence Tao]

yeah basically. It could be almost entirely syntactic sugar.

[Mario Carneiro]

Is there a way to get these results presented as double implications to avoid the quadratic blowup?

[Terence Tao]

It is indeed less relevant now when the number of outstanding implications is in the low hundreds and we are not expecting a large number of contributions from the general public. When I proposed it, there were still tens of thousands of open implications, and it was not clear that ATPs would clear out so many. I was anticipating a very crowdsourced phase in which we could get members of the public with relatively little Lean experience contributing short individual proofs, and so we would want to give them as user-friendly tools as possible. This is not really the case any more, but still I think it wouldn't hurt to have these tactics in the codebase.

[Mario Carneiro]

sure, for a "teaching tactic" it's a lot easier to design

[Mario Carneiro]

my thoughts are mostly in the direction of having a complete proof of 22 million implications with the minimum stress on lean (and also less low entropy text in files)

[Terence Tao]

I think there is some scope of refactoring the LiftingMagmaFamily stuff using Facts to compress things substantially. As it turns out, we aren't actually making significant use of this particular tool for the main implication graph (the finite magma examples basically took care of all these implications beforehand), they are mostly being used to demonstrate implications involving the equations past the standard 4692 currently.

[Terence Tao]

OK. Then I think we aren't really in disagreement, we are just focused on slightly different end goals, both of which are worthwhile.

[Mario Carneiro]

Do you know if the existing magma examples also furnish disproofs for the extra equations if you just evaluate them to see what holds or doesn't?

[Mario Carneiro]

I wouldn't be surprised if there is some kind of robertson-seymour-like result here where some finite counterexamples are actually complete for these lifting magma families, at least for bounded variable number

[Terence Tao]

My guess is that they do, it's just that the finite magma examples weren't run on those extra equations. We do have some implications which we know for sure that they can only be disproven using infinite magma examples, but they are rather subtle. Some of the constructions based on confluence may fall under this category (there was some technical debate about saturation that I didn't really follow that may be relevant here).

[Terence Tao]

in principle every anti-implication can be proven by at least one lifting magma family because of abstract nonsense, the problem is that most of these families do not have any tractable (or even decidable) description.

[Mario Carneiro]

Ah, so this suggests maybe an additional generalization of Facts, where the thing that links the two sides is not a specific magma but rather a lifting magma family

[Mario Carneiro]

and I guess a magma is really just a special kind of lifting magma family (which is presumably the content of your "abstract nonsense")

[Terence Tao]

It's more like a lifting magma family is a universal object in some category of magmas obeying some specified theory, but yeah.

[Mario Carneiro]

Oh yes, looking at the proof now I see that it does actually construct a specific magma G ℕ which witnesses all the invariant-preserving equations

[Anand Rao Tadipatri]

Terence Tao said:

Would resolving equational#186 help with the final step? I vaguely recall Mario Carneiro had some progress on this front, but I don't recall how far it got.

No, I think this is an issue with the definitions in Lean itself. I've asked a question on #lean4 with a minimized example to check if there's a way around this.

[Anand Rao Tadipatri]

Terence Tao said:

Anand Rao Tadipatri Will the use of LiftingMagmaFamilyInstance to disprove implications between laws require generating a magma in a Type 1 universe or higher?

The magma generated using a LiftingMagmaFamilyInstance is not necessarily in Type 1 or higher universes (and in all the cases so far, the model is in Type).

[Terence Tao]

Oh, okay. So the appearance of higher type Magmas in our codebase is still purely a future theoretical possibility at present.

[Mario Carneiro]

Mario Carneiro said:

The approach I'm currently thinking of is a Equations/Duality.lean file that proves LawN <-> LawM and EquationN G <-> EquationM G for every pair N,M of duals

I've implemented this (ish) In equational#769, so in particular all duality claims are now being checked by lean

[Andrés Goens]

cool, it's a nice approach to define a new dual command and just give them to Lean as annotations! I put off/(had given up on) doing this because I didn't want to write the meta code for doing all of that directly in meta, and didn't think of this solution