Stream: general

Topic: non-equational simp lemmas

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?

Scott Morrison (Sep 08 2019 at 11:12):

It seems very appealing...

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]

Scott Morrison (Sep 08 2019 at 12:00):

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

Scott Morrison (Sep 08 2019 at 12:01):

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

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


Scott Morrison (Sep 08 2019 at 12:05):

No, that's not it.

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'.

Chris Hughes (Sep 08 2019 at 16:45):

Never use >

Reid Barton (Sep 08 2019 at 17:32):

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

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 <?

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.

Floris van Doorn (Sep 09 2019 at 04:58):

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

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