Stream: math-comp users

Topic: Nonincreasing sequences: one step is equivalent to global


view this post on Zulip 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.)

view this post on Zulip Pierre Roux (Oct 11 2022 at 13:47):

I don't think there is much about sequences in MathComp, that rather belongs to Analysis.

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Oct 11 2022 at 14:13):

It is already there in the library.

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Oct 11 2022 at 14:13):

One direction is trivial and the other is nonincnP.

view this post on Zulip 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}

view this post on Zulip 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}

Last updated: Feb 08 2023 at 04:04 UTC