Making a contribution to mathlib - lattice ordered groups

Stream: new members

[Christopher Hoskin]

Hello, I'd like to offer a contribution to mathlib - a basic theory of lattice ordered groups: https://github.com/leanprover-community/mathlib/pull/8663

If this is of interest, please could I have write access to non-master branches of the mathlib repository? My GitHub username is mans0954.

Thank you,

Christopher Hoskin

[Johan Commelin]

https://github.com/leanprover-community/mathlib/invitations

[Alex J. Best]

@Christopher Hoskin once you've accepted the invite you can open a new version of that PR from a branch on mathlib and the CI will run on it.

[Yury G. Kudryashov]

Note that we have docs#covariant_class and docs#contravariant_class.

[Alex J. Best]

Some random thoughts from looking over the code, it looks pretty good overall!:

• You use simp in some places where it doesn't close the goal (pos_meet_neg_eq_zero), this is called a non-terminal simp and is generally discouraged as if the set of simp lemmas later changes (someone adds a new simplification perhaps) it can break your proof, its better in such situations to change simp to squeeze_simp which will output a call to simp only [...] instead that will be more robust.
• In lemmas like join_eq_add_pos_sub the proof is a pure calc block, so doesn't need to be in a begin... end just := calc ... will do.
• Some of your very short proofs in tactic more are term mode one-liners, like lemma pos_sub_neg' (a : α) : a⁺ - a⁻ = a := (pos_sub_neg _).symm getting more experience with writing direct lean terms like this is always helpful to get rid of small goals faster.
• if you have multiple rewrites in a row they can be combined like rw a, rw b, is equivalent to rw [a, b]
• are you aware of tactic#library_search? in abs_pos_eq where you write -- I feel there ought to be a simpler way of finishing from here? putting instead library_search tells me the proof can be finished with exact nsmul_nonneg h 2, instead.

[Patrick Massot]

You should also read https://leanprover-community.github.io/contribute/style.html, especially the part about braces.

[Christopher Hoskin]

Thanks, I've created a branch within mathlib, but the CI is failing with the message "Error: ERR_RNT: Reserved notation outside tactic.reserved_notation" https://github.com/leanprover-community/mathlib/runs/3328082790

Having looked in reserved_notation it's not obvious to me what I've done wrong. Is there a way of seeing which line it's failing at?

Thanks.

[Julian Berman]

CI is hiding that for some reason (I have vague recollection there's desire to make that integrate better with the GitHub UI which is why that happened). Running it locally (by running ./scripts/lint-style.sh) it shows me:

:error file=src/algebra/lattice_ordered_group.lean,line=214,code=ERR_RNT::ERR_RNT: Reserved notation outside tactic.reserved_notation
::error file=src/algebra/lattice_ordered_group.lean,line=222,code=ERR_RNT::ERR_RNT: Reserved notation outside tactic.reserved_notation

[Eric Wieser]

The error message is also visible at https://github.com/leanprover-community/mathlib/compare/lattice_ordered_group

[Eric Wieser]

Where it is attached to the correct line number