nth_rewrite without mathlib

Stream: new members

[Sara Fish]

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]

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]

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]

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

[Reid Barton]

er, I guess I really meant working forwards!

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

[Kyle Miller]

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]

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]

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]

docs#nat.succ_inj'

[Kyle Miller]

@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]

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]

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

[Kyle Miller]

@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]

strictly speaking that's an open question