linarith failing

Stream: mathlib4

[Chris Hughes]

linarith is failing for me on the following

example (x : ℝ) (h0 : 0 < x) (h1 : x ≤ 1) : x * (5 / 96) + x / 6 < x :=
  by linarith --fails

Is there something easy I can do about this?

[Kevin Buzzard]

Works for me on mathlib(edit: 3) from Jan

[Kevin Buzzard]

oh sorry, just noticed lean 4

[Jireh Loreaux]

Does linarith support rationals yet? I can't remember. @Thomas Murrills weren't you working on cancel_denoms at some point in order to support this?

[Joël Riou]

I had a similar problem with the following :

example (t : ℝ) (h₁ : t ≤ 1 / 2) (h₂ : 1 - t ≤ 1 / 2) : t = 1 / 2 := by linarith

see https://github.com/leanprover-community/mathlib4/pull/2825/files#diff-e5aadca59b7b28686fba9dce98b624b6bef606e0615c3142c6e86c89fb756d53R278-R296

[Kevin Buzzard]

Quick sanity check (I'm not at a computer right now): does lean 4 interpret the numeral division as real division? Because the algorithm changed it occurred to me that it might be natural division

[Kevin Buzzard]

We're no longer outside-in

[Chris Hughes]

Kevin Buzzard said:

Quick sanity check (I'm not at a computer right now): does lean 4 interpret the numeral division as real division? Because the algorithm changed it occurred to me that it might be natural division

It does interpret it as real number division.

[Jireh Loreaux]

Kevin Buzzard said:

We're no longer outside-in

@Kevin Buzzard what do you mean?

[Kevin Buzzard]

lean4#1915 -- oh -- maybe we're no longer left-to-right but we're still outside-in? I don't really understand the new algorithm yet.

[Thomas Murrills]

Jireh Loreaux said:

Does linarith support rationals yet? I can't remember. Thomas Murrills weren't you working on cancel_denoms at some point in order to support this?

Yep, still working on it! Sorry for the delay, I’ve lost some time recently on which I’d otherwise work on it; also, just wrapping up mono first (it’s done, just needs some refactoring and prettifying today), then cancel_denoms is up next

[Jeremy Tan]

@Thomas Murrills Are you still working on !4#2323?

[Scott Morrison]

@Jeremy Tan, does this message have any connection to this thread? It seems offtopic.

[Jeremy Tan]

Yes, the last message talked about the mono tactic. I'm trying to see how to port cancel_denoms myself right now

[Thomas Murrills]

Yep, I’ve just gotten somewhat busy this past week or so. (Ah, I see that I didn’t yet push the commit which merges the version of the solve_by_elim refactor branch which passed checks, whoops; will do tomorrow, away from my computer rn. As mentioned in other threads the basic version works, I’m just seeing if I can refine the behavior.)

Do you need cancel_denoms for something urgently? I’ve roughly laid out some of the code already but haven’t committed anything anywhere. See the tactic porting tracking issue for who’s working on what so we don’t duplicate work!

EDIT: re: mono, nvm, can't sleep—I'll fix the branch now

[Jeremy Tan]

I'm not urgently needing cancel_denoms; I saw this thread which is about linarith and how it currently can't handle fractions

[Jeremy Tan]

And I thought "oh, cancel_denoms can provide some of that functionality"

[Jeremy Tan]

And you mentioned that cancel_demons was coming up after mono

[Thomas Murrills]

Ah, sorry, my earlier message by itself wasn't clear: I meant that I would try to wrap up cancel_denoms after mono. i.e. it was up next on my to-do list :)

[Thomas Murrills]

But, still, there does seem to be a need for it soon...I'll have some time starting monday and push forward on it! :)

[Thomas Murrills]

@Jeremy Tan , please don't add labels to PRs that you're not (co-)managing! The mono PR is green and can likely be used in other PR's (see here) but I'm not putting it out for review just yet because it's not sufficiently tested and/or factored properly. (Also, I'm trying to refine the mono* behavior if I can.)

[Patrick Massot]

Some news from linarith: Floris, Kyle and I have just opened !4#3797 which ports docs#cancel_denoms which is the missing preprocessor that is meant to allow linarith to get rid of denominators. The application to linarith is not part of this PR. @Thomas Murrills @Scott Morrison @Rob Lewis

[Patrick Massot]

@Heather Macbeth

[Floris van Doorn]

!4#3797