succ_succ_ne_one

Stream: Is there code for X?

[Benjamin Davidson]

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]

open nat

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

[Kevin Buzzard]

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]

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]

Also because (1 : fin 1) = 0

[Benjamin Davidson]

@Kevin Buzzard Ah thanks! That makes sense.

[Benjamin Davidson]

Would these be useful statements to have nonetheless?

[Benjamin Davidson]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

These now seem very simple, but the fact that library_search does not procure their proofs compels me to still add them.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Benjamin Davidson]

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]

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]

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]

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

[Benjamin Davidson]

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

[Eric Wieser]

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]

Thanks!!

[Scott Morrison]

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]

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