Zulip Chat Archive

Stream: general

Topic: new lemmas for `int`


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 13 2021 at 23:38):

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

view this post on Zulip Kevin Buzzard (Feb 13 2021 at 23:39):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Feb 14 2021 at 00:43):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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