PADEC - Coq Library

Library Padec.MessagePassing.StreamUtil

From Coq Require Import Streams.
Set Implicit Arguments.

Until: P P P P Q ...

Inductive Until (A : Type) (P Q: Stream A -> Prop) (x : Stream A) : Prop :=
| until_now: Q x -> Until P Q x
| until_later: P x -> Until P Q (tl x) -> Until P Q x.

First Until Included:

Definition FUntilI (A : Type) (P Q: Stream A -> Prop) (x : Stream A) : Prop :=
Until (fun e => (P e /\ ~Q e))
(fun e => (P e /\ Q e)) x.

Weak Until: P P P P Q ... or P P P P P P ...

CoInductive WUntil (A : Type) (P Q: Stream A -> Prop) (x : Stream A) : Prop :=
| wuntil_now: Q x -> WUntil P Q x
| wuntil_later: P x -> WUntil P Q (tl x) -> WUntil P Q x.

First Weak Until Included:

Definition FWUntilI (A : Type) (P Q: Stream A -> Prop) (x : Stream A) : Prop :=
  WUntil (fun e => (P e /\ ~Q e))
         (fun e => (P e /\ Q e)) x.

Definition FExists (A : Type) (P: Stream A -> Prop) (x : Stream A) : Prop :=
  Until (fun e => ~P e) P x.

Lemma warm_up1 (A : Type) (P Q: Stream A -> Prop) (x : Stream A):
  FWUntilI P Q x -> P x.

Lemma warm_up2 (A : Type) (P Q: Stream A -> Prop) (x : Stream A):
  FWUntilI P Q x ->
  FExists Q x ->
    FUntilI P Q x.

Lemma temporal_prop (A : Type) (P Q R: Stream A -> Prop)
        (Q_dec: forall x, {Q x } + {~ Q x }) (x : Stream A):
  WUntil P Q x ->
  Exists R x ->
  (Exists Q x ) \/ (Exists (fun x0 => R x0 /\ WUntil P Q x0) x ).

Lemma ABS (A : Type) (inS inS': A -> Prop) (P Q: Stream A -> Prop) :
  (forall x, {P x } + {~ P x }) ->
  (forall x, {Q x } + {~ Q x }) ->
  (forall x, ~(Q x /\ ~ P x )) ->
  (forall x, inS (hd x) -> ~ Q x -> inS (hd (tl x))) ->
  (forall x, inS (hd x) -> ~ Q x -> P x ) ->
    (forall x, inS (hd x) -> FWUntilI P Q x ).