Zulip Chat Archive

Stream: new members

Topic: more casting issues


Alex Kontorovich (Apr 21 2020 at 23:35):

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 (Apr 22 2020 at 00:25):

@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 (Apr 22 2020 at 00:33):

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

Dan Stanescu (Apr 22 2020 at 00:36):

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

Bryan Gin-ge Chen (Apr 22 2020 at 00:43):

If you're willing to use mathlib:

import tactic

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

Alex J. Best (Apr 22 2020 at 00:56):

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.


Last updated: Dec 20 2023 at 11:08 UTC