Lessness (Aug 11 2021 at 15:53): 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.
Admitted.
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.
Lessness has marked this topic as resolved.
Last updated: Oct 01 2023 at 17:01 UTC