PADEC - Coq Library
Library Padec.Tools.Stream
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.
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.
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.
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.
Section StreamA.
Context {A: Type} `{SA: PartialSetoid A}.
CoInductive Stream: Type :=
| s_one: A -> Stream
| s_cons: A -> Stream -> Stream.
Context {A: Type} `{SA: PartialSetoid A}.
CoInductive Stream: Type :=
| s_one: A -> Stream
| s_cons: A -> Stream -> Stream.
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_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.
Global Instance eqStream_Transitive: Transitive eqStream.
Stream is a partial setoid:
Global Instance Stream_PartialSetoid: PartialSetoid Stream :=
@Build_PartialSetoid _ eqStream (Build_PER _ _ _).
@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.
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.
Global Instance s_one_compat: Proper fequiv s_one.
Global Instance s_cons_compat: Proper fequiv s_cons.
Global Instance s_cons_compat: Proper fequiv s_cons.
Access to the head of a stream:
Access to the tail of a stream:
Definition s_tl (s: Stream): option Stream :=
match s with
| (s_cons _ tl) => Some tl
| _ => None
end.
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.
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.
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.
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.
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.
Section LTL_StreamA.
Context {A: Type} `{SA: PartialSetoid A}.
Notation Stream := (Stream (A := A)).
Context {A: Type} `{SA: PartialSetoid A}.
Notation Stream := (Stream (A := A)).
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).
| 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.
| 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.
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).
| 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).
| 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).
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).
| 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).
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 Always_forall' (P Q: Stream -> Prop):
(forall s, Q s -> P s) -> forall s, Always Q s -> 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.
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 Always_forall' (P Q: Stream -> Prop):
(forall s, Q s -> P s) -> forall s, Always Q s -> 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.
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.
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.
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.
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.
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 depR 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.
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 depR 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.
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.
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.
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.
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.
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.
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.
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.
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.