Looking for a Nat theorem

Stream: new members

[Alex Meiburg]

I've been looking for half an hour and can't find a theorem to this effect:

theorem sub_sub_of_ge {a b c : ℕ} (h : b > c) : a - (b - c) = a + c - b := by sorry

_Surely_ there is something like this in mathlib, or some similar way to make a "sub of sub" into a shallower expression. But the only ones I can find in mathlib are:

Nat.sub_sub_eq_min : ∀ (a b : ℕ), a - (a - b) = min a b
Nat.sub_sub_self : ∀ {n m : ℕ}, m ≤ n → n - (n - m) = m

which both involve having the same thing on the lhs

[Alex Meiburg]

(More generally, I find myself frustrated with the amount of work needed for basic linear inequalities over nats... I feel like I must be missing some powerful tools to handle these for me, because right now it's a lot of crawling through lists of inequalities by hand. A simple problem like

k1 k2 n1 : ℕ
hnp: n1 + 1 < k1 + 1
hd: k1 ≥ k2 + 1
hnp2: n1 ≥ k1 - (k2 + 1)
⊢ k1 - Nat.succ n1 = k2 - (n1 - (k1 - (k2 + 1)))

takes many many steps and a long time to write... Any tips?)

[Kevin Buzzard]

Use zify and then linarith?

[Ruben Van de Velde]

Hrm, docs#Nat.sub_add_eq and docs#Nat.sub_sub seem duplicates

[Ruben Van de Velde]

Kevin's correct, of course, but I thought this lemma existed

[Kevin Buzzard]

Why are you using natural subtraction anyway? I usually try and work around this

[Alex Meiburg]

I'm trying to prove some things about lists appending and so on, and so all these natural numbers are coming from List.length and List.get

[Kevin Buzzard]

right, but instead of making a variable k1 and having a proof k1 >= k2 + 1, why not instead make a variable t which is k1 - (k2 + 1) and let k1 be t + (k2 + 1)? Every natural subtraction is an obstacle to making thngs easy. Are you sure you can't use integers?

[Alex Meiburg]

Oh hm, gotcha. So at any point I get a <=, I could obtain Nat.exists_eq_add_of_le and then use that new variable instead?

[Eric Wieser]

I would expect this to exist as tsub_tsub_eq_add_tsub

[Kevin Buzzard]

Alex Meiburg said:

Oh hm, gotcha. So at any point I get a <=, I could obtain Nat.exists_eq_add_of_le and then use that new variable instead?

More generally my rule is "never ever ever use natural subtraction" and you're beginning to see why. Natural subtraction is a pathological operation. If you know your subtraction makes sense then another possibility is integer subtraction. The moment you're using integers then linarith does all the heavy lifting for you.

I suspect that omega might be able to solve these goals soon, but we don't quite have it yet. Watch this space!

[Ruben Van de Velde]

Yeah,

example (a b c : ℕ) (h : c ≤ b) : a - (b - c) = a + c - b := by
  obtain ⟨b, rfl⟩ := exists_add_of_le h
  rw [Nat.add_sub_self_left]
  rw [Nat.sub_add_eq]
  rw [Nat.add_sub_cancel]
  done

[Yakov Pechersky]

I would expect to find it near tsub_add_eq_add_tsub

[Ruben Van de Velde]

There's docs#tsub_tsub_assoc about a - (b - c), but that seems to be all

[Alex Meiburg]

https://loogle.lean-lang.org/?q=%22tsub%22%2C+_+-+%28_+-+_%29
There's tsub_tsub_assoc, but that's b ≤ a → c ≤ b → a - (b - c) = a - b + c

[Alex Meiburg]

ah yeah what Ruben said

[Ruben Van de Velde]

My last hope is that @Yaël Dillies knows where it is

[Alex Meiburg]

Ah! docs#sub_sub_eq_add_sub

[Alex Meiburg]

oh no, wait. no

[Yaël Dillies]

We have that

[Eric Wieser]

I have a working tsub version back at my desk

[Eric Wieser]

/-- The `tsub` version of `sub_sub_eq_add_sub`. -/
theorem tsub_tsub_eq_add_tsub_of_le {a b c : α} [AddCommMonoid α] [PartialOrder α] [Sub α] [OrderedSub α] [ExistsAddOfLE α]
    [CovariantClass α α HAdd.hAdd LE.le] [ContravariantClass α α HAdd.hAdd LE.le]
    (h : c ≤ b) : a - (b - c) = a + c - b := by
  obtain ⟨d, rfl⟩ := exists_add_of_le h
  rw [add_tsub_cancel_left, add_comm a c, add_tsub_add_eq_tsub_left]

[Eric Wieser]

The assumptions look pretty ridiculous, but I think they match docs#add_tsub_add_eq_tsub_left

[Eric Wieser]

Maybe it should just be a linearly ordered additive monoid

[Yaël Dillies]

No, because it applies to ℕ × ℕ

[Yaël Dillies]

You could replace [AddCommMonoid α] [PartialOrder α] [CovariantClass α α HAdd.hAdd LE.le] [ContravariantClass α α HAdd.hAdd LE.le] by [OrderedCancelAddCommMonoid α] though

[Eric Rodriguez]

I'm surprised it's not been mentioned, but mathlib prefers </<= to the other side by a lot - this is to avoid theorem duplication. They are defeq however. I wouldn't go as far as Kevin with natural subtraction but it is often unfun to deal with.

[Kevin Buzzard]

I nearly mentioned the whole < vs > thing but I'm less sure about how much it matters in lean 4 so kept quiet

[Eric Wieser]

Yaël Dillies said:

You could replace [AddCommMonoid α] [PartialOrder α] [CovariantClass α α HAdd.hAdd LE.le] [ContravariantClass α α HAdd.hAdd LE.le] by [OrderedCancelAddCommMonoid α] though

Loogle has no matches for OrderedCancelAddCommMonoid, OrderedSub, so it sounds like my spelling is better

[Eric Wieser]

#8804

[Yaël Dillies]

Eric Wieser said:

so it sounds like my spelling is better

*more in line with the current mess is what you meant to say :wink: