Stream: math-comp users

Topic: ssrnat: missing lemma?


view this post on Zulip Julien Puydt (Oct 19 2022 at 11:36):

In ssrnat, I saw:

From mathcomp Require Import all_ssreflect.

Check leq_trans. (* forall n m p : nat, m <= n -> n <= p -> m <= p *)

Check ltn_trans.(* forall n m p : nat, m < n -> n < p -> m < p *)

Check leq_ltn_trans. (* forall n m p : nat, m <= n -> n < p -> m < p *)

but I didn't see:

Check ltn_leq_trans. (* forall n m p: nat, m <n -> n <= p -> m < p *)

there are other combinations of <= and < missing, but I think using ltnW: forall m n: nat, m <n -> m <= n makes them useless, while for ltn_leq_trans, I don't think that's the case.

view this post on Zulip Ana de Almeida Borges (Oct 19 2022 at 11:50):

That's just an instance of leq_trans due to the way ltn is defined:

Goal forall n m p: nat, m <n -> n <= p -> m < p.
Proof. by move=> n m p; apply: leq_trans. Qed.

view this post on Zulip Julien Puydt (Oct 19 2022 at 11:57):

Hmmm... and that same proof doesn't work for leq_ltn_trans?

view this post on Zulip Julien Puydt (Oct 19 2022 at 11:57):

Ah, no because the S doesn't apply to the right variable, if I get it.

view this post on Zulip Julien Puydt (Oct 19 2022 at 11:59):

(The fact that the strict inequalities all involve large ones on S m makes the proof work.)

view this post on Zulip Julien Puydt (Oct 19 2022 at 12:01):

I guess that's a case where the special definition of < for type nat has an impact on proofs.

view this post on Zulip Julien Puydt (Oct 19 2022 at 17:02):

@Cyril Cohen Isn't that precisely an example what you mentioned this morning about adding structure on nat possibly giving issues because there are special hand-written (hence tight) things which will be replaced by something more automatic and hence looser?


Last updated: Feb 08 2023 at 04:04 UTC