Julien Puydt (Oct 19 2022 at 11:36): 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.
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: Feb 08 2023 at 04:04 UTC