Stream: math-comp users

Topic: ssrnat: missing lemma?

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.

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.
``````

Julien Puydt (Oct 19 2022 at 11:57):

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

Julien Puydt (Oct 19 2022 at 11:57):

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

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.)

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.

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: Jul 23 2024 at 20:01 UTC