Equivalences preserve properties

Stream: Is there code for X?

[Michael Stoll]

In the context of #13348 (which adds the statement that an equivalence of monoids preserves the orders of elements), I was idly wondering whether it might be possible to formalize the "meta-theorem" that (say) monoid isomorphisms preserve monoid properties. I.e., something like

import Mathlib

universe u
lemma MulEquiv.preserves {α : Type*} (f : {M : Type u} → [Monoid M] → M → α)
    {M M' : Type u} [Monoid M] [Monoid M'] (e : M ≃* M') (m : M) :
    f (e m) = f m := by
  sorry

example {M M' : Type u} [Monoid M] [Monoid M'] (e : M ≃* M') (m : M) :
    orderOf (e m) = orderOf m :=
  e.preserves orderOf m

(One small problem seems to be that f cannot be universe polymorphic: replacing Type u by Type* gives something that does not typecheck.)

Is there any chance something like this is actually provable in Lean? The informal argument is roughly that f has access only to the monoid structure of M and so anything f does can be transported to M' via e. But this sounds like it would require some sort of "induction over the structure of f", which I have a feeling we cannot really do...

[Edward van de Meent]

besides the universe problem, i think it might be the case that this formulation of MulEquiv.preserves doesn't work? because you could imagine a property f : Type u -> ... -> Fin 2 where @f x _ _ = if x = A then 1 else 0 for some specific type A. in other words, a property of type {M:Type u} -> [Monoid M] -> M -> a can look at more things than just the monoid properties. Even when looking more general, i think this kind of lemma only scarcely holds, if it isn't never. i think that for this, you generally need some kind of univalent foundations.

[Michael Stoll]

I would think x = A doesn't type-check when A is some fixed type. Can you produce a concrete example of an f that would lead to a contradiction?

[Damiano Testa]

If you have two 1-element types A and B that you know are different, then you can use if M = A then [map the element to true] else to false.

[Damiano Testa]

Note that the "you know are different" is actually undecidable (and there are a few threads about this).

[Michael Stoll]

I was going to say something like this...

[Damiano Testa]

Anyway, I suspect that at best your lemma is undecidable.

[Edward van de Meent]

well... you can always use classical for the decidability instance

[Damiano Testa]

What I had almost convinced myself of, when I had a similar thought about proving statements about a monoid and its opposite, is that you can probably write a metaprogram that writes the converted statement and attempts at converting the proof. For every "reasonable" statement that you prove, this will work, but artificial things (that may not exist) will not work.

[Edward van de Meent]

import Mathlib.GroupTheory.SemidirectProduct
import Mathlib.Algebra.Ring.Defs
import Mathlib.Algebra.CharP.Defs
import Mathlib.Algebra.Ring.Pi

-- variable (ι : Type*) (R : Type*) [Semiring R] (p:ℕ) [CharP R p] [Nonempty ι]

-- #synth AddMonoidWithOne (ι → R)

-- #check MulEquiv
noncomputable section stuff
open Classical

def foo (M : Type) [Monoid M] : Fin 2 :=
  letI := Classical.propDecidable (M = Unit);
  if M = Unit then 1 else 0

end stuff

this seems to work...

[Edward van de Meent]

feel free to replace Unit with Nat or anything else you might want

[Michael Stoll]

Yes, but you still cannot use it to prove False using my lemma, because you cannot prove that some type is not equal to Unit.

[Michael Stoll]

I think Damiano is right about the undecidability. Maybe we can actually prove that? :smile:

[Edward van de Meent]

ahhh.... i kind of assumed that equality of types is just defeq? or does that contradict stuff?

[Edward van de Meent]

surely not?

[Damiano Testa]

What about replacing M = Unit by a genuinely undecidable statement? E.g. if Peano arithmetic is consistent, then 1 else 0.

[Michael Stoll]

You cannot prove Unit \ne Fin 1, for example.

[Kevin Buzzard]

Michael Stoll said:

I think Damiano is right about the undecidability. Maybe we can actually prove that? :smile:

The proof is: there's a model whre it's true and a model where it's false.

[Michael Stoll]

Damiano Testa said:

What about replacing M = Unit by a genuinely undecidable statement? E.g. if Peano arithmetic is consistent, then 1 else 0.

If it doesn't depend on M, it will not make the lemma false. In this case f will be constant (and one can prove that without needing to know what the constant is).

[Michael Stoll]

Kevin Buzzard said:

Michael Stoll said:

I think Damiano is right about the undecidability. Maybe we can actually prove that? :smile:

The proof is: there's a model whre it's true and a model where it's false.

Can you do it in Lean?

[Kevin Buzzard]

Damiano Testa said:

What I had almost convinced myself of, when I had a similar thought about proving statements about a monoid and its opposite, is that you can probably write a metaprogram that writes the converted statement and attempts at converting the proof. For every "reasonable" statement that you prove, this will work, but artificial things (that may not exist) will not work.

This is the transfer tactic which nobody ever wrote because on the rare occasion that this comes up, people just knock up the easy mathlib proof rather than writing a new tactic. Note that in a homotopy type theory prover they don't need this tactic because they can just rw (isomorphisms and equality are "the same thing"; things can be equal in more than one way, in contrast to Lean, so rw is more powerful).

[Michael Stoll]

Coming back to the original question: is there a way of formalising the notion of a function that is a "monoid property" of monoid elements? Then there would be hope to be able to prove such a lemma for these functions. (And then one would need another proof that orderOf actually is a suitable function...)

[Kevin Buzzard]

I think that you can't write a Lean predicate for "monoid property" but you can write a metaprogram which attempts to check this and which would work for the kinds of inputs which we want in practice (and hence you can write a transfer tactic, although the issue is that it would take far longer than just writing the code of the kind Eric wrote in the other thread).

[Edward van de Meent]

this statement that the function can be lifted is Precisely what you want.

[Edward van de Meent]

or at least, my intuition tells me so, i could be wrong

[Jireh Loreaux]

Cyril Cohen spoke at LftCM 2024 about transfer without univalence. I don't think it was recorded, but here is the abstract

[Michael Stoll]

Kevin Buzzard said:

I think that you can't write a Lean predicate for "monoid property"

One could perhaps produce an inductive type MonoidProperty (that captures the idea of an expression only involving the monoid structure and the given element, plus logic etc.) with a FunLike instance. This would allow to prove the lemma by induction on MonoidProperty.
Then one could construct a termorderOf' : MonoidProperty and show that ⇑orderOf' = orderOf.

[Jireh Loreaux]

Here is the associated paper

[Jireh Loreaux]

I think this is more about transferring between different inductive types that are equivalent, but it may be applicable here too. (Perhaps not, I have not thought much about it since he spoke.)

[Yaël Dillies]

Michael Stoll said:

I think Damiano is right about the undecidability. Maybe we can actually prove that?

Yes, it is undecidable. The only way to prove that two types aren't equal is by cardinality. But here your two types are the same because e : M ≃* M'` forces them to be the same size.

[Yaël Dillies]

Kevin Buzzard said:

This is the transfer tactic which nobody ever wrote

@Kim Morrison wrote it, but it hasn't yet made it to mathlib

[Kim Morrison]

I wrote a partial prototype with Jake Levinson (and a different, not so good prototype separately back in Lean 3) back in 2023. It was not at all ready to go.

[Kim Morrison]

I could find the branch if someone wanted to try playing with it further, but I won't be doing this.

[Johan Commelin]

I think a Lean port of trocq (the Rocq tactic that Jireh mentioned that Cyril presented at CIRM) would be really nice.

[Filippo A. E. Nuccio]

ping @Cyril Cohen @Assia Mahboubi :smile: