int.to_nat_eq_zero

Stream: Is there code for X?

[Damiano Testa]

Dear All,

are the two lemmas below already in mathlib? If not, should they go in? With the simp attribute?

Thanks!

import data.int.basic

@[simp]
lemma int.coe_nat_nonpos_iff {n : ℕ} : (n : ℤ) ≤ 0 ↔ n = 0 :=
by exact_mod_cast nat.le_zero_iff

@[simp]
lemma int.to_nat_eq_zero {n : ℤ} : n.to_nat = 0 ↔ n ≤ 0 :=
begin
  induction n,
  { simp only [int.of_nat_eq_coe, int.to_nat_coe_nat, int.coe_nat_nonpos_iff] },
  { simp [int.neg_succ_of_nat_coe'] }
end

[Eric Rodriguez]

for the second one, maybe docs#int.to_nat_eq_max or docs#int.to_nat_of_nonpos is sufficient? there's also docs#norm_num.int_to_nat_neg (+ a pos variant too), but I think we're encouraged to not use tactic lemmas

the first one i'm 90% sure isn't anyhwere, I think it should be around docs#int.coe_nat_pos but it doesn't seem like it is

[Damiano Testa]

Eric, thanks! int.to_nat_of_nonpos is one of the implications (the mpr direction) of the second lemma. I am trying to see if I can get a term-mode proof!

[Yaël Dillies]

Have a look at file#algebra/order/floor

[Yaël Dillies]

In particular, docs#floor_ring.to_floor_semiring

[Damiano Testa]

Yaël, I have not been able to use your suggestion, but I also do not know my way around the floor library.

[Damiano Testa]

I found a term-mode proof, if it is preferable, though certainly there are multiple golfing possibilities!

import data.int.basic

namespace int

@[simp]
lemma coe_nat_nonpos_iff {n : ℕ} : (n : ℤ) ≤ 0 ↔ n = 0 :=
⟨ λ h, le_antisymm (int.coe_nat_le.mp (h.trans int.coe_nat_zero.le)) n.zero_le,
  λ h, (coe_nat_eq_zero.mpr h).le⟩

lemma to_nat_neg_nat : ∀ {n : ℕ},  (-(n : ℤ)).to_nat = 0
| 0       := rfl
| (n + 1) := rfl

@[simp]
lemma to_nat_eq_zero : ∀ {n : ℤ}, n.to_nat = 0 ↔ n ≤ 0
| (n : ℕ) := calc _ ↔ (n = 0) : ⟨(to_nat_coe_nat n).symm.trans, (to_nat_coe_nat n).trans⟩
                ... ↔ _       : int.coe_nat_nonpos_iff.symm
| -[1+ n] := show ((-((n : ℤ) + 1)).to_nat = 0) ↔ (-(n + 1) : ℤ) ≤ 0, from
calc _ ↔ true : ⟨λ _, trivial, λ h, to_nat_neg_nat⟩
   ... ↔ _    : ⟨λ h, int.neg_nonpos_of_nonneg (int.coe_zero_le (n + 1)), λ _, trivial⟩

end int

Also, CI is happy with the new lemmas being marked as simp, in case it matters!

[Damiano Testa]

I went ahead and made a PR : #12380.