Stream: math-comp users

Topic: ✔ Nonincreasing sequences: one step is equivalent to global

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

Cyril Cohen (Oct 11 2022 at 14:13):

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

Cyril Cohen (Oct 11 2022 at 14:17):

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

Julien Puydt (Oct 11 2022 at 15:05):

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