to_multiplicative

Stream: general

[Johan Commelin]

490,725 {# change these line numbers
  /lemma/ { h
    /@/ { s/@\[\(.*\)\] lemma \([a-z_.']*\).*/@[\1, to_additive \2]/;b goto }
    s/lemma \([a-z_.']*\).*/@[to_additive \1]/
    : goto
    p; x
    s/@\[.*\] // }
  s/nonneg/one_le/g
  s/nonpos/le_one/g
  s/pos/one_lt/g
  s/neg/lt_one/g
  s/add/mul/g
  s/zero/one/g
  s/+/*/g
  s/0/1/g }

[Johan Commelin]

This :up: sed script might be helpful if you want to turn some additive file into a multiplicative file with @[to_additive] attributes.

[Johan Commelin]

Also, it doesn't understand theorem, at the moment.

[Johan Commelin]

How hard would it be to have a to_multiplicative attribute that is the inverse of to_additive. That way, users can determine in which "language/notation" they primarily want to develop a certain part of a theory, and automatically translate from mul to add using to_additive but alternatively also translate from add to mul using to_multiplicative.

We recently had a PR on lattice groups where this would have been the more natural approach (only the additive story is presented in the informal literatue). I can imagine that certain argument about abelian groups are typically presented using additive notation, but are currently in multiplicative notation because that's how mathlib wants it.

[Kevin Buzzard]

How hard would it be to have $\geq$? Definitely possible, but a huge PITA for lots of reasons. Would it be as bad as this?

[Ruben Van de Velde]

I guess not, because lean would generate the same code in both cases, just from different source

[Kevin Buzzard]

Oh it's not the same as that at all is it, you're just asking for an attribute which makes a multiplicative lemma from an additive one? Then the CS people will complain about code duplication but actually to me as a mathematician this sounds like a lovely idea.

[Ruben Van de Velde]

Which makes me wonder if $\ge$ could be notation for has_le.le with the arguments flipped, but that would probably be an actual bad idea

[Johan Commelin]

Kevin Buzzard said:

Oh it's not the same as that at all is it, you're just asking for an attribute which makes a multiplicative lemma from an additive one? Then the CS people will complain about code duplication but actually to me as a mathematician this sounds like a lovely idea.

I guess to_additive and to_multiplicative could even share quite a bit of code. So the code duplication shouldn't even be too bad, hopefully.

[Yaël Dillies]

I think code duplication isn't too bad, but to_additive seems already brittle enough that you don't want to also maintain the reverse attribute.