Equality vs. definitional equality when taking quotients

Stream: general

[Axel Boldt]

I must admit that I don't completely understand the difference between definitional equality and equality. That's probably why the following statement in Mathematics in Lean about quotient groups gives me a hard time:

the type G ⧸ N really depends on N (up to definitional equality), so having a proof that two normal subgroups N and M are equal is not enough to make the corresponding quotients equal.

What's the issue here? I would expect that if f : Type → Type and N = M, then f N = f M. Is that true, and if so, doesn't it resolve the above problem?

Further, in ordinary math, N = M implies G/N = G/M. Is it at all problematic that math-equality and Lean-equality diverge here?

[Kyle Miller]

The sentence does not seem to be accurate as it is. If N is definitionally equal to N', then G ⧸ N is definitionally equal to G ⧸ N', and also if N = N' then G ⧸ N = G ⧸ N'.

The thing about mere propositional equality of types though is that it's got lots of bad properties. Basically you only ever want definitional equalities. The suggestion after that paragraph that if N = N' you get an isomorphism G ⧸ N =* G ⧸ N' is an important part of the picture, since this is how you can avoid propositional equalities of types.

My guess is that the quoted sentence means to say "is not enough to make the corresponding quotients definitionally equal". The slip might be because definitional equal types is the only kind of equality you'd seriously consider (most of the time).

Am I misunderstanding this, @Patrick Massot?

[Mirek Olšák]

That looks confusing to me too. I would expect G / N = G / M should be easily provable too, and this is just a warning about using such quotients in practice.

Let me explain my view on definitional equality: Two expressions are definitionally equal if they are "obviously enough" equal to the kernel. There is a specific definition of what that means (expanding definitions, other reductions...) but that is a bit secondary. The most important moment if something is equal is when doing type checking. If we have an element x : Fin (2+2), and we give it as an argument to a function that expects Fin 4, Lean will accept it with it because they are definitionally equal. On the other hand, if we have an element x : Fin (a + b), and we try to plug it into a function expecting Fin (b+a), Lean will complain, and it must be converted.

To my knowledge this conversion should be always possible in principle to keep up with the standard mathematical expectations but can become so annoying in practice, that it is usually worth it to design things definitionally equal, so Lean accepts the retyping automatically.

[Kevin Buzzard]

Here is what we teach the undergraduate (maths) students at Imperial about this.

[Kevin Buzzard]

Re:

Is it at all problematic that math-equality and Lean-equality diverge here?

I would say "no". What is going on is that sometimes to prove that things are equal you can take a short cut and use rfl instead of giving the "normal" proof. So in fact the concept of definitional equality accelerates formalization of mathematics, rather than hindering it.

[Trebor Huang]

Isn't the answer "they don't diverge (here, at least)"? Because indeed if N = M then G/N = G/M.

[Kevin Buzzard]

That is true, but I would say that in Lean's type theory this would be an unwise way of thinking about things.

[Kevin Buzzard]

docs#Subgroup.quotientEquivOfEq (or even better docs#QuotientGroup.quotientMulEquivOfEq ) is the function which gives the isomorphism $G/M\cong G/N$ given a proof of $M=N$ and this is a much more robust approach because it avoids dependent type hell if the proof that $M=N$ is not rfl.

[Kyle Miller]

(@Kevin Buzzard That second one is the function that's mentioned right after the quoted paragraph in MIL.)

[Kevin Buzzard]

You can think about it this way: if $M\subseteq N$ are normal subgroups then it's certainly the case that there's a natural map $G/M\to G/N$ and it's not "the identity", so you would not attempt to identify $G/M$ and $G/N$ in that case. In the case where $M\subseteq N$ happen to be equal you're still "changing groups" so you should still use a function to change groups rather than rely on equality of types, which is a slippery concept in type theory. Remember that $\N=\Z$ is undecidable in Lean!

[Mirek Olšák]

Coincidentally, I am just thinking about a lecture about definitional / provable equality, and I am always hitting weird edge cases. Like "is (fun a : ℕ ↦ a) syntactically equal to (fun b : ℕ ↦ b)? Well no but almost yes because they are Bool-equal in metaprogramming... Or "Is Rat.add 1 1 definitionally equal to (2 : ℚ)?" well according to kernel they are, but it doesn't feel that way because Rat.add has a nonreducible flag...

[Mirek Olšák]

I tried to build the docs#QuotientGroup.quotientMulEquivOfEq on my own, and it was not that bad

def iso (G : Type) [Group G] (M N : Subgroup G) (eq : M = N) [M.Normal] [N.Normal] : G ⧸ M ≃* G ⧸ N := by
  rw! [eq]
  exact MulEquiv.refl _

so it should be often possible to avoid these isomorphisms, and hope rw! would help with the DTT hell.

[Aaron Liu]

You don't get good defeqs

[Aaron Liu]

docs#QuotientGroup.quotientMulEquivOfEq_mk is no longer a definitional equality

[Kyle Miller]

Mirek Olšák said:

it was not that bad

That's expected; for all of these definitions, there's a default implementation you can use that comes from substituting equalities and then using reflexivity of some sort. The key is that once you define such a function, you can add simp lemmas for equational reasoning. It's putting the rewrite behind an abstraction barrier, so to speak. There's little algebraic meaning to an "unconstrained" rewrite. The DTT design pattern we have is to write cast functions when we need to rewrite types, rather than rewriting the types directly.

Aaron's point though is that sometimes there are better choices for these functions than a rewrite. Fin.cast comes to mind.

[Mirek Olšák]

I am not saying this should be the definition of quotientMulEquivOfEq. I was rather pondering if the function is really needed when we can do the rewrites in a proof.

[Mirek Olšák]

Perhaps it is useful in defitions, I suppose...

[Kevin Buzzard]

You've used tactics (and in particular rw) to fill in a definition and this is a recipe for disaster.

[Kevin Buzzard]

Another problem you've caused here is this: Lean's typeclass inference only want to see one Mul on a type, up to reducible defeq. But the Muls on G / M and G / N probably won't be equal in this way if you identify the types using =.

[Mirek Olšák]

Kevin Buzzard said:

You've used tactics (and in particular rw) to fill in a definition and this is a recipe for disaster.

I understand that, it was rather an example that in proofs, I could usually rewrite directly, without having to go through isomorphisms.

[Kevin Buzzard]

I am not convinced that you can: you might screw up typeclass inference because you now have two (equal but perhaps not equal enough) multiplications on one type: "multiplication coming from M" and "multiplication coming from N" and I am worried if M = N isn't rfl.

[Kevin Buzzard]

But maybe I'm just being paranoid here; I always use the isomorphism and the ideas that Kyle described above.

[Kevin Buzzard]

Axel asked if this situation is problematic, and I argued "actually in some cases it makes life easier because you can use rfl instead of supplying more information" but here is a situation where I am extremely nervous about not supplying the extra information. (but this might just be because I know how to do it my "safe" way and don't know enough about type theory to be happy with the "easy" way)

[Riccardo Brasca]

My experience is that at beginning rw is fine, but at some point it gets very painful, and it's usually even more painful to go back and change everything, so one usually prefers to use isomorphisms from the beginning. Of course it really depends on your particular situation, but in practice equality of type is very difficult to use.

[Kevin Buzzard]

So this does work:

import Mathlib

example (G : Type) [Group G] (M N : Subgroup G) (eq : M = N) [M.Normal] [N.Normal]
    (h : IsSimpleGroup (G ⧸ M)) : IsSimpleGroup (G ⧸ N) := by
  rw! [← eq]
  exact h

so maybe my fears are unfounded? I was expecting an obscure error of the form "there are two different multiplications here"

[Mirek Olšák]

To me it was extremely painful before I discovered rw!, then it was usually manageable. But I am talking about being in a proof state, I agree putting rw into definitions messes things up.

[Kevin Buzzard]

Note that rw not rw! does indeed give you obscure errors (by which I mean "motive is not type correct", which is confusing for new users)

[Mirek Olšák]

I wonder if there is a fundamental reason why simp doesn't solve this

example (m n : ℕ) (h : m = n) (a : Fin n) : a = (h ▸ (h ▸ a : Fin m) : Fin n) := by simp

(grind, or rw! [h] does, and if I use cast instead of ▸, simp works)

[Mirek Olšák]

By the way, mathematically it is still all equal. I can prove that the iso I defined is equal to QuotientGroup.quotientMulEquivOfEq. So it is indeed just about the convenience of usage.

[Kyle Miller]

Mirek Olšák said:

I am not saying this should be the definition of quotientMulEquivOfEq. I was rather pondering if the function is really needed when we can do the rewrites in a proof.

To clarify: I understood that, and I was explaining part of the reason why not use type rewrites in proofs.

Kevin mentions another important reason, which is typeclass inference. If you replace a type with something that's not definitionally equal, then the corresponding instances are liable to no longer apply. Tactics like simp assume that all of the instances in your terms can be resynthesized from the inferred type. Rewriting types breaks that assumption.

[Kyle Miller]

Mirek Olšák said:

I wonder if there is a fundamental reason why simp doesn't solve this

It could be possible to get simp to collapse Eq.rec-based casts, but these unconstrained rewrites don't generally compose well. It makes sense that cast could help, since there's a cast_cast algebraic lemma for it that simp can easily apply.

It makes sense that grind works for this since it's comfortable working with HEq (so it can eliminate these casts while it's processing the goal, right at the beginning), but it's for closing goals, unlike simp whose main purpose is rewriting in the middle of proofs.

However, I think right answer here is to use Fin.cast, which avoids type equalities altogether, and preserves the equality on n in Fin n. There are simp lemmas for Fin.cast:

import Mathlib

example (m n : ℕ) (h : m = n) (a : Fin n) : a = (a.cast h.symm).cast h := by
  simp

While for Fin you can obtain m = n from Fin m = Fin n by a cardinality argument, it's not true in general that if you have an inductive type T that T x y z = T x' y' z' implies x = x', y = y', and z = z'. Type formers need not be injective. This is a strong reason for having these custom cast operations per type, to preserve exactly how the type is being rewritten.

[Patrick Massot]

That sentence in MIL is indeed a bit too dramatic, I should improve it. But the conclusion is still that one should use the isomorphism instead.

[Mirek Olšák]

Can you give a specific example of a setup in a proof where a rw! solution doesn't work, and you need the isomorphism?

[Mirek Olšák]

My suspicion is that using an isomorphism can be annoying too, I would like to rather make things actually equal than convert there and back with an isomorphism.

[Kyle Miller]

@Mirek Olšák To be clear, the situation isn't that nobody has thought to use Eq.rec/rewrites instead of isomorphisms, it's that people started with rewrites and discovered that isomorphisms solve numerous problems. This thread has a number of reasons why they are better behaved.

You're not going to see examples where rw! (or at least a hand-written Eq.rec/cast term) can't work, since like I said the isomorphisms are wrapping a rewrite. I think I'd rather see examples where rw! solves things — without doing anything that would break assumptions in other tactics — that can't be made cleaner using isomorphisms. (I'm sure they exist sometimes, especially with complicated dependent types; I'd like to collect realistic examples.)

[Mirek Olšák]

I am not sure if the style I am proposing is understood, that is one of the reasons I was asking for an example. In my view, the ideal case is when I have no weird conversions in my proof state, no casts, no isomorphisms, because I could just align all the relevant elements into equal (typically syntactically equal except proofs) types. If rw! can help me achieve such state, I am happy, and I see no reason I shouldn't be.

If that cannot happen (and I was similarly curious about practical examples when this cannot happen). I get that having explicit isomorphisms is more transparent than casts. On the other hand, you get only somewhat far with isomorphisms because it is only an isomorphism. Whenever you want the isomorphism to be preserving a little more, you need to dig inside the casts again.

[Mirek Olšák]

I could imagine something evil happening in the typeclasses, but it doesn't seem to be the case here, because the cast is inserted into M.Normal = N.Normal, which is a proposition.

[Andrew Yang]

Here's a random example from algebraic geometry. I don't think there is a sane way to avoid the eqToHom and start the proof with rw! (castMode := .all) [← basicOpen_one].

open AlgebraicGeometry LocallyRingedSpace Opposite CategoryTheory StructureSheaf PrimeSpectrum in
example (X : LocallyRingedSpace) :
    toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 _ := by
  unfold toSpecΓ
  rw [← toOpen_res _ (basicOpen (1 : Γ.obj (op X))) ⊤ (eqToHom basicOpen_one.symm),
    Category.assoc, NatTrans.naturality]
  refine (X.toΓSpecSheafedSpace_app_spec_assoc 1 _).trans ?_
  dsimp [toΓSpec]
  rw [← Functor.map_comp, ← X.presheaf.map_id]
  rfl

[Andrew Yang]

Okay you could do something like this but I feel this proof is a lot less predictable and much more brittle.

open AlgebraicGeometry LocallyRingedSpace Opposite CategoryTheory StructureSheaf PrimeSpectrum in
example (X : LocallyRingedSpace) :
    toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 _ := by
  rw! (castMode := .all) [← basicOpen_one]
  unfold toSpecΓ
  convert X.toΓSpecSheafedSpace_app_spec 1
  · simp [basicOpen_one]
  · simp
  · simp; rfl
  · dsimp [toToΓSpecMapBasicOpen, toΓSpecMapBasicOpen]
    convert (X.presheaf.map_id _).symm
    · simp [basicOpen_one]; rfl
    · dsimp; simp
    · dsimp; simp; rfl
    · rw [basicOpen_one]; rfl

[Mirek Olšák]

Thanks, I still need to understand a bit what it is about but I believe you that using a homomorphism works best here.