Julien Puydt (Oct 11 2022 at 13:11): Julien Puydt (Oct 11 2022 at 13:11):I ended up not needing the leq_eq_addn lemma I wrote yesterday, but I still needed to prove this, and wondered if it's somewhere and I missed it:
From mathcomp Require Import all_ssreflect.
Open Scope order_scope.
Section Name.
Context {disp: unit} {T: orderType disp}.
Lemma seq_nonincr_iff_onestep {u: nat -> T}:
(forall n, u n.+1 <= u n) <-> (forall m n, m <= n -> u n <= u m).
Proof.
split ; last first.
move=> nonincr n.
by apply: (nonincr n n.+1).
move=> onestep m n m_le_n.
rewrite -(subnKC m_le_n).
have nameless: forall p, u (m+p) <= u m.
elim=> [ | p Hp]; first by rewrite addn0.
rewrite -addn1 addnA addn1.
apply Order.POrderTheory.le_trans with (y:= u (m+p)).
by [].
by [].
by [].
Qed.
End Name.
(notice that it should also come with its three brothers and sisters about increasing, decreasing and nondecreasing sequences.)
Pierre Roux (Oct 11 2022 at 13:47):I don't think there is much about sequences in MathComp, that rather belongs to Analysis.
Pierre Jouvelot (Oct 11 2022 at 14:12):I have the feeling that this lemma can be seen as a variant of telescope_big on booleans with f = fun n m => u m <= u n and op = (&&). If this is the case, i'm not sure the proof would be shorter than a simple elim though.
Cyril Cohen (Oct 11 2022 at 14:13):It is already there in the library.
Cyril Cohen (Oct 11 2022 at 14:13):From mathcomp Require Import all_ssreflect.
Open Scope order_scope.
Section Name.
Context {disp: unit} {T: orderType disp}.
Lemma seq_nonincr_iff_onestep {u: nat -> T}:
(forall n, u n.+1 <= u n) <-> (forall m n, m <= n -> u n <= u m).
Proof. by split=> [u_noninc m n|+ n] => [|-> //]; apply: nonincnP. Qed.
End Name.
One direction is trivial and the other is nonincnP.
Cyril Cohen (Oct 11 2022 at 14:15):The four lemmas you were thinking about are:
Context {disp : unit} {T : porderType disp} [f : nat -> T].
nonincnP: (forall i : nat, f i.+1 <= f i) -> {homo f : j i / i <= j >-> j <= i}
nondecnP: (forall i : nat, f i <= f i.+1) -> {homo f : i j / i <= j >-> i <= j}
incnP: (forall i : nat, f i < f i.+1) -> {mono f : i j / i <= j >-> i <= j}
decnP: (forall i : nat, f i.+1 < f i) -> {mono f : j i / i <= j >-> j <= i}
And weaker variants :
homo_ltn_lt: (forall i : nat, f i < f i.+1) -> {homo f : i j / i < j >-> i < j}
nhomo_ltn_lt: (forall i : nat, f i.+1 < f i) -> {homo f : j i / i < j >-> j < i}
Ah, it was here all along! Thanks!
Notification Bot (Oct 11 2022 at 15:05):Julien Puydt has marked this topic as resolved.
Last updated: Dec 06 2023 at 14:01 UTC