Equations vs Laws

Stream: Equational

[Terence Tao]

I propose to make a formal distinction between "equations" on one hand, and "laws" on the other. (Roughly speaking, equations are to semantics as laws are to syntax.)

A law is a formal string w == w' where w, w' are elements of the free magma FreeMagma ℕ over the natural numbers, and == is a formal equality symbol with no prior semantic content. A typical example of a law is the commutative law

0 ∘ 1 == 1 ∘ 0

An equation is an expression $f(x_1,\dots,x_n) = g(x_1,\dots,x_n)$ in several variables $x_1,\dots,x_n$ living in some magma G. A typical example of an equation is the commutative equation

x ∘ y = y ∘ x

for some variables x y: G.

Every law can be interpreted in a given magma as an equation; if the equation is universally satisfied by the magma, we say that the magma obeys the law. For instance, a magma G will obey the commutative law 0 ∘ 1 == 1 ∘ 0 if and only if the commutative equation x ∘ y = y ∘ x is obeyed for all x y : G. In the language of model theory, the former statement would be expressed as G ⊧ 0 ∘ 1 == 1 ∘ 0.

Right now, the Lean codebase is organized around equations, but as discussed in #Equational > Syntax , it would be preferable to organize it around laws instead. A start has been made at https://github.com/teorth/equational_theories/blob/main/equational_theories/FreeMagma.lean with the basic definitions of a free magma. I am working on updating blueprint with an outline of more API for free magmas, equations, and laws, which should appear on the repo soon (it is building as we speak).

Laws will be a better "back end" representation than equations because it is significantly easier to prove metatheorems about laws than about equations (they are elements of the type FreeMagma ℕ × FreeMagma ℕ, which can be equipped within Lean with a preorder (implication), a duality operation, etc.), whereas for equations this sort of structure can only be extracted through metaprogramming or from scraping tools external to Lean.

However, this still leaves the question of what to use for the "front end" - the representation that human and automated contributors will use by default. For instance, should the databases of equations and implications that are autogenerated be expressed using equations such as x ∘ y = y ∘ x, or laws such as 0 ∘ 1 == 1 ∘ 0? The conversion between the two is easy so this is mostly an aesthetic issue. Also, some API within Lean will be needed to convert, for instance, the assertion G ⊧ 0 ∘ 1 == 1 ∘ 0 that a magma G obeys the commutative law 0 ∘ 1 == 1 ∘ 0, with the (logically equivalent) assertion ∀ x y : G, x ∘ y == y ∘ x that G obeys the commutative equation x ∘ y = y ∘ x.

How should we proceed here? For instance, we could have every equation, e.g.,

abbrev Equation43 (G: Type u) [Magma G] := ∀ x y : G, x ∘ y = y ∘ x

paired with a law

abbrev Law43 := 0 ∘ 1 == 1 ∘ 0

(this requires some notation for == that has not yet been set up), as well as an easy theorem

theorem Equiv43 (G: Type u) [Magma G]: Equation43 G ↔ G ⊧ Law43

Not sure if this is the most efficient approach though.

[Shreyas Srinivas]

You can add syntax and unexpanders or notation to move from Lean's data type for the syntax and string representations.

[Shreyas Srinivas]

This is relatively straightforward and used in programming language theory a lot

[Adam Topaz]

I think all of this can be done in a straightforward way using lean4’s metaprogramming infrastructure. But I don’t see why you would want to use string representations for any of this.

[Shreyas Srinivas]

Data sets

[Shreyas Srinivas]

Stored in .txt files or CSV files

[Adam Topaz]

Ok, I understand, but I suppose you would want to parse a string to an expression representing a term in the free magma, and beyond that there should not be any need to use strings

[Shreyas Srinivas]

Yeah that was my idea

[Shreyas Srinivas]

Parse strings into TSyntax and serialise them on the other direction. But apart from that use lean syntax/notation

[Adam Topaz]

But why go via syntax and not just to expr?

[Adam Topaz]

The syntax still has to be elaborated to be useful

[Adam Topaz]

To be fair, the distinction between syntax and elaborated expressions is quite minimal in this case of magma words

[Shreyas Srinivas]

Sure that also works. Ultimately we just need magma term objects.

[Shreyas Srinivas]

We could simply write a parser and serialiser for magmas into lean.

[Shreyas Srinivas]

The notation stuff is to work nicely with infoview

[Shreyas Srinivas]

And inside lean in general

[Adam Topaz]

If you want to open an issue with what’s needed from the meta side then I’ll claim it

[Terence Tao]

One consideration is that I am expecting many contributors to not come with an background in advanced algebra, model theory, or the computer science of syntax. So it may be less intimidating for such contributors to use the language of equations such as ∀ x y : G, x ∘ y = y ∘ x rather than more abstruse-looking syntactical expressions such as G ⊧ 0 ∘ 1 == 1 ∘ 0. I'm hoping though that there is some way to use both equations and laws almost interchangeably, so that the representation one wants for a particular use case is primarily an aesthetic choice.

[Adam Topaz]

If we write elaborators, then at least in the infoview it would look completely familiar

[Terence Tao]

If one can set it up so that in the Lean front end it looks like equations, in the back end it is formalized as laws, and on the data end it can be text strings associated to either laws or equations, I guess it will work out. (It should be fairly trivial to convert a text string of a law to a text string of an equation; the only silly issue is that we have only specified the first six letters x y z w u v of the alphabet used in an equation, whereas the law string can handle any number of distinct variables.)

[Shreyas Srinivas]

within lean, I think you will find notation convenient

[Terence Tao]

I guess if it can be set up so that G ⊧ 0 ∘ 1 == 1 ∘ 0 and ∀ x y : G, x ∘ y = y ∘ x are definitionally equivalent then the distinction becomes essentially irrelevant to anyone working within Lean

[Shreyas Srinivas]

I don't understand. One is saying that for a specific instantiation of x and y to resp 0 and 1, G entails this equation. The other is a universally quantified property from which this relation can be derived. Definitionally equivlanet would mean I could go in the other direction: from one special case to a general rule

[Daniel Weber]

(deleted)

[Edward van de Meent]

Shreyas Srinivas said:

I don't understand. One is saying that for a specific instantiation of x and y to resp 0 and 1, G entails this equation. The other is a universally quantified property from which this relation can be derived. Definitionally equivlanet would mean I could go in the other direction: from one special case to a general rule

this notation uses numbers to refer to variables, rather than conventional letters. it does not carry the semantics usually assigned to 0 or 1.

[Terence Tao]

Oh perhaps I am using the entailment relation incorrectly. What I mean by G ⊧ 0 ∘ 1 == 1 ∘ 0 is that every interpretation of 0 1 in G represents 0 ∘ 1 == 1 ∘ 0 as a true equation. One could use something like G.obeys 0 ∘ 1 == 1 ∘ 0 if that is less confusing.

[Terence Tao]

One could set up a parallel copy of ℕ with copies x₀ x₁ x₂ ... of 0 1 2 ... (representing formal indeterminate variables) if this is less confusing, but for back end purposes at least it seems simpler to me to use the natural numbers directly to represent the indeterminates

[Edward van de Meent]

right, but for syntax purposes i'd expect using general identifiers shouldn't be difficult?

[Terence Tao]

I guess there is a slight tension between choices of notation that make it (a) easy for a human to read; (b) easy for an automated prover to read; and (c) easy for Lean to work with. Ideally I want all of (a), (b), (c), of course.

[Terence Tao]

Well the advantage of fixing the alphabet to be, say, ℕ, is that I can now easily formalize in Lean statements such as "The type FreeMagma ℕ × FreeMagma ℕ of laws is a pre-order (with respect to implication), with 0==0 as a minimal element, 0==1 as a maximal element, and the duality operation [to be defined] as a pre-order isomorphism".

[Edward van de Meent]

but what about 1 == 1?

[Terence Tao]

1 == 1 is equivalent to 0 == 0. It's a pre-order, not a partial order.

[Terence Tao]

If one quotients out by equivalence, one gets a partial order, but that's a different type

[Terence Tao]

in particular a type in which equality is likely undecidable, so not great to work with inside Lean. I think the pre-ordered type FreeMagma ℕ × FreeMagma ℕ will be a more convenient base type to encode the notion of a law.

[Edward van de Meent]

i think that using G ⊧ x ∘ y = y ∘ x should at the very least satisfy (c), and it's not too difficult for lean (i think) to parse, if one simply uses a DSL-embedding. (use order of appearance to assign numbers to identifiers). whether it satisfies (a) is not for me to judge

[Terence Tao]

I also want to refer to laws as first class objects. The expression x ∘ y = y ∘ x is of type Prop in Lean, I think? (assuming x y are already introduced as variables). This is why I wanted to introduce a distinct equality symbol == for laws

[Edward van de Meent]

what i mean by DSL embedding is we can define notation law(x ∘ y = y ∘ x) to refer to the law, not the prop

[Terence Tao]

Oh, that's nice

[Terence Tao]

didn't realize Lean's elaborator could do that

[Edward van de Meent]

yea, Lean's language extention feature is quite extensive :upside_down:

[Terence Tao]

we could then have the best of both worlds, with two notations law(x ∘ y = y ∘ x) and 0 ∘ 1 == 1 ∘ 0 to refer to the same Law object; it would internally be stored as basically the type FreeMagma ℕ × FreeMagma ℕ with some additional API, but this would be invisible to anyone not actually trying to prove metatheorems about equations.

[Terence Tao]

There would still need to be some general tool within Lean to equate G ⊧ x ∘ y = y ∘ x with ∀ x y : G, x ∘ y = y ∘ x though, since this is not going to be rfl

[Daniel Weber]

I think it's possible to make it defeq, but I'm not sure how well the kernel would like it, it might be very slow

[Edward van de Meent]

let me take a look if i can whip something up

[Terence Tao]

So there is always the quick and dirty solution I proposed above, which is to have both an equation and a law for each of the 4692 equations we care about, as well as 4692 theorems linking the two. Not elegant, but it would work and perhaps not choke the Lean compiler if it could be compiled once and then cached?

[Amir Livne Bar-on]

About the name == for the "law" operator - this makes sense to me as an easy-to-write symbol, and it looks good enough on chats and programming editors. But it doesn't render very nicely in latex. Maybe we can use a symbol such as \circeq there?

[Terence Tao]

I am partial to the idea of encoding implications using the pre-order one can place on Law, e.g., Law1163 ≥ Law3521, and anti-implications as ¬ Law1163 ≥ Law3521, so that the entire API of Mathlib.Order becomes available (in particular to do transitive closure etc.), but then we need some metatheorems that allow one to convert these statements to ∀ (G: Type *) (hG: Magma G): Equation1163 G → Equation3521 G and ∃ (G: Type *) (_: Magma G), Equation1163 G ∧ ¬ Equation3521 G respectively.

[Terence Tao]

I'm open to other suggestions on names. One could simply permit both to be used, for instance, since neither symbol collides with anything commonly used in Mathlib. EDIT: i misread your comment. Sure, i’ll change == to \circeq in the blueprint shortly.

[Shreyas Srinivas]

I think you can use ordinary variables instead of Nats.

[Shreyas Srinivas]

It's not super difficult. Lean already has a substantial parsing infrastructure

[Shreyas Srinivas]

There are countably many identifiers

[Shreyas Srinivas]

So you get the same cardinality for the variable set

[Terence Tao]

OK that would be nice. I had in my mind a conceptual separation between indeterminates (purely syntactic objects) and variables (quantities with a specified type), so for me it worked out well to use different symbols for the two (Nats for indeterminants, and x y z w u v for variables) but perhaps it would be easier for the majority of contributors to use the same symbol for both. So one could write things like G ⊧ x ∘ y = y ∘ x in one line of code (in which x y are purely syntactic indeterminates) and then x ∘ y = y ∘ x in a later line of code (where now x y : G are variables of type G) without either the human or Lean getting confused

[Terence Tao]

In LaTeX I typically use a different font to denote indeterminates (e.g., $G \models \mathrm{x} \circ \mathrm{y} = \mathrm{y} \circ \mathrm{x}$) as opposed to variables (e.g., $x \circ y = y \circ x$) but I don't think Lean supports fonts

[Edward van de Meent]

Shreyas Srinivas said:

I think you can use ordinary variables instead of Nats.

by this, do you mean to use FreeMagma String? or something else?

[Shreyas Srinivas]

Lean ident

[Adam Topaz]

That's an alias for all of Syntax, you probably want to use Name instead:

import Lean

open Lean

inductive MagmaWord where
  | of : Name → MagmaWord
  | mul : MagmaWord → MagmaWord → MagmaWord
deriving Repr

declare_syntax_cat magma_word

syntax ident : magma_word
syntax "(" magma_word "∘" magma_word ")" : magma_word

partial
def elabMagmaWord : Syntax → MetaM Expr
  | `(magma_word|$i:ident) => Meta.mkAppM ``MagmaWord.of #[toExpr i.getId]
  | `(magma_word|($i ∘ $j)) => do
    let i ← elabMagmaWord i
    let j ← elabMagmaWord j
    Meta.mkAppM ``MagmaWord.mul #[i,j]
  | _ => Elab.throwUnsupportedSyntax

elab "elabMagmaWord" w:magma_word : term => elabMagmaWord w

#eval elabMagmaWord ((x1 ∘ x2) ∘ x3)

[Edward van de Meent]

i was already on a similar path:

syntax ident:magma_term

syntax magma_term "∘" magma_term : magma_term
syntax "(" magma_term ")" : magma_term

declare_syntax_cat magma_law

syntax magma_term "=" magma_term : magma_law


partial def elabMagmaTerm : Syntax → MetaM Expr
  | `(magma_term| $n:ident) => do

    mkAppM ``FreeMagma.Leaf #[mkStrLit n.getId.toString]
  | `(magma_term| $l:magma_term ∘ $r:magma_term) => do
    mkAppM ``FreeMagma.Fork #[← elabMagmaTerm l, ← elabMagmaTerm r]
  | `(magma_term| ($t:magma_term)) => elabMagmaTerm t
  | _ => throwUnsupportedSyntax

partial def elabMagmaLaw : Syntax → MetaM Expr
  | `(magma_law| $l:magma_term = $r:magma_term) => do
    mkAppM ``Prod.mk #[← elabMagmaTerm l, ← elabMagmaTerm r]
  | _ => throwUnsupportedSyntax


elab "law{" l:magma_law "}" : term => elabMagmaLaw l

#check law{x ∘ y = ζ}

[Adam Topaz]

Nice!

[Edward van de Meent]

this elaborates to a FreeMagma String, for which we can likely write a simple function to transform it into FreeMagma Nat in a canonically reduced way?
right now i'm still concerned a bit about the fact that i haven't mentioned to lean if ∘ is left- or right-associative, could someone give me a pointer?

[Shreyas Srinivas]

With the syntax approach you will need unexpanders. I think if you express the above with notation you will get the unexpanders for free

[Adam Topaz]

BTW, if you're happy to use json for serializing words, you could get the serialization and parsing automatically by deriving ToJson and FromJson. Using json might be useful anyway as it's easy to parse with essentially all other programming languages and already has the correct tree structure.

[Terence Tao]

One thought: we could have a custom tactic to convert inequalities or anti inequalities between laws to their equational counterparts or vice versa. Then it is just one line of Lean code invoking the tactic to pass back and forth

[Adam Topaz]

An alternative is to do something similar to the reassoc attribute to automatically generate the equational lemmas from proofs of inequalities

[Terence Tao]

Terence Tao said:

One thought: we could have a custom tactic to convert inequalities or anti inequalities between laws to their equational counterparts or vice versa. Then it is just one line of Lean code invoking the tactic to pass back and forth

e.g. if one has to prove Law25 ≥ Law166, the tactic (let's call it eqintros for sake of argument) would introduce G: Type *, [Magma G], h: Equation25 G, and enough variables x y z: G to state Equation166 G x y z, which is now the goal. If one instead had to prove ¬ Law25 ≥ Law166, a separate tactic (e.g., counterexample G hG x y z) would take a magma (G:Type *) (hG: Magma G) and return two goals: one to show Equation25 G (perhaps introducing relevant variables first), and the other to disprove Equation166 G x y z.

[Terence Tao]

Actually with the tactic approach, we no longer actually need the EquationX abbrevs, the tactic handles the unfolding of all the LawX to appropriate universally quantified statements.

[Amir Livne Bar-on]

We probably want a more general tactic in addition to counterexample, that converts to the existential, in case we find a non-constructive proof? And then counterexample = notimplies.exists + use

[Edward van de Meent]

Shreyas Srinivas said:

With the syntax approach you will need unexpanders. I think if you express the above with notation you will get the unexpanders for free

i'm having trouble finding a way to express this with merely notation, and looking at the metaprogramming guidebook i'm having a hard time writing unexpanders or delaborators... could someone else give it a go?

[Shreyas Srinivas]

Unexpanders are a pain to write, especially when you want to embed lean declarations which expand into a magma term. If no one takes it up, I'll try in a few hours when I am on a machine.

[Shreyas Srinivas]

Inside which PR can I find this in? Also did you try notation3?

[Edward van de Meent]

my approach was the DSL approach, as described in the metaprogramming book.
find my code at equational#113

[Cody Roux]

Dang y'all are fast; I'm almost done with soundness, so we'll have a "deep" proof system at least.

[Terence Tao]

I just created a task equational#114 to set up the standard API for homomorphisms between magmas, I have a feeling this will be useful in all the other syntactic tasks, including equational#104 and the rest of equational#36.

[Shreyas Srinivas]

Edward van de Meent said:

my approach was the DSL approach, as described in the metaprogramming book.
find my code at equational#113

I think I can make notation work for this bit

[Terence Tao]

@Cody Roux How are you planning to formalize equations in Lean? As pairs in FreeMagma X for some alphabet X?

[Cody Roux]

https://github.com/teorth/equational_theories/pull/115

[Cody Roux]

Correct, just pairs (with names), I call them lhs and rhs, as is tradition, and use the notation ≃ (\simeq) because it's close to what's in "Term Rewriting and All that".

[Cody Roux]

All this can be easily changed before merge, I'm about to start on Birkhoff's theorem though I need to remember how quotients work in Lean.

[Shreyas Srinivas]

I would put the pair behind a constructor.

[Cody Roux]

A record is exactly an inductive with a single constructor, if that's what you mean.

[Cody Roux]

I call it SynEqn, though I'm not in love with the name (seems Synfull)

[Terence Tao]

I think Law would be a good name, I think it is rather consistent with the universal algebra literature (but I'd love for a universal algebraist to weigh in on this!)

[Terence Tao]

I like \simeq, I think I will adopt it for the blueprint

[Cody Roux]

I think we lost most of them to category theory, sadly, TRaAT calls them "Σ-identities". I'll go with Law for now though.

[Edward van de Meent]

unfortunately that will collide with mathlibs notation for Equiv

[Edward van de Meent]

i think MagmaLaw would be a bit more descriptive...

[Shreyas Srinivas]

Use a higher priority

[Shreyas Srinivas]

You can override an imported notation by increasing the priority of your declaration

[Terence Tao]

I was proposing in equational#114 to introduce MagmaHom and MagmaEquiv, so MagmaLaw will fit right in

[Terence Tao]

"commutative law" and "associative law" are in widespread use even in undergraduate mathematics, so I hope the meaning of "law" should be pretty accessible to the target audience here

[Shreyas Srinivas]

@Edward van de Meent : May I start working on equational#113?

[Shreyas Srinivas]

I don't want to create merge conflicts for you

[Adam Topaz]

This may have been discussed elsewhere, but, concerning MagmaHom is there a reason the project is not using Mul and docs#MulHom ?

[Terence Tao]

Adam Topaz said:

This may have been discussed elsewhere, but, concerning MagmaHom is there a reason the project is not using Mul and docs#MulHom ?

Reposting my previous comment from the syntax thread:

Terence Tao12:17 PM

By the way, I initially used [Mul α] (or more precisely [Add α]) to encode Magmas but then ran into weird instance diamond issues when trying to create counterexample Magmas in which I wanted to redefine the addition or multiplication law on, say, the natural numbers. This was why I eventually created a new Magma class with a new infix symbol ∘that did not conflict with the existing + and *symbols. By doing so I forego any API that Mathlib already has for [Mul α] or [Add α], but for this project I'm not expecting much synergy with Mathlib anyway (although the API for basic number systems is useful to verify axioms for counterexamples, e.g., using ring, and simp has been working wonders also).

[there is also the psychological effect that I at least think of a Mul structure as likely to be associative.]

[Adam Topaz]

I see. Thanks.

[Edward van de Meent]

Shreyas Srinivas said:

Edward van de Meent : May I start working on equational#113?

Feel free, I won't be able to work on it anyway while I'm asleep

[Shreyas Srinivas]

Thanks. Will get to it now

[Shreyas Srinivas]

Done

[Shreyas Srinivas]

Also your MagmaLaw was capturing identifiers as strings. So if I had defined x to be some other Magma, you would end up with a magma law that treated x as a new identifier

[Shreyas Srinivas]

There is some complicated quoting and unquoting that I have seen experts use and that's a huge reason to use notation whenever you can

[Shreyas Srinivas]

I suspect I can also recover the usual composition notation.

[Shreyas Srinivas]

Nvm, I think you are using it as notation for the Magma typeclass, so it makes very little sense to overload it.

[Shreyas Srinivas]

@Terence Tao : I simplified the DSL, but I want to ask if you would still like Magma "laws" to be tagged as such

[Shreyas Srinivas]

see examples : https://github.com/teorth/equational_theories/pull/113/files

[Shreyas Srinivas]

I added the tag magma law: to denote magma laws.
Examples without and with this tag can be found respectively on the left and right hand side panel of this link : https://github.com/teorth/equational_theories/pull/113/commits/022d8de73ed0cd2f90894c7d8ec27900072d0e61

EDIT: It seems I may have posted two variations on labelling magma laws. Nevertheless, the previous two links can show the comparisons when taken together.

[Cody Roux]

Done with completeness! I'm not sure how what I've done clashes with the discussion above; I'm happy to amend the PR: https://github.com/teorth/equational_theories/pull/115

[Cody Roux]

Hopefully only notation needs to be updated (if that)

[Terence Tao]

Shreyas Srinivas said:

Terence Tao : I simplified the DSL, but I want to ask if you would still like Magma "laws" to be tagged as such

I'm not sure what the precise technical advantages of this are, but as long as it is easy for automated tools (either within Lean, or external scrapers) to collect all the laws that are defined in a given file (in particular, presumably Equations.lean and AllEquations.lean will eventually transition over to defining some laws, rather than the current situation of having them define equations), it should be fine.

[Shreyas Srinivas]

These are essentially independent issues. There should be no trouble extracting these laws as data. The notation labelling merely allows readers of the code to separate laws from other stuff

[Shreyas Srinivas]

Cody Roux said:

Hopefully only notation needs to be updated (if that)

I think your notation mostly matches what we have.

[Cody Roux]

I now notice that the definitions in the completeness proof uses modelsEq instead of "satisfies" in the doc, that's an easy change, but there's also models and modelsSet which need more harmonious names.

Certainly I should have used modelsLaw at least.

[Cody Roux]

The notations seem to align.

[Terence Tao]

Shreyas Srinivas said:

These are essentially independent issues. There should be no trouble extracting these laws as data. The notation labelling merely allows readers of the code to separate laws from other stuff

It looks like a fairly lightweight addition to the code, so I'm happy to put it in. There should basically only be two files where we have to create laws, namely Equations.lean and AllEquations.lean, all the other files will just import these files (which I expect to be rather stable, other than the occasional transferring of a law from the latter to the former), so if we add relevant tags and stuff to these files it shouldn't affect the workflow of most of the contributors.

[Shreyas Srinivas]

Okay. So based on the above message @Cody Roux : only a cosmetic change in the notation of laws is required. I think the easiest thing is to borrow the notation I just wrote for MagmaLaw

[Cody Roux]

Where is it defined?

[Shreyas Srinivas]

It's in

Shreyas Srinivas said:

I added the tag magma law: to denote magma laws.
Examples without and with this tag can be found respectively on the left and right hand side panel of this link : https://github.com/teorth/equational_theories/pull/113/commits/022d8de73ed0cd2f90894c7d8ec27900072d0e61

EDIT: It seems I may have posted two variations on labelling magma laws. Nevertheless, the previous two links can show the comparisons when taken together.

It's in the link

[Shreyas Srinivas]

Another thing, we can use a little trick to define the notation for derive beforehand

[Shreyas Srinivas]

And use it in the inductive type

[Cody Roux]

Ah that'd be nice! I knew this in Coq, but I didn't figure it out in Lean.

[Cody Roux]

Let me try to fix rebase-hell and fix the notation thing.

[Shreyas Srinivas]

I just added the suggestion as a review comment.

[Cody Roux]

Whew, I don't know how I always bork things up with Git. Thanks for the suggestion @Shreyas Srinivas. I'll refer to the correct MagmaLaw notation as soon as it's merged.

[Cody Roux]

Hey, I have compactness now! https://github.com/codyroux/equational_theories/blob/0827d2a480dd8c82b66974f7819cd674ca192f81/equational_theories/Compactness.lean#L81

I'll create a PR if desired, but for now I'll just sleep.

[Edward van de Meent]

Shreyas Srinivas said:

Also your MagmaLaw was capturing identifiers as strings. So if I had defined x to be some other Magma, you would end up with a magma law that treated x as a new identifier

Indeed, as the purpose of the syntax I suggested was to capture concrete laws.

[Edward van de Meent]

It seems we had different ideas in mind as to the purpose of the syntax

[Edward van de Meent]

In my mind, it would be a way to construct a concrete law

[Shreyas Srinivas]

It constructs the same concept

[Shreyas Srinivas]

It's just that with notation to construct a term in multiple pieces

[Edward van de Meent]

It doesn't. What you defined constructs laws with free variables

[Edward van de Meent]

That's not a concrete law

[Shreyas Srinivas]

I actually only replaced the syntax parts

[Edward van de Meent]

The elaboration is different now

[Edward van de Meent]

It was on purpose that it turned the identifiers into strings

[Shreyas Srinivas]

Yeah it creates free variables

[Shreyas Srinivas]

A Leaf Node

[Edward van de Meent]

A leaf node is not the same as a free variable

[Shreyas Srinivas]

But that's exactly what you were doing in line 24

[Shreyas Srinivas]

Screenshot_20240930-092901.png

[Shreyas Srinivas]

What I have done is an exact syntactic replacement

[Edward van de Meent]

It isn't? Your code doesn't produce leaf nodes

[Edward van de Meent]

You changed the semantics

[Shreyas Srinivas]

One second

[Edward van de Meent]

and the syntax

[Shreyas Srinivas]

I'll check it again. Not on a laptop

[Shreyas Srinivas]

I simply removed the extra syntax you had built which still elaborated to a freemagma structure

[Shreyas Srinivas]

We can reintroduce it

[Shreyas Srinivas]

But from the point of view of theorems, I don't see the difference. Lean will see the same Expr

[Shreyas Srinivas]

And so the same theorems will be true modulo the fact that my second example would be a syntax error in your case, which would only be disallowing you to construct large terms in many steps.

[Shreyas Srinivas]

The only difference is in surface level syntax

[Shreyas Srinivas]

Shreyas Srinivas said:

I simply removed the extra syntax you had built which still elaborated to a freemagma structure

We can replicate your syntax in the file by altering the FreeMagma notation, but the outcome is the same

[Shreyas Srinivas]

To make my claim more concrete, lean is seeing the same Expr object in both our syntaxes (except the star notation instead of \o, but this can be changed). So the metatheorems that can be proved are identical. Only the surface rendering of syntax has changed, and now we can construct the Expr in many steps and get the unexpander for free. I haven't altered the semantic content in anyway (I might have added the universe polymorphism thing)

[Shreyas Srinivas]

But yeah the changes can be reset or rolled back

[Edward van de Meent]

it was my intention to eventually have law{x * y = y * x} (modulo notation for Fork) translate effectively to (Fork (Node 0) (Node 1),Fork (Node 1) (Node 0)), with explicit nodes. (i.e. always interpret identifiers inside law{...} as variables of the law)

[Shreyas Srinivas]

Ah then the syntax that was there before doesn't quite do that

[Shreyas Srinivas]

It simply interprets identifiers as is

[Edward van de Meent]

indeed, but it does already produce the nodes. changing from String to Nat is a matter of defining a recursive function, and applying it.

[Edward van de Meent]

in that sense, interpreting the identifiers as String does help along the way.

[Shreyas Srinivas]

Right, so I just took the syntax def and converted it

[Shreyas Srinivas]

And then removed what felt like redundant Notation

[Shreyas Srinivas]

I have a suggestion though. These indices can be hard to maintain

[Edward van de Meent]

what indices?

[Shreyas Srinivas]

Nat indices that you use for variables

[Edward van de Meent]

how do you mean maintain?

[Shreyas Srinivas]

You would need to track multiple occurrences of the same variable through rewrites, simplifications, and substitution

[Shreyas Srinivas]

I am guessing

[Edward van de Meent]

i was under the impression that we won't do those operations on laws, but rather on equations.

[Edward van de Meent]

so imo that's a non-issue

[Shreyas Srinivas]

Okay, but then you will need that for equations

[Shreyas Srinivas]

In any case, adapting this notation to the Nat index variables is not too hard

[Shreyas Srinivas]

The current notation is, modulo surface level syntactic differences, just the same as the syntax as it was in the file before.

[Edward van de Meent]

that's not true?

[Shreyas Srinivas]

How is it different?

[Edward van de Meent]

like i said, your syntax produces free variables, while mine produces nodes

[Shreyas Srinivas]

Shreyas Srinivas said:

Screenshot_20240930-092901.png

Not here

[Shreyas Srinivas]

Anyway, I think there is still one challenge

[Shreyas Srinivas]

With nat indexed Nodes

[Shreyas Srinivas]

When translating syntax recursively, for each identifier, you have to keep track of whether it has already been assigned a number or not

[Shreyas Srinivas]

And how many numbers have already been used for up for variables.

[Shreyas Srinivas]

Invariably this will require a 'context' that maps Nats to identifier strings.

[Edward van de Meent]

with your syntax, #check magma law: x ⋆ (combine x y) ⋆ z ≃ z requires x:FreeMagma ?m, which is not an explicit leaf. it can be a fork.

[Edward van de Meent]

so it is not the same.

[Shreyas Srinivas]

Okay, we can actually get the underlying Expr

[Shreyas Srinivas]

I think I see your point in that you don't want identifiers to represent FreeMagma terms

[Shreyas Srinivas]

This can be fixed.

[Shreyas Srinivas]

The fix is to add a separate identifier type, and a FreeMagma "var" constructor that takes values of this type.

[Shreyas Srinivas]

@Edward van de Meent : we can roll the notation to your commit if that is your preference. Here is an example for unexpanders I wrote a year ago:

[Bhavik Mehta]

You might like to compare with the formulae in mathlib's model theory, which already seems to have many of the features you are discussing (in particular nat indexed nodes and correct assignment)

[Terence Tao]

Opened equational#147 to formalize the base versions of tactic mentioned earlier, tentatively named equation_to_law and law_to_equation, though other name suggestions are welcome.

[Eric Wieser]

Terence Tao said:

Terence Tao said:

One thought: we could have a custom tactic to convert inequalities or anti inequalities between laws to their equational counterparts or vice versa. Then it is just one line of Lean code invoking the tactic to pass back and forth

e.g. if one has to prove Law25 ≥ Law166,

I think that actually Lean is already happy for you to use equalities like this using the existing Equation25 ≤ Equation166?

[Eric Wieser]

Via the LE instance on function types and on propositions:

import Mathlib.Order.Basic

-- change to Mul just to make a mwe
abbrev Equation1 (G: Type _) [Mul G] := ∀ x : G, x = x
abbrev Equation2 (G: Type _) [Mul G] := ∀ x y : G, x = y

-- this spelling of implication is legal!
theorem foo : Equation2 ≤ Equation1 := by
  intros G _inst _h x
  rfl

[Edward van de Meent]

the issue with that is that for all those we'll have all of them equivalent?

[Shreyas Srinivas]

Yeah I don't think mathlib type classes ought to be used when developing a syntactic metatheory

[Edward van de Meent]

or almost all, since they represent the statement "for all magmas G, this holds" nvm i think i was confused

[Eric Wieser]

Edward van de Meent said:

the issue with that is that for all those we'll have all of them equivalent?

What do you mean by this?

[Eric Wieser]

Shreyas Srinivas said:

Yeah I don't think mathlib type classes ought to be used when developing a syntactic metatheory

I don't think there is any reason to reject Pi.instLE from mathlib if it's useful.

[Eric Wieser]

To be clear, I'm not arguing against building the metatheory; but if you're going to use ≤ in the metatheory, why not also use it in the theory for consistency?

[Andrés Goens]

Eric Wieser said:

Via the LE instance on function types and on propositions

oh, I had a PR for that, not sure if it's the same (PR: equational#135, issue: equational#132)

[Andrés Goens]

(as in, not sure if you're saying we'd get the same instance synthesized from Mathlib somewhere)

[Shreyas Srinivas]

It's a design issue. When you are invoking any mathlib typeclass, you also get a number of other theorems and equalities that come with that typeclass. It is easier to build and study syntactic relations you need from scratch as inductive types so that you start with the weakest form of that relation.

[Shreyas Srinivas]

Namely the one that lean's definitional equality gives it.

[Edward van de Meent]

i think it should be enough to allow it, so long as we add proofs that it means what you think it means.

[Eric Wieser]

Edited above with an example, the definitional equality is the same as the one you'd write by hand

[Eric Wieser]

So you can get the order structure you want on laws by just pulling back from the order structure on equations

[Edward van de Meent]

i'm basically finished making the delaborator (unexpander) for laws. i'm pretty sure that people with more experience writing code related to the prettyprinter can touch it up more though, so if, for example, you know how to work the parenthesiser, feel free to suggest a change. however, please make sure the examples still work as documented... find the code here

[Edward van de Meent]

a small excerpt:

-- magmaterm{(x ∘ (y ∘ (z ∘ zks)))} : FreeMagma String
#check magmaterm{x ∘ y ∘ (z ∘ zks)}

-- magmalaw{x ∘ y ∘ z ≃ z} : MagmaLaw String
#check magmalaw{x ∘ y ∘ z ≃ z}

-- magmalaw{x ∘ y ≃ y ∘ x} : MagmaLaw Nat
#reduce reduce_law magmalaw{x ∘ y ≃ y ∘ x}

-- magmalaw{x ∘ y ≃ y ∘ x} : MagmaLaw Nat
#check MagmaLaw.mk
  (FreeMagma.Fork (FreeMagma.Leaf 0) (FreeMagma.Leaf 1))
  (FreeMagma.Fork (FreeMagma.Leaf 1) (FreeMagma.Leaf 0))

[Edward van de Meent]

code style nitpicks are welcome too

[Shreyas Srinivas]

I think you should test this setup by proving a few syntactic theorems. While doing so, do check if the unexpander experience is optimal.

[Edward van de Meent]

i've written a proof about equation1 and equation2 as examples. it's not trivial to transform the goal into the usual shape, but that's not an issue with the notation/unexpander, just with the fact that we're doing meta theorems. it is definitely imaginable that a tactic does the "meta"-transformation.

[Edward van de Meent]

another feasible addition might be some sort of "escaping" syntax to allow variables to be used in declaring laws and expressions.

[Eric Wieser]

it's not trivial to transform the goal into the usual shape

i would expect it to be straightforward to train dsimp to do this

[Edward van de Meent]

I dont know, can dsimp turn quantification over f:a->b into multiple quantification over b, for every point where f is evaluated?

[Edward van de Meent]

Because I don't think that's defeq

[Edward van de Meent]

(i suspect there's a way to make this work anyway, but i also suspect it involves a custom elaborator)

[Eric Wieser]

Where are you defining the conversion between laws and Prop?

[Eric Wieser]

I'm confused by the three different PRs doing this

[Shreyas Srinivas]

I think the project is moving in a more distributed fashion

[Edward van de Meent]

here

[Eric Wieser]

Ah I see, it reduces to ∀ (f : ℕ → G), f 0 ∘ f 1 = f 1 ∘ f 0 rather than the nested quanfiers you could get by having a special evaluation function for Fin-indexed equations

[Edward van de Meent]

i suppose you could recursively define the "support" of the law, and then make the domain of f only that support (or something like that)...

[Edward van de Meent]

but i still don't know that that would allow dsimp to "unfold" the universal quantifier...

[Cody Roux]

Yep that's how it works in https://leanprover-community.github.io/mathlib4_docs/Mathlib/ModelTheory/Syntax.html#FirstOrder.Language.BoundedFormula

[Cody Roux]

Not sure it's worth the hassle here, since there's only quantifiers at the top level.