Zulip Chat Archive

Stream: new members

Topic: nth_rewrite without mathlib


Sara Fish (Jul 15 2021 at 21:38):

I'm playing around with naked lean without mathlib. How do I rewrite at a specific spot? I know I can do this using nth_rewrite, but I am not wanting to use "import tactic".

Working example:

def divides_N (a b :  ) :=  k : , b = k * a
def less_N (a b :  ) :=  k : , a + k = b

lemma div_less (a b :  ) : divides_N a b  less_N a b :=
begin
  intros h,
  cases h with k h,
  rw h,
  unfold less_N,
  existsi (k - 1) * a,
  rw  one_mul a,
  --struck since it rewrites everywhere, except just in the first spot I want
  sorry,
end

How do I get it to write 1 * a only at the first a, not at subsequent a's? My best guess is something involving lots of _ and type inference but I couldn't get anything working. Many thanks.

Sara Fish (Jul 15 2021 at 21:39):

Here is the tactic state before one_mul

1 goal
a b k : ,
h : b = k * a
 a + (k - 1) * a = k * a

Here is the tactic state after one_mul

1 goal
a b k : ,
h : b = k * a
 1 * a + (k - 1) * (1 * a) = k * (1 * a)

Reid Barton (Jul 15 2021 at 21:42):

I don't think there is a way to do this with the built-in rw tactic, because the expression a you want to rewrite appears again elsewhere in the term. I would suggest using suffices to give the exact new goal you want, and working backwards.

Bryan Gin-ge Chen (Jul 15 2021 at 21:43):

You might be able to use rewrites in conv mode to do this.

Reid Barton (Jul 15 2021 at 21:45):

er, I guess I really meant working forwards!

  suffices : 1 * a + (k - 1) * a = k * a, { rwa nat.one_mul at this },

Kyle Miller (Jul 15 2021 at 23:26):

I don't think a + (k - 1) * a = k * a is true, so it might be hard to prove. If k = 0, then since 0 - 1 = 0, you would need to prove a = 0.

Kyle Miller (Jul 15 2021 at 23:30):

Yeah, when b = 0, the lemma div_less is false since every a divides 0, but most values of a aren't less than or equal to 0.

Kyle Miller (Jul 15 2021 at 23:35):

I forget how I'm supposed to use the injectivity of nat.succ, but nat.no_confusion seems to do the trick. (I just wanted to see if I could disprove the lemma without importing anything.)

def divides_N (a b : ) :=  k : , b = k * a
def less_N (a b : ) :=  k : , a + k = b

lemma not_div_less : ¬( (a b : ), divides_N a b  less_N a b) :=
begin
  intro h,
  have hd : divides_N 1 0,
  { existsi 0,
    trivial },
  specialize h 1 0 hd,
  cases h with k hk,
  rw nat.add_comm at hk,
  injection hk,  -- (was exact nat.no_confusion hk)
end

Yakov Pechersky (Jul 15 2021 at 23:37):

docs#nat.succ_inj'

Kyle Miller (Jul 15 2021 at 23:43):

@Yakov Pechersky That needs to be imported though. I guess I meant whether there was some basic tactic that could deduce hk : k.succ = 0 is a contradiction. That jogged my memory, though, about injection hk

Kyle Miller (Jul 15 2021 at 23:46):

I guess I also said the wrong thing. I didn't mean the injectivity of succ, but that the image of succ is disjoint from 0. (It's sort of like injectivity of the constructors in total.)

Sara Fish (Jul 16 2021 at 00:00):

Thanks all. Both for the tactic suggestions and for pointing out that the lemma was actually false. Classic mistake :smile:

Kyle Miller (Jul 16 2021 at 00:22):

@Sara Fish Back when I was doing the natural number game, I remember late one night asking how I was supposed to deal with the goal 0 = succ b, and Kevin Buzzard kindly informed me that this cannot be proved :smile:

Mario Carneiro (Jul 16 2021 at 00:53):

strictly speaking that's an open question


Last updated: Dec 20 2023 at 11:08 UTC