PNat and sub

Stream: new members

[Ralf Stephan]

There is an absence of theorems containing "sub" in the PNat domain. Does this mean the following cannot be proven, even given the condition?

import Mathlib

set_option autoImplicit false
variable {a b x: ℕ+}

theorem PNat.sub_le_self (ha: b < a): a - b ≤ a := by sorry

Also if I add the following line, I get an ''ambigous" error. If possible, how to resolve these?

  apply add_le_add (a := (a - b)) (b := a) (c := b) (d := b)

ambiguous, possible interpretations
  _root_.add_le_add : a - b ≤ a → b ≤ b → a - b + b ≤ a + b

  Nat.add_le_add : ↑a - ↑b ≤ ↑a → ↑b ≤ ↑b → ↑a - ↑b + ↑b ≤ ↑a + ↑b

[Ruben Van de Velde]

You can write _root... or Nat.... as suggested by the error

[Ruben Van de Velde]

import Mathlib

set_option autoImplicit false
variable {a b x: ℕ+}

theorem PNat.sub_le_self : a - b ≤ a := by
  rw [← coe_le_coe, PNat.sub_coe]
  split_ifs with h
  · simp
  · exact NeZero.one_le

[Ralf Stephan]

Completely missed sub_coe. But your code fails here with

invalid field notation, type is not of the form (C ...) where C is a constant
  NeZero
has type
  ?m.7842 → Prop

[Ruben Van de Velde]

apply? found that. exact a.2 also works

[Ralf Stephan]

Remarkable, thanks. So sub_coe does not specify which type/domain to coerce to, but leaves it open until later operations require a, e.g., Sub?

[Ruben Van de Velde]

What makes you say that? Those two lemmas are specifically about the coercion from PNat to Nat, as far as I can tell

[Ralf Stephan]

I tried several theorems from other domains but often got "can't construct something N+"(for reasons I can follow with time), and, since you use theorems from Order.Sub and Order.Monoid I somehow expected them not to work, either. But I only now notice that Sub and LinearOrderedCancelCommMonoidare part of instance statements in PNat.Basic.

So, working with PNat, I should have first groked what is still possible by looking at what structures apply. But that gung-ho attitude is because of me more being a developer than a mathematician. Also why I suffer from these error messages, and would welcome any small improvement there.

[Ralf Stephan]

But then, I'm only three weeks into it..

[Ruben Van de Velde]

For what it's worth, I was surprised not to find anything nicer. I'm not sure if that's because PNat is just poorly behaved, so not many general results can apply to it, or there's just gaps in the development because people don't use PNat much. Maybe @Yaël Dillies knows

[Yaël Dillies]

I think PNat simply didn't get(/doesn't deserve?) much love

[Yaël Dillies]

Certainly I've come up with plenty of niche formalisms that cover only a few concrete types but cover them nicely, yet I have never been able to fit PNat in one of them (except for docs#SuccOrder)

[Damiano Testa]

Yaël Dillies said:

I think PNat simply didn't get(/doesn't deserve?) much love

Ooooh surely everyone deserves love...