more casting issues

Stream: new members

[Alex Kontorovich]

Can someone please help with this proof? I realize I'm using subtraction within naturals, but nothing I've tried has worked on this...

lemma z (n m :ℕ ): 1 + (↑m - ↑n)= (1 + ↑m) - ↑n :=
begin
  sorry,
end

Thanks!

[Dan Stanescu]

@Alex Kontorovich I could make this work with some effort. You can probably trim this down to half the size by working on the goal instead of G, and I can bet someone with more experience can prove it in a couple lines or so.

lemma z (n m :ℕ ): 1 + ((m:ℤ) - (n:ℤ)) = (1 + (m:ℤ)) - (n:ℤ) :=
begin
  have G : 1 + ((m:ℤ) - (n:ℤ)) = 1 + ((m:ℤ) - (n:ℤ)), refl,
  rw add_comm at G {occs := occurrences.pos [1]},
  rw add_comm,
  have F : -↑n = (-1:ℤ)*↑n, norm_num,
  have E : ↑m - ↑n = ↑m + (-1:ℤ)*↑n, norm_num, linarith,
  rw E at G {occs := occurrences.pos [2]},
  set zn := (-1:ℤ)*↑n with hzn,
  have D : 1 + (↑m + zn) = 1 + ↑m + zn, linarith,
  rw D at G,
  rw ← F at G,
  exact G,
end

Without the casts it wouldn't be valid, of course:

#eval 1 + (0-1)    --  1
#eval (1+0) - 1    -- 0

[Alex Kontorovich]

Amazing, thank you! (Glad I wasn't missing something trivial...)

[Dan Stanescu]

These casting problems have a tendency to be tough because they're so counter-intuitive for most of us!

[Bryan Gin-ge Chen]

If you're willing to use mathlib:

import tactic

lemma z (n m :ℕ ): 1 + ((m:ℤ) - (n:ℤ)) = (1 + (m:ℤ)) - (n:ℤ) :=
by ring

[Alex J. Best]

If you are casting to any add_group this is the lemma add_sub in mathlib

lemma z (n m :ℕ ): 1 + ((↑m:ℤ) - ↑n)= (1 + ↑m) - ↑n := add_sub 1 (↑ m) (↑ n)

and by library_search should find it for you.