linarith lemmas

Stream: general

[Damiano Testa]

Dear All,

in the process of working on the ordered refactor, I broke linarith... where can I find the lemmas that linarith uses, in order to state them with the correct assumptions?

Thanks!

[Eric Rodriguez]

presumably here, but it'll take a lot of sifting :(

[Damiano Testa]

Thanks Eric! I was hoping for something simpler, but I can also try and find out which lemmas changed since the last time linarith worked.
However, Mario was able to find the norm_num lemmas, I think easily, and I was hoping for something similar, if available. I do not know how Mario did it, though...

[Kevin Buzzard]

Mario wrote norm_num.

[Damiano Testa]

Ah, that may be the reason why he knew the lemmas... although, Mario also knows lean! :wink:

[Patrick Massot]

You can trying asking @Rob Lewis who wrote linarith

[Damiano Testa]

Ah, thanks Patrick! Anyway, I am done for the day: thank you all for your input!

[Rob Lewis]

If you ctrl-f for ` on https://github.com/leanprover-community/mathlib/blob/master/src/tactic/linarith/preprocessing.lean and https://github.com/leanprover-community/mathlib/blob/master/src/tactic/linarith/verification.lean you'll find the large majority of what linarith uses

[Damiano Testa]

Rob, thanks a lot! Tomorrow I will try it! I imagine that ` is what introduces a mathlib lemma in a tactic, right?

[Rob Lewis]

The syntax for referring to a lemma by name in a metaprogram is `lemma_name. This isn't the only way to do it but it probably catches all the occurrence in linarith

[Damiano Testa]

I have not tested that reformulating these lemmas with the previous hypotheses will fix linarith, but these appear to be most of the linarith lemmas:

add_neg
add_neg_of_neg_of_nonpos
add_neg_of_nonpos_of_neg
add_nonpos
eq.symm
le_of_not_gt
lt_of_not_ge
mul_nonneg_of_nonpos_of_nonpos
mul_pos_of_neg_of_neg
mul_self_nonneg
mul_zero_eq
neg_eq_zero
neg_neg_of_pos
neg_nonpos_of_nonneg
sq_nonneg
sub_eq_zero_of_eq
sub_neg_of_lt
sub_nonpos_of_le
zero_lt_one
zero_mul_eq

[Mario Carneiro]

linarith uses ring so you should also include all the ring lemmas

[Mario Carneiro]

Damiano Testa said:

However, Mario was able to find the norm_num lemmas, I think easily, and I was hoping for something similar, if available. I do not know how Mario did it, though...

I did what Rob said: I searched for uses of `lemma or ``lemma, except I ignored the lemmas that were defined in the norm_num file

[Damiano Testa]

Mario, thank you very much! I will also look for the ring lemmas, then!

[Mario Carneiro]

although I guess since you are working on ordered rings probably nothing ring uses is an issue

[Damiano Testa]

Update: these are the ones that I have actually changed, from the 'linarith` list above:

#print add_neg_of_neg_of_nonpos
#print add_nonpos
#print neg_neg_of_pos
#print neg_nonpos_of_nonneg

[Damiano Testa]

Ah, if ring uses no inequalities, then I should be fine there!