Definitional commutativity

Stream: general

[Daniel Weber]

Is it possible to define boolean operators such that commutativity is definitional? Concretely, I'm looking for something which could be used for Or' here:

def Or' (p q : Prop) : Prop := sorry

theorem Or'_eq_Or : Or' = Or := sorry

variable (p q : Prop)

#guard_expr Or' p q =~ Or' q p

[Kevin Buzzard]

Why?

A few years ago when we were trying to figure out how to do homological algebra in lean a related question came up: could we redefine addition on the naturals and integers such that associativity was rfl? I think the conclusion was that even if it were possible (and I don't think anyone ever managed to do it) the question was moot anyway because core would not be accepting such a PR.

[Luigi Massacci]

Now I’m genuinely curious as to how that came up while doing homological algebra

[Markus Himmel]

You can try to write down the definition of a chain complex and see for yourself where it goes wrong :) There have been many threads on Zulip about this over the years. The first I could find is #general > morphisms between objects that are "equal" @ 💬 . Mathlib has a rather elegant solution for this; see the module doc for file#Algebra/Homology/ComplexShape.

[Niels Voss]

This is super informal, so take it with a grain of salt, but if such an Or' could exist, wouldn't that mean that both Or' p q and Or' q p reduce to the same expression E[p,q] depending on p and q? This would mean that E[p,q] and E[q,p] are definitionally the same, but since they are both irreducible, if they are syntactically different this would mean that Or' p q has essentially two normal forms. So either E[p,q] is syntactically symmetric with respect to p and q, or Or' p q has two normal forms. Either of these options seems really strange to me, so I'd be surprised if you could find a way to make this work.

[Daniel Weber]

Kevin Buzzard said:

Why?

A few years ago when we were trying to figure out how to do homological algebra in lean a related question came up: could we redefine addition on the naturals and integers such that associativity was rfl? I think the conclusion was that even if it were possible (and I don't think anyone ever managed to do it) the question was moot anyway because core would not be accepting such a PR.

I'm just curious, not for any real usage

[Riccardo Brasca]

Luigi Massacci said:

Now I’m genuinely curious as to how that came up while doing homological algebra

Long story short: if you define a complex of groups (that mathematically is just a group G_i for every integer i and maps d_i : G_i → G_(i+1) such that the composition of two consecutive maps is zero) just as a function ℤ → GroupCat with the maps then Lean complains that the composition d_(i-1) with d_i is meaningless, because it doesn't realize that G_(i-1+1) and G_i are the same.

[Riccardo Brasca]

the same happens with various operations on ℤ, and definitional equality would help.

[Trebor Huang]

Commutativity is impossible unless the type theory directly supports it (for example universe levels are definitionally commutative, but obviously that can't be leveraged here). Associativity can be done via the D-List technique. We define AssocNat as a function Nat -> Nat that commutes with successor. Then addition is just composition which is definitionally associative (there is that extra component, but Prop-valued types are definitional subsingletons so it doesn't matter). This should be generalizable to make definitionally associative categories via representable functors, but I haven't thought about it.

[Kevin Buzzard]

I think the OG thread where associativity was first mentioned was this one. If you have a graded algebra graded by pieces $A(n)$ and multiplications $A(i)\times A(j)\to A(i+j)$ then stating associativity in the naive way results in a type mismatch as $A((i+j)+k)$ and $A(i+(j+k))$ aren't defeq.