PADEC
Coq Library
Toc
Tools
PADEC - Coq Library

Library Padec.Tools.Stream_Length

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Lia.

Local Imports

From Padec Require Import Stream.
From Padec Require Import SetoidUtil.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Stream Length

Tools to measure the length of
Section Stream_Length.

Stream of elements of type A
  Context {A: Type} `{SA: PartialSetoid A}.

Number of steps in a stream until reaching some predicate P.
(Relational definition)
Note that the definition is made deterministic, namely, we require that
  Section with_P.

    Variable (P: Stream (A:=A) -> Prop).
    Inductive length_until_P: Stream -> nat -> Prop :=
    | in_P: forall s, P s -> length_until_P s 0
    | add_step: forall a s n, ~ P (s_cons a s) ->
                              length_until_P s n ->
                              length_until_P (s_cons a s) (S n)
    .

    Lemma length_until_P_inv_0: forall s, length_until_P s 0 -> P s.

    Lemma length_until_P_inv_1:
      forall a s n, length_until_P (s_cons a s) (S n) -> ~ P (s_cons a s).

    Lemma length_until_P_inv_2: forall a s n, length_until_P (s_cons a s) (S n) -> length_until_P s n.

  End with_P.

Length of a finite stream
Relational definition
  Definition has_length (s: Stream) (n: nat): Prop :=
    length_until_P
      (fun s => match s with s_one _ => True
                        | s_cons _ _ => False
                end) s n.

Compatibility
  Global Instance length_until_P_compat: Proper fequiv length_until_P.

  Global Instance has_length_compat: Proper fequiv has_length.

A stream has a length iff it is finite.
  Lemma has_length_finite:
    forall (s: Stream), (exists n, has_length s n) <-> finite s.

Functional definitions

Actually counting the number of steps until reaching P.
Requires that the stream actually reaches P.
Either reachability of P is required with
  Fixpoint count_steps_aux (P: Stream -> Prop) (s: Stream)
           (F: @Finally A P s): nat :=
    match F in Finally _ _ return nat with
    | finally_now _ _ _ => 0%nat
    | finally_not_yet a s' F' => S (count_steps_aux F')
    end.

  Definition count_steps
             (P: Stream -> Prop) (s: Stream)
             (P_dec: Weak_Dec pequiv P)
             (ps: Proper pequiv s) (hs: Eventually P s): nat :=
    count_steps_aux (Eventually_Dec_Finally' P_dec ps hs).

Compatibility
  Global Instance count_steps_aux_compat:
    Proper (respectful_dep_param
              (equiv (A:=nat))
              ((Stream -> Prop)::Stream::nil)
              (fequiv,(pequiv,tt))
              (inr Finally::nil))
           (@count_steps_aux).

    Global Instance count_steps_compat:
      Proper (respectful_dep_param
              (equiv (A:=nat))
              ((Stream -> Prop)::Stream::nil)
              (fequiv,(pequiv,tt))
              (inr (fun P s => Weak_Dec pequiv P)
                   ::inl (fun P s => Proper pequiv s)
                   ::inl Eventually :: nil))
             (@count_steps).

Relational and functional counting provides the same result! NB: requires P to be weakly decicable so that counting can decide when to stop.
    Lemma steps_until_P_def_equiv:
      forall (P: Stream -> Prop) (P_dec: Weak_Dec pequiv P)
             (s: Stream) (ps: Proper pequiv s) (hs: Eventually P s)
             (n: nat),
        count_steps P_dec ps hs = n <-> length_until_P P s n.

When predicate P is reachable by some stream s, s has finite length until P.
NB: P is required to be weakly classical to be able to stop.
    Lemma Reachable_Steps:
      forall (P: Stream -> Prop),
        (forall s, (Proper pequiv s -> P s) \/ ~ P s) ->
        forall s, Proper pequiv s -> Eventually P s ->
                  exists n, length_until_P P s n.

Conversely, when a stream has some length until P, it eventually reaches P
    Lemma Reachable_steps_converse:
      forall (P: Stream -> Prop) (s: Stream) (n: nat),
        length_until_P P s n -> Eventually P s.

Furthermore, if P is weakly decidable, the stream finally reaches P
    Lemma Reachable_steps_converse':
      forall (P: Stream -> Prop),
        Weak_Dec pequiv P ->
        forall (s: Stream), Proper pequiv s ->
                            forall n, length_until_P P s n -> Finally P s.

Inclusion of predicates: the stream reaches the bigger one first
    Lemma length_until_P_le:
      forall (P: Stream -> Prop) (s: Stream) (n: nat),
        length_until_P P s n ->
        forall (Q: Stream -> Prop) (incl: forall s, P s -> Q s) (n': nat),
          length_until_P Q s n' -> n' <= n.

    Lemma length_until_P_le_ex':
      forall (P: Stream -> Prop) (s: Stream) (n: nat),
        length_until_P P s n ->
        forall (Q: Stream -> Prop)
               (Q_weak_clas: forall s, (Proper pequiv s -> Q s) \/ ~ Q s)
               (incl: forall s, P s -> Q s),
          Proper pequiv s -> exists n', length_until_P Q s n'.

    Lemma length_until_P_le_ex:
      forall (P: Stream -> Prop) (s: Stream) (n: nat),
        length_until_P P s n ->
        forall (Q: Stream -> Prop)
               (Q_weak_clas: forall s, (Proper pequiv s -> Q s) \/ ~ Q s)
               (incl: forall s, P s -> Q s),
          Proper pequiv s -> exists n', n' <= n /\ length_until_P Q s n'.

If a finite stream reaches P, it reaches it in less than its length
    Lemma longer_length:
      forall (P: Stream -> Prop) (s: Stream) (n n': nat),
        length_until_P P s n -> has_length s n' -> n' >= n.

Decreasing potential:

This section provides a tool to prove that a relational stream reaches a given predicate within at least n steps.
    Section Decreasing_Potential.

Relation that links elements in a relational stream until dum.
NB: there is no assumption on dum, this could be (fun _ => True)
      Variable (R: relation A) (dum: A -> Prop).

Predicate to be reached by the relational stream
      Variable (P: A -> Prop)
               (P_weak_classical: forall a,
                   (Proper pequiv a -> P a) \/ ~ P a).

Potential that measures an element of the relational stream
      Variable (Pot: nat -> A -> Prop).

Hypothesis that inductively makes the potential decrease step by step in the relational stream
      Hypothesis (base: forall a, Pot 0 a -> P a).
      Hypothesis (step: forall n a a', Pot (S n) a -> R a' a -> Pot n a').

For a given relational stream, if its head has Potential n, then either it is too short (length < n) or it reaches P in less than n steps
      Lemma pot_invariant_rel_stream:
        forall (n: nat) (s: Stream),
          Proper pequiv s ->
          Always (fun s =>
                    match s with
                      s_one a => dum a
                    | s_cons a s => R (s_hd s) a end) s ->
          Pot n (s_hd s) ->
          (exists n', n' < n /\ has_length s n')
          \/
          exists n', n' <= n /\
                     length_until_P (fun s => P (s_hd s)) s n'.
      Lemma pot_invariant_rel_stream':
        forall n s,
          Proper eqStream s ->
                    Always (fun s =>
                    match s with
                      s_one a => dum a
                    | s_cons a s => R (s_hd s) a end) s ->
          Eventually (fun s => P (s_hd s)) s ->
          Pot n (s_hd s) ->
          exists n', n' <= n /\
                     length_until_P (fun s => P (s_hd s)) s n'.

      Variable (N: nat).
      Hypothesis (bound: forall a, Pot N a).

      Lemma length_pot_bound:
        forall (s: Stream),
          Proper pequiv s ->
          Always (fun s =>
                    match s with
                      s_one a => dum a
                    | s_cons a s => R (s_hd s) a end) s ->
          Eventually (fun s => P (s_hd s)) s ->
          exists n, n <= N /\
                    length_until_P (fun s => P (s_hd s)) s n.

    End Decreasing_Potential.

End Stream_Length.


Close Scope nat_scope.
Close Scope signature_scope.
Unset Implicit Arguments.
You can change colors, if you wish ;)