## 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.mprwhere 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)

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