# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: succ_succ_ne_one

#### Benjamin Davidson (Mar 05 2021 at 09:43):

While reviewing #6456, I realized that the following lemmas seem to only exist for `fin`

and not `nat`

.

```
import number_theory.bernoulli
namespace nat
lemma one_lt_succ_succ (n : ℕ) : 1 < n.succ.succ :=
begin
induction n with n ih,
{ exact one_lt_two },
{ exact lt_succ_of_lt ih },
end
@[simp]
lemma succ_succ_ne_one (n : ℕ) : n.succ.succ ≠ 1 :=
(nat.one_lt_succ_succ n).ne'
end nat
```

Do these lemmas already exist? If not, can I add them? I think they are generally useful and will help with golfing #6456.

#### Kevin Buzzard (Mar 05 2021 at 10:28):

```
open nat
lemma one_lt_succ_succ (n : ℕ) : 1 < n.succ.succ := succ_lt_succ $ succ_pos _
```

#### Kevin Buzzard (Mar 05 2021 at 10:29):

All the ingredients are there -- remember 1 = 0.succ by definition.

By the way, `simp`

lemmas are usually of the form `X = Y`

or `X <-> Y`

because `simp`

is a rewrite system. I'm not sure `succ_succ_ne_one`

is a good `simp`

lemma because it is not of this form.

#### Yakov Pechersky (Mar 05 2021 at 15:15):

For nat, it is not. But for fin, it might be if someone is using fin.sum_univ_succ and there are long chains of (i : fin n).succ.succ.succ

#### Yakov Pechersky (Mar 05 2021 at 15:16):

Also because (1 : fin 1) = 0

#### Benjamin Davidson (Mar 06 2021 at 09:48):

@Kevin Buzzard Ah thanks! That makes sense.

#### Benjamin Davidson (Mar 06 2021 at 09:49):

Would these be useful statements to have nonetheless?

#### Benjamin Davidson (Mar 06 2021 at 09:52):

And re the `simp`

, I don't know anything about these things, it just seemed to accomplish what I was looking for and passed the linter so I had figured it was fine.

#### Benjamin Davidson (Mar 06 2021 at 23:13):

I was trying to think about this more generally and realized that it might be useful to have `ne`

versions of `add_left_inj`

, `add_right_inj`

, and `succ_inj'`

. Specifically,

```
open nat
lemma add_ne_add_left {a b c : ℕ} : a + c ≠ b + c ↔ a ≠ b := by simp only [ne, add_left_inj]
lemma add_ne_add_right {a b c : ℕ} : c + a ≠ c + b ↔ a ≠ b := by simp only [ne, add_right_inj]
lemma succ_ne_succ {n m : ℕ} : succ n ≠ succ m ↔ n ≠ m := by simp only [ne]
```

Does that make sense? Is there a way to generalize these further? (I know the first two lemmas should be for some group and not `ℕ`

, but should I choose a group without zero so that they can be done as `to_additive`

? Is there something else I'm not taking into consideration?) Any and all help is appreciated.

#### Yakov Pechersky (Mar 06 2021 at 23:45):

Would you expect to use these lemmas to transform goals or hypotheses?

#### Kevin Buzzard (Mar 06 2021 at 23:54):

There will surely be some lemma in logic.basic saying (p iff q) implies (not p iff not q) so you could make a term mode proof using that

#### Benjamin Davidson (Mar 06 2021 at 23:59):

Goals, I think? Really my motivation is to be able to have these as direct statements. For example instead of needing to include

```
have h : n.succ.succ ≠ (0:ℕ).succ := by simpa using succ_ne_zero n,
```

I could just use `succ_ne_succ.mpr`

where `h`

would have been required.

#### Benjamin Davidson (Mar 07 2021 at 00:02):

Update using Kevin's suggestion:

```
open nat
lemma add_ne_add_left {a b c : ℕ} : a + c ≠ b + c ↔ a ≠ b := not_congr (add_left_inj c)
lemma add_ne_add_right {a b c : ℕ} : c + a ≠ c + b ↔ a ≠ b := not_congr (add_right_inj c)
lemma succ_ne_succ {n m : ℕ} : succ n ≠ succ m ↔ n ≠ m := not_congr succ_inj'
```

#### Benjamin Davidson (Mar 07 2021 at 00:18):

These now seem very simple, but the fact that `library_search`

does not procure their proofs compels me to still add them.

#### Kevin Buzzard (Mar 07 2021 at 00:20):

It doesn't find them because they're combinations of two things in the library. My instinct is that I look at these things and I can instantly see how to build them from things which will be in the library so I would not think to add them, but maybe they're useful for some people?

#### Benjamin Davidson (Mar 07 2021 at 00:21):

I did not see them instantly so I suppose I am one of those people :upside_down:

#### Kevin Buzzard (Mar 07 2021 at 00:25):

When I see the name `not_congr`

I kick myself for not guessing that this is what it was called. There should be a "guess the name of this proof" competition/website/whatever where stuff like this is thrown at you and you have to guess the correct name.

#### Benjamin Davidson (Mar 07 2021 at 00:27):

I agree with you that adding them is now really just a question regarding accessibility (for lack of a better word)

#### Benjamin Davidson (Mar 07 2021 at 00:28):

Kevin Buzzard said:

When I see the name

`not_congr`

I kick myself for not guessing that this is what it was called. There should be a "guess the name of this proof" competition/website/whatever where stuff like this is thrown at you and you have to guess the correct name.

Hahaha, this is the exact game I play as I wait for `library_search`

to do its thing! I try to beat it to the result.

#### Benjamin Davidson (Mar 07 2021 at 00:30):

Kevin Buzzard said:

It doesn't find them because they're combinations of two things in the library. My instinct is that I look at these things and I can instantly see how to build them from things which will be in the library so I would not think to add them, but maybe they're useful for some people?

To quote something @Scott Morrison once commented on one of my PRs,

"I'm in favour of adding lemmas like these. I don't think their existence causes any harm, and easy inequalities have such a high Lean-effort : IRL-effort ratio that any help (e.g. `library_search`

) is useful."

Admittedly, though, these lemmas are even simpler than the ones that were in question there.

#### Julian Berman (Mar 07 2021 at 00:44):

This may be offtopic for this topic considering all its participants likely know it already but I just today watched Kevin's own https://www.youtube.com/watch?v=bghu6jVt0SY which helped crystalize a bit of this "accessibility" question for me

#### Kevin Buzzard (Mar 07 2021 at 01:48):

I could make a bunch more videos like that if only I knew what people were looking for

#### Benjamin Davidson (Mar 07 2021 at 02:00):

How about a video for people looking for the video? :stuck_out_tongue_wink: (slippery slope)

#### Eric Wieser (Mar 07 2021 at 04:28):

The lemma you ask for exists in dot notation as `add_left_injective.ne_iff`

: (docs#function.injective.ne_iff, docs#add_left_injective)

#### Benjamin Davidson (Mar 07 2021 at 04:58):

Thanks!!

#### Scott Morrison (Mar 08 2021 at 05:30):

Kevin Buzzard said:

By the way,

`simp`

lemmas are usually of the form`X = Y`

or`X <-> Y`

because`simp`

is a rewrite system. I'm not sure`succ_succ_ne_one`

is a good`simp`

lemma because it is not of this form

In fact, `≠`

lemmas can make good simp lemmas:

```
@[simp]
lemma foo : 5 ≠ 7 := by norm_num
example (h : 5 = 7) : false :=
begin
simp at h,
exact h
end
```

That is, if you mark an `a ≠ b`

lemma with `@[simp]`

, then the `simp`

tactic will simplify any appearance of `a = b`

to `false`

, which is often quite useful.

#### Benjamin Davidson (Mar 11 2021 at 06:13):

I opened a PR (#6637) with the lemmas discussed here; we can continue the conversation there.

Last updated: May 16 2021 at 05:21 UTC