How to access the multiplication inside the monoid inside ..

Stream: new members

[Agnishom Chattopadhyay]

In line 23, here, I have the structure monoid_recognizer which supposedly consists of a monoid m among other things.

In line 41, I would like to use the multiplication involved with this monoid. However, simply refering to it as * would not work as would be evident from running the code. I have also tried other things like M.is_monoid.mul, etc.

How do I get it to work?

[Mario Carneiro]

You need to make it an instance, i.e.:

instance {A} (M : monoid_recognizer A) : monoid M.m := M.is_monoid

[Agnishom Chattopadhyay]

That is a good idea. Thanks

[Agnishom Chattopadhyay]

What other way is there to do this? My understanding is that something like M.is_monoid.mul or similar thing should work

[Chris B]

This works for me :

def recognizer_to_dfa {alphabet : Type} [fintype alphabet] (M : monoid_recognizer alphabet) : dfa alphabet :=
let MONOID_MUL : M.m → M.m → M.m := M.is_monoid.mul
in @dfa.mk _ _ M.m M.is_finite M.has_decidable_eq (λ q a, MONOID_MUL q (M.h [a])) (M.h []) M.fin

What error message are you getting?

[Agnishom Chattopadhyay]

That works, thanks!

While this works:

def recognizer_to_dfa {alphabet : Type} [fintype alphabet] (M : monoid_recognizer alphabet) : dfa alphabet :=
let MONOID_MUL : M.m → M.m → M.m := M.is_monoid.mul
in @dfa.mk _ _ M.m M.is_finite M.has_decidable_eq (λ q a, MONOID_MUL q (M.h [a])) (M.h []) M.fin

the following variants however do not:

def recognizer_to_dfa {alphabet : Type} [fintype alphabet] (M : monoid_recognizer alphabet) : dfa alphabet :=
@dfa.mk _ _ M.m M.is_finite M.has_decidable_eq (λ q a, M.is_monoid.mul q (M.h [a])) (M.h []) M.fin

or

def recognizer_to_dfa {alphabet : Type} [fintype alphabet] (M : monoid_recognizer alphabet) : dfa alphabet :=
let MONOID_MUL : M.m → M.m → M.m := M.is_monoid.mul
in @dfa.mk _ _ M.m M.is_finite M.has_decidable_eq (λ q a, M.is_monoid.mul q (M.h [a])) (M.h []) M.fin

I get the error message invalid field notation, function 'monoid.mul' does not have explicit argument with type (monoid ...).

I wonder why?

[Chris B]

That's a great question... And one that I'm sure Mario or someone can answer for you lol. FWIW this works too.

def recognizer_to_dfa {alphabet : Type} [fintype alphabet] (M : monoid_recognizer alphabet) : dfa alphabet :=
@dfa.mk _ _ M.m M.is_finite M.has_decidable_eq (λ q a, @monoid.mul M.m M.is_monoid q (M.h [a])) (M.h []) M.fin

[Mario Carneiro]

The problem, as the error message says, is that monoid.mul has an argument of type monoid A, but it is not explicit, so you aren't allowed to use projection notation on an element of type monoid A to apply monoid.mul. You can write @monoid.mul _ M.is_monoid q (M.h [a])

[Agnishom Chattopadhyay]

well, why does it work when it is bound using a let then? As in Chris's example?

[Mario Carneiro]

Lean appears to be a bit inconsistent in the handling of partial applications and built in projections here. Demo:

constant X : monoid nat
constant monoid.func {A} [monoid A] : A → A → A
noncomputable theory
example : nat → nat → nat := X.mul   -- works
example : nat → nat → nat := X.func  -- failed to synth monoid (monoid ℕ)
example (a : nat) : nat → nat := X.mul a  -- invalid field notation, insufficient number of arguments
example (a : nat) : nat → nat := X.func a -- invalid field notation, insufficient number of arguments
example (a b : nat) : nat := X.mul a b   -- invalid field notation, no explicit (monoid ...) arg
example (a b : nat) : nat := X.func a b  -- invalid field notation, no explicit (monoid ...) arg

Note that the types of monoid.mul and monoid.func are exactly the same; the only difference is that monoid.mul is a built in structure projection and monoid.func is a defined (well, axiomatized) function on monoid