funext for inequalities

Stream: Is there code for X?

[Filippo A. E. Nuccio]

Just for fun, I wanted to prove the

example : (λ n : ℕ, 6 * n^2 ) ≥ (λ n : ℕ, 3 * n) * (λ n : ℕ, 2 * n) :=

which I proved doing

begin
  simp [pi.le_def],
  intro n,
  linarith,
end

and I was wondering why I can't do by {funext, linarith}. I guess this is because function extensionality is meant to be an axiom (?) about equality of functions; but is there any deep reason why function extensionality cannot be an axiom about any relation of functions, rather than only about eq? Would it be nonsensical to be able to add some @[funext] attribute to a lemma like pi.le_def that would turn the goal of my example to the inequality between natural numbers that can be solved with linarith? Is the problem (for the example at hand) related to the fact that eq : α → Prop while le : α → α → Prop?

[Mario Carneiro]

There is nothing inherent about le or any other relation that would make a funext-like theorem true. This one is only true because this is how le on functions is defined (and that's what pi.le_def is saying)

[Mario Carneiro]

You obviously wouldn't want such a theorem for ne!

[Mario Carneiro]

The theorem is also false for lt

[Filippo A. E. Nuccio]

RIght: you mean that two functions are different even if somewhere they coincide.

[Filippo A. E. Nuccio]

And ext is really saying something like "the relation you want between functions is "equivalent" to the relation you want between their values".

[Filippo A. E. Nuccio]

But for le is true, so it should be possible to add my @[funext] stuff to it, and not to ne or lt, no?

[Mario Carneiro]

Well that attribute would be @[ext] I suppose

[Mario Carneiro]

but it seems a little niche

[Filippo A. E. Nuccio]

But I tried to add it; in the sense that in my file I copied with a different name the lemma pi.le_def and put a @[ext] before it. Yet funext was not advancing.

[Mario Carneiro]

indeed, because ext assumes it's working with equality

[Filippo A. E. Nuccio]

Ah, so it only looks for equalities, not for every lemma which is marked @[ext] that would match the current goal?

[Mario Carneiro]

That would be too inefficient

[Mario Carneiro]

it could be extended to allow arbitrary relations, but at that point it's really just applying random theorems that have some vague topical resemblance to extensionality

[Filippo A. E. Nuccio]

But isn't it what simp does?

[Mario Carneiro]

not quite, simp also uses indexing to speed up the search

[Mario Carneiro]

ext uses indexing on the type of the equality that is the goal

[Mario Carneiro]

if it's not equality then it is less clear where to find the type

[Filippo A. E. Nuccio]

I see, this seems to answer my initial question. Thanks!

But on the other hand, wouldn't it be nice to add the @[simp] attribute to pi.le_def? This works in my example.

[Mario Carneiro]

I suppose, although it is only indexed on le and matches anything so it might be expensive

[Mario Carneiro]

that is, any application of simp to any inequality will apply this lemma

[Filippo A. E. Nuccio]

Got it! On the other hand, it seems that "inequalities of functions" show up pretty often and it would look natural to me that they immediately simplify to inequalities of values.

[Mario Carneiro]

Actually on second thought it's not a good idea even ignoring the performance angle, because that kind of expansion is not always desirable

[Filippo A. E. Nuccio]

Ah, right.

[Filippo A. E. Nuccio]

OKOK, thanks for your time, I have a much clearer picture now.

[Mario Carneiro]

Usually, theorems that you apply right at the beginning of the proof, unfolding definitions in the theorem statement, are not good simp lemmas because in most other cases you won't want to unfold the definitions, and this theorem is some internal API theorem that wants to unfold

[Filippo A. E. Nuccio]

And what is the general philosophy behind good simp lemmas?

[Mario Carneiro]

they are things that "simplify" the goal

[Mario Carneiro]

things that make the goal smaller are usually good, but things that reduce the complexity of the statement in other senses can also be useful

[Filippo A. E. Nuccio]

OK, so it is really a matter of experience to understand what simple or complex mean (a part from trivial examples).

[Mario Carneiro]

we have the concept of "simp-normal form" for the terms that simp will not simplify any longer, and it helps to keep in mind what you want the simp normal form to look like

[Mario Carneiro]

Having pi.le_def as a simp lemma is saying that we don't want inequalities of function types to ever be part of simp normal form

[Mario Carneiro]

but I can certainly imagine proofs where you want to work at that level and having simp undo that would be annoying

[Filippo A. E. Nuccio]

AH! This I can understand is bad.

[Filippo A. E. Nuccio]

Mario Carneiro said:

but I can certainly imagine proofs where you want to work at that level and having simp undo that would be annoying

Sure :pray:

[Mario Carneiro]

unfortunately it's hard to give a precise definition because simp is used across all domains in mathlib and the notion of simp-normal form is defined in some semi-consistent way across the board

[Filippo A. E. Nuccio]

And will some of this change in lean-4? I mean to ask: will the simplifier be more or less the same as in lean-3?

[Mario Carneiro]

so you will probably just have to get a feel for it

[Mario Carneiro]

I don't think so; simp already exists in lean 4 and we're likely to use it in more or less the same way

[Eric Wieser]

Note that instead of simp [pi.le_def]you can just do intro x

[Filippo A. E. Nuccio]

I have checked this and something which I can't really understand happens:

lemma nice : (λ n : ℕ, 6 * n^2 ) ≥ (λ n : ℕ, 3 * n) * (λ n : ℕ, 2 * n) :=
begin
  simp [pi.le_def],
  intro n,
  linarith,
end

gives me a :tada:, while

lemma ugly : (λ n : ℕ, 6 * n^2 ) ≥ (λ n : ℕ, 3 * n) * (λ n : ℕ, 2 * n) :=
begin
  intro n,
  simp,
  linarith,
end

does not finish, ending with linarith failed to find a contradiction. The (to me) incredible thing is that the state both after intro n in the first and after simp in the second is

  n : ℕ
  ⊢ 3 * n * (2 * n) ≤ 6 * n ^ 2

(and hovering over all terms, it seems that they are interpreted as being of the same type, both in nice and in ugly). Yet, in one case linarith works and in the other it does not, although the local hypotheses seem identical.

[Eric Wieser]

Adding a dsimp after the simp fixes it

[Eric Wieser]

ugly is about has_le.le ((λ (n : nat), nat) n), nice is about has_le.le nat

[Filippo A. E. Nuccio]

Great! Thanks.

[Scott Morrison]

I also recently wrote a bunch of proofs that began with simp only [pi.le_def],, and was a bit sad about it. I think it would be a very reasonable extension of ext to handle inequalities, although, as Mario essentially says, not obviously worth the effort of implementing.