Last sorries in mathlib4

Stream: mathlib4

[Heather Macbeth]

As ported files replace ad-hoc files written to support tactics, the sorry count in mathlib4 has gone down. See eg mathlib4#1100, mathlib4#1106.

Now it seems the only sorries left in mathlib4 are these three in Tactic.Positivity.Core:

lemma pos_of_isNat [PartialOrder A] [AddMonoidWithOne A]
  (_ : NormNum.IsNat e n) (_ : Nat.ble 1 n = true) : 0 < (e : A) := sorry

lemma nonneg_of_isNat [PartialOrder A] [AddMonoidWithOne A]
  (_ : NormNum.IsNat e n) : 0 ≤ (e : A) := sorry

lemma nz_of_isNegNat [PartialOrder A] [Ring A]
  (_ : NormNum.IsInt e (.negOfNat n)) (_ : Nat.ble 1 n = true) : (e : A) ≠ 0 := sorry

Does anyone who knows about boolean-le and OfNat want to take them on?

[David Renshaw]

Looks like at least the first one is invalid, as currently written.

import Mathlib.Data.Nat.Cast.Basic
import Mathlib.Tactic.Positivity.Core

example : False := by
  have h := @Mathlib.Meta.Positivity.pos_of_isNat ℤᵒᵈ 1 1 _ _ ⟨rfl⟩ rfl
  norm_num at h

[David Renshaw]

I guess maybe we need to add [ZeroLEOneClass A]?

[Heather Macbeth]

Sounds reasonable!

[Heather Macbeth]

I opened an issue, mathlib4#1362, for these sorries. It'd be great if someone could take them on!

[Mario Carneiro]

I think at the time the appropriate partial order / semiring combo class was not available, and I wasn't interested in working out what it should be. I don't think ZeroLEOneClass is the answer though

[Heather Macbeth]

Mario Carneiro said:

I think at the time the appropriate partial order / semiring combo class was not available

Do you know if this class is now available?

[Heather Macbeth]

E.g. were you thinking of CanonicallyOrderedAddMonoid?

[Mario Carneiro]

canonically ordered sounds a bit strong

[Mario Carneiro]

what we want is to know that Nat.cast (n+1) > 0, something like an ordered semiring should suffice

[Mario Carneiro]

the relevant lemma in lean 3 (docs#nat.cast_pos) is stated for nontrivial ordered semirings

[Scott Morrison]

lemma pos_of_isNat [StrictOrderedSemiring A]
    (h : NormNum.IsNat e n) (w : Nat.ble 1 n = true) : 0 < (e : A) := by
  rw [NormNum.IsNat.to_eq h rfl]
  apply Nat.cast_pos.2
  simpa using w

lemma nonneg_of_isNat [OrderedSemiring A]
    (h : NormNum.IsNat e n) : 0 ≤ (e : A) := by
  rw [NormNum.IsNat.to_eq h rfl]
  exact Nat.cast_nonneg n

lemma nz_of_isNegNat [StrictOrderedRing A]
    (h : NormNum.IsInt e (.negOfNat n)) (w : Nat.ble 1 n = true) : (e : A) ≠ 0 := by
  rw [NormNum.IsInt.neg_to_eq h rfl]
  simp only [ne_eq, neg_eq_zero]
  apply ne_of_gt
  simpa using w

work, but then def normNumPositivity can't generate the relevant typeclasses.

[Heather Macbeth]

Huh ... do you think it's because the Qq business in the existing code for normNumPositivity needs to be adapted to the new typeclasses?

[Scott Morrison]

I wasn't sure how to resolve this. The problem is that NormNum.derive is returning results with (weaker) typeclasses in them, so we can't just add let _ ← synthInstanceQ (q(StrictOrderedSemiring $α) : Q(Type u)).

[Mario Carneiro]

This issue already comes up in the other positivity extensions, you have to clear the weaker typeclasses and then use type ascriptions to tell Qq that it should pretend the original exprs have a type written in terms of the new typeclass

[Scott Morrison]

mathlib4#1375