PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Tools.Stream

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global imports

From Coq Require Import Setoid.
From Coq Require Import SetoidList.
From Coq Require Import Morphisms.
From Coq Require Import RelationClasses.
From Coq Require Import SetoidClass.
From Coq Require Import RelationPairs.
From Coq Require Import Arith.

Local imports

From Padec Require Import OptionUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import WellfoundedUtil.
From Padec Require Import RelationA.

Open Scope signature_scope.
Set Implicit Arguments.

Scheme Acc_ind_dep := Induction for Acc Sort Prop.
Scheme Acc_rec_dep := Induction for Acc Sort Type.

Stream Definition

Finite or infinite sequence of at least one element of a given type A
Section StreamA.

  Context {A: Type} `{SA: PartialSetoid A}.

  CoInductive Stream: Type :=
  | s_one: A -> Stream
  | s_cons: A -> Stream -> Stream.

Equality on Stream eqStream

Pointwise equality on streams, based on equality on elements
  CoInductive eqStream: relation Stream :=
  | eqStream_one: forall a1 a2, pequiv a1 a2 -> eqStream (s_one a1) (s_one a2)
  | eqStream_cons: forall a1 a2 s1 s2,
      pequiv a1 a2 -> eqStream s1 s2 -> eqStream (s_cons a1 s1) (s_cons a2 s2).

eqStream is a partial equivalence relation (PER)
  Global Instance eqStream_Symmetry: Symmetric eqStream.

  Global Instance eqStream_Transitive: Transitive eqStream.

Stream is a partial setoid:
  Global Instance Stream_PartialSetoid: PartialSetoid Stream :=
    @Build_PartialSetoid _ eqStream (Build_PER _ _ _).

eqStream: inversion tools
  Lemma eqStream_inv: forall a1 a2 s1 s2,
      s_cons a1 s1 =~= s_cons a2 s2 -> s1 =~= s2.

  Lemma eqStream_inv_l: forall a1 a2 s1 s2,
      s_cons a1 s1 =~= s_cons a2 s2 -> a1 =~= a2.

  Lemma eqStream_inv_one: forall a1 a2,
      s_one a1 =~= s_one a2 -> a1 =~= a2.

  Lemma eqStream_inv_cons: forall a1 a2 s1 s2,
      s_cons a1 s1 =~= s_cons a2 s2 -> a1 =~= a2 /\ s1 =~= s2.

  Lemma eqStream_inv_False_1: forall a1 a2 s1,
      s_cons a1 s1 =~= s_one a2 -> False.
  Lemma eqStream_inv_False_2: forall a1 a2 s2,
      s_one a1 =~= s_cons a2 s2 -> False.

Tools on the Stream definition

  Global Instance s_one_compat: Proper fequiv s_one.

  Global Instance s_cons_compat: Proper fequiv s_cons.

Access to the head of a stream:
  Definition s_hd (s: Stream): A :=
    match s with (s_one a | s_cons a _) => a end.

Access to the tail of a stream:
  Definition s_tl (s: Stream): option Stream :=
    match s with
    | (s_cons _ tl) => Some tl
    | _ => None
    end.

Access to the n-th suffix of a stream:
  Fixpoint s_nth (n: nat) (s: Stream): Stream :=
    match n with
      O => s
    | S n' =>
      match s with
        s_one a => s_one a
      | s_cons a s' => s_nth n' s'
      end
    end.

  Lemma s_nth_one: forall (a: A) n, s_nth n (s_one a) = (s_one a).

  Global Instance hd_compat: Proper fequiv s_hd.

  Global Instance tl_compat: Proper fequiv s_tl.

  Global Instance nth_compat: Proper ((@eq nat) ==> fequiv) s_nth.

Stream unfolding

  Definition Stream_decompose (s: Stream): Stream :=
    match s with
      s_one x => s_one x | s_cons x s => s_cons x s
    end.

  Lemma Stream_decomposition_lemma: forall (s: Stream), s = Stream_decompose s.

  Global Instance Stream_decompose_compat: Proper fequiv Stream_decompose.

  Lemma Stream_decompose_inv:
    forall s1 s2,
      (Stream_decompose s1) =~= (Stream_decompose s2) ->
      s1 =~= s2.

End StreamA.

Tactic for eqStream
Ltac ssplit pe :=
  
  try unfold Proper in pe;
  match (type of pe) with
  | s_cons ?a1 ?s1 =~= s_cons ?a2 ?s2 =>
    let X := fresh "X" in
    assert (X := eqStream_inv_cons pe);
    clear pe; rename X into pe
  | s_one ?a1 =~= s_one ?a2 =>
    let X := fresh "X" in
    assert (X := eqStream_inv_one pe);
    clear pe; rename X into pe
  | s_one ?a1 =~= s_cons ?a2 ?s2 =>
    let X := fresh "X" in
    assert (X := eqStream_inv_False_2 pe);
    tauto
  | s_cons ?a1 ?s1 =~= s_one ?a2 =>
    assert (X := eqStream_inv_False_1 pe);
    tauto
  end.

Some LTL Operators on Stream

Section LTL_StreamA.

  Context {A: Type} `{SA: PartialSetoid A}.
  Notation Stream := (Stream (A := A)).

Definitions

Eventually, definitions and tools

  Inductive Eventually (P: Stream -> Prop): Stream -> Prop :=
  | eventually_now: forall s, P s -> Eventually P s
  | eventually_later: forall a s, Eventually P s -> Eventually P (s_cons a s).

Finally is the counter part of Eventually in Type
  Inductive Finally (P: Stream -> Prop): Stream -> Type :=
  | finally_now: forall s, P s -> Finally P s
  | finally_not_yet: forall a s, ~P (s_cons a s) -> Finally P s ->
                                 Finally P (s_cons a s).

  Lemma Finally_Eventually (P: Stream -> Prop):
    forall s, Finally P s -> Eventually P s.

  Lemma Eventually_Dec_Finally (P: Stream -> Prop)
        (Pdec: forall s, {P s} + {~P s}):
    forall s, Eventually P s -> Finally P s.

  Lemma Eventually_Dec_Finally'
        (P: Stream -> Prop) (Pdec: Weak_Dec pequiv P):
    forall s, Proper pequiv s -> Eventually P s -> Finally P s.

Always

  CoInductive Always (P: Stream -> Prop): Stream -> Prop :=
  | always_one: forall a, P (s_one a) -> Always P (s_one a)
  | always_cons: forall a s, P (s_cons a s) -> Always P s ->
                             Always P (s_cons a s).

Finally is the counter part of Eventually in Type
  CoInductive Forever (P: Stream -> Type): Stream -> Type :=
  | forever_one: forall a, P (s_one a) -> Forever P (s_one a)
  | forever_cons: forall a s, P (s_cons a s) -> Forever P s ->
                              Forever P (s_cons a s).

(Weak) Until

  CoInductive WUntil (P Q: Stream -> Prop): Stream -> Prop :=
  | wuntil_now: forall s, Q s -> WUntil P Q s
  | wuntil_later: forall a s, P (s_cons a s) -> WUntil P Q s ->
                              WUntil P Q (s_cons a s).

  Inductive Until (P Q: Stream -> Prop): Stream -> Prop :=
  | until_now: forall s, Q s -> Until P Q s
  | until_later: forall a s, P (s_cons a s) -> Until P Q s ->
                             Until P Q (s_cons a s).

Properties

  Lemma Always_inv_2: forall (P: Stream -> Prop) a s,
      Always P (s_cons a s) -> Always P s.

  Lemma Always_P_P:
    forall P (s: Stream), Always P s -> P s.

  Lemma Forever_P_P:
    forall P (s: Stream), Forever P s -> P s.

  Lemma Always_impl_P:
    forall (P Q: Stream -> Prop),
      (forall s, P s -> Q s) -> forall s, Always P s -> Always Q s.

  Lemma Always_MP:
    forall (P Q: Stream -> Prop) s,
      Always (fun s => P s -> Q s) s -> Always P s -> Always Q s.

  Lemma Always_conj:
    forall (P Q: Stream -> Prop) s,
      Always (fun s => P s /\ Q s) s <-> Always P s /\ Always Q s.

  Lemma Always_Always:
    forall (P: Stream -> Prop) s, Always P s <-> Always (Always P) s.

  Lemma Forever_forall (P Q: Stream -> Prop):
    (forall s, Q s -> P s) -> forall s, Always Q s -> Forever P s.

  Lemma Forever_forall_Type (P: Stream -> Type) (Q: Stream -> Prop):
    (forall s, Q s -> P s) -> forall s, Always Q s -> Forever P s.

  Lemma Eventually_impl_P:
    forall (P Q: Stream -> Prop),
      (forall s, P s -> Q s) -> forall s, Eventually P s -> Eventually Q s.

  Lemma Eventually_P_Always_not_P:
    forall P (s: Stream), Eventually P s -> Always (fun s' => ~ P s') s -> False.

  Lemma Always_P_Eventually_not_P:
    forall P (s: Stream), Always P s -> Eventually (fun s' => ~ P s') s -> False.

  Lemma AE_not_EA:
    forall P (s: Stream), Always (Eventually P) s ->
                          ~ Eventually (Always (fun s' => ~P s')) s.

  Lemma AE_tool:
    forall (P Q: Stream -> Prop) s,
      Always (fun s': Stream => Q s' -> Eventually P s') s ->
      Eventually Q s -> Eventually P s.

  Lemma AE_tool2:
    forall P (s: Stream) a,
      Always (Eventually P) s -> Always (Eventually P) (s_cons a s).

  Lemma AE_tool3:
    forall (P Q: Stream -> Prop) s,
      Always (fun s': Stream => Q s' -> Eventually P s') s ->
      Always (Eventually Q) s -> Always (Eventually P) s.

  Lemma AE_tool4:
    forall (P Q: Stream -> Prop)
           (Q_dec: forall s, { Q s } + { ~Q s }) s,
      Always (fun s': Stream => Q s' -> Eventually P s') s ->
      ~ Eventually (Always (fun s': Stream => Q s' /\ ~ P s')) s.

    Lemma Eventually_Dec_Finally'' (P: Stream -> Prop):
    forall s, Proper pequiv s -> Forever (fun s => {P s} + {~P s}) s ->
              Eventually P s -> Finally P s.

Compatibility

  Global Instance Eventually_compat: Proper fequiv Eventually.

  Lemma Finally_compat_impl:
    forall (P Q: Stream -> Prop) (pq: P =~= Q) x y (exy: x =~= y),
      Finally P x -> Finally Q y.

  Global Instance Always_compat: Proper fequiv Always.

  Global Instance WUntil_compat: Proper fequiv WUntil.

  Global Instance Until_compat: Proper fequiv Until.

  Lemma Forever_compat_impl:
    forall P Q (pq: forall a b, a =~= b -> P a -> Q b)
           x y (exy: x =~= y), Forever P x -> Forever Q y.

  Lemma Always_forall: forall X (P: X -> Stream -> Prop) s,
      (forall x ,(Always (P x)) s) <-> Always (fun s_ => forall x, P x s_) s.

  Lemma Always_Proper:
    forall s, Proper pequiv s -> Always (fun s => Proper pequiv s) s.

  Lemma forall_WUntil:
    forall (P Q: Stream -> Prop),
      (forall s, P s -> Q s) ->
      forall s, Eventually P s -> Always (fun s => P s \/~ P s) s ->
                WUntil (fun s => ~P s) Q s.

  Lemma Forall_Always:
    forall (Q: Stream -> Prop), (forall s, Q s) -> forall s, Always Q s.

if C is stable on a stream and P implies Q under hypothesis C and C is true on Stream s then Always P s implies Always Q s.
  Lemma Always_impl_2':
    forall (C: Stream -> Prop) (hC: forall (s: Stream), C s -> Always C s),
    forall (P Q: Stream -> Prop)
           (P_implies_Q: forall (s: Stream), C s -> P s -> Q s),
    forall (s: Stream), C s -> Always P s -> Always Q s.

  Lemma Eventually_impl_2':
    forall (C: Stream -> Prop) (hC: forall (s: Stream), C s -> Always C s),
    forall (P Q: Stream -> Prop)
           (P_implies_Q: forall (s: Stream), C s -> P s -> Q s),
    forall (s: Stream), C s -> Eventually P s -> Eventually Q s.

End LTL_StreamA.

Section Stream_Properties.

  Context {A: Type} `{SA: PartialSetoid A}.
  Notation Stream := (Stream (A := A)).

  Definition moves (s: Stream): Prop :=
    match s with
      s_one _ => True
    | s_cons a ss => ~(a =~= s_hd ss)
    end.

  Global Instance moves_compat: Proper fequiv moves.

  Definition strict_moves (s: Stream): Prop :=
    match s with
      s_one _ => False
    | s_cons a ss => ~(a =~= s_hd ss)
    end.

  Global Instance strict_moves_compat: Proper fequiv moves.

Finite Streams VS Infinite Streams

Finite or Infinite stream?
  Definition finite: Stream -> Prop :=
    Eventually (fun s => match s with
                         | s_one _ => True | s_cons _ _ => False end).

  Global Instance finite_compat: Proper fequiv finite.

  Lemma finite_inv: forall (a: A) s, finite (s_cons a s) -> finite s.

  Definition infinite: Stream -> Prop :=
    Always (fun s => match s with | s_one _ => False | s_cons _ _ => True end).

  Global Instance infinite_compat: Proper fequiv infinite.

  Lemma infinite_not_finite:
    forall (s: Stream), infinite s <-> ~ finite s.

Removing a finite prefix from a stream
  Section When.

    Variable (P: Stream -> Prop).
    Hypothesis P_compat: Proper fequiv P.

    Fixpoint When e (W: Finally P e): Stream :=
      match W with
        finally_not_yet ee _ WW => When WW
      | finally_now _ _ _ => e
      end.

    Global Instance When_compat:
      Proper (respectful_dep_param pequiv (Stream::nil) (pequiv,tt)
                                   (inr (Finally P)::nil)) When.

    Lemma When_P: forall e (W: Finally P e), P (When W).

    Lemma Always_When:
      forall Q e (W: Finally P e), Always Q e -> Always Q (When W).

    Lemma When_eq:
      forall e (fe: Finally P e),
        Proper pequiv e -> P e -> When fe = e.

  Lemma When_fst:
    forall g e (pge: Proper pequiv (s_cons g e))
           (P_compat: Proper fequiv P)
           (fe: Finally P e) (fge: Finally P (s_cons g e))
           (nP: ~ P (s_cons g e)),
      When fge =~= When fe.
  End When.

Suffix of Stream

Definition

  Definition is_suffix (s s_suf: Stream): Prop :=
    Eventually (fun s => s =~= s_suf) s.

Compatibility

  Global Instance is_suffix_compat: Proper fequiv is_suffix.

  Lemma is_suffix_inv_cons1:
    forall s suf b, is_suffix s (s_cons b suf) -> is_suffix s suf.

  Lemma is_suffix_inv_cons2:
    forall s suf a b, is_suffix (s_cons a s) (s_cons b suf) -> is_suffix s suf.

  Lemma is_suffix_id: forall s, Proper pequiv s -> is_suffix s s.

  Lemma is_suffix_Proper:
    forall s suf, is_suffix s suf -> Proper pequiv suf.

  Lemma suffix_of_suffix:
    forall e c cc, is_suffix e c -> is_suffix c cc -> is_suffix e cc.
  Lemma Always_suffix:
    forall P (P_compat: Proper pequiv P) s suf,
          Always P s -> is_suffix s suf -> Always P suf.

  Lemma When_suffix:
    forall P (P_compat: Proper fequiv P)
           (s: Stream) (ps: Proper pequiv s) (W: Finally P s),
      is_suffix s (When W).

  Lemma Eventually_suffix:
    forall P s, Proper pequiv s -> Proper pequiv P ->
                (Eventually P s <->
                 exists suf, is_suffix s suf /\ Eventually P suf).

  Lemma Eventually_conj:
    forall P Q s, Proper pequiv s -> Eventually P s ->
                  (forall s', is_suffix s s' -> P s' -> Always P s') ->
                  (forall s', is_suffix s s' -> P s' -> Eventually Q s') ->
                  Eventually (fun s => P s /\ Q s) s.

Parcimonious

  Section Parcimonious.

    Context {B: Type} `{SB: PartialSetoid B}.

    Fixpoint non_empty_parcimonious (s: Stream) (b: B) (l: list B): Prop :=
      match s with
      | s_one a => match l with
                    | nil => True
                    | b'::q => b =~= b' /\ non_empty_parcimonious (s_one a) b' q
                    end
      | s_cons a e' => match l with
                        | nil => True
                        | b'::q =>
                          (a =~= s_hd e' -> b =~= b') /\
                          non_empty_parcimonious e' b' q
                        end
      end.

    Global Instance non_empty_parcimonious_compat:
      Proper (pequiv ==> pequiv ==> eqlistA pequiv ==> iff)
             non_empty_parcimonious.

    Definition parcimonious (s: Stream) (l: list B): Prop :=
      match l with
      | nil => True
      | a::l => non_empty_parcimonious s a l
      end.

    Lemma non_empty_parcimonious_parcimonious: forall a s b l,
        non_empty_parcimonious (s_cons a s) b l ->
        parcimonious s l.

    Global Instance parcimonious_compat:
      Proper (pequiv ==> eqlistA pequiv ==> iff) parcimonious.

  End Parcimonious.

Stream constantly made of a single element

  Section is_constant.

    Definition is_constant (a: A): Stream -> Prop :=
      Always (fun s => s_hd s =~= a).

    Global Instance is_constant_compat: Proper fequiv is_constant.

    Lemma is_constant_inv:
      forall a x s, is_constant a (s_cons x s) -> is_constant a s.

    Lemma is_constant_hd:
      forall a s, is_constant a s -> s_hd s =~= a.

    Lemma is_constant_Proper_l:
      forall a s, is_constant a s -> Proper pequiv a.

    Lemma is_constant_Proper_r:
      forall a s, is_constant a s -> Proper pequiv s.

    Lemma constant_suffix:
      forall s suf, is_suffix s suf ->
                    forall x, is_constant x s -> is_constant x suf.

  End is_constant.

End Stream_Properties.

Map on stream

CoFixpoint s_map {A B: Type} (f: A -> B) (s: Stream) :=
  match s with
    | s_one a => @s_one B (f a)
    | s_cons a s => s_cons (f a) (s_map f s)
  end.

Global Instance s_map_compat {A: Type} `{SA: PartialSetoid A}
       {B: Type} `{SB: PartialSetoid B}:
  Proper (fequiv ==> pequiv ==> pequiv) (@s_map A B).

Unset Implicit Arguments.
Close Scope signature_scope.