## Stream: Coq users

### Topic: ✔ Any hints?

#### Lessness (Aug 11 2021 at 15:53):

``````Require Import VST.floyd.proofauto.

Definition sequence A := nat -> A.
Definition increasing (f: sequence Z) := forall (n: nat), f n < f (S n).

Definition unnamed (f: sequence Z) (H: increasing f) (max: Z): { n | forall i, (i < n)%nat <-> f i <= max }.
Proof.
``````

Any hints how to do this (`unnamed`)? Right now I'm stuck but, of course, I will keep thinking and tinkering.

#### Olivier Laurent (Aug 12 2021 at 19:59):

I would try to first move to `sequence nat` and `max : nat` by considering `g n := f n - f 0`, and then prove the lemma by induction on `max`.

#### Lessness (Aug 12 2021 at 23:08):

Thank you! The idea was great.

``````Require Import VST.floyd.proofauto.

Definition sequence A := nat -> A.

Definition increasing (f: sequence Z) := forall (n: nat), f n < f (S n).

Theorem thm0 (g: sequence nat) (H: forall n, (g n < g (S n))%nat) (a b: nat) (H0: (a < b)%nat): (g a < g b)%nat.
Proof.
induction H0.
+ apply H.
+ pose (H m). lia.
Qed.

Theorem thm1 (g: sequence nat) (H: forall n, (g n < g (S n))%nat) (a b: nat) (H0: (g a < g b)%nat): (a < b)%nat.
Proof.
revert b H0. induction a; intros.
+ destruct b.
- lia.
- lia.
+ pose (H a). assert (g a < g b)%nat by lia. apply IHa in H1.
inversion H1.
- subst. lia.
- lia.
Qed.

Definition unnamed0 (g: sequence nat) (H: forall i, (g i < g (S i))%nat) (M: nat) (H0: g 0%nat = 0%nat):
{ n | forall i, (i < n <-> g i <= M)%nat }.
Proof.
induction M.
+ exists 1%nat. split; intros.
- assert (i = 0)%nat by lia. subst. lia.
- assert (g i = 0)%nat by lia. clear H2. destruct i.
* lia.
* pose (H i). lia.
+ destruct IHM. destruct (le_dec (g x) (S M)).
- exists (S x). split; intros.
* assert (i0 <= x)%nat by lia. clear H1. inversion H2.
++ subst. auto.
++ subst. assert (i0 < S m)%nat by lia. apply i in H3. lia.
* inversion l.
++ clear l. assert (i0 <= x \/ x < i0)%nat by lia. destruct H2; try lia.
apply (thm0 g H) in H2. lia.
++ subst. apply i in H3. lia.
- exists x. split; intros.
* apply i in H1. lia.
* assert (g i0 < g x)%nat by lia. apply (thm1 g H) in H2. auto.
Qed.

Definition unnamed1 (f: sequence Z) (H: increasing f) (max: Z): { n | forall i, (i < n)%nat <-> f i <= max }.
Proof.
destruct (Z_lt_le_dec max (f 0%nat)).
+ exists 0%nat. split; intros.
- lia.
- induction i.
* lia.
* pose (H i). lia.
+ pose (fun (n: nat) => Z.to_nat (f n - f 0%nat)) as g.
assert (forall i, (g i < g (S i))%nat) as H0.
{ intros. unfold g. induction i.
+ pose (H 0%nat). lia.
+ pose (H (S i)). lia. }
assert (g 0%nat = 0%nat) as H1.
{ unfold g. lia. }
pose proof (unnamed0 g H0 (Z.to_nat (max - f 0%nat)) H1) as H2.
destruct H2. exists x. split; intros.
- apply i in H2. unfold g in H2. lia.
- apply i. unfold g. lia.
Qed.
``````

#### Notification Bot (Aug 12 2021 at 23:10):

Lessness has marked this topic as resolved.

Last updated: Jun 24 2024 at 12:02 UTC