Library prosa.util.unit_growth

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
Require Import prosa.util.tactics prosa.util.notation.

We say that a function f is a unit growth function iff for any time instant t it holds that f (t + 1) ≤ f t + 1.

Definition unit_growth_function (f : → ) :=
∀ t, f (t + 1) ≤ f t + 1.

In this section, we prove a few useful lemmas about unit growth functions.

Section Lemmas.

Let f be any unit growth function over natural numbers.

Variable f : → .
Hypothesis H_unit_growth_function : unit_growth_function f.

In the following section, we prove a result similar to the intermediate value theorem for continuous functions.

Section ExistsIntermediateValue.

Consider any interval , .

Variable : .
Hypothesis H_is_interval : ≤ .

Let t be any value such that f ≤ y < f .

Variable y : .
Hypothesis H_between : f ≤ y < f .

Then, we prove that there exists an intermediate point x_mid such that f x_mid = y.

    Lemma exists_intermediate_point :
      ∃ x_mid , ≤ x_mid < ∧ f x_mid = y.
    Proof.
      rename H_is_interval into INT, H_unit_growth_function into UNIT, H_between into BETWEEN.
      move: INT BETWEEN; clear .
      suff DELTA:
        ∀ delta,
          f ≤ y < f ( + ) →
          ∃ x_mid , ≤ x_mid < + ∧ f x_mid = y.
      { move ⇒ LE /andP [GEy LTy].
        (* apply DELTA. *)
        specialize (DELTA ( - )); feed DELTA.
        { by apply/andP; split; last by rewrite addnBA // addKn. }
        by rewrite subnKC in DELTA.
      }
      induction .
      { rewrite addn0; move ⇒ /andP [ ].
        by apply (leq_ltn_trans ) in ; rewrite ltnn in .
      }
      { move ⇒ /andP [GT LT].
        specialize (UNIT ( + )); rewrite leq_eqVlt in UNIT.
        have LE: y ≤ f ( + ).
        { move: UNIT ⇒ /orP [/eqP EQ | UNIT]; first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.
          rewrite [X in _ < X]addn1 ltnS in UNIT.
          apply: (leq_trans _ UNIT).
          by rewrite addn1 -addnS ltnW.
        } clear UNIT LT.
        rewrite leq_eqVlt in LE.
        move: LE ⇒ /orP [/eqP EQy | LT].
        { ∃ ( + ); split; last by rewrite EQy.
          by apply/andP; split; [apply leq_addr | rewrite addnS].
        }
        { feed (IHdelta); first by apply/andP; split.
          move: IHdelta ⇒ [x_mid [/andP [ ] ]].
          ∃ x_mid; split; last by done.
          apply/andP; split; first by done.
          by apply: (leq_trans ); rewrite addnS.
        }
      }
    Qed.

  End ExistsIntermediateValue.

In this section, we, again, prove an analogue of the intermediate value theorem, but for predicates over natural numbers.

Section ExistsIntermediateValuePredicates.

Let P be any predicate on natural numbers.

Variable P : → bool.

Consider a time interval [t1,t2] such that ...

Variables : .
Hypothesis H_t1_le_t2 : ≤ .

... P doesn't hold for ...

Hypothesis H_not_P_at_t1 : ~~ P .

... but holds for .

Hypothesis H_P_at_t2 : P .

Then we prove that within time interval [t1,t2] there exists time instant t such that t is the first time instant when P holds.

    Lemma exists_first_intermediate_point :
      ∃ t , ( < t ≤ ) ∧ (∀ x, ≤ x < t → ~~ P x ) ∧ P t.
    Proof.
      have EX: ∃ x , P x && ( < x ≤ ).
      { ∃ .
        apply/andP; split; first by done.
        apply/andP; split; last by done.
        move: H_t1_le_t2; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | ]; last by done.
        by exfalso; subst ; move: H_not_P_at_t1 ⇒ /negP .
      }
      have MIN := ex_minnP EX.
      move: MIN ⇒ [x /andP [Px /andP [ ]] MIN]; clear EX.
      ∃ x; repeat split; [ apply/andP; split | | ]; try done.
      move ⇒ y /andP [ ]; apply/negPn; intros Py.
      feed (MIN y).
      { apply/andP; split; first by done.
        apply/andP; split.
        - move: . rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | ]; last by done.
          by exfalso; subst y; move: H_not_P_at_t1 ⇒ /negP .
        - by apply ltnW, leq_trans with x.
      }
      by move: ; rewrite ltnNge; move ⇒ /negP .
    Qed.

  End ExistsIntermediateValuePredicates.

End Lemmas.