a+b -c = a + (b-c) in N

Stream: new members

[RedPig]

I have a trivial problem which is the associative of integers. The following code actually fails. The struggle here is that $\N$ is not SubNegMonoid. How do we deal with such cases where we to inherent obvious operation from $\Z$. Similar question could apply to field extension type of operation where a real number is also a complex number.

import Mathlib

theorem trivial_math (a b c : ℕ) : a + b - c = a + (b - c):= by
  rw [add_sub_assoc]

[Scott Carnahan]

If a = 1, b = 0, c = 1, then the left side is 0 and the right side is 1. This is because Nat subtraction truncates at zero.

[RedPig]

Scott Carnahan said:

If a = 1, b = 0, c = 1, then the left side is 0 and the right side is 1. This is because Nat subtraction truncates at zero.

I see, in order to make sense, a + (b - c) must be represented in $\Z$ as (b-c) could be negative. Can we have sth like $a \in \N \implies a \in \Z$ to transform the type

[Julian Berman]

A good piece of advice from someone in a previous thread (maybe Damiano? or Henrik?) is "literally any time you put - somewhere with Nats, either don't do that if you can afford it, or if not, then try slim_check" -- in particular in your case:

import Mathlib

theorem trivial_math (a b c : ℕ) : a + b - c = a + (b - c):= by
  slim_check

immediately finds a counterexample like the one Scott mentioned.

[Kevin Buzzard]

import Mathlib.Tactic

theorem trivial_math (a b c : ℕ) : (a : ℤ) + b - c = a + (b - c):= by
  rw [add_sub_assoc]

[Terence Tao]

If you absolutely have to use natural number subtraction for some reason, then many statements can be proven using the zify tactic to convert (assuming suitable inequalities) to integer subtraction.

[Riccardo Brasca]

Nowadays we have omega that works very well.