## 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,
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