Zulip Chat Archive

Stream: general

Topic: non-equational simp lemmas


view this post on Zulip Scott Morrison (Sep 08 2019 at 11:11):

In a previous discussion we talked about having simp do more. As an example, as well as
lemma succ_pos (n : ℕ) : succ n > 0 := ...
we could have
@[simp] lemma succ_pos_iff (n : ℕ) : succ n > 0 ↔ true := ...
Why don't we do this?

view this post on Zulip Scott Morrison (Sep 08 2019 at 11:12):

It seems very appealing...

view this post on Zulip Mario Carneiro (Sep 08 2019 at 11:17):

They are equivalent; simp automatically applies eq_true_iff if you mark a non equality thing as @[simp]

view this post on Zulip Scott Morrison (Sep 08 2019 at 12:00):

Hmm, I can't seem to get this to work.

view this post on Zulip Scott Morrison (Sep 08 2019 at 12:01):

Maybe something is different if you add the [simp] attribute later?

view this post on Zulip Scott Morrison (Sep 08 2019 at 12:03):

This works:

@[simp] lemma succ_pos' (n : ℕ) : succ n > 0 := succ_pos n
example (n : ℕ) : succ n > 0 := by simp

but this doesn't

attribute [simp] succ_pos
example (n : ℕ) : succ n > 0 := by simp

view this post on Zulip Scott Morrison (Sep 08 2019 at 12:05):

No, that's not it.

view this post on Zulip Floris van Doorn (Sep 08 2019 at 16:43):

I think it's because the statement of succ_pos is 0 < succ n, which is not syntactically equal to succ_pos'.

view this post on Zulip Chris Hughes (Sep 08 2019 at 16:45):

Never use >

view this post on Zulip Reid Barton (Sep 08 2019 at 17:32):

Could we just make > notation? Even though it is already defined in core?

view this post on Zulip Scott Morrison (Sep 08 2019 at 22:46):

How would people feel about a PR going through e.g. data/nat/basic.lean and flipping all the > for <?

view this post on Zulip Scott Morrison (Sep 09 2019 at 03:18):

Could we just make > notation? Even though it is already defined in core?

@Reid Barton, unfortunately this nice idea doesn't seem to work. I get lots of ambiguous overload errors.

view this post on Zulip Floris van Doorn (Sep 09 2019 at 04:58):

We could make it a local(ized) notation in every file.

view this post on Zulip Keeley Hoek (Sep 09 2019 at 05:18):

I think that won't work Floris, since

import tactic

notation b `>` a := a < b

def nnn : 2 > 1 := by linarith

just won't compile in any file


Last updated: May 09 2021 at 18:17 UTC