Stream: Coq users

Topic: ✔ Any hints?


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

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

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

view this post on Zulip Notification Bot (Aug 12 2021 at 23:10):

Lessness has marked this topic as resolved.


Last updated: Feb 04 2023 at 20:02 UTC