Manipulating inequalities in `ENat`

Stream: Is there code for X?

[Anatole Dedecker]

What is the most efficient ways of filling in these sorries? You only realize how useful linarith is when you can't use it...

import Mathlib.Data.ENat.Basic

example {n : ℕ∞} {i : ℕ} : True := by
  rcases lt_or_ge (i : ℕ∞) n with (hin|hin)
  · have hin' : i + 1 ≤ n := sorry
    have hin'' : i ≤ n - 1 := sorry
    have hn : n ≠ 0 := sorry
    trivial
  · have hin' : i + 1 > n := sorry
    have hin'' : i > n - 1 := sorry
    trivial

[Junyan Xu]

The last one isn't true but the others are:

example {n : ℕ∞} {i : ℕ} (hin : (i : ℕ∞) < n) : n ≠ 0 := by
  rintro rfl; exact not_lt_bot hin

example {n : ℕ∞} {i : ℕ} : ((i : ℕ∞) < n) ↔ i + 1 ≤ n :=
  (ENat.add_one_le_iff <| ENat.coe_ne_top i).symm

example {n : ℕ∞} {i : ℕ} (hin : (i : ℕ∞) < n) : i ≤ n - 1 := by
  cases' n with n
  · exact le_top
  · exact WithTop.coe_le_coe.2 (Nat.le_pred_of_lt <| WithTop.coe_lt_coe.1 hin)

example : ¬ ∀ {n : ℕ∞} {i : ℕ}, n ≤ (i : ℕ∞) → n - 1 < i :=
  fun h => not_lt_bot (@h 0 0 rfl.le)

[Anatole Dedecker]

Oh indeed the last one can't be true

[Yury G. Kudryashov]

BTW, see docs#ENat.add_one_le_of_lt

[Yury G. Kudryashov]

For i ≤ n - 1, you can also use docs#le_tsub_of_add_le_right

[Anatole Dedecker]

Yury G. Kudryashov said:

For i ≤ n - 1, you can also use docs#le_tsub_of_add_le_right

No I can't unfortunately :sob: because addition is not ContravariantClass on ENat. I can use docs#AddLECancellable.le_tsub_of_add_le_right in theory, but there's no API around docs#AddLECancellable in ENat.

[Kalle Kytölä]

These are good illustrations of some still common headaches --- and indeed great reminders of how good linarith is when it applies!

[Anatole Dedecker]

Yes, I'm starting to understand why you'd want to do probabilities in Real :sweat_smile:

[Kalle Kytölä]

ring is also amazing.

[Jireh Loreaux]

One thing I would really argue for here: let's develop the necessary API (whatever that may be, possibly including tactics). In general, I'm much more a fan of "do the thing that is mathematically what you want" as opposed to "sacrifice mathematical meaning in order to make formalizing less painful". Of course, if the situations are mathematically equivalent, then make your life easy.

[Anatole Dedecker]

I completely agree with you, but when these things pop up while doing interesting maths and suddenly you're stuck for this kind of stupid reasons, you have to admit that it's pretty tempting to just go around. But of course this isn't the right solution.

[Anatole Dedecker]

I'm very patient with Lean usually, but for some reason this one is just too much for me :sweat_smile:

[Jireh Loreaux]

I totally understand the predicament!

[Kevin Buzzard]

@Mario Carneiro is there anything that mathematicians can do in order to make linarith work for PNat? For example I have it in the back of my mind that you once said "there is a missing typeclass" -- have I misremembered though and this was why ring doesn't work on PNat? Here are some examples of failures. What is a route to making these work?

import Mathlib

example : (1 : PNat) + 1 = 2 := by norm_num -- works
example : (1 : PNat) + x = x + 1 := by ring -- fails
example : (1 : PNat) < x + 1 := by linarith -- fails

noncomputable example : LinearOrderedCommSemiring NNReal := inferInstance

example : (1 : NNReal) + 1 = 2 := by norm_num -- works
example : (1 : NNReal) + x = x + 1 := by ring -- works
example : (1 : NNReal) ≤ x + 1 := by linarith -- fails

inductive MyNat
| zero : MyNat
| S : MyNat → MyNat

instance : LinearOrderedCommSemiring MyNat := sorry

example : (2 : MyNat) + 2 = 4 := by norm_num -- works
example : (2 : MyNat) + x = x + 2 := by ring -- works
example (h : (x : MyNat) ≤ y) : 1 + x ≤ 1 + y := by linarith -- fails

[Mario Carneiro]

the ring issue should be self explanatory, it needs a LinearOrderedCommSemiring instance and PNat isn't

[Kevin Buzzard]

But it is something, right? Do we need to write a new ring for PNat or is it a case of making LinearOrderedCommPreSemiring or whatever PNat is and then generalising 50% of the lemmas in ring to this more general typeclass? Or does that have disadvantages, e.g. it makes ring slower in 98% of use cases?

[Mario Carneiro]

the linarith issue is that it expects the base ring to be an additive group and MyNat isn't

[Mario Carneiro]

"so why does Nat work?" because it has specific support in linarith which works by lifting everything to Int

[Mario Carneiro]

Maybe it should be lifting into the AddLocalization instead of specifically Nat -> Int

[Mario Carneiro]

I suspect something like that is also how to handle the PNat issue, just lift things into the appropriate completion instead of trying to work in whatever gimped structure PNat is and hope it is good enough to have good normal forms

[Kevin Buzzard]

Aah that's a good idea: extend zify to PNat and hope that it's enough for Anatole! Then linarith and ring become available...

[Anatole Dedecker]

Except I’m in ENat, not PNat 😅

[Anatole Dedecker]

And I don’t think you can hope to embed that in a nice structure

[Alex J. Best]

It's still under development (and perhaps a bit overcomplicated right now), but for the Tate's algorithm project (with Huriot and Dahmen) I wrote a tactic for solving linear arithmetic ENat goals, seeings as we had so many of them there.
https://github.com/KisaraBlue/ec-tate-lean/blob/master/ECTate/Tactic/ELinarith.lean
The idea is simple, find all the enats appearing as atoms in the goal and hypotheses, do cases on whether they are infinite or not, simplify (which will reduce all statements with an infinity in to some more straightforward things that should follow from propositional logic at that point), and then with remaining goals with no infinite variables in, pass to the naturals and run the usual linarith. (note this same strategy should also work for ereal, erat etc.)
In fact the presburger-esque theory of extended naturals is decidable (by a similar argument) so in theory there could be a tactic doing much much more than this.
Unfortunately our tactic isn't yet useful widely (i.e copy-pastable) for a couple of reasons, 1. we started the project before mathlib4 got going, so we rolled our own enat, which we still need to remove. 2. the implementation uses a custom version of simp that avoids a bug in the core simp that i need to upstream sometime 3. its not 100% finished yet and presumably not theoretically complete yet, and perhaps a little overcomplicated now who knows. It does work in the nontrivial cases we needed it to.
When the project reaches a more complete state I hope to PR a good version of this to mathlib.

[Mario Carneiro]

#6570 implements ring for PNat via lifting to Nat

[Damiano Testa]

@Alex J. Best there was a discussion of a similar tactic to what you describe in this thread. I did not really start any serious attempt on it, but the idea is very similar: decide what counts as "junk" value, possibly via an attribute and then let the tactic do the case split and try to simp-away the "trivial" case.