# Zulip Chat Archive

## 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