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
< 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.
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
Ah, no because the
S doesn't apply to the right variable, if I get it.
(The fact that the strict inequalities all involve large ones on
S m makes the proof work.)
I guess that's a case where the special definition of
< for type
nat has an impact on proofs.
@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