Proving: z.natAbs = z.toNat for non negative z.

Stream: new members

[Kajani Kaunda]

How do I resolve the following? Any help is much appreciated.

lemma natAbs_eq_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) :  z.natAbs = z.toNat := by sorry

[Aaron Liu]

@loogle Int.natAbs, Int.toNat, |- @Eq Nat _ _

[loogle]

:search: Int.toNat_add_toNat_neg_eq_natAbs, Int.emod_natAbs_of_nonneg, and 1 more

[Kajani Kaunda]

Aaron Liu said:

loogle Int.natAbs, Int.toNat, |- @Eq Nat _ _

How exactly do I code this in a Lemma? Sorry for my ignorance!

[Aaron Liu]

I guess you can use docs#Int.toNat_add_toNat_neg_eq_natAbs along with docs#Int.toNat_of_nonpos

[Kajani Kaunda]

Aaron Liu said:

I guess you can use docs#Int.toNat_add_toNat_neg_eq_natAbs along with docs#Int.toNat_of_nonpos

Let me try these out... :)

[Kajani Kaunda]

mmm. I cant get anything to compile without error... :hurt:

[Kajani Kaunda]

import Mathlib

lemma natAbs_eq_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) : z.natAbs = z.toNat := by sorry

[Rider Kirkpatrick]

Something like this?

import Mathlib

lemma natAbs_eq_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) : z.natAbs = z.toNat := by
  rw [← Int.toNat_add_toNat_neg_eq_natAbs, Nat.add_eq_left, Int.toNat_of_nonpos]
  linarith

[Kevin Buzzard]

lemma natAbs_eq_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) :  z.natAbs = z.toNat := by
  obtain ⟨n, rfl⟩ : ∃ (n : ℕ), z = n := Int.eq_ofNat_of_zero_le hz -- found with `exact?`
  simp

[Kenny Lau]

import Mathlib

lemma natAbs_eq_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) : z.natAbs = z.toNat := by
  lift z to ℕ using hz
  simp

[Kajani Kaunda]

Thank you to you all. And at @Rider Kirkpatrick and @Kevin Buzzard , thank you so very much, both of your codes compiled without error!

[Kenny Lau]

import Mathlib

lemma natAbs_eq_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) : z.natAbs = z.toNat := by
  grind

[Kenny Lau]

import Mathlib

lemma natAbs_eq_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) : z.natAbs = z.toNat := by
  omega

[Kajani Kaunda]

Kenny Lau said:

import Mathlib

lemma natAbs_eq_toNat_of_nonneg {z : ℤ} (hz : 0 ≤ z) : z.natAbs = z.toNat := by
  grind

@Kenny Lau , thank you too! Your code works too!

[Alfredo Moreira-Rosa]

As a reminder, for simple lemma like these, you can find tactics that solve the goal with hint, try?,
and for even simpler ones with exact?

[Kajani Kaunda]

ecyrbe said:

As a reminder, for simple lemma like these, you can find tactics that solve the goal with hint, try?,
and for even simpler ones with exact?.

Oh!, thanks for the tip @ecyrbe. Will try that first next time.