## Stream: general

### Topic: new lemmas for int

#### Scott Morrison (Feb 13 2021 at 23:36):

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 (Feb 13 2021 at 23:38):

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

#### Kevin Buzzard (Feb 13 2021 at 23:39):

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

#### Kevin Buzzard (Feb 13 2021 at 23:40):

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

#### Eric Wieser (Feb 14 2021 at 00:12):

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 (Feb 14 2021 at 00:18):

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 (Feb 14 2021 at 00:20):

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 (Feb 14 2021 at 00:40):

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

#### Mario Carneiro (Feb 14 2021 at 00:42):

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 (Feb 14 2021 at 00:43):

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

#### Scott Morrison (Feb 14 2021 at 01:01):

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 (Feb 14 2021 at 01:02):

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 (Feb 14 2021 at 04:37):

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

Last updated: May 13 2021 at 06:15 UTC