new lemmas for `int`

Stream: general

[Scott Morrison]

I'd like to have the following lemmas:

@[simp] lemma int.add_minus_one (i : ℤ) : i + -1 = i - 1 := rfl

@[simp] lemma int.neg_succ_not_nonneg (n : ℕ) : 0 ≤ -[1+ n] ↔ false :=
by { simp only [not_le, iff_false], exact int.neg_succ_lt_zero n, }

@[simp] lemma int.neg_succ_sub_one (n : ℕ) : -[1+ n] - 1 = -[1+ (n+1)] := rfl

lemma int.pred_to_nat (i : ℤ) : (i - 1).to_nat = i.to_nat - 1 :=
begin
  cases i,
  { cases i,
    { simp, refl, },
    { simp, }, },
  { simp only [int.neg_succ_sub_one, int.to_nat], }
end

Any suggestions for alternatives / better names / better proofs / objections?

[Kevin Buzzard]

Do we really need to ever talk about the hideous -[1+ n]?

[Kevin Buzzard]

Wasn't it winner of the least popular constructor 2020?

[Kevin Buzzard]

Of course I'm not objecting, but I always nat_abs when I want to get from int to nat.

[Eric Wieser]

Presumably the point in int.add_minus_one (which should be add_neg_one) is that it's simp, unlike docs#sub_eq_add_neg .symm?

[Scott Morrison]

Eric Wieser said:

Presumably the point in int.add_minus_one (which should be add_neg_one) is that it's simp, unlike docs#sub_eq_add_neg .symm?

Yes. (I'll change the name.)

[Scott Morrison]

Johan also told me he uses nat_abs in preference to to_nat. Is there a reason for this beyond the paucity of lemmas for to_nat? I feel like in the long run we should just make sure both are usable.

[Mario Carneiro]

I think that it is just a API surface area mismatch. Feel free to use either one

[Mario Carneiro]

I assume int.pred_to_nat can be golfed simply because it's a theorem for int.basic that is 7 lines long :laughing:

[Mario Carneiro]

Is there a reason for add_minus_one to not be about general add groups?

[Scott Morrison]

Mario Carneiro said:

Is there a reason for add_minus_one to not be about general add groups?

Perhaps only to be conservative about new simp lemmas? This one seemed fine, but I can check if it hurts anything when available generally.

[Mario Carneiro]

we had the reverse as a simp lemma for a long time but I think we can just make up the difference with enough lemmas about (a - b) + c = a + (-b + c) and so on

[Johan Commelin]

I would prefer to simp -[1+ n] away in favour of -(n+1)...