monotone vs strict_mono

Stream: general

[Damiano Testa]

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]

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]

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]

Yes, it is an order_embedding iirc

[Damiano Testa]

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.