Zulip Chat Archive

Stream: general

Topic: monotone vs strict_mono


Damiano Testa (Jun 11 2021 at 09:55):

Dear All,

I noticed that monotone assumes preorder, while strict_mono assumes has_lt. In the spirit of generalizing, I thought that I would change the assumptions on monotone to just has_le and essentially everything works smoothly... except that one of the tests of apply_fun fails.

If you want to take a look, this is on the branch adomani_monotone_strict. The only issue for CI is the failed apply_fun test. Note that the failure is not terrible: it created three side goals, instead of two, and only two get closed. You can close the remaining goal with apply order_embedding.monotone, though this is not the point.

@Scott Morrison, I am pinging you, since you said that you were interested in this issue here

Permalink to GitHub line with one unsolved goal

Floris van Doorn (Jun 11 2021 at 17:05):

It looks like apply_fun tries to call mono, which now fails because of the change (so you get an unsolved goal). @Simon Hudon would you be able to take a look?

Simon Hudon (Jun 11 2021 at 17:12):

It seems like the issue is that mono needs to assume monotone ⇑fin.cast_succ which it cannot discharge automatically (anymore?) and just leaves the goal there. Is there a proof that fin.cast_succ is monotone somewhere?

Yakov Pechersky (Jun 11 2021 at 17:25):

Yes, it is an order_embedding iirc

Damiano Testa (Jun 11 2021 at 18:58):

Thank you for looking into this issue!

It is partially satisfying that I am not the only one who is surprised by this behaviour.

Btw, while it would be nice to be able to simply state monotonicity as a condition on a general relation, I do not actually have a use case for the definition with has_le as opposed to preorder.


Last updated: Dec 20 2023 at 11:08 UTC