# Library Cpo_streams_type

``` Require List. Require Export Cpo. Set Implicit Arguments. ```

# Cpo_streams_type.v: Domain of possibly infinite streams on a type

``` CoInductive DStr (D:Type) : Type     := Eps : DStr D -> DStr D | Con : D -> DStr D -> DStr D. Lemma DS_inv : forall (D:Type) (d:DStr D),    d = match d with Eps x => Eps x | Con a s => Con a s end. destruct d; auto. Save. Hint Resolve DS_inv. ```
• Extraction of a finite list from the n first constructors of a stream
``` Fixpoint DS_to_list (D:Type)(d:DStr D) (n : nat) {struct n}: List.list D :=  match n with O => List.nil                  | S p => match d with Eps d' => DS_to_list d' p                                                  | Con a d' => List.cons a (DS_to_list d' p)                                end  end. ```

## Removing Eps steps

``` Definition pred (D:Type) d : DStr D := match d with Eps x => x | Con _ _ => d end. Inductive isCon (D:Type) : DStr D -> Prop :=             isConEps : forall x, isCon x -> isCon (Eps x)           | isConCon : forall a s, isCon (Con a s). Hint Constructors isCon. Lemma isCon_pred : forall D (x:DStr D), isCon x -> isCon (pred x). destruct 1; simpl; auto. Save. Hint Resolve isCon_pred. Definition isEps (D:Type) (x:DStr D) := match x with Eps _ => True | _ => False end. ```
Less general than isCon_pred but the result is a subterm of the argument (isCon x), used in uncons
``` Lemma isConEps_inv : forall D (x:DStr D), isCon x -> isEps x -> isCon (pred x). destruct 1; simpl; intros. assumption. case H. Defined. Lemma isCon_intro : forall D (x:DStr D), isCon (pred x) -> isCon x. destruct x; auto. Save. Hint Resolve isCon_intro. Fixpoint pred_nth D (x:DStr D) (n:nat) {struct n} : DStr D :=              match n with 0 => x                               | S m => pred_nth (pred x) m              end. Lemma pred_nth_switch : forall D k (x:DStr D), pred_nth (pred x) k = pred (pred_nth x k). induction k; intros; simpl; auto. Save. Hint Resolve pred_nth_switch . Lemma pred_nthS : forall D k (x:DStr D), pred_nth x (S k) = pred (pred_nth x k). exact pred_nth_switch. Save. Hint Resolve pred_nthS. Lemma pred_nthCon : forall D a (s:DStr D) n, pred_nth (Con a s) n = (Con a s). induction n; simpl; auto. Save. Hint Resolve pred_nthCon. Definition decomp D (a:D) (s x:DStr D) : Prop := exists k, pred_nth x k = Con a s. Hint Unfold decomp. Lemma decomp_isCon : forall D a (s x:DStr D), decomp a s x -> isCon x. intros D a s x Hd; case Hd; intro k; generalize x; induction k; simpl; intros; auto. subst x0; auto. Save. Lemma decompCon : forall D a (s:DStr D), decomp a s (Con a s). exists (0%nat); auto. Save. Hint Resolve decompCon. Lemma decompCon_eq :     forall D a b (s t:DStr D), decomp a s (Con b t) -> Con a s = Con b t. destruct 1. transitivity (pred_nth (Con b t) x); auto. Save. Hint Immediate decompCon_eq. Lemma decompEps : forall D a (s x:DStr D), decomp a s x -> decomp a s (Eps x). destruct 1. exists (S x0); auto. Save. Hint Resolve decompEps. Lemma decompEps_pred : forall D a (s x:DStr D), decomp a s x -> decomp a s (pred x). destruct 1; intros. exists x0; auto. transitivity (pred (pred_nth x x0)); auto. rewrite H; auto. Save. Lemma decompEps_pred_sym : forall D a (s x:DStr D), decomp a s (pred x) -> decomp a s x. destruct x; simpl; intros; auto. Save. Hint Immediate decompEps_pred_sym decompEps_pred. Lemma decomp_ind : forall D a (s:DStr D) (P : DStr D-> Prop),    (forall x, P x -> decomp a s x -> P (Eps x))  -> P (Con a s) -> forall x, decomp a s x -> P x. intros D a s P HE HC x H; case H; intro n; generalize x H; clear x H. induction n; simpl; intros. subst; auto. destruct x. assert (decomp a s x); auto. exact (decompEps_pred H). simpl in H0; rewrite pred_nthCon in H0. injection H0; intros; subst; auto. Save. Lemma DStr_match : forall D (x:DStr D), {a:D & {s:DStr D | x = Con a s}}+{isEps x}. intros D x; case x; simpl; auto; intros a s. left; exists a; exists s; trivial. Defined. Lemma uncons : forall D (x:DStr D), isCon x ->{a:D & {s:DStr D| decomp a s x}}. intro D; fix 2; intros x ic. case (DStr_match x); intros. case s; clear s; intros a (s, eqx); exists a; exists s; subst x; auto. case (uncons (pred x) (isConEps_inv ic i)); intros a (s,dx). exists a; exists s; auto. Defined. ```

## Definition of the order

``` CoInductive DSle (D:Type) : DStr D -> DStr D -> Prop :=                    DSleEps : forall x y, DSle x y -> DSle (Eps x) y                 | DSleCon : forall a s t y, decomp a t y -> DSle s t -> DSle (Con a s) y. Hint Constructors DSle. ```

## Properties of the order

``` Lemma DSle_pred_eq : forall D (x y:DStr D), forall n, x=pred_nth y n -> DSle x y. intro D; cofix; intros x y n. case x; intros. apply DSleEps; apply (DSle_pred_eq d y (S n)). replace (pred_nth y (S n)) with (pred (pred_nth y n)). rewrite <- H; trivial. rewrite <- pred_nth_switch; auto. apply DSleCon with d0. exists n; auto. auto. apply (DSle_pred_eq d0 d0 (0%nat)); auto. Save. Lemma DSle_refl : forall D (x:DStr D), DSle x x. intros; apply (DSle_pred_eq (x:=x) x 0); auto. Save. Hint Resolve DSle_refl. Lemma DSle_pred_right : forall D (x y:DStr D), DSle x y -> DSle x (pred y). intro D; cofix; intros x y H1; case H1; intros. apply DSleEps. apply DSle_pred_right; assumption. apply DSleCon with t; auto. Save. Lemma DSleEps_right_elim : forall D (x y:DStr D), DSle x (Eps y) -> DSle x y. intros D x y H; exact (DSle_pred_right H). Save. Lemma DSle_pred_right_elim : forall D (x y:DStr D), DSle x (pred y) -> DSle x y. cofix; destruct x; simpl; intros. apply DSleEps. apply DSle_pred_right_elim; inversion H; assumption. inversion H. apply DSleCon with t; auto. Save. Lemma DSle_pred_left : forall D (x y:DStr D), DSle x y -> DSle (pred x) y. destruct 1; simpl; intros; trivial. apply DSleCon with t; auto. Save. Hint Resolve DSle_pred_left DSle_pred_right. Lemma DSle_pred : forall D (x y:DStr D), DSle x y -> DSle (pred x) (pred y). auto. Save. Hint Resolve DSle_pred. Lemma DSle_pred_left_elim : forall D (x y:DStr D), DSle (pred x) y -> DSle x y. intro D; cofix; destruct x; simpl; intros; try assumption. apply DSleEps; trivial. Save. Lemma DSle_decomp : forall D a (s x y:DStr D),    decomp a s x -> DSle x y -> exists t, decomp a t y /\ DSle s t. intros D a s x y Hdx; case Hdx; intros k; generalize x; induction k; simpl; intros; auto. simpl in H; rewrite H in H0; inversion H0. exists t; auto. case (IHk (pred x0)); auto. intros t (Hd,Hle). exists t; auto. Save. Lemma DSle_trans : forall D (x y z:DStr D), DSle x y -> DSle y z -> DSle x z. intro D; cofix; intros x y z H1; case H1; intros. apply DSleEps. apply DSle_trans with y0; assumption. case (DSle_decomp H H2); intros u (He,Ht). apply DSleCon with u; try assumption. apply DSle_trans with t; trivial. Save. ```

### Defintion of the ordered set

``` Definition DS_ord (D:Type) : ord := mk_ord (DSle_refl (D:=D)) (DSle_trans (D:=D)). ```

### more Properties

``` Lemma DSleEps_right : forall (D:Type) (x y : DS_ord D), x <= y -> x <= Eps y. intros; apply (DSle_pred_right_elim (x:=x) (Eps y)); auto. Save. Hint Resolve DSleEps_right. Lemma DSleEps_left : forall D (x y : DS_ord D), x <= y -> (Eps x:DS_ord D) <= y. intros; apply (DSle_pred_left_elim (Eps x) (y:=y)); auto. Save. Hint Resolve DSleEps_left. Lemma DSeq_pred : forall D (x:DS_ord D), x == pred x. intros; apply Ole_antisym. apply (DSle_pred_right (x:=x) (y:=x)); auto. apply (DSle_pred_left (x:=x) (y:=x)); auto. Save. Hint Resolve DSeq_pred. Lemma pred_nth_eq : forall D n (x:DS_ord D), x == pred_nth x n. induction n; simpl; intros; auto. apply Oeq_trans with (pred x); auto. Save. Hint Resolve pred_nth_eq. Lemma DSleCon0 :      forall D a (s t:DS_ord D), s <= t -> (Con a s:DS_ord D) <= Con a t. intros. apply (DSleCon (a:=a) (s:=s) (t:=t) (y:=Con a t)); auto. Save. Hint Resolve DSleCon0. Lemma Con_compat :  forall D a (s t:DS_ord D), s == t -> (Con a s:DS_ord D) == Con a t. intros; apply Ole_antisym; auto. Save. Hint Resolve Con_compat. Lemma DSleCon_hd : forall (D:Type) a b (s t:DS_ord D),      (Con a s:DS_ord D) <= Con b t-> a = b. intros D a b s t H; inversion H. assert (Con a t0=Con b t); auto. injection H5; intros; subst; auto. Save. Lemma Con_hd_simpl : forall D a b (s t : DS_ord D), (Con a s:DS_ord D) == Con b t-> a = b. intros; apply DSleCon_hd with s t; auto. Save. Lemma DSleCon_tl : forall D a b (s t:DS_ord D), (Con a s:DS_ord D) <= Con b t -> (s:DS_ord D) <= t. intros D a b s t H; inversion H. assert (Con a t0=Con b t); auto. injection H5; intros; subst; auto. Save. Lemma Con_tl_simpl : forall D a b (s t:DS_ord D), (Con a s:DS_ord D) == Con b t -> (s:DS_ord D) == t. intros; apply Ole_antisym. apply DSleCon_tl with a b; auto. apply DSleCon_tl with b a; auto. Save. Lemma eqEps : forall D (x:DS_ord D), x == Eps x. intros; apply Ole_antisym; auto. Save. Hint Resolve eqEps. Lemma decomp_eqCon : forall D a s (x:DS_ord D), decomp a s x -> x == Con a s. intros D a s x Hdx; case Hdx; intro k; generalize x; induction k; auto. intros; apply Oeq_trans with (pred x0); auto. Save. Hint Immediate decomp_eqCon. Lemma decomp_DSleCon : forall D a s (x:DS_ord D), decomp a s x -> x <= Con a s. intros; case (decomp_eqCon H); auto. Save. Lemma decomp_DSleCon_sym :    forall D a s (x:DS_ord D), decomp a s x -> (Con a s:DS_ord D)<=x. intros; case (decomp_eqCon H); auto. Save. Hint Immediate decomp_DSleCon decomp_DSleCon_sym. Lemma DSleCon_exists_decomp :       forall D (x:DS_ord D) a (s:DS_ord D), (Con a s:DS_ord D) <= x                    -> exists b, exists t, decomp b t x /\ a = b /\ s <= t. intros D x a s H; inversion H; eauto. Save. Lemma Con_exists_decompDSle :       forall D (x:DS_ord D) a (s:DS_ord D),       (exists t, decomp a t x /\ s <= t) -> (Con a s:DS_ord D) <= x. intros D x a s (t,(H,H1)). simpl; apply DSleCon with t; auto. Save. Hint Immediate DSleCon_exists_decomp Con_exists_decompDSle. Lemma DSle_isCon : forall D a (s x : DS_ord D), (Con a s : DS_ord D) <= x -> isCon x. intros D a s x H; case (DSleCon_exists_decomp H); intros b (t,(H1,(H2,H3))); auto. apply (decomp_isCon H1). Save. Lemma DSle_uncons :    forall D (x:DS_ord D) a (s:DS_ord D), (Con a s:DS_ord D) <= x                    -> { t : DS_ord D | decomp a t x /\ s <= t}. intros; case (@uncons D x); auto. apply (DSle_isCon H). intros b (t,Hd). exists t. assert ((Con a s : DS_ord D) <= Con b t). apply Ole_trans with x; auto. split; auto. assert (a=b). apply DSleCon_hd with s t; trivial. rewrite H1; auto. apply DSleCon_tl with a b; trivial. Defined. Lemma DSle_rec : forall D (R : DStr D -> DStr D -> Prop),    (forall x y, R (Eps x) y -> R x y) ->    (forall a s y, R (Con a s) y -> exists t, decomp a t y /\ R s t)    -> forall x y : DS_ord D, R x y -> x <= y. intros D R REps RCon; cofix; destruct x; intros. simpl; apply DSleEps; apply DSle_rec; auto. case (RCon d x y H); intros u (H1,H2); simpl; apply DSleCon with u; try assumption. apply DSle_rec; assumption. Save. Lemma isEps_Eps : forall D (x:DS_ord D), isEps (Eps x). repeat red; auto. Save. Lemma not_isEpsCon : forall D a (s:DS_ord D), ~ isEps (Con a s). repeat red; auto. Save. Hint Resolve isEps_Eps not_isEpsCon. Lemma isCon_le : forall D (x y : DS_ord D), isCon x -> x <= y -> isCon y. intros D x y H; generalize y; induction H; intros. inversion_clear H0; auto. inversion_clear H; auto. apply decomp_isCon with a t; trivial. Save. Lemma decomp_eq : forall D a (s x:DS_ord D),      x == Con a s -> exists t, decomp a t x /\ s==t. intros; assert ((Con a s :DS_ord D) <= x); auto. inversion_clear H0. exists t. assert ((Con a t :DS_ord D) <= Con a s). apply Ole_trans with x; auto. split; auto. split; auto. apply (DSleCon_tl H0); auto. Save. Lemma DSle_rec_eq : 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 a s (y:DS_ord D), R (Con a s) y -> exists t, y==Con a t /\ R s t)    -> forall x y : DS_ord D, R x y -> x <= y. intros D R Req RCon; cofix; destruct x; intros. simpl; apply DSleEps; apply DSle_rec_eq. apply Req with (Eps x) y; auto. case (RCon d x y H); intros u (H1,H2). case (decomp_eq H1); intros u' (H4,H5). simpl; apply DSleCon with u'; try assumption. apply DSle_rec_eq. apply Req with x u; auto. Save. Lemma DSeq_rec : 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 a s (y:DS_ord D), R (Con a s) y -> exists t, y==Con a t /\ R s t)->    (forall a s (x:DS_ord D), R x (Con a s) -> exists t, x==Con a t /\ R t s)   -> forall x y : DS_ord D, R x y -> x == y. intros; apply Ole_antisym. apply DSle_rec_eq with R; auto; intros. apply DSle_rec_eq with (R:=fun x y => R y x); intros; trivial. apply H with y1 x1; auto. case (H1 a s y0 H3); intros t (H4,H5); exists t; auto. Save. ```

## Bottom is given by an infinite chain of Eps

``` CoFixpoint DS_bot (D:Type) : DS_ord D := Eps (DS_bot D). Lemma DS_bot_eq (D:Type) : DS_bot D = Eps (DS_bot D). intro D; transitivity match DS_bot D with Eps x => Eps x | Con a s => Con a s end; auto. apply (DS_inv (DS_bot D)). Save. Lemma DS_bot_least : forall D (x:DS_ord D), DS_bot D <= x. intro D; cofix; intro x. rewrite DS_bot_eq; destruct x. simpl; apply DSleEps; apply DS_bot_least. simpl; apply DSleEps; apply DS_bot_least. Save. Hint Resolve DS_bot_least. ```

## Construction of least upper bounds

``` Lemma chain_tl : forall D (c:natO-m> DS_ord D), isCon (c O) -> natO -m> DS_ord D. intros D c H. assert (H':forall n, isCon (c n)). intros; apply isCon_le with (c O); auto with arith. exists (fun n => let (b,r) := uncons (H' n) in let (t,_) := r in t). intros n m H1; case (uncons (H' n)); intros b (t,hn); case (uncons (H' m)); intros d (u,hm). assert ((Con b t : DS_ord D)<=Con d u). apply Ole_trans with (c n); auto. apply Ole_trans with (c m); auto. apply (DSleCon_tl H0). Defined. Lemma chain_uncons :    forall D (c:natO -m> DS_ord D), isCon (c O) ->       {hd:D & {ctl : natO -m> DS_ord D | forall n, c n == Con hd (ctl n)}}. intros D c H; case (uncons H); intros hd (tl,H1); exists hd; exists (chain_tl c H); intros. unfold chain_tl; simpl. case (uncons (isCon_le H (fmon_le_compat c (le_O_n n)))); intros. case s; clear s; intros t H2; auto. apply Oeq_trans with (Con x t); auto. assert ((Con hd tl : DS_ord D) <= Con x t). apply Ole_trans with (c O); auto. apply Ole_trans with (c n); auto with arith. assert (hd=x). apply DSleCon_hd with tl t; trivial. rewrite H3; apply Con_compat; auto. Defined. Lemma fCon : forall D (c:natO -m> DS_ord D) (n:nat),             {hd: D &             {tlc:natO -m> DS_ord D|                  exists m, m < n /\ forall k, c (k+m) == Con hd (tlc k)}}             + {forall k, k<n -> isEps (c k)}. induction n. right; intros; absurd (k<0); omega. case IHn; clear IHn; intro. case s; clear s; intros hdc (tlc,H). left; exists hdc; exists tlc; case H; intro m; exists m; intuition. case (DStr_match (c n)); intros. case s; clear s; intros a (s,H); left. assert (isCon (mseq_lift_left c n O)). unfold mseq_lift_left; simpl. replace (n+0) with n; auto with arith; rewrite H; auto. case (chain_uncons (mseq_lift_left c n) H0); intros hdc (tlc, H1). exists hdc; exists tlc; exists n; auto; intuition. unfold mseq_lift_left in H1; simpl in H1. replace (k+n) with (n+k); auto with arith. right; intros. assert (H0:(k<n \/ k=n)%nat); try omega. case H0; intro; subst; auto with arith. Defined. ```

## Lubs on streams

``` Definition cpred D (c:natO -m> DS_ord D) : natO -m> DS_ord D. intros D c; exists (fun n => pred (c n)). intros n m H; simpl; apply DSle_pred; auto. apply (fmonotonic c H). Defined. CoFixpoint DS_lubn D (c:natO -m> DS_ord D) (n:nat) : DS_ord D :=     match fCon c n with       inleft (existS hd (exist tlc _)) => Con hd (DS_lubn tlc 1)    | inright _ => Eps (DS_lubn (cpred c) (S n))     end. Definition DS_lub (D:Type) (c:natO -m> DS_ord D) := DS_lubn c 1. Lemma DS_lubn_inv : forall D (c:natO -m> DS_ord D) (n:nat), DS_lubn c n =      match fCon c n with         inleft (existS hd (exist tlc _)) => Con hd (DS_lub tlc)      | inright _ => Eps (DS_lubn (cpred c) (S n))     end. intros; rewrite (DS_inv (DS_lubn c n)). simpl; case (fCon c n); trivial. destruct s; simpl. destruct s; trivial. Save. Lemma DS_lubn_pred_nth : forall D a (s:DS_ord D) n k p (c:natO -m> DS_ord D),    (n<k+p)%nat -> pred_nth (c n) k = Con a s ->    exists d:natO -m> DS_ord D,                  DS_lubn c p == Con a (DS_lub d) /\ (s:DS_ord D) <= d n. intros D a s n k; pattern k; apply Wf_nat.lt_wf_ind; intros. rewrite (DS_lubn_inv c p). case (fCon c p); intros. case s0; clear s0; intros hd (tlc,(m,(H2,H3))). assert ((Con a s : DS_ord D) <= Con hd (tlc n)). apply Ole_trans with (c (n+m)); auto. rewrite <- H1; apply Ole_trans with (c n); auto with arith. exists tlc; split; auto. assert (Heq:=DSleCon_hd H4). rewrite Heq; apply Con_compat; auto. apply DSleCon_tl with a hd; auto. destruct n0; simpl pred_nth in *|-*. absurd (isEps (c n)); auto. rewrite H1; auto. case (H n0) with (p:=S p) (c:=cpred c); auto with zarith. intros d (H2,H3); exists d; split; auto. apply Oeq_trans with (DS_lubn (cpred c) (S p)); auto. Save. Lemma DS_lubn_pred_nth_inv : forall D a (s:DS_ord D) k p (c:natO -m> DS_ord D),    pred_nth (DS_lubn c p) k = Con a s ->    exists tlc :natO -m> DS_ord D, s= DS_lub tlc /\ exists m, forall l, c (l+m) == Con a (tlc l). intros D a s k; pattern k; apply Wf_nat.lt_wf_ind; clear k; intros n IH p c. rewrite (DS_lubn_inv c p). case (fCon c p). intros (hdc,(tlc,(m,(H2,H3)))) H. exists tlc. assert (Heq:Con hdc (DS_lub tlc)=Con a s). transitivity (pred_nth (Con hdc (DS_lub tlc)) n); auto. injection Heq; auto. intros; subst; repeat split; auto. exists m; auto. destruct n; simpl pred_nth; intros. discriminate H. case (IH n) with (p:=S p) (c:=cpred c); auto with arith; clear IH. intros tlc (H1,(m,H3)). exists tlc; split; auto. exists m; intro l; apply Oeq_trans with (cpred c (l + m)); auto. unfold cpred; simpl; auto. Save. Lemma DS_lubCon_inv : forall D a (s:DS_ord D) (c:natO -m> DS_ord D),    (DS_lub c == Con a s) ->    exists tlc :natO -m> DS_ord D,            s==DS_lub tlc /\ exists m, forall l, c (l+m) == Con a (tlc l). intros; case (decomp_eq H); intros t (H1,H2). case H1; intros k H4. case (@DS_lubn_pred_nth_inv D a t k 1 c H4); intros tlc (H5,(m,H7)). exists tlc; split; subst; auto. exists m; intros. apply Oeq_trans with (Con a (tlc l)); auto. Save. Lemma DS_lubCon : forall D a s n (c:natO -m> DS_ord D),    (Con a s :DS_ord D) <= c n ->    exists d:natO -m> DS_ord D,              DS_lub c == Con a (DS_lub d) /\ (s:DS_ord D) <= d n. intros D a s n c H; inversion_clear H. case H0; intros k H3. case (@DS_lubn_pred_nth D a t n (n+k) 1 c); auto with zarith. pattern n at 2; elim n; intros; simpl; auto. transitivity (pred (pred_nth (c n) (n0 + k))); auto. rewrite H; auto. intros d (H4,H5). exists d; split; eauto. Save. Lemma DS_lub_upper : forall D (c:natO -m> DS_ord D), forall n, c n <= DS_lub c. intros; apply DSle_rec_eq   with (R:= fun x y:DS_ord D =>exists c:natO -m> DS_ord D, x<=c n /\ y==DS_lub c); intuition. clear c; case H; intros c (H2,H3); exists c; split. apply Ole_trans with x1; auto. apply Oeq_trans with y1; auto. clear c; case H; clear H; intros c (H1,H2). case (DS_lubCon n c H1); intros d (H3,H4). assert (H6:(y:DS_ord D)==Con a (DS_lub d)). apply Oeq_trans with (DS_lub c); trivial. exists (DS_lub d); split; auto. exists d; auto. exists c; auto. Save. Lemma DS_lub_least : forall D (c:natO -m> DS_ord D) x,                       (forall n, c n <= x) -> DS_lub c <= x. intros; apply DSle_rec_eq   with (R:= fun x y: DS_ord D=>exists c, x==DS_lub c /\ forall n, c n <= y); intros. case H0; intros d (H3,H4); exists d; split; eauto. case H0; intros d (H3,H4). assert (H5:(Con a s:DS_ord D) <= DS_lub d); auto. inversion_clear H5. case (@DS_lubCon_inv D a s d); auto; intros tlc (H7,(m,H9)). assert ((Con a (tlc O) :DS_ord D) <= y). apply Ole_trans with (d (0+m)); auto. inversion_clear H5. assert (y==Con a t0); auto. exists t0; split; auto. assert (forall l, (Con a (tlc l): DS_ord D) <= Con a t0). intro; apply Ole_trans with (d (l+m)); auto. apply Ole_trans with y; auto. exists tlc; split; auto; intros. apply DSleCon_tl with a a; auto. exists c; auto. Save. ```

## Definition of the cpo of streams

``` Definition DS : Type -> cpo. intro D; exists (DS_ord D) (DS_bot D) (DS_lub (D:=D)); auto. exact (DS_lub_upper (D:=D)). exact (DS_lub_least (D:=D)). Defined. Lemma DS_lub_inv : forall D (c:natO -m> DS D), lub c =      match fCon c 1 with         inleft (existS hd (exist tlc _)) => Con hd (lub (c:=DS D) tlc)      | inright _ => Eps (DS_lubn (cpred c) 2)     end. intros D c; exact (DS_lubn_inv c 1). Save. Definition cons D (a : D) (s: DS D) : DS D := Con a s. Lemma cons_le_compat :      forall D a b (s t:DS D), a = b -> s <= t -> cons a s <= cons b t. intros; simpl; unfold cons; rewrite H; apply DSleCon0; auto. Save. Hint Resolve cons_le_compat. Lemma cons_eq_compat :  forall D a b (s t:DS D), a = b -> s == t -> cons a s == cons b t. intros; apply Ole_antisym; auto. Save. Hint Resolve cons_eq_compat. Add Morphism cons with signature eq ==> Oeq ==> Oeq as cons_eq_compat_morph. intros; apply (cons_eq_compat (a:=x) (b:=x) (s:=x1) (t:=x2)); auto. Save. Lemma not_le_consBot: forall D a (s:DS D), ~ cons a s <= 0. intros D a s H. inversion_clear H. case H0; intros. induction x; auto. simpl in H. rewrite DS_bot_eq in H. discriminate H. Save. Hint Resolve not_le_consBot. Lemma DSle_intro_cons :        forall D (x y:DS D), (forall a s, x==cons a s -> cons a s <= y) -> x <= y. intros; simpl; apply DSle_rec_eq with     (R:= fun (x y :DS D) => forall a s, x==cons a s -> cons a s <= y); auto; intros. apply Ole_trans with y1; auto. apply (H0 a s); auto. apply Oeq_trans with x2; auto. assert (cons a s <= y0); eauto. inversion_clear H1. exists t; split; intros; auto. apply Ole_trans with s; auto. Save. Definition is_cons D (x:DS D) := isCon x. Lemma is_cons_intro : forall D (a:D) (s:DS D), is_cons (cons a s). red; unfold cons; auto. Save. Hint Resolve is_cons_intro. Lemma is_cons_elim : forall D (x:DS D), is_cons x -> exists a, exists s : DS D, x == cons a s. intros; elim (uncons H); intros a (s,H1). exists a; exists s. unfold cons; simpl; auto. Save. Lemma not_is_consBot : forall D, ~ is_cons (0:DS D). red; intros. case (is_cons_elim H); intros a (s,Heq). apply (not_le_consBot (a:=a) (s:=s)); auto. Save. Hint Resolve not_is_consBot. Lemma is_cons_le_compat : forall D (x y:DS D), x <= y -> is_cons x -> is_cons y. intros; unfold is_cons; simpl; apply isCon_le with x; auto. Save. Lemma is_cons_eq_compat : forall D (x y:DS D), x == y -> is_cons x -> is_cons y. intros; apply is_cons_le_compat with x; auto. Save. Lemma DSle_intro_is_cons : forall D (x y:DS D), (is_cons x -> x <= y) -> x <= y. intros; apply DSle_intro_cons; intros. apply Ole_trans with x; auto. apply H; apply is_cons_eq_compat with (cons a s); auto. Save. Lemma DSeq_intro_is_cons : forall D (x y:DS D),              (is_cons x -> x <= y) -> (is_cons y -> y <= x) -> x == y. intros; apply Ole_antisym; apply DSle_intro_is_cons; auto. Save. Add Morphism is_cons with signature Oeq ==> iff as is_cons_eq_iff. split; intro. apply is_cons_eq_compat with x1; auto. apply is_cons_eq_compat with x2; auto. Save. Add Morphism cons with signature eq ==> Ole ++> Ole as cons_le_morph. intros; apply (cons_le_compat (D:=D)); trivial. Save. Hint Resolve cons_le_morph. ```

## Basic functions

``` Section Simple_functions. ```

### Build a function F such that F (Con a s) = f a s and F (Eps x) = Eps (F x)

``` Variable D D': Type. Variable f : D -> DS D -m> DS D'. CoFixpoint DScase (s:DS D) : DS D':=     match s with Eps x => Eps (DScase x) | Con a l => f a l end. Lemma DScase_inv :    forall (s:DS D), DScase s = match s with Eps l => Eps (DScase l) | Con a l => f a l end. intros; rewrite (DS_inv (DScase s)); simpl; auto. Save. Lemma DScaseEps : forall (s:DS D), DScase (Eps s) = Eps (DScase s). intros; rewrite (DScase_inv (Eps s)); trivial. Save. Lemma DScase_cons : forall a (s:DS D), DScase (cons a s) = f a s. intros; rewrite (DScase_inv (cons a s)); trivial. Save. Hint Resolve DScaseEps DScase_cons. Lemma DScase_decomp : forall a (s x:DS D), decomp a s x -> DScase x == f a s. intros a s x Hd. pattern x; apply decomp_ind with (3:=Hd); intros; auto. rewrite DScaseEps; auto. apply Oeq_trans with (DScase x0); simpl; auto. rewrite <- (DScase_cons a s); trivial. Save. Lemma DScase_eq_cons : forall a (s x:DS D), x == cons a s -> DScase x == f a s. intros; elim (decomp_eq H); intros t (H1,H2). apply Oeq_trans with (f a t). apply DScase_decomp; auto. apply (fmon_stable (f a)); auto. Save. Hint Resolve DScase_eq_cons. Lemma DScase_bot : DScase 0 <= 0. cofix; simpl. pattern (DS_bot D) at 1; rewrite DS_bot_eq. rewrite DScaseEps. apply DSleEps; trivial. Save. Lemma DScase_le_cons : forall a (s x:DS D), cons a s <= x -> f a s <= DScase x. intros a s x H; inversion H. apply Ole_trans with (f a t). apply (fmonotonic (f a)); auto. case (DScase_decomp H2); auto. Save. Lemma DScase_le_compat : forall (s t:DS D), s <= t -> DScase s <= DScase t. cofix. intros s t H; rewrite (DScase_inv s); case H; intros. simpl; apply DSleEps. apply DScase_le_compat; trivial. apply Ole_trans with (f a t0); auto. pattern y; apply decomp_ind with (3:=H0); auto; intros. rewrite DScaseEps. apply Ole_trans with (DScase x). exact H2. simpl; apply DSleEps_right. simpl; apply DSle_refl. change (f a t0 <= DScase (cons a t0)); auto. Save. Hint Resolve DScase_le_compat. Lemma DScase_eq_compat : forall (s t:DS D), s == t -> DScase s == DScase t. intros; apply Ole_antisym; auto. Save. Hint Resolve DScase_eq_compat. Add Morphism DScase with signature Oeq ==> Oeq as DScase_eq_compat_morph. exact DScase_eq_compat. Save. Definition DSCase : DS D -m> DS D'. exists DScase; red; auto. Defined. Lemma DSCase_simpl : forall (s:DS D), DSCase s = DScase s. trivial. Save. Lemma DScase_decomp_elim : forall a (s:DS D') (x:DS D),    decomp a s (DScase x) -> exists b, exists t, x==cons b t /\ f b t == Con a s. intros a s x H; case H; clear H. intro k; generalize x; clear x; pattern k; apply Wf_nat.lt_wf_ind; intros. rewrite DScase_inv in H0; destruct x. destruct n; simpl in H0. discriminate H0. case (H n) with (2:=H0); auto. intros b (t,(H1,H2)). exists b; exists t; split; auto. apply Oeq_trans with x; auto. apply Oeq_sym; apply (eqEps x). exists d; exists x; split; auto. rewrite <- H0; simpl; auto. Save. Lemma DScase_eq_cons_elim : forall a (s : DS D') (x:DS D),    DScase x == cons a s -> exists b, exists t, x==cons b t /\ f b t == cons a s. intros a s x H; case (decomp_eq H); intros t (H1,H2). case (DScase_decomp_elim x H1); intros c (u,(H4,H5)). exists c; exists u; split; auto. apply Oeq_trans with (cons a t); simpl; auto. apply Oeq_sym; exact (cons_eq_compat (refl_equal a) H2). Save. Lemma DScase_is_cons : forall (x:DS D), is_cons (DScase x) -> is_cons x. intros; case (is_cons_elim H); intros a (s,H1). case (DScase_eq_cons_elim x H1); intros b (t,(H2,H3)). red; apply DSle_isCon with b t; auto. Save. Lemma is_cons_DScase : (forall a (s:DS D), is_cons (f a s)) -> forall (x:DS D), is_cons x -> is_cons (DScase x). intros; case (is_cons_elim H0); intros a (s,H1). apply is_cons_eq_compat with (f a s); auto. rewrite H1; auto. Save. Hypothesis fcont : forall c, continuous (f c). Lemma DScase_cont : continuous DSCase. red; intros; rewrite DSCase_simpl; apply DSle_intro_cons; intros. case (DScase_eq_cons_elim (a:=a) (s:=s) (lub h)); auto; intros b (t,(H3,H4)). case (DS_lubCon_inv h H3). intros tlc (H5,(m,H6)). apply Ole_trans with (f b t); auto. apply Ole_trans with (f b (lub (c:=DS D) tlc)); auto. apply Ole_trans with (lub (f b @ tlc)); auto. rewrite (lub_lift_right (DSCase @ h) m); auto. apply (lub_le_compat (D:=DS D')). unfold mseq_lift_right; simpl; intros. apply DScase_le_cons; unfold cons; auto. Save. Hint Resolve DScase_cont. Lemma DScase_cont_eq : forall (c:natO-m>DS D), DScase (lub c) == lub (DSCase @ c). intros; apply lub_comp_eq with (f:=DSCase); auto. Save. End Simple_functions. Hint Resolve DScaseEps DScase_cons DScase_le_compat DScase_eq_compat DScase_bot DScase_cont. Definition DSCASE_mon : forall D D', (D-O->(DS D -M-> DS D')) -M-> DS D -M-> DS D'. intros D D'; exists (DSCase (D:=D)(D':=D')); red; intros f g Hle; intro s. repeat (rewrite DSCase_simpl). simpl; apply DSle_intro_cons; intros. case (DScase_eq_cons_elim f (a:=a) (s:=s0) s); auto; intros b (t,(Hs,Hf)). assert (DScase g s == g b t). apply (DScase_eq_cons g Hs). apply Ole_trans with (f b t); auto. apply Ole_trans with (g b t); auto. Defined. Lemma DSCASE_mon_simpl : forall D D' f s, DSCASE_mon D D' f s = DScase f s. trivial. Save. Lemma DSCASE_mon_cont : forall D D', continuous (DSCASE_mon D D'). red; intros; intro s; rewrite (DSCASE_mon_simpl (D:=D) (D':=D')). apply DSle_intro_cons; intros. case (DScase_eq_cons_elim (lub h) (a:=a) (s:=s0) s);          auto; intros b (t,(Hs,Hf)). rewrite fmon_lub_simpl. apply Ole_trans with (lub ((h <o> b) <_> t)); auto. apply (lub_le_compat (D:=DS D')); intro n. repeat (rewrite fmon_app_simpl); rewrite fmon_comp_simpl. rewrite DSCASE_mon_simpl. rewrite (DScase_eq_cons (h n) Hs); auto. Save. Definition DSCASE_cont : forall D D', (D-O->(DS D -C-> DS D')) -m> (DS D -C-> DS D'). intros D D'; exists (fun f => mk_fconti (DScase_cont (fun a => fcontit (f a))                                                                         (fun a => fcontinuous (f a)))). intros f g Hle; intro s;simpl. apply DSle_intro_cons; intros. case (DScase_eq_cons_elim (fun a : D => fcontit (f a)) (a:=a) (s:=s0) s); auto; intros b (t,(Hs,Hf)). assert (DScase (fun a0 => fcontit (g a0)) s == g b t). apply (DScase_eq_cons (fun a0 => fcontit (g a0)) Hs). apply Ole_trans with (f b t); auto. apply Ole_trans with (g b t); auto. apply (fcont_le_elim (Hle b)). Defined. Lemma DSCASE_cont_simpl : forall D D' f s,         DSCASE_cont D D' f s = DScase (fun a => fcontit (f a)) s. trivial. Save. Definition DSCASE : forall D D', (D-O->DS D -C->DS D')-c> DS D -C->DS D'. intros; exists (DSCASE_cont D D'). red; intros; intro s. change (DSCASE_cont D D' (lub h) s <= lub (DSCASE_cont D D' @ h) s). rewrite DSCASE_cont_simpl. apply DSle_intro_cons; intros. case (DScase_eq_cons_elim (fun a : D => fcontit ((lub h) a)) (a:=a) (s:=s0) s); auto; intros b (t,(Hs,Hf)). rewrite fcont_lub_simpl. apply Ole_trans with (lub ((h <o> b) <__> t)); auto. apply (lub_le_compat (D:=DS D')); intro n. repeat (rewrite fcont_app_simpl). rewrite fmon_comp_simpl. rewrite DSCASE_cont_simpl. rewrite (DScase_eq_cons (fun a0 : D => fcontit (h n a0)) Hs); auto. Defined. Lemma DSCASE_simpl : forall D D' f s, DSCASE D D' f s = DScase (fun a => fcontit (f a)) s. trivial. Save. ```

## Basic functions on streams

``` ```
• Cons is continuous
``` Definition Cons (D:Type): D -o> (DS D -m> DS D). intros D b; exists (cons b). red; intros; auto. Defined. Lemma Cons_simpl : forall D (a : D) (s : DS D), Cons a s = cons a s. trivial. Save. Lemma Cons_cont : forall D (a : D), continuous (Cons a). red; intros D a h. case (DS_lubCon (a:=a) (s:=h O) O (Cons a @ h)); trivial. intros d (H1,H2). case (DS_lubCon_inv (Cons a @ h) H1). intros tlc (H4,H5). apply Ole_trans with (cons a (lub (c:=DS D) d)); auto. case H5; clear H5; intros m H5. rewrite Cons_simpl; apply cons_le_compat; trivial. rewrite H4. assert (forall l : nat, h (l + m) == tlc l). intro l; simpl; apply Con_tl_simpl with a a. apply (H5 l). rewrite (lub_lift_right h m). apply (lub_le_compat (D:=DS D) (f:=mseq_lift_right (O:=DS D) h m) (g:=tlc)); intro n; simpl. case (H n); auto. Save. Hint Resolve Cons_cont. Definition CONS D (a : D) : DS D -c> DS D := mk_fconti (Cons_cont a). Lemma CONS_simpl : forall D (a : D) (s : DS D), CONS a s = cons a s. trivial. Save. ```
• first takes a stream and return the stream with only the first element f a s = cons a nil
``` Definition firstf (D:Type) : D -> DS D -m>DS D:= fun (d:D) => fmon_cte (DS D) (O2:=DS D) (cons d (0:DS D)). Lemma firstf_simpl : forall D (a:D) (s:DS D), firstf a s = cons a (0:DS D). trivial. Save. Lemma firstf_cont : forall D (a:D) c, firstf a (lub c) <= lub (firstf a @ c). intros; rewrite firstf_simpl. unfold firstf. apply Ole_trans with (lub (c:=DS D) (fmon_cte natO (O2:=DS D) (cons a (0 : DS D)))); auto. Save. Hint Resolve firstf_cont. Definition First (D:Type) : DS D -m> DS D := DSCase (firstf (D:=D)). Definition first D (s:DS D) := First D s. Lemma first_simpl : forall D (s:DS D), first s = DScase (firstf (D:=D)) s. trivial. Save. Lemma first_le_compat : forall D (s t:DS D), s <= t -> first s <= first t. unfold first; auto. Save. Hint Resolve first_le_compat. Lemma first_eq_compat : forall D (s t:DS D), s == t -> first s == first t. intros; apply Ole_antisym; auto. Save. Hint Resolve first_eq_compat. Lemma first_cons : forall D a (s:DS D), first (cons a s) = cons a (0:DS D). intros; rewrite first_simpl; intros. rewrite DScase_cons; trivial. Save. Lemma first_bot : forall D, first (D:=D) 0 <= 0. intros; rewrite first_simpl; auto. Save. Lemma first_cons_elim : forall D a (s t:DS D),     first t == cons a s -> exists u, t == cons a u /\ s==(0:DS D). intros D a s t; rewrite first_simpl; intros. case (DScase_eq_cons_elim (firstf (D:=D)) t H). intros b (u,(H1,H2)). exists u. assert (b=a). apply (Con_hd_simpl H2). assert ((0:DS D) ==s). apply (Con_tl_simpl H2). split; auto. apply Oeq_trans with (1:=H1); auto. Save. Add Morphism first with signature Oeq ==> Oeq as first_eq_compat_morph. exact first_eq_compat. Save. Add Morphism first with signature Ole ++> Ole as first_le_compat_morph. exact first_le_compat. Save. Lemma is_cons_first : forall D (s:DS D), is_cons s -> is_cons (first s). unfold first, First; intros. rewrite DSCase_simpl; apply is_cons_DScase; auto. intros; unfold firstf; simpl; auto. Save. Hint Resolve is_cons_first. Lemma first_is_cons : forall D (s:DS D), is_cons (first s) -> is_cons s. unfold first, First; intros. apply DScase_is_cons with D (firstf (D:=D)); auto. Save. Hint Immediate first_is_cons. Lemma first_cont : forall D, continuous (First D). intro; unfold First; apply DScase_cont; intros. exact (firstf_cont c). Save. Hint Resolve first_cont. Definition FIRST (D:Type) : DS D -c> DS D. intro; exists (First D); auto. Defined. Lemma FIRST_simpl : forall D s, FIRST D s = first s. trivial. Save. ```
• rem returns the stream without the first element
``` Definition remf D (d: D) : DS D -m> DS D := fmon_id (DS D). Lemma remf_simpl : forall D (a:D) s, remf a s = s. trivial. Save. Lemma remf_cont : forall D (a:D) s, remf a (lub s) <= lub (remf a @ s). intros; rewrite remf_simpl; auto. Save. Hint Resolve remf_cont. Definition Rem D : DS D -m> DS D := DSCase (remf (D:=D)). Definition rem D (s:DS D) := Rem D s. Lemma rem_simpl : forall D (s:DS D), rem s = DScase (remf (D:=D)) s. trivial. Save. Lemma rem_cons : forall D (a:D) s, rem (cons a s) = s. intros; rewrite rem_simpl; rewrite DScase_cons; trivial. Save. Lemma rem_bot : forall D, rem (D:=D) 0 <= 0. intros; rewrite rem_simpl; auto. Save. Lemma rem_le_compat : forall D (s t:DS D), s<=t -> rem s <= rem t. unfold rem; auto. Save. Hint Resolve rem_le_compat. Lemma rem_eq_compat : forall D (s t:DS D), s==t -> rem s == rem t. intros; apply Ole_antisym; auto. Save. Hint Resolve rem_eq_compat. Add Morphism rem with signature Oeq ==> Oeq as rem_eq_compat_morph. exact rem_eq_compat. Save. Add Morphism rem with signature Ole ++> Ole as rem_le_compat_morph. exact rem_le_compat. Save. Lemma rem_is_cons : forall D (s:DS D), is_cons (rem s) -> is_cons s. unfold rem, Rem; intros. apply DScase_is_cons with D (remf (D:=D)); auto. Save. Hint Immediate rem_is_cons. Lemma rem_cont : forall D, continuous (Rem D). intros; unfold Rem; apply DScase_cont; intros; auto. exact (remf_cont c). Save. Hint Resolve rem_cont. Definition REM (D:Type) : DS D -c> DS D. intros; exists (Rem D); auto. Defined. Lemma REM_simpl : forall D (s:DS D), REM D s = rem s. trivial. Save. ```
• app s t concatenates the first element of s to t
``` Definition appf D (t:DS D) (d: D) : DS D -m>DS D := fmon_cte (DS D) (Cons d t). Lemma appf_simpl D (t:DS D) : forall a s, appf t a s = cons a t. trivial. Save. Definition Appf : forall D, DS D -m> D -o> (DS D -m> DS D). intro D; exists (appf (D:=D)); red; intros; intros a s; repeat (rewrite appf_simpl); auto. Defined. Lemma Appf_simpl : forall D t, Appf D t = appf t. trivial. Save. Lemma appf_cont D (t:DS D) : forall a c, appf t a (lub c) <= lub (appf t a @ c). intros; rewrite appf_simpl. unfold appf. apply Ole_trans with (lub (c:=DS D) (fmon_cte natO (O2:=DS D) (Cons a t))); auto. Save. Hint Resolve appf_cont. Lemma appf_cont_par : forall D, continuous (D2:=D -O-> (DS D -M->DS D)) (Appf D). red; intros. intros a s. rewrite (Appf_simpl (D:=D)); rewrite appf_simpl. apply Ole_trans with (lub (c:=DS D) (Cons a @ h)); auto. apply (Cons_cont a h). rewrite fcpo_lub_simpl; rewrite fmon_lub_simpl. apply lub_le_compat; intro n; auto. Save. Hint Resolve appf_cont_par. Definition AppI : forall D, DS D -m> DS D -m> DS D. intros; exists (fun t => DSCase (appf t)); red; intros. apply (fmonotonic (DSCASE_mon D D) (x:=appf x) (y:=appf y)). apply (fmonotonic (Appf D) (x:=x) (y:=y)); trivial. Defined. Lemma AppI_simpl : forall D s t, AppI D t s = DScase (appf t) s. trivial. Save. Definition App (D:Type) := fmon_shift (AppI D). Lemma App_simpl : forall D s t, App D s t = DScase (appf t) s. trivial. Save. Definition app D s t := App D s t. Lemma app_simpl : forall D (s t:DS D), app s t = DScase (appf t) s. trivial. Save. Lemma app_cons : forall D a (s t:DS D), app (cons a s) t = cons a t. intros; rewrite app_simpl; rewrite DScase_cons; trivial. Save. Lemma app_bot : forall D (s:DS D), app 0 s <= 0. intros; rewrite app_simpl; auto. Save. Lemma app_mon_left : forall D (s t u : DS D), s <= t -> app s u <= app t u. intros; repeat (rewrite app_simpl); auto. Save. Lemma app_cons_elim : forall D a (s t u:DS D), app t u == cons a s ->              exists t', t == cons a t' /\ s == u. intros D a s t u; rewrite app_simpl; intros. case (DScase_eq_cons_elim (appf u) t H). intros b (t',(H1,H2)). exists t'. assert (b=a). apply (Con_hd_simpl H2). assert (u==s). apply (Con_tl_simpl H2). split; auto. apply Oeq_trans with (1:=H1); auto. Save. Lemma app_mon_right : forall D (s t u : DS D), t <= u -> app s t <= app s u. intros; apply (fmonotonic (App D s) H); auto. Save. Hint Resolve first_cons first_bot app_cons app_bot                     app_mon_left app_mon_right rem_cons rem_bot. Lemma app_le_compat : forall D (s t u v:DS D), s <= t -> u <= v -> app s u <= app t v. intros; apply Ole_trans with (app t u); auto. Save. Hint Immediate app_le_compat. Lemma app_eq_compat : forall D (s t u v:DS D), s == t -> u == v -> app s u == app t v. intros; apply Ole_antisym; apply app_le_compat; auto. Save. Hint Immediate app_eq_compat. Add Morphism app with signature Oeq ==> Oeq ==> Oeq as app_eq_compat_morph. intros; apply (app_eq_compat H H0); auto. Save. Add Morphism app with signature Ole ++> Ole ++> Ole as app_le_compat_morph. intros; apply (app_le_compat H H0); auto. Save. Lemma is_cons_app : forall D (x y : DS D), is_cons x -> is_cons (app x y). intros; rewrite app_simpl. apply is_cons_DScase; simpl; auto. Save. Hint Resolve is_cons_app. Lemma app_is_cons : forall D (x y : DS D), is_cons (app x y) -> is_cons x. intros D x y; rewrite app_simpl; intros; apply DScase_is_cons with D (appf y); auto. Save. Lemma app_cont : forall D, continuous2 (App D). intro D; apply continuous_continuous2; intros. red; intros. rewrite (App_simpl (D:=D)). apply Ole_trans with (DScase (lub (c:=D-O->(DS D -M->DS D)) (Appf D @ h)) k). assert (DSCase (appf (lub (c:=DS D) h)) <= DSCase (lub (c:=D -O-> (DS D -M-> DS D)) (Appf D @ h))); auto. apply (fmonotonic (DSCASE_mon D D) (x:=appf (lub h)) (y:=lub (c:=D -O-> DS D -M-> DS D) (Appf D @ h))). apply (appf_cont_par (D:=D) h). apply Ole_trans with (lub (c:=DS D -M->DS D) (DSCASE_mon D D @ (Appf D @ h)) k); auto. apply (DSCASE_mon_cont (Appf D @ h) k). red; intros; intro k. rewrite fmon_lub_simpl. assert (continuous (D1:=DS D) (D2:=DS D) (DSCase (appf k))). apply DScase_cont; intros. exact (appf_cont k c). exact (H h). Save. Hint Resolve app_cont. Definition APP (D:Type) : DS D -c> DS D -C-> DS D := continuous2_cont (app_cont (D:=D)). Lemma APP_simpl : forall D (s t : DS D), APP D s t = app s t. trivial. Save. ```

### Basic equalities

``` Lemma first_eq_bot : forall D, first (D:=D) 0 == 0. intros; apply Ole_antisym; auto. Save. Lemma rem_eq_bot : forall D, rem (D:=D) 0 == 0. auto. Save. Lemma app_eq_bot : forall D (s:DS D), app 0 s == 0. auto. Save. Hint Resolve first_eq_bot rem_eq_bot app_eq_bot. Lemma DSle_app_bot_right_first : forall D (s:DS D), app s 0 <= first s. intros; apply DSle_intro_cons; intros. case (app_cons_elim s 0 H); intros b (H1,H2). apply Ole_trans with (cons a (0:DS D)); auto. apply Ole_trans with (first (cons a b)); auto. Save. Lemma DSle_first_app_bot_right : forall D (s:DS D), first s <= app s 0. intros; apply DSle_intro_cons; intros. case (first_cons_elim s H); intros s' (H1,H2); auto. Save. Lemma app_bot_right_first : forall D (s:DS D), app s 0 == first s. intros; apply Ole_antisym. apply DSle_app_bot_right_first. apply DSle_first_app_bot_right. Save. Lemma DSle_first_app_first : forall D (x y:DS D), first (app x y) <= first x. intros; apply DSle_intro_cons; intros. case (first_cons_elim (app x y) H); intros s' (H1,H2). case (app_cons_elim x y H1); intros x' (H3,H4). apply Ole_trans with (first (cons a x')); auto. apply Ole_trans with (cons a (0:DS D)); auto. Save. Lemma DSle_first_first_app : forall D (x y:DS D), first x <= first (app x y). intros; apply DSle_intro_cons; intros. case (first_cons_elim x H); intros x' (H1,H2). apply Ole_trans with (first (app (cons a x') y)); auto. apply Ole_trans with (first (cons a y)); auto. apply Ole_trans with (cons a (0:DS D)); auto. Save. Lemma first_app_first : forall D (x y:DS D), first (app x y)==first x. intros; apply Ole_antisym. apply DSle_first_app_first. apply DSle_first_first_app. Save. Hint Resolve app_bot_right_first first_app_first. Lemma DSle_app_first_rem : forall D (x:DS D), app (first x) (rem x) <= x. intros; apply DSle_intro_cons; intros. case (app_cons_elim (first x) (rem x) H); intros t (H1,H2). case (first_cons_elim x H1); intros x' (H3,H4). apply Ole_trans with (cons a x'); auto. apply cons_le_compat; auto. apply Ole_trans with (rem x); auto. apply Ole_trans with (rem (cons a x')); auto. Save. Lemma DSle_app_first_rem_sym : forall D (x:DS D), x <= app (first x) (rem x). intros; apply DSle_intro_cons; intros. apply Ole_trans with (app (first (cons a s)) (rem (cons a s))). rewrite first_cons; rewrite rem_cons; rewrite app_cons; trivial. apply Ole_trans with (app (first x) (rem (cons a s))); auto. Save. Lemma app_first_rem : forall D (x:DS D), app (first x) (rem x) == x. intros; apply Ole_antisym. apply DSle_app_first_rem. apply DSle_app_first_rem_sym. Save. Hint Resolve app_first_rem. Lemma rem_app : forall D (x y:DS D), is_cons x -> rem (app x y) == y. intros; case (is_cons_elim H); intros a (s,H1). rewrite H1. rewrite app_cons; rewrite rem_cons; trivial. Save. Hint Resolve rem_app. Lemma rem_app_le : forall D (x y:DS D), rem (app x y) <= y. intros; apply DSle_intro_is_cons; intros. assert (is_cons (app x y)); auto. assert (is_cons x); auto. apply app_is_cons with y; trivial. Save. Hint Resolve rem_app_le. Lemma is_cons_rem_app : forall D (x y : DS D), is_cons x -> is_cons y -> is_cons (rem (app x y)). intros; apply is_cons_eq_compat with y; auto. apply Oeq_sym; auto. Save. Hint Resolve is_cons_rem_app. Lemma rem_app_is_cons : forall D (x y : DS D), is_cons (rem (app x y)) -> is_cons y. intros; assert (is_cons (app x y)); auto. assert (is_cons x). apply app_is_cons with y; trivial. apply is_cons_eq_compat with (rem (app x y)); auto. Save. Lemma first_first_eq : forall D (s:DS D), first (first s) == first s. intros; apply Oeq_trans with (first (app (first s) (rem s))); auto. Save. Hint Resolve first_first_eq. Lemma app_app_first : forall D (s t : DS D), app (first s) t == app s t. intros; apply DSeq_intro_is_cons; intros. assert (is_cons s). assert (is_cons (first s)); auto. apply app_is_cons with t; trivial. case (is_cons_elim H0); intros a (s',H1). rewrite H1; rewrite first_cons; repeat rewrite app_cons; trivial. assert (is_cons s). apply app_is_cons with t; trivial. case (is_cons_elim H0); intros a (s',H1). rewrite H1; rewrite first_cons; repeat rewrite app_cons; trivial. Save. ```

## Proof by co-recursion

``` Lemma DS_bisimulation : 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)    -> (forall (x y:DS D), (is_cons x \/ is_cons y) -> R x y -> R (rem x) (rem y))    -> forall x y, R x y -> x == y. intros; apply (DSeq_rec R); auto; intros. assert (Hf:=H0 (cons a s) y0 (or_introl (is_cons y0) (is_cons_intro a s)) H3). assert (Hr:=H1 (cons a s) y0 (or_introl (is_cons y0) (is_cons_intro a s)) H3). rewrite first_cons in Hf. case (first_cons_elim (a:=a) (s:=0:DS D) y0); auto; intros x0 (H4,_). exists x0; split; auto. apply H with (rem (cons a s)) (rem y0); auto. apply Oeq_trans with (rem (cons a x0)); auto. assert (Hf:=H0 x0 (cons a s) (or_intror (is_cons x0) (is_cons_intro a s)) H3). assert (Hr:=H1 x0 (cons a s) (or_intror (is_cons x0) (is_cons_intro a s)) H3). rewrite first_cons in Hf. case (first_cons_elim (a:=a) (s:=0:DS D) x0); auto; intros y0 (H4,_). exists y0; split; auto. apply H with (rem x0) (rem (cons a s)); auto. apply Oeq_trans with (rem (cons a y0)); auto. Save. Lemma DS_bisimulation2 : 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)    -> (forall (x y:DS D), (is_cons (rem x) \/ is_cons (rem y)) -> R x y -> first (rem x) == first (rem y))    -> (forall (x y:DS D), (is_cons (rem x) \/ is_cons (rem y)) -> R x y -> R (rem (rem x)) (rem (rem y)))    -> forall x y, R x y -> x == y. intros; apply DS_bisimulation    with (R:= fun x y => R x y \/ ((is_cons x \/ is_cons y)                                                  -> (first x == first y /\                                                       R (rem x) (rem y)))); intros. case H4; clear H4; intros. left; apply H with x1 y1; trivial. right; intros. assert (is_cons x1 \/ is_cons y1). case H7; clear H7; intro. left; apply is_cons_eq_compat with x2; auto. right; apply is_cons_eq_compat with y2; auto. assert (H9:=H4 H8); clear H4 H7 H8; intuition. rewrite <- H5; rewrite <- H6; trivial. apply H with (rem x1) (rem y1); auto. case H5; clear H5; intros; auto. case (H5 H4); trivial. case H5; clear H5; intros; auto. case (H5 H4); clear H4 H5; intros. auto. auto. Save. ```

## Finiteness of streams

``` CoInductive infinite (D:Type) (s: DS D) : Prop :=       inf_intro : is_cons s -> infinite (rem s) -> infinite s. Lemma infinite_le_compat : forall D (s t:DS D), s <= t -> infinite s -> infinite t. intro D; cofix; intros. case H0; intros. apply inf_intro. apply is_cons_le_compat with s; auto. apply infinite_le_compat with (rem s); auto. Save. Add Morphism infinite with signature Oeq ==> iff as infinite_morph. split; intros. apply infinite_le_compat with x1; auto. apply infinite_le_compat with x2; auto. Save. Lemma not_infiniteBot : forall D, ~ infinite (0:DS D). red; intros D H; case H; intros. apply (not_is_consBot (D:=D)); auto. Save. Hint Resolve not_infiniteBot. Inductive finite (D:Type) (s:DS D) : Prop :=       fin_bot : s <= 0 -> finite s | fin_cons : finite (rem s) -> finite s. Lemma finite_mon : forall D (s t:DS D), s <= t -> finite t -> finite s. intros. generalize s H. elim H0; clear s t H H0; intros. apply fin_bot. apply Ole_trans with s; auto. apply fin_cons; auto. Save. Add Morphism finite with signature Oeq ==> iff as finite_morph. split; intros. apply finite_mon with x1; auto. apply finite_mon with x2; auto. Save. Lemma not_finite_infinite : forall D (s:DS D), finite s -> ~ infinite s. induction 1; intros; auto. red; intro; apply (not_infiniteBot (D:=D)). apply infinite_le_compat with s; auto. red; intro; apply IHfinite. case H0; trivial. Save. ```

## Mapping a function on a stream

``` Section MapStream. Variable D D': Type. Variable F : D -> D'. Definition mapf : (DS D -C-> DS D') -m> D-O-> DS D -C->DS D'. exists (fun f (a:D) => CONS (F a) @_ f). red; intros f g Hle a. apply (fcont_le_intro (D1:=DS D) (D2:=DS D')); intro s. repeat rewrite fcont_comp_simpl. auto. Defined. Lemma mapf_simpl : forall f, mapf f = fun a => CONS (F a) @_ f. trivial. Save. Definition Mapf : (DS D -C-> DS D') -c> D-O-> DS D -C->DS D'. exists mapf. red; intros h a. rewrite mapf_simpl. rewrite fcpo_lub_simpl. apply (fcont_le_intro (D1:=DS D) (D2:=DS D')); intro s. rewrite fcont_lub_simpl. repeat rewrite fcont_comp_simpl; repeat rewrite fcont_lub_simpl; intros. rewrite (fcontinuous (CONS (F a)) (h <__> s)). apply lub_le_compat; intro n; auto. Defined. Lemma Mapf_simpl : forall f, Mapf f = fun a => CONS (F a) @_ f. trivial. Save. Definition MAP : DS D -C-> DS D' := FIXP (DS D-C->DS D') (DSCASE D D' @_ Mapf). Lemma MAP_eq : MAP == DSCASE D D' (Mapf MAP). exact (FIXP_eq (DSCASE D D' @_ Mapf)). Save. Definition map (s: DS D) := MAP s. Lemma map_eq : forall s:DS D, map s == DScase (fun a => Cons (F a) @ (fcontit MAP)) s. intros; apply (fcont_eq_elim MAP_eq s). Save. Lemma map_bot : map 0 == 0. unfold map. rewrite (fcont_eq_elim MAP_eq 0). rewrite DSCASE_simpl; auto. Save. Lemma map_eq_cons : forall a s,             map (cons a s) == cons (F a) (map s). intros; unfold map at 1. rewrite (fcont_eq_elim MAP_eq (cons a s)). rewrite DSCASE_simpl. rewrite DScase_cons; auto. Save. Lemma map_le_compat : forall s t, s <= t -> map s <= map t. intros; unfold map; apply (fcont_monotonic MAP); trivial. Save. Lemma map_eq_compat : forall s t, s == t -> map s == map t. intros; apply (fcont_stable MAP H). Save. Add Morphism map with signature Oeq ==> Oeq as map_eq_compat_morph_local. exact map_eq_compat. Save. Lemma is_cons_map : forall (s:DS D), is_cons s -> is_cons (map s). intros; case (is_cons_elim H); intros a (t,H1). rewrite H1. rewrite map_eq_cons; auto. Save. Hint Resolve is_cons_map. Lemma map_is_cons : forall s, is_cons (map s) -> is_cons s. intros; case (is_cons_elim H); intros a (t,H1). generalize H1; rewrite map_eq. intros; apply DScase_is_cons with (f:=fun a0 : D => Cons (F a0) @ fcontit MAP). rewrite H0; auto. Save. Hint Immediate map_is_cons. End MapStream. Hint Resolve map_bot map_eq_cons map_le_compat map_eq_compat is_cons_map. Add Morphism map with signature eq ==> Oeq ==> Oeq as map_eq_compat_morph. exact map_eq_compat. Save. ```

## Filtering a stream

``` Section FilterStream. Variable D : Type. Variable P : D -> Prop. Variable Pdec : forall x, {P x}+{~ P x}. Definition filterf : (DS D -C-> DS D) -m> D-O-> DS D -C->DS D. exists (fun f a => if Pdec a then CONS a @_ f else f). red; intros f g Hle a. case (Pdec a); intros; auto. apply (fcont_le_intro (D1:=DS D) (D2:=DS D)); intro s. repeat rewrite fcont_comp_simpl. auto. Defined. Lemma filterf_simpl : forall f, filterf f = fun a => if Pdec a then CONS a @_ f else f. trivial. Save. Definition Filterf : (DS D -C-> DS D) -c> D-O-> DS D -C->DS D. exists filterf. red; intros h a. rewrite filterf_simpl. rewrite fcpo_lub_simpl. apply (fcont_le_intro (D1:=DS D) (D2:=DS D)); intro s. rewrite fcont_lub_simpl. case (Pdec a); repeat rewrite fcont_comp_simpl; repeat rewrite fcont_lub_simpl; intros. rewrite (fcontinuous (CONS a) (h <__> s)). apply lub_le_compat; intro n. rewrite fmon_comp_simpl. repeat rewrite fcont_app_simpl. rewrite ford_app_simpl. rewrite fmon_comp_simpl. rewrite filterf_simpl. case (Pdec a); intuition. apply lub_le_compat; intro m. repeat rewrite fcont_app_simpl. rewrite ford_app_simpl. rewrite fmon_comp_simpl. rewrite filterf_simpl. case (Pdec a); intuition. Defined. Lemma Filterf_simpl : forall f, Filterf f = fun a => if Pdec a then CONS a @_ f else f. trivial. Save. Definition FILTER : DS D -C-> DS D := FIXP (DS D-C->DS D) (DSCASE D D @_ Filterf). Lemma FILTER_eq : FILTER == DSCASE D D (Filterf FILTER). exact (FIXP_eq (DSCASE D D @_ Filterf)). Save. Definition filter (s: DS D) := FILTER s. Lemma filter_bot : filter 0 == 0. unfold filter. rewrite (fcont_eq_elim FILTER_eq 0). rewrite DSCASE_simpl; auto. Save. Lemma filter_eq_cons : forall a s,             filter (cons a s) == if Pdec a then cons a (filter s) else filter s. intros; unfold filter at 1. rewrite (fcont_eq_elim FILTER_eq (cons a s)). rewrite DSCASE_simpl. rewrite DScase_cons. rewrite Filterf_simpl; case (Pdec a); auto. Save. Lemma filter_le_compat : forall s t, s <= t -> filter s <= filter t. intros; unfold filter; apply (fcont_monotonic FILTER); trivial. Save. Lemma filter_eq_compat : forall s t, s == t -> filter s == filter t. intros; apply (fcont_stable FILTER H). Save. End FilterStream. Hint Resolve filter_bot filter_eq_cons filter_le_compat filter_eq_compat. ```
 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (238 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (179 entries) Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (9 entries) Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (5 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (44 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

# Global Index

## A

app [definition, in Cpo_streams_type]
App [definition, in Cpo_streams_type]
APP [definition, in Cpo_streams_type]
appf [definition, in Cpo_streams_type]
Appf [definition, in Cpo_streams_type]
appf_cont [lemma, in Cpo_streams_type]
appf_cont_par [lemma, in Cpo_streams_type]
Appf_simpl [lemma, in Cpo_streams_type]
appf_simpl [lemma, in Cpo_streams_type]
AppI [definition, in Cpo_streams_type]
AppI_simpl [lemma, in Cpo_streams_type]
app_app_first [lemma, in Cpo_streams_type]
app_bot [lemma, in Cpo_streams_type]
app_bot_right_first [lemma, in Cpo_streams_type]
app_cons [lemma, in Cpo_streams_type]
app_cons_elim [lemma, in Cpo_streams_type]
app_cont [lemma, in Cpo_streams_type]
app_eq_bot [lemma, in Cpo_streams_type]
app_eq_compat [lemma, in Cpo_streams_type]
app_first_rem [lemma, in Cpo_streams_type]
app_is_cons [lemma, in Cpo_streams_type]
app_le_compat [lemma, in Cpo_streams_type]
app_mon_left [lemma, in Cpo_streams_type]
app_mon_right [lemma, in Cpo_streams_type]
APP_simpl [lemma, in Cpo_streams_type]
app_simpl [lemma, in Cpo_streams_type]
App_simpl [lemma, in Cpo_streams_type]

## C

chain_tl [lemma, in Cpo_streams_type]
chain_uncons [lemma, in Cpo_streams_type]
Con [constructor, in Cpo_streams_type]
CONS [definition, in Cpo_streams_type]
Cons [definition, in Cpo_streams_type]
cons [definition, in Cpo_streams_type]
Cons_cont [lemma, in Cpo_streams_type]
cons_eq_compat [lemma, in Cpo_streams_type]
cons_le_compat [lemma, in Cpo_streams_type]
Cons_simpl [lemma, in Cpo_streams_type]
CONS_simpl [lemma, in Cpo_streams_type]
Con_compat [lemma, in Cpo_streams_type]
Con_exists_decompDSle [lemma, in Cpo_streams_type]
Con_hd_simpl [lemma, in Cpo_streams_type]
Con_tl_simpl [lemma, in Cpo_streams_type]
Cpo_streams_type [library]
cpred [definition, in Cpo_streams_type]

## D

decomp [definition, in Cpo_streams_type]
decompCon [lemma, in Cpo_streams_type]
decompCon_eq [lemma, in Cpo_streams_type]
decompEps [lemma, in Cpo_streams_type]
decompEps_pred [lemma, in Cpo_streams_type]
decompEps_pred_sym [lemma, in Cpo_streams_type]
decomp_DSleCon [lemma, in Cpo_streams_type]
decomp_DSleCon_sym [lemma, in Cpo_streams_type]
decomp_eq [lemma, in Cpo_streams_type]
decomp_eqCon [lemma, in Cpo_streams_type]
decomp_ind [lemma, in Cpo_streams_type]
decomp_isCon [lemma, in Cpo_streams_type]
DS [definition, in Cpo_streams_type]
DSCase [definition, in Cpo_streams_type]
DSCASE [definition, in Cpo_streams_type]
DScase [definition, in Cpo_streams_type]
DScaseEps [lemma, in Cpo_streams_type]
DScase_bot [lemma, in Cpo_streams_type]
DScase_cons [lemma, in Cpo_streams_type]
DScase_cont [lemma, in Cpo_streams_type]
DSCASE_cont [definition, in Cpo_streams_type]
DScase_cont_eq [lemma, in Cpo_streams_type]
DSCASE_cont_simpl [lemma, in Cpo_streams_type]
DScase_decomp [lemma, in Cpo_streams_type]
DScase_decomp_elim [lemma, in Cpo_streams_type]
DScase_eq_compat [lemma, in Cpo_streams_type]
DScase_eq_cons [lemma, in Cpo_streams_type]
DScase_eq_cons_elim [lemma, in Cpo_streams_type]
DScase_inv [lemma, in Cpo_streams_type]
DScase_is_cons [lemma, in Cpo_streams_type]
DScase_le_compat [lemma, in Cpo_streams_type]
DScase_le_cons [lemma, in Cpo_streams_type]
DSCASE_mon [definition, in Cpo_streams_type]
DSCASE_mon_cont [lemma, in Cpo_streams_type]
DSCASE_mon_simpl [lemma, in Cpo_streams_type]
DSCASE_simpl [lemma, in Cpo_streams_type]
DSCase_simpl [lemma, in Cpo_streams_type]
DSeq_intro_is_cons [lemma, in Cpo_streams_type]
DSeq_pred [lemma, in Cpo_streams_type]
DSeq_rec [lemma, in Cpo_streams_type]
DSle [inductive, in Cpo_streams_type]
DSleCon [constructor, in Cpo_streams_type]
DSleCon0 [lemma, in Cpo_streams_type]
DSleCon_exists_decomp [lemma, in Cpo_streams_type]
DSleCon_hd [lemma, in Cpo_streams_type]
DSleCon_tl [lemma, in Cpo_streams_type]
DSleEps [constructor, in Cpo_streams_type]
DSleEps_left [lemma, in Cpo_streams_type]
DSleEps_right [lemma, in Cpo_streams_type]
DSleEps_right_elim [lemma, in Cpo_streams_type]
DSle_app_bot_right_first [lemma, in Cpo_streams_type]
DSle_app_first_rem [lemma, in Cpo_streams_type]
DSle_app_first_rem_sym [lemma, in Cpo_streams_type]
DSle_decomp [lemma, in Cpo_streams_type]
DSle_first_app_bot_right [lemma, in Cpo_streams_type]
DSle_first_app_first [lemma, in Cpo_streams_type]
DSle_first_first_app [lemma, in Cpo_streams_type]
DSle_intro_cons [lemma, in Cpo_streams_type]
DSle_intro_is_cons [lemma, in Cpo_streams_type]
DSle_isCon [lemma, in Cpo_streams_type]
DSle_pred [lemma, in Cpo_streams_type]
DSle_pred_eq [lemma, in Cpo_streams_type]
DSle_pred_left [lemma, in Cpo_streams_type]
DSle_pred_left_elim [lemma, in Cpo_streams_type]
DSle_pred_right [lemma, in Cpo_streams_type]
DSle_pred_right_elim [lemma, in Cpo_streams_type]
DSle_rec [lemma, in Cpo_streams_type]
DSle_rec_eq [lemma, in Cpo_streams_type]
DSle_refl [lemma, in Cpo_streams_type]
DSle_trans [lemma, in Cpo_streams_type]
DSle_uncons [lemma, in Cpo_streams_type]
DStr [inductive, in Cpo_streams_type]
DStr_match [lemma, in Cpo_streams_type]
DS_bisimulation [lemma, in Cpo_streams_type]
DS_bisimulation2 [lemma, in Cpo_streams_type]
DS_bot [definition, in Cpo_streams_type]
DS_bot_eq [lemma, in Cpo_streams_type]
DS_bot_least [lemma, in Cpo_streams_type]
DS_inv [lemma, in Cpo_streams_type]
DS_lub [definition, in Cpo_streams_type]
DS_lubCon [lemma, in Cpo_streams_type]
DS_lubCon_inv [lemma, in Cpo_streams_type]
DS_lubn [definition, in Cpo_streams_type]
DS_lubn_inv [lemma, in Cpo_streams_type]
DS_lubn_pred_nth [lemma, in Cpo_streams_type]
DS_lubn_pred_nth_inv [lemma, in Cpo_streams_type]
DS_lub_inv [lemma, in Cpo_streams_type]
DS_lub_least [lemma, in Cpo_streams_type]
DS_lub_upper [lemma, in Cpo_streams_type]
DS_ord [definition, in Cpo_streams_type]
DS_to_list [definition, in Cpo_streams_type]

## E

Eps [constructor, in Cpo_streams_type]
Eps [definition, in Cpo_streams_type]
eqEps [lemma, in Cpo_streams_type]

## F

fCon [lemma, in Cpo_streams_type]
filter [definition, in Cpo_streams_type]
FILTER [definition, in Cpo_streams_type]
filterf [definition, in Cpo_streams_type]
Filterf [definition, in Cpo_streams_type]
Filterf_simpl [lemma, in Cpo_streams_type]
filterf_simpl [lemma, in Cpo_streams_type]
filter_bot [lemma, in Cpo_streams_type]
FILTER_eq [lemma, in Cpo_streams_type]
filter_eq_compat [lemma, in Cpo_streams_type]
filter_eq_cons [lemma, in Cpo_streams_type]
filter_le_compat [lemma, in Cpo_streams_type]
finite [inductive, in Cpo_streams_type]
finite_mon [lemma, in Cpo_streams_type]
fin_bot [constructor, in Cpo_streams_type]
fin_cons [constructor, in Cpo_streams_type]
First [definition, in Cpo_streams_type]
first [definition, in Cpo_streams_type]
FIRST [definition, in Cpo_streams_type]
firstf [definition, in Cpo_streams_type]
firstf_cont [lemma, in Cpo_streams_type]
firstf_simpl [lemma, in Cpo_streams_type]
first_app_first [lemma, in Cpo_streams_type]
first_bot [lemma, in Cpo_streams_type]
first_cons [lemma, in Cpo_streams_type]
first_cons_elim [lemma, in Cpo_streams_type]
first_cont [lemma, in Cpo_streams_type]
first_eq_bot [lemma, in Cpo_streams_type]
first_eq_compat [lemma, in Cpo_streams_type]
first_first_eq [lemma, in Cpo_streams_type]
first_is_cons [lemma, in Cpo_streams_type]
first_le_compat [lemma, in Cpo_streams_type]
first_simpl [lemma, in Cpo_streams_type]
FIRST_simpl [lemma, in Cpo_streams_type]

## I

infinite [inductive, in Cpo_streams_type]
infinite_le_compat [lemma, in Cpo_streams_type]
inf_intro [constructor, in Cpo_streams_type]
inleft [definition, in Cpo_streams_type]
isCon [inductive, in Cpo_streams_type]
isConCon [constructor, in Cpo_streams_type]
isConEps [constructor, in Cpo_streams_type]
isConEps_inv [lemma, in Cpo_streams_type]
isCon_intro [lemma, in Cpo_streams_type]
isCon_le [lemma, in Cpo_streams_type]
isCon_pred [lemma, in Cpo_streams_type]
isEps [definition, in Cpo_streams_type]
isEps_Eps [lemma, in Cpo_streams_type]
is_cons [definition, in Cpo_streams_type]
is_cons_app [lemma, in Cpo_streams_type]
is_cons_DScase [lemma, in Cpo_streams_type]
is_cons_elim [lemma, in Cpo_streams_type]
is_cons_eq_compat [lemma, in Cpo_streams_type]
is_cons_first [lemma, in Cpo_streams_type]
is_cons_intro [lemma, in Cpo_streams_type]
is_cons_le_compat [lemma, in Cpo_streams_type]
is_cons_map [lemma, in Cpo_streams_type]
is_cons_rem_app [lemma, in Cpo_streams_type]

## M

MAP [definition, in Cpo_streams_type]
map [definition, in Cpo_streams_type]
Mapf [definition, in Cpo_streams_type]
mapf [definition, in Cpo_streams_type]
mapf_simpl [lemma, in Cpo_streams_type]
Mapf_simpl [lemma, in Cpo_streams_type]
map_bot [lemma, in Cpo_streams_type]
map_eq [lemma, in Cpo_streams_type]
MAP_eq [lemma, in Cpo_streams_type]
map_eq_compat [lemma, in Cpo_streams_type]
map_eq_cons [lemma, in Cpo_streams_type]
map_is_cons [lemma, in Cpo_streams_type]
map_le_compat [lemma, in Cpo_streams_type]

## N

not_finite_infinite [lemma, in Cpo_streams_type]
not_infiniteBot [lemma, in Cpo_streams_type]
not_isEpsCon [lemma, in Cpo_streams_type]
not_is_consBot [lemma, in Cpo_streams_type]
not_le_consBot [lemma, in Cpo_streams_type]

## P

pred [definition, in Cpo_streams_type]
pred_nth [definition, in Cpo_streams_type]
pred_nthCon [lemma, in Cpo_streams_type]
pred_nthS [lemma, in Cpo_streams_type]
pred_nth_eq [lemma, in Cpo_streams_type]
pred_nth_switch [lemma, in Cpo_streams_type]

## R

rem [definition, in Cpo_streams_type]
Rem [definition, in Cpo_streams_type]
REM [definition, in Cpo_streams_type]
remf [definition, in Cpo_streams_type]
remf_cont [lemma, in Cpo_streams_type]
remf_simpl [lemma, in Cpo_streams_type]
rem_app [lemma, in Cpo_streams_type]
rem_app_is_cons [lemma, in Cpo_streams_type]
rem_app_le [lemma, in Cpo_streams_type]
rem_bot [lemma, in Cpo_streams_type]
rem_cons [lemma, in Cpo_streams_type]
rem_cont [lemma, in Cpo_streams_type]
rem_eq_bot [lemma, in Cpo_streams_type]
rem_eq_compat [lemma, in Cpo_streams_type]
rem_is_cons [lemma, in Cpo_streams_type]
rem_le_compat [lemma, in Cpo_streams_type]
rem_simpl [lemma, in Cpo_streams_type]
REM_simpl [lemma, in Cpo_streams_type]

## U

uncons [lemma, in Cpo_streams_type]

# Lemma Index

## A

appf_cont [in Cpo_streams_type]
appf_cont_par [in Cpo_streams_type]
Appf_simpl [in Cpo_streams_type]
appf_simpl [in Cpo_streams_type]
AppI_simpl [in Cpo_streams_type]
app_app_first [in Cpo_streams_type]
app_bot [in Cpo_streams_type]
app_bot_right_first [in Cpo_streams_type]
app_cons [in Cpo_streams_type]
app_cons_elim [in Cpo_streams_type]
app_cont [in Cpo_streams_type]
app_eq_bot [in Cpo_streams_type]
app_eq_compat [in Cpo_streams_type]
app_first_rem [in Cpo_streams_type]
app_is_cons [in Cpo_streams_type]
app_le_compat [in Cpo_streams_type]
app_mon_left [in Cpo_streams_type]
app_mon_right [in Cpo_streams_type]
APP_simpl [in Cpo_streams_type]
app_simpl [in Cpo_streams_type]
App_simpl [in Cpo_streams_type]

## C

chain_tl [in Cpo_streams_type]
chain_uncons [in Cpo_streams_type]
Cons_cont [in Cpo_streams_type]
cons_eq_compat [in Cpo_streams_type]
cons_le_compat [in Cpo_streams_type]
Cons_simpl [in Cpo_streams_type]
CONS_simpl [in Cpo_streams_type]
Con_compat [in Cpo_streams_type]
Con_exists_decompDSle [in Cpo_streams_type]
Con_hd_simpl [in Cpo_streams_type]
Con_tl_simpl [in Cpo_streams_type]

## D

decompCon [in Cpo_streams_type]
decompCon_eq [in Cpo_streams_type]
decompEps [in Cpo_streams_type]
decompEps_pred [in Cpo_streams_type]
decompEps_pred_sym [in Cpo_streams_type]
decomp_DSleCon [in Cpo_streams_type]
decomp_DSleCon_sym [in Cpo_streams_type]
decomp_eq [in Cpo_streams_type]
decomp_eqCon [in Cpo_streams_type]
decomp_ind [in Cpo_streams_type]
decomp_isCon [in Cpo_streams_type]
DScaseEps [in Cpo_streams_type]
DScase_bot [in Cpo_streams_type]
DScase_cons [in Cpo_streams_type]
DScase_cont [in Cpo_streams_type]
DScase_cont_eq [in Cpo_streams_type]
DSCASE_cont_simpl [in Cpo_streams_type]
DScase_decomp [in Cpo_streams_type]
DScase_decomp_elim [in Cpo_streams_type]
DScase_eq_compat [in Cpo_streams_type]
DScase_eq_cons [in Cpo_streams_type]
DScase_eq_cons_elim [in Cpo_streams_type]
DScase_inv [in Cpo_streams_type]
DScase_is_cons [in Cpo_streams_type]
DScase_le_compat [in Cpo_streams_type]
DScase_le_cons [in Cpo_streams_type]
DSCASE_mon_cont [in Cpo_streams_type]
DSCASE_mon_simpl [in Cpo_streams_type]
DSCASE_simpl [in Cpo_streams_type]
DSCase_simpl [in Cpo_streams_type]
DSeq_intro_is_cons [in Cpo_streams_type]
DSeq_pred [in Cpo_streams_type]
DSeq_rec [in Cpo_streams_type]
DSleCon0 [in Cpo_streams_type]
DSleCon_exists_decomp [in Cpo_streams_type]
DSleCon_hd [in Cpo_streams_type]
DSleCon_tl [in Cpo_streams_type]
DSleEps_left [in Cpo_streams_type]
DSleEps_right [in Cpo_streams_type]
DSleEps_right_elim [in Cpo_streams_type]
DSle_app_bot_right_first [in Cpo_streams_type]
DSle_app_first_rem [in Cpo_streams_type]
DSle_app_first_rem_sym [in Cpo_streams_type]
DSle_decomp [in Cpo_streams_type]
DSle_first_app_bot_right [in Cpo_streams_type]
DSle_first_app_first [in Cpo_streams_type]
DSle_first_first_app [in Cpo_streams_type]
DSle_intro_cons [in Cpo_streams_type]
DSle_intro_is_cons [in Cpo_streams_type]
DSle_isCon [in Cpo_streams_type]
DSle_pred [in Cpo_streams_type]
DSle_pred_eq [in Cpo_streams_type]
DSle_pred_left [in Cpo_streams_type]
DSle_pred_left_elim [in Cpo_streams_type]
DSle_pred_right [in Cpo_streams_type]
DSle_pred_right_elim [in Cpo_streams_type]
DSle_rec [in Cpo_streams_type]
DSle_rec_eq [in Cpo_streams_type]
DSle_refl [in Cpo_streams_type]
DSle_trans [in Cpo_streams_type]
DSle_uncons [in Cpo_streams_type]
DStr_match [in Cpo_streams_type]
DS_bisimulation [in Cpo_streams_type]
DS_bisimulation2 [in Cpo_streams_type]
DS_bot_eq [in Cpo_streams_type]
DS_bot_least [in Cpo_streams_type]
DS_inv [in Cpo_streams_type]
DS_lubCon [in Cpo_streams_type]
DS_lubCon_inv [in Cpo_streams_type]
DS_lubn_inv [in Cpo_streams_type]
DS_lubn_pred_nth [in Cpo_streams_type]
DS_lubn_pred_nth_inv [in Cpo_streams_type]
DS_lub_inv [in Cpo_streams_type]
DS_lub_least [in Cpo_streams_type]
DS_lub_upper [in Cpo_streams_type]

## E

eqEps [in Cpo_streams_type]

## F

fCon [in Cpo_streams_type]
Filterf_simpl [in Cpo_streams_type]
filterf_simpl [in Cpo_streams_type]
filter_bot [in Cpo_streams_type]
FILTER_eq [in Cpo_streams_type]
filter_eq_compat [in Cpo_streams_type]
filter_eq_cons [in Cpo_streams_type]
filter_le_compat [in Cpo_streams_type]
finite_mon [in Cpo_streams_type]
firstf_cont [in Cpo_streams_type]
firstf_simpl [in Cpo_streams_type]
first_app_first [in Cpo_streams_type]
first_bot [in Cpo_streams_type]
first_cons [in Cpo_streams_type]
first_cons_elim [in Cpo_streams_type]
first_cont [in Cpo_streams_type]
first_eq_bot [in Cpo_streams_type]
first_eq_compat [in Cpo_streams_type]
first_first_eq [in Cpo_streams_type]
first_is_cons [in Cpo_streams_type]
first_le_compat [in Cpo_streams_type]
first_simpl [in Cpo_streams_type]
FIRST_simpl [in Cpo_streams_type]

## I

infinite_le_compat [in Cpo_streams_type]
isConEps_inv [in Cpo_streams_type]
isCon_intro [in Cpo_streams_type]
isCon_le [in Cpo_streams_type]
isCon_pred [in Cpo_streams_type]
isEps_Eps [in Cpo_streams_type]
is_cons_app [in Cpo_streams_type]
is_cons_DScase [in Cpo_streams_type]
is_cons_elim [in Cpo_streams_type]
is_cons_eq_compat [in Cpo_streams_type]
is_cons_first [in Cpo_streams_type]
is_cons_intro [in Cpo_streams_type]
is_cons_le_compat [in Cpo_streams_type]
is_cons_map [in Cpo_streams_type]
is_cons_rem_app [in Cpo_streams_type]

## M

mapf_simpl [in Cpo_streams_type]
Mapf_simpl [in Cpo_streams_type]
map_bot [in Cpo_streams_type]
map_eq [in Cpo_streams_type]
MAP_eq [in Cpo_streams_type]
map_eq_compat [in Cpo_streams_type]
map_eq_cons [in Cpo_streams_type]
map_is_cons [in Cpo_streams_type]
map_le_compat [in Cpo_streams_type]

## N

not_finite_infinite [in Cpo_streams_type]
not_infiniteBot [in Cpo_streams_type]
not_isEpsCon [in Cpo_streams_type]
not_is_consBot [in Cpo_streams_type]
not_le_consBot [in Cpo_streams_type]

## P

pred_nthCon [in Cpo_streams_type]
pred_nthS [in Cpo_streams_type]
pred_nth_eq [in Cpo_streams_type]
pred_nth_switch [in Cpo_streams_type]

## R

remf_cont [in Cpo_streams_type]
remf_simpl [in Cpo_streams_type]
rem_app [in Cpo_streams_type]
rem_app_is_cons [in Cpo_streams_type]
rem_app_le [in Cpo_streams_type]
rem_bot [in Cpo_streams_type]
rem_cons [in Cpo_streams_type]
rem_cont [in Cpo_streams_type]
rem_eq_bot [in Cpo_streams_type]
rem_eq_compat [in Cpo_streams_type]
rem_is_cons [in Cpo_streams_type]
rem_le_compat [in Cpo_streams_type]
rem_simpl [in Cpo_streams_type]
REM_simpl [in Cpo_streams_type]

## U

uncons [in Cpo_streams_type]

# Constructor Index

## C

Con [in Cpo_streams_type]

## D

DSleCon [in Cpo_streams_type]
DSleEps [in Cpo_streams_type]

## E

Eps [in Cpo_streams_type]

## F

fin_bot [in Cpo_streams_type]
fin_cons [in Cpo_streams_type]

## I

inf_intro [in Cpo_streams_type]
isConCon [in Cpo_streams_type]
isConEps [in Cpo_streams_type]

# Inductive Index

## D

DSle [in Cpo_streams_type]
DStr [in Cpo_streams_type]

## F

finite [in Cpo_streams_type]

## I

infinite [in Cpo_streams_type]
isCon [in Cpo_streams_type]

# Definition Index

## A

app [in Cpo_streams_type]
App [in Cpo_streams_type]
APP [in Cpo_streams_type]
appf [in Cpo_streams_type]
Appf [in Cpo_streams_type]
AppI [in Cpo_streams_type]

## C

CONS [in Cpo_streams_type]
Cons [in Cpo_streams_type]
cons [in Cpo_streams_type]
cpred [in Cpo_streams_type]

## D

decomp [in Cpo_streams_type]
DS [in Cpo_streams_type]
DSCase [in Cpo_streams_type]
DSCASE [in Cpo_streams_type]
DScase [in Cpo_streams_type]
DSCASE_cont [in Cpo_streams_type]
DSCASE_mon [in Cpo_streams_type]
DS_bot [in Cpo_streams_type]
DS_lub [in Cpo_streams_type]
DS_lubn [in Cpo_streams_type]
DS_ord [in Cpo_streams_type]
DS_to_list [in Cpo_streams_type]

## E

Eps [in Cpo_streams_type]

## F

filter [in Cpo_streams_type]
FILTER [in Cpo_streams_type]
filterf [in Cpo_streams_type]
Filterf [in Cpo_streams_type]
First [in Cpo_streams_type]
first [in Cpo_streams_type]
FIRST [in Cpo_streams_type]
firstf [in Cpo_streams_type]

## I

inleft [in Cpo_streams_type]
isEps [in Cpo_streams_type]
is_cons [in Cpo_streams_type]

## M

MAP [in Cpo_streams_type]
map [in Cpo_streams_type]
Mapf [in Cpo_streams_type]
mapf [in Cpo_streams_type]

## P

pred [in Cpo_streams_type]
pred_nth [in Cpo_streams_type]

## R

rem [in Cpo_streams_type]
Rem [in Cpo_streams_type]
REM [in Cpo_streams_type]
remf [in Cpo_streams_type]

# Library Index

## C

Cpo_streams_type

 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (238 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (179 entries) Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (9 entries) Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (5 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (44 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)

This page has been generated by coqdoc