between N and Z

Stream: new members

[Jeremy Kahn]

Hi there! I'm learning lean and trying to understand coercions between N and Z.

For example I'd like to prove

lemma abx (a b: ℕ ) (x: ℤ ): ↑a = ↑b * x -> b ∣ a

and I'd like to be able to state

lemma an (a: ℕ ): (↑ a).nat_abs = a

without getting some sort of strange error.

Any suggestions?

[Kyle Miller]

Lean needs some hint about what the target type for a coercion is to be able to use dot notation. (↑ a : ℤ).nat_abs should work. (Formatting hint: #backticks)

[Kyle Miller]

Another way to write this is as int.nat_abs a since that's what the dot notation resolves to and since Lean auto-inserts coercions.

[David Renshaw]

Here's a proof of your lemma:

lemma abx (a b: ℕ ) (x: ℤ ): ↑a = ↑b * x -> b ∣ a :=
begin
  intro h,
  cases a,
  { use 0, apply nat.mul_zero b },
  { cases b,
    { rw [int.coe_nat_zero, int.zero_mul] at h,
      have ha : a.succ = 0 := int.coe_nat_eq_zero.mp h,
      rw[ha] },
    { have ha : 0 < (a.succ : ℤ) := int.coe_succ_pos a,
      have hb : 0 < (b.succ : ℤ) := int.coe_succ_pos b,
      rw[h] at ha,
      have hx : 0 < x := (zero_lt_mul_left hb).mp ha,
      have hx' : 0 ≤ x := le_of_lt hx,
      obtain ⟨y, hy⟩ : ∃ y : ℕ, (y:ℤ) = x := can_lift.prf x hx',
      use y,
      rw [←hy] at h,
      exact int.of_nat.inj h } }
end

[David Renshaw]

It seems likely that a nicer proof should be possible.

[Junyan Xu]

This one is almost in the library (I just found it yesterday):

import data.int.basic

lemma abx (a b : ℕ) (x : ℤ): ↑a = ↑b * x → b ∣ a :=
begin
  rw ← int.coe_nat_dvd,
  intro h, exact ⟨x, h⟩,
end