Coercion for free algebraic objects

Stream: new members

[Frédéric Marbach]

I am trying to learn Lean to formalize results on free algebraic structures (for example : free magmas). When working with the free magma over a type α, it would be natural to see the elements of α as being part of the free magma through the canonical embedding (the constructor FreeMagma.of). Reading the documentation, I understand that this should be done by coercion? I tried the implementation below, which correctly accepts that, in FreeMagma.mul a b, the letter a should be coerced, but unfortunately, the b term triggers an error.

import Mathlib.Algebra.Free

instance (α : Type*) : Coe α (FreeMagma α) := ⟨FreeMagma.of⟩

theorem length_of_pair_eq_two (α : Type*) (a b : α) : (FreeMagma.mul a b).length = 2 := by
  exact rfl

What am I doing wrong? Being able to write such statements would be a lot more natural for manipulations (avoiding to distinguish between elements of the alphabet and their image in the free structure).

Error message

FreeMagma.mul ?m.161 b
argument
b
has type
α : Type u_1
but is expected to have type
FreeMagma ?m.224 : Type ?u.221

Thanks,

[Kevin Buzzard]

For some reason which I've never really understood, Lean is unable to figure out that if it's faced with a coercion from X to FreeMagma ?m then it should try ?m=X and then use the only coercion which can possibly work. The consequence is that you have to explicitly tell Lean the type of the target:

theorem length_of_pair_eq_two (α : Type*) (a b : α) : (FreeMagma.mul a b : FreeMagma α).length = 2 := by
  exact rfl

I can also not guarantee that Coe is correct, there are all manner of variants the differences between which I don't understand and I also don't understand the algorithm for working out which one you should use in any given case (there's CoeHead, CoeTail and probably some others).

[Sebastien Gouezel]

Try instead

theorem length_of_pair_eq_two (α : Type*) (a b : α) : ((a : FreeMagma α) * b).length = 2 := by
  exact rfl

or

theorem length_of_pair_eq_two' {α : Type*} (a b : α) : (a * b : FreeMagma α).length = 2 := by
  exact rfl

The way to indicate to Lean that you want a coercion is to give a type ascription on one of the terms. You should never need to useFreeMagma.mul, but just *.

By the way, your by exact rfl can be replaced by rfl (or by rfl).

[Sebastien Gouezel]

As Kevin says, the problem is that in your initial formulation, when you use FreeMagma.length, Lean doesn't know which free magma you want to use. If you tell it that you want to use the free magma based on α, then everything works fine:

theorem length_of_pair_eq_two''' {α : Type*} (a b : α) : FreeMagma.length (α := α) (a * b) = 2 := rfl

But the two suggestions above are better, this formulation here is just for educational purposes.

[Frédéric Marbach]

Thank you both for your quick answers !

I was surprised that none of these coercions seems to be currently implemented. Shouln't they be part of Mathlib4 for all free structures (free magma, monoid, semigroup, group, algebra, Lie algebra and so on)?

[Kevin Buzzard]

I guess we're more used to type theory than you are :-) I don't immediately see why these coercions would be a bad idea... On the other hand, maybe once you're used to type theory you like to keep track of these things explicitly :-)