From Coq Require Import Morphisms List.
From Velus Require Import Common.CommonList.
From Velus.Lustre.Denot.Cpo Require Import Cpo_streams_type Systems.
Import ListNotations.
Require Import Cpo_def_ext.
Extension of the Cpo library
Cpo_streams_type.v
Global Hint Rewrite
first_cons
CONS_simpl Cons_simpl
DSCASE_simpl DScase_cons
REM_simpl rem_cons
app_cons
filter_eq_cons map_eq_cons
rem_bot map_bot filter_bot first_eq_bot
:
cpodb.
Lemma bot_not_cons :
forall D (
x :
D)
s, 0 ==
cons x s ->
False.
Proof.
Lemma Con_eq_simpl :
forall D a b (
s t :
DS_ord D),
(
Con a s:
DS_ord D) ==
Con b t->
a =
b /\
s ==
t.
Proof.
Lemma Con_le_simpl :
forall D a b (
s t :
DS_ord D),
(
Con a s:
DS_ord D) <=
Con b t ->
a =
b /\
s <=
t.
Proof.
Lemma DSle_cons_elim :
forall D (
x :
DS D)
a (
s :
DS D),
(
Con a s :
DS D) <=
x ->
exists t,
x ==
Con a t /\
s <=
t.
Proof.
Lemma Con_le_le :
forall D x xs y ys t,
(
Con x xs :
DS D) <=
t ->
(
Con y ys :
DS D) <=
t ->
x =
y.
Proof.
intros *
Le1 Le2.
eapply DSle_cons_elim in Le1 as (?&
Hx &?),
Le2 as (?&
Hy &?).
rewrite Hx in Hy.
now apply Con_eq_simpl in Hy as [].
Qed.
Lemma app_app :
forall D (
s t u :
DS D),
app (
app s u)
t ==
app s t.
Proof.
Lemma FILTER_filter :
forall D P Pdec (
s:
DS D),
FILTER P Pdec s =
filter P Pdec s.
Proof.
reflexivity.
Qed.
Global Hint Rewrite FILTER_filter :
cpodb.
Lemma MAP_map :
forall D1 D2 (
F:
D1->
D2) (
s:
DS D1),
MAP F s =
map F s.
Proof.
reflexivity.
Qed.
Global Hint Rewrite MAP_map :
cpodb.
Lemma DScase_bot_eq :
forall D D' f, @
DScase D D' f 0 == 0.
Proof.
auto.
Qed.
Global Hint Rewrite DScase_bot_eq :
cpodb.
Lemma DScase_bot2_le :
forall D D' (
f :
D ->
DS D -
m>
DS D') (
Fbot :
forall a x,
f a x == 0),
forall x,
DScase f x <= 0.
Proof.
Lemma DScase_bot2 :
forall D D' (
f :
D ->
DS D -
m>
DS D') (
Fbot :
forall a x,
f a x == 0),
forall x,
DScase f x == 0.
Proof.
Lemma cons_is_cons :
forall D a (
x t :
DS D),
x ==
cons a t ->
is_cons x.
Proof.
now intros * ->.
Qed.
Lemma Epsdecomp :
forall D a (
s x:
DStr D),
decomp a s (
Eps x) ->
decomp a s x.
Proof.
destruct 1 as [[|k] Hp].
inversion Hp.
now exists k.
Qed.
Lemma decomp_decomp :
forall A (
s :
DS A)
x x' t t',
decomp x t s ->
decomp x' t' s ->
x =
x' /\
t =
t'.
Proof.
clear.
intros * [
k kth].
generalize dependent s.
induction k;
simpl;
intros *
Hp Hd;
subst.
-
apply decompCon_eq in Hd.
now inversion Hd.
-
destruct s;
simpl in *.
+
apply Epsdecomp in Hd.
eauto.
+
apply decompCon_eq in Hd.
inversion Hd;
subst;
eauto.
Qed.
DS_bisimulation with two obligations in one
Lemma DS_bisimulation_allin1 :
forall D (
R:
DS D ->
DS D ->
Prop),
(
forall x1 x2 y1 y2,
R x1 y1 ->
x1==
x2 ->
y1==
y2 ->
R x2 y2)
-> (
forall (
x y:
DS D), (
is_cons x \/
is_cons y) ->
R x y ->
first x ==
first y /\
R (
rem x) (
rem y))
->
forall x y,
R x y ->
x ==
y.
Proof.
intros *
IH Hfr x t.
apply (
DS_bisimulation R);
auto;
intros ??
Hic ?;
now apply Hfr in Hic.
Qed.
ds_eq, a coinductive equivalence principle that is sometimes
less cumbersome to use than DS_bsimulation_allin1
Section DS_eq.
Variable (
D :
Type).
CoInductive ds_eq :
DS D ->
DS D ->
Prop :=
|
De :
forall x y,
(
is_cons x \/
is_cons y ->
first x ==
first y /\
ds_eq (
rem x) (
rem y)) ->
ds_eq x y.
Lemma Oeq_ds_eq :
forall x y,
x ==
y ->
ds_eq x y.
Proof.
cofix Cof;
intros.
apply De;
auto.
Qed.
Lemma ds_eq_Oeq :
forall x y,
ds_eq x y ->
x ==
y.
Proof.
intros.
apply DS_bisimulation_allin1 with (
R :=
fun U V =>
exists x y,
ds_eq x y /\
U ==
x /\
V ==
y).
-
intros *
Eq Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
eauto.
-
clear.
intros U V Hc (
x &
y &
Eq &
Hu &
Hv).
rewrite Hu,
Hv in Hc.
inversion_clear Eq.
destruct H;
auto.
setoid_rewrite Hu.
setoid_rewrite Hv.
split;
auto.
exists (
rem x), (
rem y);
split;
auto.
-
eauto.
Qed.
Lemma ds_eq_Oeq_iff :
forall x y,
ds_eq x y <->
x ==
y.
Proof.
Global Instance :
Reflexive ds_eq.
Proof.
Global Add Parametric Morphism :
ds_eq
with signature @
Oeq (
DS D) ==> @
Oeq (
DS D) ==>
iff
as DS_eq_morph.
Proof.
clear.
intros *
Eq1 *
Eq2.
split;
intro Heq;
rewrite ds_eq_Oeq_iff in *;
eauto.
Qed.
End DS_eq.
Tactic Notation "remember_ds" uconstr(
s)
"as" ident(
x) :=
let Hx :=
fresh "H"x in
remember s as x eqn:
Hx;
apply Oeq_refl_eq in Hx.
Ltac revert_all :=
repeat match goal with
|
H:_ |- _ =>
revert H
end.
Ltac coind_Oeq H :=
intros
;
match goal with
|- ?
l == ?
r =>
remember_ds l as U
;
remember_ds r as V
end
;
apply ds_eq_Oeq
;
revert_all;
cofix H
;
intros.
Lemma first_rem_eq :
forall D (
xs ys :
DS D),
first xs ==
first ys ->
rem xs ==
rem ys ->
xs ==
ys.
Proof.
Simpler principle than DSle_rec_eq
Lemma DSle_rec_eq2 :
forall D (
R :
DStr D ->
DStr D ->
Prop),
(
forall x1 x2 y1 y2:
DS_ord D,
R x1 y1 ->
x1==
x2 ->
y1==
y2 ->
R x2 y2) ->
(
forall x y,
is_cons x ->
R x y ->
first x ==
first y /\
R (
rem x) (
rem y))
->
forall x y :
DS_ord D,
R x y ->
x <=
y.
Proof.
intros *
R1 R2 x y Hr.
apply DSle_rec_eq with R;
auto.
intros ??
y' Hr'.
eapply R2 in Hr' as (?&?);
auto.
autorewrite with cpodb in *.
exists (
rem y');
split;
auto.
apply symmetry,
first_cons_elim in H as (?& -> &?).
now autorewrite with cpodb.
Qed.
The constant stream
CoFixpoint DS_const {
A} (
a :
A) :
DS A :=
Con a (
DS_const a).
Lemma DS_const_eq :
forall {
A} (
a :
A),
DS_const a =
cons a (
DS_const a).
Proof.
intros.
now rewrite DS_inv at 1.
Qed.
Lemma is_cons_DS_const :
forall {
A} (
a :
A),
is_cons (
DS_const a).
Proof.
Lemma DS_const_inf :
forall {
A} (
a :
A),
infinite (
DS_const a).
Proof.
Lemma first_DS_const :
forall D (
c :
D),
first (
DS_const c) ==
cons c 0.
Proof.
Lemma map_DS_const :
forall {
A B} (
f :
A ->
B)
c,
map f (
DS_const c) ==
DS_const (
f c).
Proof.
Global Add Parametric Morphism A B : (@
MAP A B)
with signature (
respectful eq eq) ==> @
Oeq (
DS A) ==> @
Oeq (
DS B)
as MAP_morph.
Proof.
Lemma DSle_cons :
forall D x (
xs :
DS D)
y ys,
cons x xs <=
cons y ys ->
xs <=
ys.
Proof.
Lemma app_rem_app :
forall A (
f :
DS A -
C->
DS A) (
x y :
DS A),
app x (
f (
rem (
app x y))) ==
app x (
f y).
Proof.
clear.
intros.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
U ==
V
\/
exists x y,
U ==
app x (
f (
rem (
app x y)))
/\
V ==
app x (
f y)).
3:
right;
exists x,
y;
auto.
{
intros * ?
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
eauto. }
clear.
intros U V Hc [
Heq | (
x &
y &
Hu &
Hv)].
{
setoid_rewrite Heq;
auto. }
destruct (@
is_cons_elim _
x)
as (
vx &
x' &
Hx).
{
destruct Hc;
eapply app_is_cons; [
rewrite <-
Hu|
rewrite <-
Hv];
auto. }
rewrite Hx,
app_cons,
rem_app in Hu;
auto.
rewrite Hx,
app_cons in Hv.
split.
-
rewrite Hu,
Hv;
auto.
-
setoid_rewrite Hu.
setoid_rewrite Hv.
auto.
Qed.
Lemma app_rem :
forall D (
s :
DS D),
app s (
rem s) ==
s.
Proof.
Lemma app_eq_impl :
forall A (
x1 x2 x3 y1 y2 y3:
DS A),
app x1 x2 ==
app y1 y2 ->
(
x2 ==
y2 ->
x3 ==
y3) ->
app x1 x3 ==
app y1 y3.
Proof.
intros *
Ha Him.
eapply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists x1 x2 x3 y1 y2 y3,
app x1 x2 ==
app y1 y2
/\ (
x2 ==
y2 ->
x3 ==
y3)
/\
U ==
app x1 x3
/\
V ==
app y1 y3).
3:
eauto 12.
{
intros * ?
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
eauto. }
clear.
intros U V Hc (
x1 &
x2 &
x3 &
y1 &
y2 &
y3 &
Ha &
Him &
Hu &
Hv).
setoid_rewrite Hu.
setoid_rewrite Hv.
rewrite Hu,
Hv in Hc.
clear Hu Hv.
split.
-
apply first_eq_compat in Ha.
now rewrite 2
first_app_first in *.
-
assert (
is_cons x1).
{
destruct Hc;
eauto using app_is_cons.
eapply app_is_cons;
rewrite Ha;
eauto using app_is_cons,
is_cons_app. }
assert (
is_cons y1).
{
destruct Hc;
eauto using app_is_cons.
eapply app_is_cons;
rewrite <-
Ha;
eauto using app_is_cons,
is_cons_app. }
apply rem_eq_compat in Ha as Har.
rewrite 2
rem_app in Har;
auto.
setoid_rewrite rem_app.
all:
auto.
exists (
first x3), 0, (
rem x3), (
first y3), 0, (
rem y3).
rewrite 2
app_first_rem,
Him;
auto.
Qed.
Lemma rem_app_app_rem :
forall A (
x y :
DS A),
rem (
app x (
app (
rem x)
y)) ==
app (
rem x)
y.
Proof.
intros.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists x y,
U ==
V
\/ (
U ==
rem (
app x (
app (
rem x)
y))
/\
V ==
app (
rem x)
y)).
3:
eauto.
-
intros * ?
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
eauto.
-
clear.
intros U V Hc (
x &
y & [
Huv|[
Hu Hv]]).
{
setoid_rewrite Huv.
unshelve eauto;
auto. }
edestruct (@
is_cons_elim _
x)
as (
vx &
xs &
Hx).
{
destruct Hc as [
Hc|
Hc].
-
rewrite Hu in Hc.
now apply rem_is_cons,
app_is_cons in Hc.
-
rewrite Hv in Hc.
now apply app_is_cons,
rem_is_cons in Hc. }
rewrite Hx,
app_cons, 2
rem_cons, <-
Hu in *.
setoid_rewrite Hv;
unshelve eauto;
auto.
Qed.
Lemma infinite_rem :
forall D (
s :
DS D),
infinite (
rem s) ->
infinite s.
Proof.
intros * Hi.
constructor; auto.
inversion Hi; auto.
Qed.
Lemma rem_infinite :
forall D (
s :
DS D),
infinite s ->
infinite (
rem s).
Proof.
intros * Hi.
inversion Hi; auto.
Qed.
Lemma infinite_app :
forall D (
U V :
DS D),
is_cons U ->
infinite V ->
infinite (
app U V).
Proof.
intros *
Hc Hi.
constructor;
auto.
now rewrite rem_app.
Qed.
Lemma infinite_le_eq :
forall D (
s t:
DS D),
s <=
t ->
infinite s ->
s ==
t.
Proof.
Lemma is_cons_rem :
forall D (
s :
DS D),
is_cons (
rem s) ->
exists x y xs,
s ==
cons x (
cons y xs).
Proof.
Lemma rem_eq_cons :
forall D (
b:
D)
s t,
rem s ==
cons b t ->
exists a,
s ==
cons a (
cons b t).
Proof.
intros *
Hrs.
destruct (
is_cons_rem _
s)
as (
a' &
b' &
t' &
Hs).
rewrite Hrs;
auto.
apply rem_eq_compat in Hs as HH.
rewrite rem_cons,
Hrs in HH.
apply Con_eq_simpl in HH as [?
Ht];
subst.
exists a'.
now rewrite Hs,
Ht.
Qed.
Lemma map_eq_cons_elim :
forall D D' (
f :
D ->
D')
a s x,
map f x ==
cons a s ->
exists b,
exists t,
x ==
cons b t /\
f b =
a /\
map f t ==
s.
Proof.
Lemma map_comp :
forall A B C (
f :
A ->
B) (
g :
B ->
C),
forall s,
map g (
map f s) ==
map (
fun x => (
g (
f x)))
s.
Proof.
intros.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists s,
U ==
map g (
map f s) /\
V ==
map (
fun x => (
g (
f x)))
s).
3:
eauto.
{
intros ???? (?&?&?) ??;
eauto. }
intros X Y [
Hcons|
Hcons] (
s1 &
HX &
HY);
(
split; [|
exists (
rem s1)]);
rewrite HX,
HY in *;
repeat apply map_is_cons in Hcons;
apply is_cons_elim in Hcons as (?&?&->);
now autorewrite with cpodb.
Qed.
Lemma rem_map :
forall A B (
f :
A ->
B)
xs,
rem (
map f xs) ==
map f (
rem xs).
Proof.
intros.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists xs,
U ==
rem (
map f xs)
/\
V ==
map f (
rem xs)).
3:
eauto.
{
intros ???? (?& -> & ->) ??.
eauto. }
clear.
intros U V Hc (? &
Hu &
Hv).
assert (
exists a b xs,
x ==
cons a (
cons b xs))
as (
a &
b &
xs &
Hx). {
rewrite Hu,
Hv in Hc.
destruct Hc as [
Hc |
Hc].
-
apply is_cons_rem in Hc as (?&?&?&
Hfx).
apply map_eq_cons_elim in Hfx as (?&?& ? & ? &
Hf');
subst.
apply map_eq_cons_elim in Hf' as (?& ? &
HH & ? &?);
subst.
rewrite HH in *;
eauto.
-
now apply map_is_cons,
is_cons_rem in Hc.
}
setoid_rewrite Hu.
setoid_rewrite Hv.
setoid_rewrite Hx.
split; [|
exists (
cons b xs)];
now autorewrite with cpodb.
Qed.
Lemma first_map :
forall A B (
f :
A ->
B)
s,
first (
map f s) ==
map f (
first s).
Proof.
intros.
eapply DS_bisimulation_allin1
with (
R :=
fun U V =>
exists s,
U ==
first (
map f s) /\
V ==
map f (
first s)).
3:
eauto.
{
intros * (?&?&?) ??.
esplit;
eauto. }
clear.
intros U V Hc (?&
Hu &
Hv).
assert (
is_cons x)
as Hx.
{
rewrite Hu,
Hv in *.
destruct Hc as
[
Hc %
first_is_cons %
map_is_cons |
Hc %
map_is_cons];
auto. }
apply is_cons_elim in Hx as (
vx &
xs &
Hx).
setoid_rewrite Hu.
setoid_rewrite Hv.
setoid_rewrite Hx.
split; [|
exists 0];
now autorewrite with cpodb.
Qed.
Lemma app_map :
forall A B (
f :
A ->
B) (
U V :
DS A),
map f (
app U V) ==
app (
map f U) (
map f V).
Proof.
Lemma map_ext :
forall D D' (
f g :
D ->
D'),
(
forall d,
f d =
g d) ->
forall x,
map f x ==
map g x.
Proof.
intros *
Hfg x.
apply DS_bisimulation_allin1
with (
R :=
fun U V =>
exists x,
U ==
map f x /\
V ==
map g x);
eauto 3.
{
intros * ?
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
auto. }
clear -
Hfg;
intros U V Hc (
xs &
Hu &
Hv).
destruct (@
is_cons_elim _
xs)
as (
x &
xs' &
Hxs).
{
rewrite Hu,
Hv in Hc.
now destruct Hc as [?%
map_is_cons|?%
map_is_cons]. }
rewrite Hxs,
map_eq_cons in *.
split;[|
exists xs'];
now rewrite Hu,
Hv, ?
first_cons, ?
rem_cons, ?
Hfg.
Qed.
Lemma map_inf :
forall A B (
f :
A ->
B)
xs,
infinite xs ->
infinite (
map f xs).
Proof.
intros *
Hi.
remember (
map f xs)
as fxs eqn:
Hfxs.
apply Oeq_refl_eq in Hfxs.
revert Hi Hfxs.
revert xs fxs.
cofix Cof;
intros.
assert (
Hi' :=
Hi).
inversion Hi.
constructor.
now rewrite Hfxs;
apply is_cons_map.
apply Cof with (
xs :=
rem xs);
auto.
now rewrite Hfxs, <-
rem_map.
Qed.
Lemma inf_map :
forall A B (
f :
A ->
B)
xs,
infinite (
map f xs) ->
infinite xs.
Proof.
cofix Cof;
intros *
Hf.
inversion_clear Hf;
rewrite rem_map in *.
constructor;
eauto using map_is_cons.
Qed.
Lemma cons_decomp :
forall D x (
s :
DS D)
t,
s ==
cons x t ->
exists t',
decomp x t' s /\
t ==
t'.
Proof.
Inductive isConP {
D:
Type} (
P :
D ->
Prop) :
DStr D ->
Prop :=
|
isConPEps :
forall x,
isConP P x ->
isConP P (
Eps x)
|
isConPnP:
forall a s,
isConP P s -> ~
P a ->
isConP P (
Con a s)
|
isConPP :
forall a s,
P a ->
isConP P (
Con a s).
Global Hint Constructors isConP :
core.
Lemma isConP_pred :
forall D (
P:
D->
Prop)
x,
isConP P (
pred x) ->
isConP P x.
Proof.
destruct x; simpl; auto.
Qed.
Lemma isConP_le_compat :
forall D (
P :
D ->
Prop) (
x y :
DS D),
x <=
y ->
isConP P x ->
isConP P y.
Proof.
intros *
Hle Hic.
generalize dependent y.
induction Hic;
intros;
inversion_clear Hle;
auto;
destruct H0 as [
n];
generalize dependent y;
induction n;
intros;
simpl in *;
subst;
auto using isConP_pred.
Qed.
Lemma isConP_eq_compat :
forall D (
P:
D->
Prop) (
x y:
DS D),
x ==
y ->
isConP P x ->
isConP P y.
Proof.
Add Parametric Morphism D P : (@
isConP D P)
with signature (@
Oeq (
DS D)) ==>
iff as isConP_eq_iff.
Proof.
Lemma filter_is_cons :
forall (
D :
Type) (
P :
D ->
Prop)
Pdec xs,
is_cons (
filter P Pdec xs) ->
isConP P xs.
Proof.
Lemma map_filter :
forall A B (
f :
A ->
B) (
P :
A ->
Prop)
Pdec (
P' :
B ->
Prop)
P'dec,
(
forall a,
P a <->
P' (
f a)) ->
forall xs,
map f (
filter P Pdec xs) ==
filter P' P'dec (
map f xs).
Proof.
intros *
HPP' xs.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists xs,
U ==
map f (
filter P Pdec xs)
/\
V ==
filter P' P'dec (
map f xs)).
3:
eauto.
{
intros ????(?&?&?&?)??.
repeat esplit;
eauto. }
clear xs.
intros xs ys Hic (
s &
Hx &
Hy).
destruct Hic as [
Hic|
Hic];
rewrite Hx,
Hy in *;
setoid_rewrite Hx;
setoid_rewrite Hy.
-
apply map_is_cons,
filter_is_cons in Hic.
revert Hx Hy.
revert xs ys.
induction Hic;
intros.
+
rewrite <-
eqEps in *.
setoid_rewrite <-
eqEps.
eapply IHHic;
eauto.
+
autorewrite with cpodb in *|- ;
destruct (
Pdec a)
as [
Hp|
Hnp], (
P'dec (
f a))
as [
Hp'|
Hnp'];
try tauto.
clear -
HPP' Hnp Hp';
exfalso;
firstorder 0.
destruct (
IHHic xs ys)
as (? &
x &?&?);
auto.
split; [|
exists x];
autorewrite with cpodb in *;
destruct (
Pdec a), (
P'dec (
f a));
tauto.
+
split; [|
exists s];
autorewrite with cpodb;
destruct (
Pdec a)
as [
Hp|
Hnp], (
P'dec (
f a))
as [
Hp'|
Hnp'];
try tauto.
1,3:
now autorewrite with cpodb.
all:
clear -
HPP' Hp Hnp';
exfalso;
firstorder 0.
-
apply filter_is_cons in Hic.
revert Hx Hy.
revert xs ys.
remember (
map f s)
as sm.
apply Oeq_refl_eq in Heqsm.
revert Heqsm.
revert s.
induction Hic;
intros.
+
rewrite <-
eqEps in *.
setoid_rewrite <-
eqEps.
eapply IHHic;
eauto.
+
apply symmetry,
map_eq_cons_elim in Heqsm as (
b &?&
Hs &?&
Hmap);
subst.
setoid_rewrite Hs.
specialize (
IHHic _ (
symmetry Hmap) _ _ (
Oeq_refl _) (
Oeq_refl _))
as (?&
y &?&?).
split; [|
exists y];
autorewrite with cpodb;
destruct (
Pdec b)
as [
Hp|
Hnp], (
P'dec (
f b))
as [
Hp'|
Hnp'];
try tauto;
clear -
HPP' Hp Hnp';
exfalso;
firstorder 0.
+
apply symmetry,
map_eq_cons_elim in Heqsm as (
b &
t&
Hs &?&?);
subst.
setoid_rewrite Hs.
split; [|
exists t];
autorewrite with cpodb.
all:
destruct (
Pdec b)
as [
Hp|
Hnp], (
P'dec (
f b))
as [
Hp'|
Hnp'];
try tauto.
all:
autorewrite with cpodb;
auto.
all:
clear -
HPP' Hnp Hp';
exfalso;
firstorder 0.
Qed.
Lemma infinite_decomp :
forall D (
s :
DS D),
infinite s ->
exists x t,
s ==
cons x t /\
infinite t.
Proof.
Lemma infinite_cons :
forall D x (
xs :
DS D),
infinite xs ->
infinite (
cons x xs).
Proof.
constructor;
rewrite ?
rem_cons;
auto.
Qed.
Lemma cons_infinite :
forall D x (
xs :
DS D),
infinite (
cons x xs) ->
infinite xs.
Proof.
destruct 1.
now rewrite rem_cons in *.
Qed.
Take the prefix of length min(n,length(s)) from a stream s
Fixpoint take {
A} (
n :
nat) :
DS A -
C->
DS A :=
match n with
|
O =>
CTE _ _ 0
|
S n => (
APP _ @2_
ID _) (
take n @_
REM _)
end.
Lemma take_eq :
forall {
A}
n (
s :
DS A),
take n s =
match n with
|
O => 0
|
S n =>
app s (
take n (
rem s))
end.
Proof.
destruct n; reflexivity.
Qed.
Lemma take_bot :
forall A n, @
take A n 0 == 0.
Proof.
destruct n;
rewrite take_eq;
auto.
Qed.
Lemma take_1 :
forall A (
x :
DS A),
take 1
x =
first x.
Proof.
reflexivity.
Qed.
Global Add Parametric Morphism A n : (
take n)
with signature @
Oeq (
DS A) ==> @
Oeq (
DS A)
as take_morph.
Proof.
induction n;
auto;
intros ??
Heq;
simpl.
autorewrite with cpodb.
rewrite Heq at 1.
rewrite (
IHn _ (
rem y));
auto.
Qed.
Lemma take_Oeq :
forall A (
xs ys :
DS A), (
forall n,
take n xs ==
take n ys) ->
xs ==
ys.
Proof.
Lemma take_is_cons :
forall A (
s :
DS A)
n,
is_cons (
take n s) ->
is_cons s.
Proof.
Lemma take_cons :
forall A n (
x :
A)
xs,
take (
S n) (
cons x xs) =
cons x (
take n xs).
Proof.
Lemma take_map :
forall A B (
f :
A ->
B),
forall n xs,
take n (
map f xs) ==
map f (
take n xs).
Proof.
Lemma take_rem :
forall A n (
x y:
DS A),
take (
S n)
x ==
take (
S n)
y ->
take n (
rem x) ==
take n (
rem y).
Proof.
Lemma take_Ole :
forall A n (
x:
DS A),
take n x <=
x.
Proof.
Lemma take_n_Ole :
forall A (
xs ys :
DS A), (
forall n,
take n xs <=
take n ys) ->
xs <=
ys.
Proof.
Definition and specification of nrem : n applications of rem.
It is useful to show the productivity of stream functions.
A function f of a stream xs is producive/length-preserving if
for all n, is_cons (nrem n xs) implies is_cons (n_rem n (f xs)).
Section Nrem.
Context {
A B C :
Type}.
Fixpoint nrem (
n :
nat) (
xs :
DS A) :
DS A :=
match n with
|
O =>
xs
|
S n =>
nrem n (
rem xs)
end.
Lemma nrem_S :
forall n (
xs :
DS A),
nrem (
S n)
xs =
nrem n (
rem xs).
Proof.
trivial.
Qed.
On prend True pour n = 0 afin de simplifier les cas de base dans
les preuves d'InftyProof (voir exp_n par exemple).
Definition is_ncons (
n :
nat) (
xs :
DS A) :
Prop :=
match n with
|
O =>
True
|
S n =>
is_cons (
nrem n xs)
end.
Lemma nrem_inf :
forall (
s :
DS A), (
forall n,
is_ncons n s) ->
infinite s.
Proof.
cofix Cof;
intros *
Hc.
constructor.
-
apply (
Hc 1).
-
apply Cof.
intros [];
simpl;
auto.
apply (
Hc (
S (
S n))).
Qed.
Lemma inf_nrem :
forall (
s :
DS A),
infinite s ->
forall n,
is_ncons n s.
Proof.
intros * Hf n.
generalize dependent s.
induction n as [|[]]; intros; inversion Hf; simpl; auto.
apply IHn; auto.
Qed.
Lemma nrem_inf_iff :
forall (
s :
DS A), (
forall n,
is_ncons n s) <->
infinite s.
Proof.
Lemma is_consn_DS_const :
forall (
c :
A)
n,
is_cons (
nrem n (
DS_const c)).
Proof.
Lemma is_ncons_DS_const :
forall (
c :
A)
n,
is_ncons n (
DS_const c).
Proof.
Lemma nrem_rem :
forall (
s :
DS A)
n,
nrem n (
rem s) ==
rem (
nrem n s).
Proof.
intros.
revert s.
induction n; simpl; auto.
Qed.
Lemma nrem_nrem :
forall n1 n2 xs,
nrem n1 (
nrem n2 xs) ==
nrem (
n1 +
n2)
xs.
Proof.
induction n1;
simpl in *;
intros;
auto.
now rewrite nrem_rem,
IHn1,
nrem_rem.
Qed.
Lemma infinite_nrem :
forall s,
infinite s ->
forall n,
is_cons (
nrem n s).
Proof.
intros * H n.
revert H; revert s.
induction n; simpl; intros; inversion H; auto.
Qed.
Lemma take_nrem_eq :
forall n1 n2 (
x y :
DS A),
take n1 x ==
take n1 y ->
take n2 (
nrem n1 x) ==
take n2 (
nrem n1 y) ->
take (
n1 +
n2)
x ==
take (
n1 +
n2)
y.
Proof.
Lemma is_ncons_S :
forall (
s :
DS A)
n,
is_ncons (
S n)
s ->
is_ncons n s.
Proof.
induction n as [|[]];
simpl;
auto.
rewrite nrem_rem;
auto.
Qed.
Lemma is_ncons_SS :
forall n (
xs :
DS A),
is_ncons (
S (
S n))
xs <->
is_ncons (
S n) (
rem xs).
Proof.
destruct n; simpl; split; auto.
Qed.
Lemma is_ncons_is_cons :
forall (
s :
DS A)
n,
is_ncons (
S n)
s ->
is_cons s.
Proof.
Lemma is_ncons_cons :
forall n x (
xs :
DS A),
is_ncons n xs ->
is_ncons (
S n) (
cons x xs).
Proof.
destruct n;
simpl;
intros *
Hc;
rewrite ?
rem_cons;
auto.
Qed.
Lemma nrem_eq_compat :
forall n (
s t:
DS A),
s==
t ->
nrem n s ==
nrem n t.
Proof.
induction n; simpl; auto.
Qed.
Global Add Parametric Morphism n : (
nrem n)
with signature (@
Oeq (
DS A)) ==> (@
Oeq (
DS A))
as nrem_eq_compat_morph.
Proof.
Global Add Parametric Morphism n : (
is_ncons n)
with signature (@
Oeq (
DS A)) ==>
iff as is_ncons_morph.
Proof.
unfold is_ncons.
intros *
H.
destruct n;
now rewrite ?
H.
Qed.
Lemma is_ncons_elim :
forall n (
xs :
DS A),
is_ncons (
S n)
xs ->
exists x1 xs',
xs ==
cons x1 xs' /\
is_ncons n xs'.
Proof.
intros *
Hc.
apply is_ncons_is_cons in Hc as HH.
apply is_cons_elim in HH as (
x &
xs' &
Hx).
exists x,
xs';
split;
auto.
destruct n;
simpl;
auto.
now simpl in Hc;
rewrite Hx,
rem_cons in Hc.
Qed.
Lemma is_ncons_elim2 :
forall n (
xs :
DS A),
is_ncons (
S (
S n))
xs ->
exists x1 x2 xs',
xs ==
cons x1 (
cons x2 xs') /\
is_ncons (
S n) (
cons x2 xs') /\
is_ncons n xs'.
Proof.
intros *
Hc.
apply is_ncons_elim in Hc as (
x1 &
xx &
Hx &
Hc).
apply is_ncons_elim in Hc as HH;
destruct HH as (
x2 &
xs' &
Hx' &
Hc').
rewrite Hx' in Hc.
exists x1,
x2,
xs'.
rewrite Hx,
Hx';
auto.
Qed.
Lemma nrem_infinite :
forall n xs,
infinite xs ->
infinite (
nrem n xs).
Proof.
induction n; simpl; intros * H; inversion H; auto.
Qed.
End Nrem.
Lemma nrem_map :
forall {
A B} (
f :
A ->
B)
n xs,
nrem n (
map f xs) ==
map f (
nrem n xs).
Proof.
induction n;
simpl;
intros;
auto.
rewrite rem_map;
auto.
Qed.
Lemma is_ncons_map :
forall A B (
f :
A ->
B)
s n,
is_ncons n s ->
is_ncons n (
map f s).
Proof.
Module Alt_inf.
example of usage
Definition alt :
DS bool :=
FIXP _ (
CONS true @_
MAP negb).
Lemma alt_inf :
infinite alt.
Proof.
apply nrem_inf.
induction n as [|[]];
simpl;
auto.
-
unfold alt.
rewrite FIXP_eq.
autorewrite with cpodb;
auto.
-
unfold alt in *.
rewrite FIXP_eq.
autorewrite with cpodb.
rewrite nrem_map;
auto.
Qed.
End Alt_inf.
Lifting stream predicates & functions to environment of streams
Section ENV.
Context {
I :
Type}.
Context {
SI :
I ->
Type}.
Definition all_cons (
env :
DS_prod SI) :
Prop :=
forall x,
is_cons (
env x).
Lemma all_cons_eq_compat :
forall (
env env' :
DS_prod SI),
all_cons env ->
env ==
env' ->
all_cons env'.
Proof.
Global Add Parametric Morphism :
all_cons
with signature @
Oeq (@
DS_prod I SI) ==>
iff
as all_cons_morph.
Proof.
Definition all_infinite (
env :
DS_prod SI) :
Prop :=
forall x,
infinite (
env x).
Lemma all_infinite_eq_compat :
forall (
env env' :
DS_prod SI),
all_infinite env ->
env ==
env' ->
all_infinite env'.
Proof.
Global Add Parametric Morphism :
all_infinite
with signature @
Oeq (@
DS_prod I SI) ==>
iff
as all_inf_morph.
Proof.
Lemma all_infinite_all_cons :
forall env,
all_infinite env ->
all_cons env.
Proof.
intros env Inf x; specialize (Inf x); now inversion Inf.
Qed.
Lemma all_infinite_le_eq :
forall env env',
env <=
env' ->
all_infinite env ->
env ==
env'.
Proof.
Infinité sur un domaine
Definition infinite_dom (
env :
DS_prod SI) (
l :
list I) :
Prop :=
forall x,
In x l ->
infinite (
env x).
Global Add Parametric Morphism :
infinite_dom
with signature @
Oeq (
DS_prod SI) ==>
eq ==>
iff
as inf_dom_morph.
Proof.
Couper la tête d'un environnement
Definition REM_env :
DS_prod SI -
C->
DS_prod SI :=
DMAPi (
fun _ =>
REM _).
Lemma REM_env_eq :
forall env i,
REM_env env i =
rem (
env i).
Proof.
reflexivity.
Qed.
Lemma REM_env_bot :
REM_env 0 == 0.
Proof.
Lemma REM_env_inf :
forall env,
all_infinite env ->
all_infinite (
REM_env env).
Proof.
intros *
Hinf x.
rewrite REM_env_eq.
specialize (
Hinf x).
now inversion Hinf.
Qed.
Lemma REM_env_inf_dom :
forall env l,
infinite_dom env l ->
infinite_dom (
REM_env env)
l.
Proof.
intros *
Hinf x Hin.
rewrite REM_env_eq.
specialize (
Hinf x).
now destruct Hinf.
Qed.
Lemma rem_env_eq_compat :
forall X Y,
X ==
Y ->
REM_env X ==
REM_env Y.
Proof.
REM_env itéré
Fixpoint nrem_env (
n :
nat) :
DS_prod SI -
C->
DS_prod SI :=
match n with
|
O =>
ID _
|
S n =>
REM_env @_
nrem_env n
end.
Lemma nrem_env_0 :
forall X,
nrem_env 0
X =
X.
Proof.
reflexivity.
Qed.
Lemma nrem_rem_env :
forall k X,
nrem_env k (
REM_env X) =
REM_env (
nrem_env k X).
Proof.
induction k; auto; intros; simpl.
autorewrite with cpodb.
rewrite IHk; auto.
Qed.
Lemma nrem_env_eq :
forall n (
X:
DS_prod SI)
i,
nrem_env n X i =
nrem n (
X i).
Proof.
Lemma nrem_env_inf :
forall n X,
all_infinite X ->
all_infinite (
nrem_env n X).
Proof.
induction n;
simpl;
intros *
HH;
auto.
apply REM_env_inf,
IHn,
HH.
Qed.
Lemma nrem_env_inf_dom :
forall n (
X:
DS_prod SI)
l,
infinite_dom X l ->
infinite_dom (
nrem_env n X)
l.
Proof.
induction n;
simpl;
intros *
HH;
auto.
apply REM_env_inf_dom,
IHn,
HH.
Qed.
Prendre la tête dans env1, la queue dans env2
Definition APP_env :
DS_prod SI -
C->
DS_prod SI -
C->
DS_prod SI.
apply curry,
Dprodi_DISTR;
intro i.
exact ((
APP _ @2_ (
PROJ _
i @_
FST _ _)) (
PROJ _
i @_
SND _ _)).
Defined.
Lemma APP_env_eq :
forall env1 env2 i,
APP_env env1 env2 i =
app (
env1 i) (
env2 i).
Proof.
reflexivity.
Qed.
Lemma app_rem_env :
forall s,
APP_env s (
REM_env s) ==
s.
Proof.
Lemma rem_app_env :
forall X Y,
all_cons X ->
REM_env (
APP_env X Y) ==
Y.
Proof.
Lemma rem_app_env_le :
forall X Y,
REM_env (
APP_env X Y) <=
Y.
Proof.
Lemma rem_app_app_rem_env :
forall X Y,
REM_env (
APP_env X (
APP_env (
REM_env X)
Y)) ==
APP_env (
REM_env X)
Y.
Proof.
Lemma app_app_env :
forall X Y Z,
APP_env (
APP_env X Y)
Z ==
APP_env X Z.
Proof.
Lemma APP_env_bot :
forall s,
APP_env 0
s == 0.
Proof.
Lemma app_env_cons :
forall X Y,
all_cons X ->
all_cons (
APP_env X Y).
Proof.
Lemma app_env_inf :
forall X Y,
all_cons X ->
all_infinite Y ->
all_infinite (
APP_env X Y).
Proof.
Lemma app_env_inf_dom:
forall X Y l,
infinite_dom X l ->
infinite_dom Y l ->
infinite_dom (
APP_env X Y)
l.
Proof.
Couper les queues
Definition FIRST_env :
DS_prod SI -
C->
DS_prod SI :=
DMAPi (
fun _ =>
FIRST _).
Lemma FIRST_env_eq :
forall X x, (
FIRST_env X)
x =
first (
X x).
Proof.
reflexivity.
Qed.
Lemma first_env_eq_compat :
forall X Y,
X ==
Y ->
FIRST_env X ==
FIRST_env Y.
Proof.
Lemma first_app_env :
forall X Y,
FIRST_env (
APP_env X Y) ==
FIRST_env X.
Proof.
Lemma app_app_first_env :
forall X Y,
APP_env (
FIRST_env X)
Y ==
APP_env X Y.
Proof.
Un prédicat co-inductif pour décrire l'égalité d'environnements.
Plus facile à manipuler dans les preuves mais nécessite souvent
une hypothèse all_infinite X
Section Env_eq.
CoInductive env_eq :
DS_prod SI ->
DS_prod SI ->
Prop :=
|
Ee :
forall X Y,
env_eq (
REM_env X) (
REM_env Y) ->
FIRST_env X ==
FIRST_env Y ->
env_eq X Y.
Lemma Oeq_env_eq :
forall X Y,
X ==
Y ->
env_eq X Y.
Proof.
cofix Cof;
intros.
apply Ee;
auto.
-
apply Cof.
now rewrite H.
-
now rewrite H.
Qed.
Lemma env_eq_Oeq :
forall X Y,
env_eq X Y ->
X ==
Y.
Proof.
intros *
Heq.
apply Oprodi_eq_intro;
intro i.
apply DS_bisimulation_allin1
with (
R :=
fun U V =>
exists X Y,
env_eq X Y
/\
U ==
X i /\
V ==
Y i).
3:
eauto.
{
intros * ?
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
auto. }
clear.
intros U V Hc (
X &
Y &
Heq &
Hu &
Hv).
inversion_clear Heq as [??
He Hf Eq1 Eq2].
split.
-
apply Oprodi_eq_elim with (
i :=
i)
in Hf.
now rewrite Hu,
Hv, <- 2
FIRST_env_eq.
-
exists (
REM_env X), (
REM_env Y);
split;
auto.
now rewrite Hu,
Hv.
Qed.
Lemma env_eq_ok :
forall X Y,
X ==
Y <->
env_eq X Y.
Proof.
Global Add Parametric Morphism :
env_eq
with signature @
Oeq (
DS_prod SI) ==> @
Oeq (
DS_prod SI) ==>
iff
as env_eq_morph.
Proof.
End Env_eq.
Extract a (min(n, length s))-prefix of all streams s
Fixpoint take_env n :
DS_prod SI -
C->
DS_prod SI :=
match n with
|
O =>
CTE _ _ 0
|
S n => (
APP_env @2_
ID _) (
take_env n @_
REM_env)
end.
Lemma take_env_eq :
forall n X,
take_env n X =
match n with
|
O => 0
|
S n =>
APP_env X (
take_env n (
REM_env X))
end.
Proof.
destruct n; reflexivity.
Qed.
Global Opaque take_env.
Lemma take_env_bot :
forall n,
take_env n (0:
DS_prod SI) == 0.
Proof.
Lemma take_env_le :
forall n env,
take_env n env <=
env.
Proof.
Lemma take_env_proj :
forall n X x,
take_env n X x =
take n (
X x).
Proof.
Global Add Parametric Morphism n : (
take_env n)
with signature @
Oeq (
DS_prod SI) ==> @
Oeq (
DS_prod SI)
as take_env_morph.
Proof.
induction n;
intros *
H;
rewrite take_env_eq;
auto.
now rewrite H.
Qed.
Lemma take_env_1 :
forall X,
take_env 1
X =
FIRST_env X.
Proof.
reflexivity.
Qed.
Lemma take_env_Oeq :
forall X Y, (
forall n,
take_env n X ==
take_env n Y) ->
X ==
Y.
Proof.
Lemma take_rem_env :
forall n X,
take_env n (
REM_env X) ==
REM_env (
take_env (
S n)
X).
Proof.
on peut éliminer REM_env (APP_env X Y) s'il est sous un APP_env X
Lemma app_rem_take_env :
forall n X Y,
APP_env X (
take_env n (
REM_env (
APP_env X Y))) ==
APP_env X (
take_env n Y).
Proof.
intros.
apply Oprodi_eq_intro;
intro i.
repeat rewrite ?
APP_env_eq, ?
REM_env_eq, ?
take_env_proj.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
U ==
V
\/
exists X Y,
U ==
app X (
take n (
rem (
app X Y)))
/\
V ==
app X (
take n Y)).
3:
right;
exists (
X i), (
Y i);
auto.
{
intros * ?
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
eauto. }
clear.
intros U V Hc [
Heq | (
X &
Y &
Hu &
Hv)].
{
setoid_rewrite Heq;
auto. }
destruct (@
is_cons_elim _
X)
as (
x &
X' &
Hx).
{
destruct Hc;
eapply app_is_cons; [
rewrite <-
Hu|
rewrite <-
Hv];
auto. }
rewrite Hx,
app_cons,
rem_app in Hu;
auto.
rewrite Hx,
app_cons in Hv.
split.
-
rewrite Hu,
Hv;
auto.
-
setoid_rewrite Hu.
setoid_rewrite Hv.
auto.
Qed.
End ENV.
First definition of zip using three functions
ZIP primitive, combines elements of two streams
Section Zip.
Context {
A B D :
Type}.
Variable bop :
A ->
B ->
D.
Definition zipf : (
DS A -
C->
DS B -
C->
DS D) -
C->
DS A -
C->
DS B -
C->
DS D.
apply curry.
apply curry.
apply (
fcont_comp2 (
DSCASE A D)).
2:
exact (
SND _ _ @_ (
FST _ _)).
apply ford_fcont_shift.
intro a.
apply curry.
apply (
fcont_comp2 (
DSCASE B D)).
2:
exact (
SND _ _ @_ (
FST _ _)).
apply ford_fcont_shift.
intro b.
apply curry.
apply (
fcont_comp (
CONS (
bop a b))).
eapply fcont_comp3.
2:
apply ID.
exact (
FST _ _ @_ (
FST _ _ @_ (
FST _ _ @_ (
FST _ _)))).
exact (
SND _ _ @_ (
FST _ _)).
exact (
SND _ _).
Defined.
Lemma zipf_eq :
forall f u U v V,
zipf f (
cons u U) (
cons v V) =
cons (
bop u v) (
f U V).
Proof.
Definition ZIP : (
DS A -
C->
DS B -
C->
DS D) :=
FIXP _
zipf.
Lemma zip_cons :
forall u U v V,
ZIP (
cons u U) (
cons v V) ==
cons (
bop u v) (
ZIP U V).
Proof.
Hint Rewrite zip_cons :
cpodb.
Lemma zipf_bot1 :
forall f xs,
zipf f 0
xs == 0.
Proof.
intros.
unfold zipf.
now autorewrite with cpodb.
Qed.
Lemma zipf_bot2 :
forall f xs,
zipf f xs 0 == 0.
Proof.
Lemma zipf_is_cons :
forall f xs ys,
is_cons (
zipf f xs ys) ->
is_cons xs /\
is_cons ys.
Proof.
Lemma zip_bot1 :
forall xs,
ZIP 0
xs == 0.
Proof.
Lemma zip_bot2 :
forall xs,
ZIP xs 0 == 0.
Proof.
Lemma zip_is_cons :
forall xs ys,
is_cons (
ZIP xs ys) ->
is_cons xs /\
is_cons ys.
Proof.
Lemma is_cons_zip :
forall xs ys,
is_cons xs /\
is_cons ys ->
is_cons (
ZIP xs ys).
Proof.
Lemma rem_zip :
forall xs ys,
rem (
ZIP xs ys) ==
ZIP (
rem xs) (
rem ys).
Proof.
intros.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists xs ys,
U ==
rem (
ZIP xs ys)
/\
V ==
ZIP (
rem xs) (
rem ys));
eauto 4.
-
intros * (?&?&?&?)
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
eauto.
-
clear.
intros U V Hc (
xs &
ys &
Hu &
Hv).
assert (
is_cons xs /\
is_cons ys)
as [
Cx Cy].
{
destruct Hc as [
Hc|
Hc].
+
rewrite Hu in Hc.
now apply rem_is_cons,
zip_is_cons in Hc.
+
rewrite Hv in Hc.
apply zip_is_cons in Hc as [];
auto using rem_is_cons. }
apply is_cons_elim in Cx as (?&
xs' &
Hx),
Cy as (?&
ys' &
Hy).
rewrite Hx,
Hy in *;
clear Hx Hy.
assert (
is_cons xs' /\
is_cons ys')
as [
Cx Cy].
{
destruct Hc as [
Hc|
Hc].
+
rewrite Hu in Hc.
rewrite zip_cons,
rem_cons in Hc.
now apply zip_is_cons in Hc.
+
rewrite Hv in Hc.
rewrite 2
rem_cons in Hc.
now apply zip_is_cons in Hc. }
apply is_cons_elim in Cx as (?&
xs'' &
Hx),
Cy as (?&
ys'' &
Hy).
rewrite Hx,
Hy,
Hu,
Hv in *.
split;
autorewrite with cpodb;
auto.
exists xs',
ys'.
rewrite Hu,
Hv,
Hx,
Hy;
now autorewrite with cpodb.
Qed.
Lemma nrem_zip :
forall n xs ys,
nrem n (
ZIP xs ys) ==
ZIP (
nrem n xs) (
nrem n ys).
Proof.
induction n;
intros;
auto.
now rewrite 3
nrem_S,
rem_zip,
IHn.
Qed.
Lemma first_zip :
forall xs ys,
first (
ZIP xs ys)
==
ZIP (
first xs) (
first ys).
Proof.
intros.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists xs ys,
U ==
first (
ZIP xs ys)
/\
V ==
ZIP (
first xs) (
first ys));
eauto 4.
-
intros * (?&?&?&?)
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
eauto.
-
clear.
intros U V Hc (
xs &
ys &
Hu &
Hv).
assert (
is_cons xs /\
is_cons ys)
as [
Cx Cy].
{
destruct Hc as [
Hc|
Hc].
+
rewrite Hu in Hc.
now apply first_is_cons,
zip_is_cons in Hc.
+
rewrite Hv in Hc.
apply zip_is_cons in Hc as [];
auto. }
apply is_cons_elim in Cx as (?&
xs' &
Hx),
Cy as (?&
ys' &
Hy).
rewrite Hx,
Hy in *;
clear Hx Hy.
repeat rewrite first_cons,
zip_cons, ?
zip_bot1 in *.
split;
autorewrite with cpodb;
eauto.
exists 0,0.
rewrite Hu,
Hv, 2
first_eq_bot,
rem_cons,
zip_bot1;
auto.
Qed.
Lemma zip_app:
forall (
xs1 xs2 :
DS A) (
ys1 ys2 :
DS B),
app (
ZIP xs1 ys1) (
ZIP xs2 ys2)
==
ZIP (
app xs1 xs2) (
app ys1 ys2).
Proof.
intros.
apply DS_bisimulation_allin1 with
(
R :=
fun U V =>
U ==
V
\/
exists X1 X2 Y1 Y2,
(
U ==
app (
ZIP X1 Y1) (
ZIP X2 Y2)
/\
V ==
ZIP (
app X1 X2) (
app Y1 Y2))).
3:
eauto 12.
{
intros * ?
Eq1 Eq2.
setoid_rewrite <-
Eq1.
now setoid_rewrite <-
Eq2.
}
clear.
intros U V Hc [
HH | (
X1 &
X2 &
Y1 &
Y2 &
Hu &
Hv)].
{
setoid_rewrite HH.
eauto. }
setoid_rewrite Hu.
setoid_rewrite Hv.
destruct (@
is_cons_elim _
X1)
as (
vx1 &
X1' &
Hx1).
{
destruct Hc.
-
eapply proj1,
zip_is_cons,
app_is_cons.
now rewrite <-
Hu.
-
eapply app_is_cons,
proj1,
zip_is_cons.
now rewrite <-
Hv. }
destruct (@
is_cons_elim _
Y1)
as (
vy1 &
Y1' &
Hy1).
{
destruct Hc.
-
eapply proj2,
zip_is_cons,
app_is_cons.
now rewrite <-
Hu.
-
eapply app_is_cons,
proj2,
zip_is_cons.
now rewrite <-
Hv. }
setoid_rewrite Hx1.
setoid_rewrite Hy1.
rewrite zip_cons, 3
app_cons,
zip_cons,
first_cons.
auto.
Qed.
Lemma zip_uncons :
forall xs ys r rs,
ZIP xs ys ==
cons r rs ->
exists x xs' y ys',
xs ==
cons x xs'
/\
ys ==
cons y ys'
/\
rs ==
ZIP xs' ys'
/\
r =
bop x y.
Proof.
Lemma zip_inf :
forall U V,
infinite U ->
infinite V ->
infinite (
ZIP U V).
Proof.
clear.
intros *
InfU InfV.
remember (
ZIP U V)
as t eqn:
Ht.
apply Oeq_refl_eq in Ht.
revert InfU InfV Ht.
revert t U V.
cofix Cof;
intros.
destruct InfU as [
Cu],
InfV as [
Cv].
apply is_cons_elim in Cu as (?&
U' &
Hu),
Cv as (?&
V' &
Hv).
rewrite Hu,
Hv,
rem_cons,
zip_cons in *.
constructor.
-
now rewrite Ht.
-
eapply Cof with (
U :=
U') (
V :=
V');
auto.
now rewrite Ht,
rem_cons.
Qed.
Lemma inf_zip :
forall s t,
infinite (
ZIP s t) ->
infinite s /\
infinite t.
Proof.
Lemma zip_const :
forall a V,
ZIP (
DS_const a)
V ==
MAP (
bop a)
V.
Proof.
intros.
eapply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists xs,
U ==
ZIP (
DS_const a)
xs
/\
V ==
MAP (
bop a)
xs).
3:
eauto.
-
intros ????(?&?&?&?)??.
repeat esplit;
eauto.
-
clear.
intros U V Hc (
xs &
Hu &
Hv).
assert (
is_cons xs)
as Hcx.
{
rewrite Hu,
Hv in Hc.
destruct Hc as [
Hc|
Hc].
+
apply zip_is_cons in Hc;
tauto.
+
apply map_is_cons in Hc;
tauto. }
apply is_cons_elim in Hcx as (
vx &
xs' &
Hx).
rewrite Hx in Hu,
Hv.
rewrite MAP_map,
map_eq_cons in Hv.
rewrite DS_const_eq,
zip_cons in Hu.
setoid_rewrite Hu.
setoid_rewrite Hv.
split.
+
autorewrite with cpodb;
auto.
+
exists xs'.
rewrite 2
rem_cons;
auto.
Qed.
Lemma zip_const2 :
forall a U,
ZIP U (
DS_const a) ==
MAP (
fun u =>
bop u a)
U.
Proof.
intros.
eapply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists xs,
U ==
ZIP xs (
DS_const a)
/\
V ==
MAP (
fun u =>
bop u a)
xs).
3:
eauto.
-
intros ????(?&?&?&?)??.
repeat esplit;
eauto.
-
clear.
intros U V Hc (
xs &
Hu &
Hv).
assert (
is_cons xs)
as Hcx.
{
rewrite Hu,
Hv in Hc.
destruct Hc as [
Hc|
Hc].
+
apply zip_is_cons in Hc;
tauto.
+
apply map_is_cons in Hc;
tauto. }
apply is_cons_elim in Hcx as (
vx &
xs' &
Hx).
rewrite Hx in Hu,
Hv.
rewrite MAP_map,
map_eq_cons in Hv.
rewrite DS_const_eq,
zip_cons in Hu.
setoid_rewrite Hu.
setoid_rewrite Hv.
split.
+
autorewrite with cpodb;
auto.
+
exists xs'.
rewrite 2
rem_cons;
auto.
Qed.
Lemma take_zip :
forall n xs ys,
take n (
ZIP xs ys) ==
ZIP (
take n xs) (
take n ys).
Proof.
Lemma zip_take_const :
forall n xs c,
ZIP (
take n xs) (
DS_const c) ==
ZIP (
take n xs) (
take n (
DS_const c)).
Proof.
Lemma is_ncons_zip :
forall n xs ys,
is_ncons n xs ->
is_ncons n ys ->
is_ncons n (
ZIP xs ys).
Proof.
End Zip.
Global Hint Rewrite @
zip_cons @
zip_bot1 @
zip_bot2 :
cpodb.
Lemma zip_ext :
forall A B C (
f g :
A ->
B ->
C),
(
forall a b,
f a b =
g a b) ->
forall x y,
ZIP f x y ==
ZIP g x y.
Proof.
intros *
Hfg x y.
apply DS_bisimulation_allin1
with (
R :=
fun U V =>
exists x y,
U ==
ZIP f x y /\
V ==
ZIP g x y);
eauto 4.
{
intros * ?
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
auto. }
clear -
Hfg;
intros U V Hc (
xs &
ys &
Hu &
Hv).
destruct (@
is_cons_elim _
xs)
as (
x &
xs' &
Hxs).
{
rewrite Hu,
Hv in Hc.
now destruct Hc as [?%
zip_is_cons|?%
zip_is_cons]. }
destruct (@
is_cons_elim _
ys)
as (
y &
ys' &
Hys).
{
rewrite Hu,
Hv in Hc.
now destruct Hc as [?%
zip_is_cons|?%
zip_is_cons]. }
rewrite Hxs,
Hys,
zip_cons in *.
split;[|
exists xs',
ys'];
now rewrite Hu,
Hv, ?
first_cons, ?
rem_cons, ?
Hfg.
Qed.
Facts about zip, map
Lemma zip_map :
forall A B C (
op :
A ->
B ->
C)
B' (
f :
B' ->
B),
forall xs ys,
ZIP op xs (
map f ys) ==
ZIP (
fun x y =>
op x (
f y))
xs ys.
Proof.
intros.
eapply DS_bisimulation with
(
R :=
fun U V =>
exists xs ys,
U ==
ZIP op xs (
map f ys)
/\
V ==
ZIP (
fun x y =>
op x (
f y))
xs ys).
4:
eauto.
-
intros ????(?&?&?&?)??.
repeat esplit;
eauto.
-
clear xs ys.
intros x y Hcons (
xs &
ys &
Hx &
Hy).
destruct Hcons as [
Hcons|
Hcons];
rewrite Hx,
Hy in *;
apply zip_is_cons in Hcons as (
Hc1 &
Hc2);
try apply map_is_cons in Hc2;
apply is_cons_elim in Hc1 as (?&?&->);
apply is_cons_elim in Hc2 as (?&?&->);
now autorewrite with cpodb.
-
clear xs ys.
intros x y Hcons (
xs &
ys &
Hx &
Hy).
destruct Hcons as [
Hcons|
Hcons];
exists (
rem xs), (
rem ys);
rewrite Hx,
Hy in *;
apply zip_is_cons in Hcons as (
Hc1 &
Hc2);
try apply map_is_cons in Hc2;
apply is_cons_elim in Hc1 as (?&?&->);
apply is_cons_elim in Hc2 as (?&?&->);
now autorewrite with cpodb.
Qed.
Lemma map_zip :
forall A B C D (
op :
A ->
B ->
C) (
f :
C ->
D),
forall xs ys,
ZIP (
fun x y =>
f (
op x y))
xs ys ==
map f (
ZIP op xs ys).
Proof.
intros.
eapply DS_bisimulation with
(
R :=
fun U V =>
exists xs ys,
U ==
ZIP (
fun x y =>
f (
op x y))
xs ys
/\
V ==
map f (
ZIP op xs ys)).
4:
eauto.
-
intros ????(?&?&?&?)??.
repeat esplit;
eauto.
-
clear xs ys.
intros x y Hcons (
xs &
ys &
Hx &
Hy).
destruct Hcons as [
Hcons|
Hcons];
rewrite Hx,
Hy in *;
[|
apply map_is_cons in Hcons];
apply zip_is_cons in Hcons as (
Hc1 &
Hc2);
apply is_cons_elim in Hc1 as (?&?&->);
apply is_cons_elim in Hc2 as (?&?&->);
now autorewrite with cpodb.
-
clear xs ys.
intros x y Hcons (
xs &
ys &
Hx &
Hy).
destruct Hcons as [
Hcons|
Hcons];
exists (
rem xs), (
rem ys);
rewrite Hx,
Hy in *;
[|
apply map_is_cons in Hcons];
apply zip_is_cons in Hcons as (
Hc1 &
Hc2);
apply is_cons_elim in Hc1 as (?&?&->);
apply is_cons_elim in Hc2 as (?&?&->);
now autorewrite with cpodb.
Qed.
Lemma zip_comm :
forall A B (
f :
A ->
A ->
B)
xs ys,
(
forall x y,
f x y =
f y x) ->
ZIP f xs ys ==
ZIP f ys xs.
Proof.
intros *
Fcomm.
eapply DS_bisimulation_allin1 with
(
R :=
fun U V =>
exists xs ys,
U ==
ZIP f xs ys
/\
V ==
ZIP f ys xs);
eauto 4.
-
intros * (?&?&?&?)
Eq1 Eq2.
setoid_rewrite <-
Eq1.
setoid_rewrite <-
Eq2.
eauto.
-
clear -
Fcomm.
intros U V Hc (
xs &
ys &
Hu &
Hv).
assert (
is_cons xs /\
is_cons ys)
as [
Hcx Hcy].
{
rewrite Hu,
Hv in Hc.
destruct Hc as [
Hc|
Hc];
apply zip_is_cons in Hc;
tauto. }
apply is_cons_elim in Hcx as (
vx &
xs' &
Hx).
apply is_cons_elim in Hcy as (
vy &
ys' &
Hy).
rewrite Hx,
Hy,
zip_cons in *.
setoid_rewrite Hu.
setoid_rewrite Hv.
split.
+
autorewrite with cpodb;
auto.
+
exists xs',
ys'.
rewrite 2
rem_cons;
auto.
Qed.
Lemma zip_zip :
forall D1 D2 D3 D4 D5,
forall (
f:
D1->
D4->
D5) (
g:
D2->
D3->
D4)
U V W,
ZIP f U (
ZIP g V W) ==
ZIP (
fun h w =>
h w) (
ZIP (
fun x y =>
fun z => (
f x (
g y z)))
U V)
W.
Proof.
intros.
apply DS_bisimulation_allin1 with
(
R :=
fun R L =>
exists U V W,
R ==
ZIP f U (
ZIP g V W)
/\
L ==
ZIP (
fun h w =>
h w) (
ZIP (
fun x y z =>
f x (
g y z))
U V)
W).
3:
eauto.
-
intros ????(?&?&?&?)
E1 E2.
setoid_rewrite <-
E1.
setoid_rewrite <-
E2.
eauto.
-
clear.
intros R L Hc (
U &
V &
W &
Hr &
Hl).
destruct Hc as [
Hc |
Hc].
+
apply is_cons_elim in Hc as (
r &
rs &
Hrs).
rewrite Hrs in *.
apply symmetry,
zip_uncons in Hr as (?&?&?&?&
Hu &
Hz &?&?).
apply zip_uncons in Hz as (?&?&?&?&
Hv &
Hw &?&?).
rewrite Hu,
Hv,
Hw, 2
zip_cons in *;
subst.
setoid_rewrite Hl.
setoid_rewrite Hrs.
rewrite 2 (
rem_cons (
f x _)).
split.
autorewrite with cpodb;
auto.
eauto 7.
+
apply is_cons_elim in Hc as (
l &
ls &
Hls).
rewrite Hls in *.
apply symmetry,
zip_uncons in Hl as (?&?&?&?&
Hz &
Hw &?&?).
apply zip_uncons in Hz as (?&?&?&?&
Hu &
Hv &?&?).
rewrite Hu,
Hv,
Hw, 2
zip_cons in *;
subst.
setoid_rewrite Hls.
setoid_rewrite Hr.
rewrite 2 (
rem_cons (
f _ _)).
split.
autorewrite with cpodb;
auto.
eauto 7.
Qed.
ZIP3 synchronizes three streams
Section Zip3.
Context {
A B C D :
Type}.
Variable op :
A ->
B ->
C ->
D.
Definition ZIP3 :
DS A -
C->
DS B -
C->
DS C -
C->
DS D :=
curry (
ZIP (
fun f x =>
f x) @_
uncurry (
ZIP (
fun x y =>
op x y))).
Lemma zip3_eq :
forall xs ys zs,
ZIP3 xs ys zs =
ZIP (
fun f x =>
f x) (
ZIP (
fun x y =>
op x y)
xs ys)
zs.
Proof.
reflexivity.
Qed.
Lemma zip3_cons :
forall u U v V w W,
ZIP3 (
cons u U) (
cons v V) (
cons w W)
==
cons (
op u v w) (
ZIP3 U V W).
Proof.
Lemma rem_zip3 :
forall xs ys zs,
rem (
ZIP3 xs ys zs) ==
ZIP3 (
rem xs) (
rem ys) (
rem zs).
Proof.
Lemma first_zip3 :
forall xs ys zs,
first (
ZIP3 xs ys zs)
==
ZIP3 (
first xs) (
first ys) (
first zs).
Proof.
Lemma zip3_is_cons :
forall xs ys zs,
is_cons (
ZIP3 xs ys zs) ->
is_cons xs /\
is_cons ys /\
is_cons zs.
Proof.
Lemma is_cons_zip3 :
forall xs ys zs,
is_cons xs /\
is_cons ys /\
is_cons zs ->
is_cons (
ZIP3 xs ys zs).
Proof.
Lemma zip3_bot1 :
forall ys zs,
ZIP3 0
ys zs == 0.
Proof.
Lemma take_zip3 :
forall n xs ys zs,
take n (
ZIP3 xs ys zs) ==
ZIP3 (
take n xs) (
take n ys) (
take n zs).
Proof.
End Zip3.
Une ancienne version de take, avec prédicat d'infinité
Module Inf_Take.
Take the prefix of length n from an infinite stream
Fixpoint take {
A :
Type} (
n :
nat) (
s :
DS A) (
si :
infinite s) :
DS A :=
match n with
|
O => 0
|
S n =>
match si with
inf_intro _
rsi =>
app s (
take n (
rem s)
rsi)
end
end.
Lemma take_1 {
A :
Type} :
forall (
s :
DS A) (
si :
infinite s),
take 1
s si ==
first s.
Proof.
Lemma take_le {
A :
Type} :
forall n (
s :
DS A) (
si :
infinite s),
take n s si <=
take (
S n)
s si.
Proof.
Lemma _take_eq {
A :
Type} :
forall n (
xs :
DS A)
xsi ys ysi,
xs ==
ys ->
take n xs xsi ==
take n ys ysi.
Proof.
induction n; simpl; intros * Heq; auto.
destruct xsi, ysi.
rewrite Heq, IHn at 1; auto.
Qed.
Lemma take_eq {
A :
Type} :
forall n (
xs :
DS A)
xsi ys,
xs ==
ys ->
exists ysi,
take n xs xsi ==
take n ys ysi.
Proof.
Lemma take_cons {
A :
Type} :
forall n x (
xs :
DS A)
xsi,
take (
S n) (
cons x xs)
xsi ==
cons x (
take n xs (
cons_infinite _ _ _
xsi)).
Proof.
Lemma take_app {
A :
Type} :
forall n (
xs ys :
DS A)
inf inf2,
take (
S n) (
app xs ys)
inf ==
app xs (
take n ys inf2).
Proof.
Lemma rem_take {
A :
Type} :
forall n (
xs :
DS A)
inf inf2,
rem (
take (
S n)
xs inf) ==
take n (
rem xs)
inf2.
Proof.
Lemma n_eq {
A :
Type} :
forall (
s t :
DS A) (
si :
infinite s) (
ti :
infinite t),
(
forall n,
take n s si ==
take n t ti) ->
s ==
t.
Proof.
intros *
Hn.
eapply DS_bisimulation_allin1
with (
R :=
fun U V =>
exists Ui Vi, (
forall n,
take n U Ui ==
take n V Vi)).
3:
esplit;
eauto.
-
intros ???? (
I1 &
I2 &
HUV)
HU HV.
setoid_rewrite (
_take_eq _ _ _ _ (
proj1 (
infinite_morph HU)
I1)
HU)
in HUV.
setoid_rewrite (
_take_eq _ _ _ _ (
proj1 (
infinite_morph HV)
I2)
HV)
in HUV.
eauto.
-
clear.
intros U V Hc (
I1 &
I2 &
Hf).
split.
+
specialize (
Hf 1).
now rewrite 2
take_1 in Hf.
+
destruct I1 as (?&
I1),
I2 as (? &
I2).
exists I1,
I2.
setoid_rewrite <-
rem_take;
auto.
Qed.
End Inf_Take.
Extract the n first elements (Con/Eps) of a stream
Fixpoint take_list {
A} (
n :
nat) (
xs :
DS A) :
list (
option A) :=
match n with
|
O => []
|
S n =>
match xs with
|
Eps xs =>
None ::
take_list n xs
|
Con x xs =>
Some x ::
take_list n xs
end
end.