## Stream: new members

### Topic: Looking for a Nat theorem

#### Alex Meiburg (Dec 03 2023 at 17:52):

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 (Dec 03 2023 at 17:57):

(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 (Dec 03 2023 at 18:00):

Use zify and then linarith?

#### Ruben Van de Velde (Dec 03 2023 at 18:00):

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

#### Ruben Van de Velde (Dec 03 2023 at 18:02):

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

#### Kevin Buzzard (Dec 03 2023 at 18:19):

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

#### Alex Meiburg (Dec 03 2023 at 18:21):

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 (Dec 03 2023 at 18:24):

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 (Dec 03 2023 at 18:26):

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 (Dec 03 2023 at 18:28):

I would expect this to exist as tsub_tsub_eq_add_tsub

#### Kevin Buzzard (Dec 03 2023 at 18:31):

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 (Dec 03 2023 at 18:32):

Yeah,

example (a b c : ℕ) (h : c ≤ b) : a - (b - c) = a + c - b := by
obtain ⟨b, rfl⟩ := exists_add_of_le h
done


#### Ruben Van de Velde (Dec 03 2023 at 18:34):

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

#### Alex Meiburg (Dec 03 2023 at 18:34):

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 (Dec 03 2023 at 18:34):

ah yeah what Ruben said

#### Ruben Van de Velde (Dec 03 2023 at 18:36):

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

oh no, wait. no

We have that

#### Eric Wieser (Dec 03 2023 at 19:06):

I have a working tsub version back at my desk

#### Eric Wieser (Dec 03 2023 at 19:50):

/-- 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 α]
(h : c ≤ b) : a - (b - c) = a + c - b := by
obtain ⟨d, rfl⟩ := exists_add_of_le h


#### Eric Wieser (Dec 03 2023 at 20:15):

Maybe it should just be a linearly ordered additive monoid

#### Yaël Dillies (Dec 03 2023 at 20:54):

No, because it applies to ℕ × ℕ

#### Yaël Dillies (Dec 03 2023 at 20:56):

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

#### Eric Rodriguez (Dec 03 2023 at 21:59):

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 (Dec 03 2023 at 22:19):

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 (Dec 03 2023 at 22:41):

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

#8804

#### Yaël Dillies (Dec 04 2023 at 07:31):

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:

Last updated: Dec 20 2023 at 11:08 UTC