A final end-to-end theorem in Lean

Stream: Equational

[Joachim Breitner]

Overnight, I thought a bit more about what an end-to-end theorem in lean could look like. Put differently, what is a “minimal” set of definitions and theorems that one would have to manually inspect and which convey the end result of this project, all checked in lean

This would be my proposal. For defs with :=, the actual value on the right-hand side is not necessary for the skeptical human to check, and would likely be filled by a macro or command.

def n  : Nat := …
/-- all our laws, in one definition -/
def law  : (Fin n) → NatMagmaLaw := …
/-- a proof that this contains all laws we claim to look at -/
theorem law_complete : ∀ (l : NatMagmaLaw), l.countOps ≤ 4, ∃ i, law i = l
/-- the final matrix -/
def implicationGraph : (i j : Fin n) → Bool := …
/-- and correctness thereof -/
theorem implicationGraph_correct : ∀ (i j : Fin n),
  implicationGraph i j = true ↔ (law i).implies (law j)

Notes:

• I am phrasing law and implementationGraph as functions, not lists or matrices or so. That’s sufficient to state these theorems in a clear and declarative way. Very likely one has to find suitable data structures, define them, and then access these in law and implementationGraph.
• Filling these definitions naively, e.g. by pure enumeration, wouldn’t be too hard, I assume, but likely be too large for lean to handle. So this needs serious proof engineering. In particular, I expect that law should be backed by a balanced binary search tree that the kernel can index into somewhat quickly (I have code for that somewhere). And not sure about the graph, maybe actually a bitmap encoded in a large Nat?
• For the graph, maybe it makes sense to re-implement the closure code in a verified and kernel-reduction-friendly way. So one step would be to define the (partial) implies and not-implies graphs, and then prove that the final graph is the result of taking the closure using a verified algorithm, rather than proving correctness of each entry in the final graph.
• Arguably the above is trivial to satisfy if one uses the axioms of classical logic in the definitions. So maybe one should also add a check that implementationGraph doesn’t use such axioms, and hence is actually computable.
• law_complete cannot be proven like this, we want to restrict it to those laws with variables in order (or up-toprenaming)

If one would want to build that, and want to build it even before proving everything, then one either has to complicate the statements somehow (excluding certain pairs from the correctness theorem). Or introduce an axiom for “conjectured implication” and build this infrastructure as if we are already done, and when we are done then that axiom will be unused.

[Notification Bot]

A message was moved here from #Equational > Thoughts and impressions thread by Joachim Breitner.

[Joachim Breitner]

Playing around in that direction. That’s a good start:

def laws : RArray Law.NatMagmaLaw := defineLaws%
example : laws[1000] = Law1001 := rfl

[Shreyas Srinivas]

Ah I see, this is a theorem that we have proved all the theorems

[Notification Bot]

6 messages were moved from this topic to #Equational > non-computable non-non-computables? by Joachim Breitner.

[Joachim Breitner]

Little experiments in that direction in https://github.com/teorth/equational_theories/pull/618
This defines a single definition that contains all laws, and a binary search function to find the index of a law therein.

But what’s missing for laws_complete is a verified(!) generator of laws up to a certain size, which is doable, but not trivial. Parking this for today.

[Shreyas Srinivas]

There is a script from which our current set of equations were defined. It is in python and I think we also have an extraction script from lean's equations list to json

[Joachim Breitner]

I know, but thats not verified. How do we know that we didn't miss a certain law? (Unlikely, but if we want an end-to-end proof of our end result, that is one necessary part.)

[Andrés Goens]

oh, that's really cool! I've been knid of slacking off integrating duality into the transitive closure computation, so I feel reassured you think it makes sense to re-implement it in a verified and kernel-reduction-friendly way (so that effort wasn't wasted :grinning: )

[Andrés Goens]

Maybe it would make sense to split up the proof of implicationGraph_correct into two parts, one that says "it suffices to prove these implications/anti implications" because of transitivity, duality, and a second part that just supplies the necessary proofs. That would also help with the issue of making this work before everything's integrated (because we can prove the "it suffices" part already without having the explicit proofs for every implication/anti-implication, and that's likely the one that's going to be more optimizable)

[Amir Livne Bar-on]

I've been away from chat, but worked on and off on converting the code generating laws to Lean.

It's now in a working state, at
https://github.com/amirlb/equational_theories/blob/generate-laws-lean/scripts/generate_laws.lean

[Amir Livne Bar-on]

I'm not fluent enough in Lean yet to prove it covers all laws up to equivalence

[Joachim Breitner]

sorry for possibly duplicating work, I'm almost through with my generator.

[Amir Livne Bar-on]

It's not that much code anyway... So the important thing is to structure it so it's easy to prove properties about it

[Vlad Tsyrklevich]

Andrés Goens said:

oh, that's really cool! I've been knid of slacking off integrating duality into the transitive closure computation, so I feel reassured you think it makes sense to re-implement it in a verified and kernel-reduction-friendly way (so that effort wasn't wasted :grinning: )

I believe duality is already integrated as of 76ace3ce93a728b536252d206bb75c9b71b4d421 unless you're referring to something else?

[Joachim Breitner]

Joachim Breitner said:

sorry for possibly duplicating work, I'm almost through with my generator.

I take the almost back, it seems tricky to recognize/generate laws up to permutation of the variables efficiently.

[Cody Roux]

I bet this is a well-known problem, but seems hard to google

[Joachim Breitner]

Ok, I got a generator that finds all equations, does not generate extra ones, but doesn’t try all permutations of variables. It’s not verified yet, but this looks promising:

/-- info: true -/
#guard_msgs in
#eval (List.range 5).all fun i => testLaws i fun l =>
  laws[findMagmaLaw l] = l

[Amir Livne Bar-on]

Very nice!

[Andrés Goens]

Vlad Tsyrklevich said:

Andrés Goens said:

oh, that's really cool! I've been knid of slacking off integrating duality into the transitive closure computation, so I feel reassured you think it makes sense to re-implement it in a verified and kernel-reduction-friendly way (so that effort wasn't wasted :grinning: )

I believe duality is already integrated as of 76ace3ce93a728b536252d206bb75c9b71b4d421 unless you're referring to something else?

right, sorry, I should have been more precise here. That piece of code is great for keeping score, but it's just taking the duals out of some json file:

let dualityRelation ← DualityRelation.ofFile "data/duals.json"

I mean formally using the duality definition and metatheorem (from equational#285) when computing the closure, as part of an end-to-end theorem in Lean

[Andrés Goens]

Joachim Breitner said:

Ok, I got a generator that finds all equations, does not generate extra ones, but doesn’t try all permutations of variables. It’s not verified yet, but this looks promising:

/-- info: true -/
#guard_msgs in
#eval (List.range 5).all fun i => testLaws i fun l =>
  laws[findMagmaLaw l] = l

cool! by the way, formalizing this also probably requires/is closely related to equational#148 and equational#184, formalizing the counts

[Joachim Breitner]

Proved

theorem laws_complete :  ∀ l : Law.MagmaLaw Nat, l.forks ≤ 4 → l.is_canonical → ∃ (i : Nat), laws[i] = l

This is using native_decide, but still a very convincing proof, I’d say.

If one defines a suitable equivalence on MagmaLaw (up to relabeling of variables, reorienting the equation), then one could even prove the slightly more high-level

theorem laws_complete :  ∀ l : Law.MagmaLaw Nat, l.forks ≤ 4 → ∃ l', l.equiv l' → ∃ (i : Nat), laws[i] = l'

and take l.is_canonical out of the “trusted spec base”. Looks like we don’t have that equivalence definition yet, though.

[Amir Livne Bar-on]

We do have logical equivalence, which is weaker. And looks even more convincing to me: it doesn't matter if we missed a few equations if we provably covered all equivalence classes.

[Joachim Breitner]

True, so we’d just™ have to prove that relabeling or symmetry preserves logical equivalence.

[Amir Livne Bar-on]

That is simple enough for even me to prove :p (and might even be exactly MagmaLaw.satisfies_map_equiv). Syntactic equivalence sounds like a useful property to have though so probably worth defining anyway.

[Joachim Breitner]

In https://github.com/teorth/equational_theories/pull/636 I am experimenting with representing the graph of proven implications in a single def, in a verified way. I think it built locally, but seems to bring the GitHub runner to its knees. This definitely needs more tuning. It needs more work to actually scale to the full graph, though.

This doesn't take the closure yet. For that I am wondering if there is a way to precalculate some data so that the actual proof doesn't have to calculate the closure, just check it. For example if for every nodes i, j in the closure it would also store the number of steps it takes from i to j, and also what the next node on that path is, then checking that for correctness should be linear. Maybe that's noticably better than running the full closure algorithm.

[Amir Livne Bar-on]

If it was a simple graph, it would be simple, right? You could prove that for one vertex you have both a forward and a backwards path to every other vertex

[Amir Livne Bar-on]

Actually I never saw the structure of the (non-)implications graph written down, so for completeness:

• There are two nodes for each equation, EqA and EqA'
• There is a node for each "Facts" statement, MagmaN
• For each statement EqA_implies_EqB two edges: EqB -> EqA and EqB' -> EqA'
• For each statement Facts [A, ...] [B, ...] edges are added EqA -> MagmaN and MagmaN -> EqB'

Then a path EqA -> ... -> EqB indicates an implication EqB => EqA and a path EqA -> ... -> EqB' indicates a non-implication not (EqA => EqB).

[Joachim Breitner]

Joachim Breitner said:

I think it built locally, but seems to bring the GitHub runner to its knees. This definitely needs more tuning. It needs more work to actually scale to the full graph, though.

Interesting, the file finishes fine in VSCode, but lake build takes a long time. :eyes:

Even worse: lake build sits there for minutes, and if I stop it and re-run it, it considers the build done. That looks like a bug somewhere…
Ah, it seems that writing the C file with the large data structure is what keeps Lean overly busy (and which doesn’t happen in vscode). I think that’s what @Henrik Böving observed before. And after Ctrl-C there is an empty .c file and lake is happy to use that :-(
But I fail to reproduce this behavior in a small example.

[Joachim Breitner]

Hmm, using large bitvectors encoded as Nat seems to hit limitations in lean:

• Compiling is super slow because Nat.repr goes via toDigits which goes via List Char, instead of mutably filling a String. Reported as https://github.com/leanprover/lean4/issues/5771.
• The generated C code runs lean_cstr_to_nat when initializing, so presumably (didn’t measure) this increases the startup time of any program importing such a module.

But maybe a single bitvector for the whole graph isn’t needed, and maybe something like Array Nat (i.e. adjacency bitvectors) would work better.

[Amir Livne Bar-on]

fwiw the closure code uses arrays of bitvectors, where each bitvector is an array of UInt64

[Joachim Breitner]

That is a good choice for native evaluation. Maybe I should first aim at proving the final theorem using native_decide and the existing code, and defer (or give up on) trying to avoid native evaluation.

[Mario Carneiro]

Joachim Breitner said:

Hmm, using large bitvectors encoded as Nat seems to hit limitations in lean:

• Compiling is super slow because Nat.repr goes via toDigits which goes via List Char, instead of mutably filling a String. Reported as https://github.com/leanprover/lean4/issues/5771.
• The generated C code runs lean_cstr_to_nat when initializing, so presumably (didn’t measure) this increases the startup time of any program importing such a module.

But maybe a single bitvector for the whole graph isn’t needed, and maybe something like Array Nat (i.e. adjacency bitvectors) would work better.

Why are you using Nat.repr?

[Mario Carneiro]

I thought the idea was that you read a data file, construct a Nat in memory at elaboration time and insert it as a nat literal into the environment

[Mario Carneiro]

you should never need to go via decimal, you really shouldn't because base conversion of huge numbers is incredibly expensive

[Mario Carneiro]

Here's an alternative proof structure, which perhaps sidesteps the questions about computability:

import equational_theories.Preorder
import equational_theories.MagmaOp

open Law renaming NatMagmaLaw -> Law

def Fact' (as bs : List Law) := ∀ a ∈ as, ∀ b ∈ bs, ¬a ≤ b

inductive Record where
  | implies : Law → Law → Record
  | notImplies : Law → Law → Record
  | fact : List Law → List Law → Record
  | dual : Law → Law → Record

def Record.WF : Record → Prop
  | .implies a b => a ≤ b
  | .notImplies a b => ¬a ≤ b
  | .fact as bs => ∀ a ∈ as, ∀ b ∈ bs, ¬a ≤ b
  | .dual a b => b = a.dual

def IsDual (l : List Record) (a a' : Law) : Prop :=
  .dual a a' ∈ l ∨ .dual a' a ∈ l

inductive Closure (l : List Record) : Law → Law → Bool → Prop
  | refl {a} : Closure l a a true
  | imp {a b} : .implies a b ∈ l → Closure l a b true
  | notimp {a b} : .notImplies a b ∈ l → Closure l a b false
  | fact {as bs a b} : .fact as bs ∈ l → a ∈ as → b ∈ bs → Closure l a b false
  | trans11 {a b c} : Closure l a b true → Closure l b c true → Closure l a c true
  | trans10 {a b c} : Closure l a b true → Closure l a c false → Closure l b c false
  | trans01 {a b c} : Closure l a c false → Closure l b c true → Closure l a b false
  | dual {a b a' b' val} : IsDual l a a' → IsDual l b b' → Closure l a b val → Closure l a' b' val

theorem Closure.wf {l} (h : ∀ r ∈ l, r.WF) (a b : Law) {val} :
    Closure l a b val ↔ (a ≤ b ↔ val) := sorry

def allLaws : List Law := [
  -- explicit list
]

def allRecords : List Record := [
  -- explicit list
]

theorem allRecords_correct : ∀ r ∈ allRecords, r.WF := sorry

theorem correct (eqA eqB : Law) {b} :
    Closure allRecords eqA eqB b ↔ (eqA ≤ eqB ↔ b) := sorry

theorem complete (eqA eqB : Law) : eqA ∈ allLaws → eqB ∈ allLaws →
    ∃ b, Closure allRecords eqA eqB b := sorry

[Joachim Breitner]

Nice. Does this scale, usings lists etc, given thousands of entries?

[Mario Carneiro]

not really, at least the way lists in lean currently work. But you can have a metaprogram that generates trees instead of lists and/or uses sub-definitions and I'm pretty sure you can push it through the kernel that way

[Joachim Breitner]

I am computing the large nat using an elaborator (so I assume reading from a file wouldn't be different here), and use it to define a top level Nat. But then lean wants to write ot to the c file, and itself uses Nat.repr in the process

[Notification Bot]

3 messages were moved here from #Equational > non-computable non-non-computables? by Mario Carneiro.

[Mario Carneiro]

@Joachim Breitner is it okay to just put noncomputable on the definition?

[Joachim Breitner]

Mario Carneiro said:

not really, at least the way lists in lean currently work. But you can have a metaprogram that generates trees instead of lists and/or uses sub-definitions and I'm pretty sure you can push it through the kernel that way

Ok, sounds like I wasn't completely on the wrong track on my Branch, with a tree-shaped proof of well-formedness of the main data structure. Fun puzzle, although it would be nice if one didn't have to puzzle to make such medium sized things work.

[Mario Carneiro]

yes, lean falls over on big proofs for distressingly small values of "big"

[Joachim Breitner]

Mario Carneiro said:

Joachim Breitner is it okay to just put noncomputable on the definition?

Possibly, but I assumed I can only do that once I no longer use native_decide

[Mario Carneiro]

IIRC there is some way to force definitions to be interpreted, but I forget what it is. Maybe just disable the compiler with an option?

[Mario Carneiro]

I would be interested to know what kind of algorithms exist for proving completeness without needing to enumerate all n^2 cases

[Mario Carneiro]

it feels like you should be able to construct a hasse diagram and extract a bunch of facts implicitly from that

[Mario Carneiro]

actually I think that's exactly the answer: a hasse diagram presentation where every edge is a proved non-implication is already complete, so the proof is just to construct a hasse diagram presentation and check that every law is somewhere in the diagram

[Amir Livne Bar-on]

A small search found an anti-chain of size 200, so we need at least 200^2 negative edges in the graph

[Mario Carneiro]

It's possible to prove those 200^2 negative edges using only 200 models though in the best case

[Mario Carneiro]

in other words, we have to consider the extended graph you mentioned that also has nodes for Facts statements

[Mario Carneiro]

@Joachim Breitner I'm looking at your RArray structure, very nice. One thing which I think would improve it is to use a slightly different version of the get function:

/-- The crucial operation, written with very little abstractional overhead -/
noncomputable def RArray.get : RArray α → Nat → α :=
  RArray.rec (fun x _ => x) (fun p _ _ l r n => (Nat.ble p n).rec (l n) (r (Nat.sub n p)))

In other words, the data stored at nodes is not the index of the middle point in the array but rather the size of the left subtree. This has the effect that many operations on it become O(log n) instead of O(n)

[Mario Carneiro]

get might also get faster, although it's unlikely to matter at these sizes, because you are comparing smaller numbers

[Joachim Breitner]

They are not O(log(n))? Then I didn't do what I intended. I stored the index there to avoid the subtraction in get

[Mario Carneiro]

get is O(log n) but insertion isn't

[Joachim Breitner]

Oh, you man other operators than get? This was designed to support exactly get.

[Mario Carneiro]

In particular, I think you can prove the theorem in LawsComplete by just building up the array instead of looking individuals up in a static array

[Joachim Breitner]

I.e. for use cases where you prepare static data at elab time, and at kernel reduction time you just index into. Hence also the garbage value when indexing out of bounds.

[Mario Carneiro]

because you know it is sorted in advance

[Joachim Breitner]

For example the denotation function in a reflection proof could use this instead of a list

[Mario Carneiro]

Joachim Breitner said:

They are not O(log(n))? Then I didn't do what I intended. I stored the index there to avoid the subtraction in get

I'm not sure what the alternative you are considering here is

[Joachim Breitner]

Right. When writing the code I wasn't sure if my generation function would end up producing the same order as Terry's script (and I'm not sure it does), hence this approach for now.

[Joachim Breitner]

Mario Carneiro said:

Joachim Breitner said:

They are not O(log(n))? Then I didn't do what I intended. I stored the index there to avoid the subtraction in get

I'm not sure what the alternative you are considering here is

Nevermind, ignore that message, I thought you said that my get wasn't O(log n).

[Joachim Breitner]

Do you want to take over working on the two end-to-end theorems? You seem to have been thinking about it already a lot, and I shouldn't get too distracted from core work anyways ?

[Mario Carneiro]

Joachim Breitner said:

Right. When writing the code I wasn't sure if my generation function would end up producing the same order as Terry's script (and I'm not sure it does), hence this approach for now.

But you never sort the list? It seems to just put Law(i+1) at position i in the list

[Mario Carneiro]

but findMagmaLaw exploits that it is sorted according to your sort order

[Mario Carneiro]

so I think this is a proof that the laws are in fact sorted

[Mario Carneiro]

Joachim Breitner said:

Do you want to take over working on the two end-to-end theorems? You seem to have been thinking about it already a lot, and I shouldn't get too distracted from core work anyways ?

lol, I need to be reviewing a paper, I'm intensely procrastinating right now

[Joachim Breitner]

(deleted)

[Mario Carneiro]

I don't think we even need to prove it is transitively reduced

[Joachim Breitner]

Sorry, I think I said nonsense, but you answer too quickly

[Joachim Breitner]

(nonsense because you also need to demonstrate non-implications between nodes that are unrelated in the graph)

[Joachim Breitner]

Right, with transitive reduction I meant we can remove some implied edges, not that it has to be fully reduced.

[Joachim Breitner]

Mario Carneiro said:

so I think this is a proof that the laws are in fact sorted

Yes, Terry's list is sorted wrt to some order that I had to find out. I don't know if my generator produces them in that order, hence generate-and-lookup.

[Mario Carneiro]

So you are saying that Law.MagmaLaw.comp is actually terry's order?

[Mario Carneiro]

but you don't know how to generate laws in that order

[Joachim Breitner]

Yes, its his order (so that binary search works), and I didn't attempt to recreate his order so far.

[Terence Tao]

By the way, the script was written by @Amir Livne Bar-on , back in the prehistory of the project on Sep 26 (when it was in a different repository).

[Notification Bot]

36 messages were moved from this topic to #Equational > proving a hasse diagrams to be complete by Joachim Breitner.

[Amir Livne Bar-on]

If we change the type of the checker from Law -> Bool to Law -> Monoid it can also be a generator. Then we can test and tweak the order if we want it to fit the list.

[Amir Livne Bar-on]

This is easier said than done. The nice way I managed to put it uses higher-order types, and I can't see how to make the induction on iterFreeMagmas (nee testFreeMagmas) work correctly.
https://github.com/amirlb/equational_theories/blob/laws_iterator/equational_theories/Equations/LawsComplete.lean#L176

The ordering is still not exactly the same, but we can probably shuffle some indices to make it output in the same order.

[Joachim Breitner]

Is it worth the bother? Generate-and-lookup seems fine to me, and the speed is acceptable.

[Amir Livne Bar-on]

Probably not worth it. Especially since (as I realized after I got the list) it doesn't generate any law more than twice

[Mario Carneiro]

well, I wanted to improve on the native_decide part

[Mario Carneiro]

@Amir Livne Bar-on do you have code?

[Amir Livne Bar-on]

Yes, the link above is a file that generates lists and checks properties with the same code. It works, only one theorem is broken.

But if we go for complicated type-classes here, we may as well use ForIn which has syntax and support for propositions.

[Mario Carneiro]

oh, I missed that that was a link to your fork

[Joachim Breitner]

Joachim Breitner said:

Is it worth the bother? Generate-and-lookup seems fine to me, and the speed is acceptable.

Maybe worth the bother if we want to get rid of native_decide, and need to make it go a lot faster.

In https://github.com/teorth/equational_theories/pull/780 I saw how far I get with using some tricks to make well-founded recursion go well and with reducing some overhead (typeclasses, Monad), but it is still far too slow.

I expect if we refactor the code to use a generator (as @Amir Livne Bar-on started to do), and either make it generate them in the right order, or go trough a lookup table for the permuation (which can be calculated at elaboration time), then maybe it’s feasible.

@Amir Livne Bar-on , List.append is likely far too slow here, due to the quadratic runtime; you probably need at least difference lists as the structure to collect the results, or maybe implement the generator as left-folds (resp. StateM) and use List.cons to add new entries to the front.

Or, don’t even generate the list, and stick closer to the current code, but keep a counter that’s passed to the predicate and then we can use that counter to avoid the (likely expensive) findMagmaLaw search.

[Mario Carneiro]

Can someone remind me where to find the definition of the magma enumeration ordering?

[Terence Tao]

Here's the lean implementation: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Reconstructing.20the.204694.20expressions.20from.20the.20ground.20up.2E/near/478350231 . I should put the ordering in the blueprint at some point.

[Mario Carneiro]

@Terence Tao said:

• The ordering on laws with a fixed length on both the left-hand side and right-hand side is a bit hard to explain (recursive lexicographic). At this point it is easier just to point to the python code than to try to describe it properly here.

What python code?

[Vlad Tsyrklevich]

scripts/generate_eqs_list.py

[Amir Livne Bar-on]

The $C_{n+1}$ factor hints at a simple explanation: consider the tree corresponding to lhs * rhs, first order by that, and then lexicographically

[Joachim Breitner]

JFTR, Mario solved the issue, as mentioned over at #Equational > LawsComplete by proof term generation

[Andrés Goens]

So I was looking back a bit at this and it seems we have solved the enumeration issue (laws complete), but we still have no proof that includes the implications/refutations. I'm not sure how we'd even want to state that theorem, saying that for every pair of laws $l_1 l_2$ we either have a proof of $l_1 \vdash l_2$ or a refutation.

The best way I can think of is defining the set of implications as an adjacency matrix implications (similar to laws in LawsComplete) and proving something like laws[i] ≤ laws[j] ↔ implications[i][j] = true. Does someone have a better idea? Is it worth adding this as an issue? (I would be interested in contributing to this, although I don't know how much time I will have for it)

[Andrés Goens]

having said that, this array is probably a bit too large to have in memory (and be efficient), so maybe we want to phrase this for the transitive closure of a sparse matrix only

[Joachim Breitner]

That is roughly the theorem, but the harder question is the necessary proof engineering that we don't generate 4000² individual proofs.

I would expect something like

• a reasonable efficient representation of all explicitly proven facts (impliciations and counter-examples), maybe transitively reduced to keep it small
• a proof that for each entry in that data structure we really have a theorem
• a proof that the the closure of this data structure cover the whole graph.

Ideally the third point can be proven in a way that does not require going through the whole graph. I believe Mario did think about this quite a bit.

[Andrés Goens]

Right, so you think that just storing the explicitly proven facts like we're currently doing (with the @equational_result tag) is going to be too inefficient?

[Joachim Breitner]

I think that depends on the algorithm used for the third step, and whether that will involve kernel-computation.

[Andrés Goens]

rg "@\[equational_result" | wc -l
12452

I just checked roughly and it seems it's about 12k explicitly proven facts. That might indeed be a bit too large for putting them all together one proof term, so we should think about how to split them up

[Andrés Goens]

(this set is probably not minimal, but ballpark it still sounds like too much)

[Joachim Breitner]

I don’t know how useful it is to split them up if you end up having to put them together for the third proof step?

[Andrés Goens]

Joachim Breitner said:

I don’t know how useful it is to split them up if you end up having to put them together for the third proof step?

but for the third proof step it doesn't have to actually look at the proof term, just its type, right?

[Joachim Breitner]

Right, but the type would still mention a data structure that contains 12k entries, woudn’t it

[Joachim Breitner]

I am not primarily worried about a def with a careful chosen data structure with 12k elements, and then a proof that the entries are correct that is essentially 12k times “see theorem foo” (step 2). It’s step 3 that worries me.

And as step3 likely influence which data structure to use here, I’m hesitant to worry about step 2 before that is determined.

[Andrés Goens]

hmm, interesting :thinking: yeah, I think I see the problem

[Joachim Breitner]

I think #Equational > proving a hasse diagrams to be complete is the thread where approaches to step 3 were discussed

[Mario Carneiro]

12k explicit facts doesn't sound that bad, that's only about 3 times larger than the list of equations itself

[Mario Carneiro]

that's a very sparse graph

[Joachim Breitner]

Note that each counter-example fact can represent a large amount of actual edges, but still.

[Mario Carneiro]

It might help for some folks to try to do an analysis of the full hasse diagram to see whether there are any interesting structures we can exploit (eg. does it have many connected components? is it almost linear? etc)

[Bruno Le Floch]

Is there some interest in porting find_equation_id.py from python to Lean? I can deal with the complexities of indices but I don't understand yet how to get started: for instance I don't understand the relation between equation in Equations/Eqns1_999.lean and EquationN in files like ParseImplications.lean. Is there some documentation of that somewhere?

[Vlad Tsyrklevich]

Yes, there are 10k implications, and ~1.3k refutations but they represent around ~500k edges. That ~500k number is not all necessary for completeness though

[Mario Carneiro]

I'm surprised there are so few refutations

[Vlad Tsyrklevich]

Most of the refutations are resolved by just looking at 3x3 magmas.

[Mario Carneiro]

The refutations are also grouped, right? i.e. they are more like "fact nodes" saying that Ai -/> Bj for all i,j in some lists A, B

[Vlad Tsyrklevich]

Yes, that's what I mean by 1.3k theorems but 500k edges.

[Mario Carneiro]

right, this is definitely going to be exploited by the proof

[Vlad Tsyrklevich]

500k is the sum of the 1.3k Satisfying*Refuting

[Mario Carneiro]

there will be no "multiply all these terms together" proof

[Mario Carneiro]

at least not if I have anything to say about it :)

[Mario Carneiro]

how many edges are there if we count a fact as having A+B edges?

[Vlad Tsyrklevich]

Mario Carneiro said:

It might help for some folks to try to do an analysis of the full hasse diagram to see whether there are any interesting structures we can exploit (eg. does it have many connected components? is it almost linear? etc)

Strongly connected components is already know, there are 1,415 equivalence classes, the largest is of size 1,496, but 1,145/1,415 are of size 1

[Mario Carneiro]

oh well that makes things easier

[Vlad Tsyrklevich]

Yes, the SCC graph is ~10x smaller than the original

[Vlad Tsyrklevich]

And there are only ~4.8k edges in the transitive reduction between equivalence classes

[Vlad Tsyrklevich]

The rest are establishing equivalence classes.

[Mario Carneiro]

or does it? If there are a huge number of isolated components (once you take off the top and bottom, I assume) don't we have to prove all the n^2 non-implications?

[Vlad Tsyrklevich]

Don't you just have to prove the most general refutations? I mean perhaps that entails some level of graph search as well, but I'm not sure that it's n^2

[Mario Carneiro]

Let's suppose that step 1 of the proof is to separate out all the size 1 components and handle them specially. What is the proof strategy?

[Joachim Breitner]

Just checking: Are you talking about the same thing if you say equivalence classes resp. connected components?

[Mario Carneiro]

I am picturing a diagram with 0 <= x_i <= 1 and all x_i incomparable

[Vlad Tsyrklevich]

Why are size 1 components special? I think you treat all SCCs equivalently, and then prove that if it's complete for SCCs it's true for the graph.

[Mario Carneiro]

They aren't, but I want to exploit known structure in the graph to make the proof smaller

[Joachim Breitner]

I think Mario is already one step ahead, and looks at a graph where equivalent laws are already represented by a single node, with the top and bottom law cut off, and now wants to know the connected components of this graph

[Mario Carneiro]

something like "80% of the graph is trivial" definitely qualifies

[Vlad Tsyrklevich]

How can there be connected components, it's already a condensed graph

[Vlad Tsyrklevich]

Ah, perhaps I'm confusing terminology with connected components and strongly connected?

[Mario Carneiro]

Yes, Joachim is correct. The connected components I'm talking about are in the undirected version of the transitive reduction graph, after collapsing equivalent nodes and deleting the top and bottom

[Vlad Tsyrklevich]

Well, take what I said above to be about strongly connected components in the base graph, not this model.

[Mario Carneiro]

SCCs would be single nodes in what I said. How many nodes are there in the graph after reducing SCCs?

[Mario Carneiro]

oh wait you answered that already (1415)

[Joachim Breitner]

In addition to knowing how many such components we have it’s also relevant to know, for each of them, their size, the number of least elements and the number of greatest elements (because we’ll need counter-examples between each greatest and each least element, unless I’m mistaken).

[Mario Carneiro]

yeah knowing the actual numbers helps a lot with determining how much engineering is overengineering

[Mario Carneiro]

e.g. no need to deploy Tarjan's SCC algorithm if it's all singletons

[Mario Carneiro]

but I think SCCs are essentially an independent part of the proof from the hasse diagram structure

[Vlad Tsyrklevich]

For least and greatest, I assume you just meant inbound edges to Equation 1 and outbound edges of Equation 2, or do you mean this recursively, since some connected components are large?

[Joachim Breitner]

I assume that you remove Eq1 and Eq2 first (“deleting top and bottom”), and then the graph falls apart into connected components. Of these components, it’s relevant to know how many least and greatest there are.

Ah, but you are right: these are indeed the edges from and to Eq1 and Eq2 in the transitively reduced graph.

[Vlad Tsyrklevich]

Here's graphiti showing outbound edges from Eq2. Open the JS console and it shows that there are 46 edges.

[Vlad Tsyrklevich]

For Equation 1 it's 57 inbounds.

[Joachim Breitner]

Thanks! That also puts upper bounds on the number of connected components (after deleting Eq 1 and Eq2)

[Vlad Tsyrklevich]

Looking at the size of the components outwards from Eq2, they have this number of elements:

2 Eq1076
2 Eq1083
2 Eq1110
2 Eq1279
2 Eq1286
2 Eq1516
2 Eq1692
2 Eq1719
2 Eq1888
2 Eq1895
2 Eq2091
2 Eq2301
2 Eq2328
2 Eq2497
2 Eq2504
2 Eq2531
2 Eq2700
2 Eq2903
2 Eq2910
2 Eq2937
2 Eq3106
2 Eq3140
2 Eq467
2 Eq501
2 Eq670
2 Eq677
2 Eq704
2 Eq907
3 Eq1313
3 Eq1489
3 Eq2098
3 Eq2294
4 Eq66
6 Eq2707
6 Eq880
9 Eq125
9 Eq222
9 Eq3113
9 Eq474
12 Eq271
12 Eq63
39 Eq168
478 Eq895
643 Eq41
693 Eq4
693 Eq5

[Joachim Breitner]

Nice! Are Eq4 and Eq5 are in the same component of size 693?

[Vlad Tsyrklevich]

No, they are dual.

[Joachim Breitner]

And the small ones have size 2 because you are including Eq1 in the count? Or are they all equivalence classes consisting of two laws?

[Andrés Goens]

so this list is already just taking a single representative of every scc?

[Vlad Tsyrklevich]

No I'm not including Eq1, for example, here is 1076

[Vlad Tsyrklevich]

Andrés Goens said:

so this list is already just taking a single representative of every scc?

Yes.

[Vlad Tsyrklevich]

I just noticed the list has sporadic equations (or order >4) included but there are only a few of them so it shouldn't affect the numbers much.

[Joachim Breitner]

Looking at 271 here it looks like repeating the process of cutting off top or bottom elements and recursing might handle a good part of the graph.

[Andrés Goens]

I guess also generating and proving the 1415 theorems that describe the scc's is a pretty good idea in any case already, right?

[Andrés Goens]

independent of how we split the collapsed graph

[Andrés Goens]

we'll need to collapse it

[Vlad Tsyrklevich]

(There are only 270 SCCs of size >1)

[Mario Carneiro]

Vlad Tsyrklevich said:

No, they are dual.

Oh, duality is also going to be super helpful here. Can we pair up the connected components into dual pairs which have the exact same structure?

[Mario Carneiro]

I guess Eq41 has to be self-dual

[Vlad Tsyrklevich]

41 is, but 895 is not.

[Vlad Tsyrklevich]

(895 is equivalent to it's dual, hence you don't see it.)

[Mario Carneiro]

I mean the cluster should be self-dual, i.e. the image of the dual map on the 895 cluster is itself

[Mario Carneiro]

Are there really no size 1 components?

[Vlad Tsyrklevich]

I don't think there can be, any >1 variable equation implies its one-variable version.

[Mario Carneiro]

but the 1 variable version could be top or bottom, no?

[Mario Carneiro]

i.e. that argument proves there are two nodes but not that neither of them is extremal (or that they are inequivalent)

[Mario Carneiro]

there might be a general argument for why reducing the variable count always results in an inequivalent equation though

[Vlad Tsyrklevich]

Mario Carneiro said:

but the 1 variable version could be top or bottom, no?

If I understand what you mean correctly, it has to be top, e.g. most general. It's only restricting elements related to the diagonal.

[Mario Carneiro]

does graphiti have an option for collapsing equivalent nodes?

[Vlad Tsyrklevich]

It already collapses them

[Mario Carneiro]

what does rounded corners mean?

[Vlad Tsyrklevich]

It means it's an SCC of size >1.

[Alex Meiburg]

It might also be possible to make the SCC computation faster by adding just a _few_ extra theorems. Like for the Eq2 equivalence class, adding a theorem for EqX -> Eq2 directly (instead of relying on dynamically finding a path through other theorems) means that we can verify everything in the SCC by just checking those O(n) extra theorems.

[Alex Meiburg]

While creating all 4000^2 theorems is obviously too much, adding a theorem for "X implies 2" for each X that does seems totally fine as overehead/optimization

[Mario Carneiro]

It's not clear why we would need that

[Mario Carneiro]

We need to prove SCCs, not non-SCCs

[Vlad Tsyrklevich]

Mario Carneiro said:

there might be a general argument for why reducing the variable count always results in an inequivalent equation though

You're right that my original argument missed this, and the argument as to why this is the case is that that setting all 0s along the diagonal always satisfies the one-variable equation, and then setting all the other elements to 1 should cause the multi-variable version to fail.

EDIT: I suppose this actually isn't true for x = (xx)(yy), though it is for other equations it's equivalent to.

[Mario Carneiro]

non-SCCs will be implied from non-implications during the hasse diagram part of the proof

[Vlad Tsyrklevich]

Got lost in something else, here's the list of component sizes looking outwards from Eq2 paired by dual:

2 Eq1076 Eq2531
2 Eq1083 Eq2504
2 Eq1110 Eq2497
2 Eq1279 Eq2328
2 Eq1286 Eq2301
2 Eq1516 Eq2091
2 Eq1692 Eq1895
2 Eq1719 Eq1888
2 Eq467 Eq3140
2 Eq501 Eq3106
2 Eq670 Eq2937
2 Eq677 Eq2910
2 Eq704 Eq2903
2 Eq907 Eq2700
3 Eq1313 Eq2294
3 Eq1489 Eq2098
4 Eq66 Eq281
6 Eq880 Eq2707
9 Eq125 Eq222
9 Eq474 Eq3113
12 Eq63 Eq271
39 Eq168
478 Eq895 Eq2789
643 Eq41
693 Eq4 Eq5

[Amir Livne Bar-on]

Some stats that I didn't see mentioned in the thread already:

• The 1415 components are comprised of 67 self-dual components and 674 pairs of dual components
• The number of transitively-reduced implications in the Hesse diagram is 4824, or 2467 up to duality
• There are 14522 irreducible non-implications needed to prove that the diagram is fully-specified, or 7286 up to duality

[Vlad Tsyrklevich]

Oh, the last number is nice. I have a PR that adds dashboard stats that computes and publishes various facts about the graph, I should add that as well. By what algorithm do you compute the minimum required non-implications?

[Amir Livne Bar-on]

Nothing too smart, went over all the non-implications and checked if each can be derived directly from an implication + a stronger non-implication. Takes a few seconds in python.

[Mario Carneiro]

Where is the actual (explicit) implication data? The graphiti json doesn't have the implications themselves, only the induced implications on SCCs

[Amir Livne Bar-on]

lake exe extract_implications outcomes

[Joachim Breitner]

Amir Livne Bar-on said:

• There are 14522 irreducible non-implications needed to prove that the diagram is fully-specified, or 7286 up to duality

How do you obtain this number? Using some algorithm that takes a Hesse diagram and gives you the least number of anti-implications you have to provide to prove that the diagram is fully specified?

[Mario Carneiro]

Amir Livne Bar-on said:

lake exe extract_implications outcomes

This seems to require the whole lean project to be built, I was hoping for a data dump file

[Vlad Tsyrklevich]

Do you know if you have a particular data format you want?

[Vlad Tsyrklevich]

e.g. extract_implications versus extract_implications outcomes etc.

[Mario Carneiro]

lake exe extract_implications doesn't run at all, it says

uncaught exception: object file '././.lake/build/lib/equational_theories.olean' of module equational_theories does not exist

[Vlad Tsyrklevich]

(deleted)

[Vlad Tsyrklevich]

Oops, different exception

[Mario Carneiro]

by which I inferred that it needs the project to be built

[Mario Carneiro]

Vlad Tsyrklevich said:

Do you know if you have a particular data format you want?

implications in json would be nice

[Mario Carneiro]

I have managed to get stuff out of outcomes.png, which I recall being a recommendation before

[Vlad Tsyrklevich]

https://tsyrklevi.ch/general.json.gz

[Vlad Tsyrklevich]

Once equational#973 lands (and assuming github pages accepts it), this should just be available on the dashboard going forward

[Vlad Tsyrklevich]

That's the outcome of just plain extract_implications

[Amir Livne Bar-on]

Joachim Breitner said:

Amir Livne Bar-on said:

• There are 14522 irreducible non-implications needed to prove that the diagram is fully-specified, or 7286 up to duality

How do you obtain this number? Using some algorithm that takes a Hesse diagram and gives you the least number of anti-implications you have to provide to prove that the diagram is fully specified?

This number doesn't include the fact that the edges of the diagram are strict implications, so the full number is actually 19346. Here's the main chunk of code I used to count these:

non_implications = {(i, j) for i in range(M) for j in range(M) if j not in implications[i] and i not in implications[j]}
simple_non_implications = {
    (i, j) for i, j in non_implications
    if all((i, k) not in non_implications for k in implications_rev[j] if k != j)
    and all((k, j) not in non_implications for k in implications[i] if k != i)
}

[Mario Carneiro]

I get 10675 explicit implications and 587150 nonimplications from that json @Vlad Tsyrklevich , is this correct?

[Mario Carneiro]

that seems higher than the numbers we've been talking about

[Mario Carneiro]

the nonimplications are unfortunately inflated because I don't think the "facts" are being tracked anywhere

[Vlad Tsyrklevich]

10,657 I think. You can check https://teorth.github.io/equational_theories/dashboard/

[Mario Carneiro]

that's weird, it's not a typo

[Amir Livne Bar-on]

This is for the equations, before reducing to SCCs. So there are more edges.

[Vlad Tsyrklevich]

For raw facts, look here https://tsyrklevi.ch/general_raw_full_entries.json

[Vlad Tsyrklevich]

Mario Carneiro said:

that's weird, it's not a typo

Ah, that may just be duplicates

[Amir Livne Bar-on]

Your numbers look slightly higher, so maybe equations beyond 4694 are included?

[Vlad Tsyrklevich]

Oh yes, also sporadic equations. The two great confounders.

[Vlad Tsyrklevich]

There are 10 duplicates on main, the rest are sporadic I think.

[Mario Carneiro]

There seem to be no implications in general_raw_full_entries.json with finite = true

[Vlad Tsyrklevich]

You need a different output for that, want the finite one?

[Mario Carneiro]

not really, just checking

[Vlad Tsyrklevich]

The output is per graph, either general or finite.

[Mario Carneiro]

I would have thought the raw data just contains all the lean-proven theorems in whatever disposition

[Mario Carneiro]

I assume the finite facts are included though

[Vlad Tsyrklevich]

Yes.

[Mario Carneiro]

there is only one :)

[Mario Carneiro]

wait nevermind, I can't count

[Amir Livne Bar-on]

By the way, I checked and even if we remove the components for equations 1 and 2 there is a single connected component.

What would a cut get us, if we find one in an inner part of the graph? It'll probably make the proof simpler to write, but will take longer to verify?

[Vlad Tsyrklevich]

How is that possible? See https://teorth.github.io/equational_theories/graphiti/?render=true&neighborhood_of_distance=3&neighborhood_of=1076

[Vlad Tsyrklevich]

Ah wait, I'm only looking up from Eq2, not down from Eq1, yes that still makes sense.

[Mario Carneiro]

Horizontal cuts are better than vertical, but that doesn't help us much in this very flat graph

[Amir Livne Bar-on]

If anyone wants to play with the SCC-reduced graph, I'm attaching my data here (script, textual output, sqlite)

analyze_comps.py
comps_graph.db
comps_graph.txt

[Vlad Tsyrklevich]

Just an FYI, that a number of the stats we've discussed here and the exported data is now available on https://teorth.github.io/equational_theories/dashboard/

[Martin Dvořák]

Sorry; I don't have anything to contribute.
I just want to say that I am really happy that people work on this.

[Mario Carneiro]

I spent a while burning brain energy on this hasse diagram problem, and my conclusion is that my previous suggestion of using some kind of sweep across the poset doesn't work, or not well enough. The new plan is much simpler:

We want to prove every pair $A,B\in Laws$ is represented in the poset (either via implication or nonimplication). Call this property $\operatorname{Dec}(A\le B)$. We generalize to the predicate $\operatorname{Dec}(S\le T)$ where $S,T\subseteq Laws$, which asserts that $\operatorname{Dec}(A\le B)$ for all $A\in S, B\in T$. We now have the following rules:

• Split left: If $S_1\cup S_2=S$, then $\operatorname{Dec}(S_1\le T)\land \operatorname{Dec}(S_2\le T)\to \operatorname{Dec}(S\le T)$
• Split right: If $T_1\cup T_2=T$, then $\operatorname{Dec}(S\le T_1)\land \operatorname{Dec}(S\le T_2)\to \operatorname{Dec}(S\le T)$
• Nonimplies: If $M=min(S)$ is the set of minimal elements of S and $N=max(T)$ similarly, and $A\not\le B$ for all $A\in M,B\in N$, then $\operatorname{Dec}(S\le T)$.

The main strategy then for certificate generation is to pick a (preferably explicit) nonimplication $A\not\le B$ for which $|{\uparrow}A|\ |{\downarrow}B|$ is as large as possible (where ${\uparrow}A$ is the set of elements of $S$ above $A$ and likewise for ${\downarrow}B$), grow it if possible to $|{\uparrow}M|\ |{\downarrow}N|$ while maintaining the property that every element of $M$ is not below every element of $N$, then use the rules:

• split left with $S={\uparrow}M\cup (S\setminus {\uparrow}M)$
  • split right with $T={\downarrow}N\cup (T\setminus {\downarrow}N)$
    • nonimplies on $M, N$
    • recurse to prove $\operatorname{Dec}({\uparrow}M\le (T\setminus {\downarrow}N))$.
  • recurse to prove $\operatorname{Dec}((S\setminus {\uparrow}M)\le T)$.

Using only splitting, we get a quadratic size proof. But the nonimplies proof is proportional only to $|{\uparrow}M|\ |{\downarrow}N|$, and $M$ and $N$ will generally be very small here (usually 1) so this knocks out entire contiguous rectangles from the implication matrix at a time.

If the procedure fails to make progress, then there must not be any nonimplications remaining. Proof strategy TODO for this case