Metatheory: meta-thread

Stream: Equational

[Cody Roux]

Given that I've been having a hard time keeping track of what's going on with metatheory tasks, I wanted to ask what the thoughts were on how to organize it; generally I have the intuition that smaller files mean fewer conflicts, with the risk that definitions are duplicated, which is already the case with MagmaLaws, and is at risk between the pre-order on laws and ordinary semantic entailment as exist in Completeness.lean.

So how should we organize?

[Terence Tao]

I'm hoping that the metatheory codebase is still small enough that it is relatively easy to refactor to align notation and remove duplicates after the fact. But it's good to have a stream here to try to coordinate.

There is the question of whether we want the magma code to be up to Mathlib standards for eventual porting. One could argue that Mathlib would prefer magmas to be modeled using [Mul] rather than [Magma]...

[Terence Tao]

I think a lot of issues with redundancy can be mitigated with reasonable API. For instance, while it would be nice if E ≥ F and {E} ⊧ F were definitionally equal, having a theorem saying that they were logically equivalent would be enough for our purposes.

[Cody Roux]

I actually wonder if they aren't definitionally equal at the moment in PR https://github.com/teorth/equational_theories/issues/132, just masked by a bunch of definitions.

[Terence Tao]

One could try proving the equivalence, it could potentially just be rfl.

[A.]

If you are really interested in merging with Mathlib at some point, worth noting that currently in Mathlib the order defined by implication is the other way round

[Terence Tao]

Oof, this is an issue we need to discuss and get consensus on. Intuitively I view a stronger law as “larger” than a weaker one, which is how the ordering is currently structured (and how the Hasse diagrams are oriented), but on the other hand a stronger law is satisfied by a smaller set of magmas so is “smaller” than a weaker law which I guess explains the Mathlib perspective. So which option will participants prefer?

1. Maintaining the current convention of stronger \geq weaker despite incompatibility with Mathlib
2. converting to the Mathlib convention stronger \leq weaker and changing all existing code, documentation, and visuals (except for legacy visuals) accordingly

[Edward van de Meent]

from the point of Prop, it makes sense though, as False is also known as bottom ⊥ while true is top ⊤. with the ordering where (. ≤ .) is the same as (. → .), this makes sense because indeed False is the bottom element of the lattice (and likewise for True).

[Adam Topaz]

For relations the motivation is that for two relations $R$ and $S$ on a type $X$, $R \le S$ induces a map $X/R \to X/S$. So in this sense, this is a "covariant" convention.

[Edward van de Meent]

let's make a poll:

[Andrés Goens]

Terence Tao said:

One could try proving the equivalence, it could potentially just be rfl.

I did prove the equivalence (it's implies_eq_singleton_models), it seems it's not quite definitional equal, at least if I replace the simp only with dsimp only it doesn't go through. At this point there's nothing preventing us to just swap it around, make that the definition and the current definition a characterization

[Edward van de Meent]

/poll What should be the ordering on MagmaLaw
(. → .) the same as (. ≤ .), like mathlib
(. → .) the same as (. ≥ .), unlike mathlib

[Andrés Goens]

Terence Tao said:

Oof, this is an issue we need to discuss and get consensus on. Intuitively I view a stronger law as “larger” than a weaker one, which is how the ordering is currently structured (and how the Hasse diagrams are oriented), but on the other hand a stronger law is satisfied by a smaller set of magmas so is “smaller” than a weaker law which I guess explains the Mathlib perspective. So which option will participants prefer?

1. Maintaining the current convention of stronger \geq weaker despite incompatibility with Mathlib
2. converting to the Mathlib convention stronger \leq weaker and changing all existing code, documentation, and visuals (except for legacy visuals) accordingly

just to be sure, if we change it that, would we also change it in the blueprint and the Hasse diagrams? (I'd vote for consistency between those three over consistency with Mathlib, so my opinion depends on that)

[Edward van de Meent]

the hasse diagrams use arrows afaik, so i don't think this changes anything for that?

[Terence Tao]

My thought is to just add a caveat to any legacy diagrams that the arrows are reversed from the new conventions, which we would enforce for diagrams going forward. The blueprint would only need to be changed in a few places (eg when referring to minimal and maximal elements) since we mostly use “implies” instead of \geq or \leq.

[Terence Tao]

new hasse diagrams would presumably ne inverted with x=x at the top and x=y at the bottom with either downward pointing arrows or upward pointing implication symbols (not sure which is better)

[Terence Tao]

/poll ASSUMING we reverse the partial ordering (so that (. → .) the same as (. ≤ .)), how should Hasse diagrams be oriented going forward?
x=y on top, x=x on bottom, -> downward arrows (current setup, incompatible with new ordering)
x=x on top, x=y on bottom, -> downward arrows
x=x on top, x=y on bottom, => upward arrows
x=x on top, x=y on bottom, unoriented edges
x=y on top, x=x on bottom, -> upward arrows
x=y on top, x=x on bottom, => downward arrows
x=y on top, x=x on bottom, unoriented edges

[Terence Tao]

Lots of options on how to orient Hasse diagrams... would be interested in people's views

[Edward van de Meent]

imo, so long as the edges are labeled in direction of the implication, what side is up or down doesn't matter too much to me

[Edward van de Meent]

i wouldn't even object to sideways if that for some reason is easier to render

[Terence Tao]

Based on the above polls, I have announced a refactor to reverse the ordering on laws and the recommended ordering on Hasse diagrams, see #Equational > REFACTOR I: Reversing the ordering on laws . Any further discussion of ordering issues should be made at that thread. However, this thread can continue to be used for other metatheory issues aside from ordering.

[Andrés Goens]

@A. just pointed out that the order was the same as in mathlib already in the code (but not in the blueprint), so in equational#273 I messed it up (should have checked more carefully, I'm always confused by such 50-50 conventions). I've fixed this in equational#289, proving the subset inclusion too for good measure