non-equational simp lemmas

Stream: general

[Scott Morrison]

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]

It seems very appealing...

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

No, that's not it.

[Floris van Doorn]

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

[Chris Hughes]

Never use >

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Keeley Hoek]

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