### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec / optim / oversampling / streams2_lus.v @ 6a93d814

History | View | Annotate | Download (17.8 KB)

1 2 3 6a93d814 xthirioux ```Definition mapT (F : Type -> Type) {A B} := (A -> B) -> (F A) -> (F B). ``` ```Definition applyT (F : Type -> Type) {A B} := (F (A -> B)) -> (F A) -> (F B). ``` ```Definition option_apply {A B} : @applyT option A B := ``` ``` fun f a => ``` ``` match f, a with ``` ``` | Some f, Some a => Some (f a) ``` ``` | _ , _ => None ``` ``` end. ``` ```Require Import Streams. ``` ```Require List. ``` ```Require Import Setoid. ``` ```Axiom eqst_eq : forall {A} (s s' : Stream A), EqSt s s' -> s = s'. ``` ```Theorem inv_inv : forall {A} (P : Stream A -> Prop) (s : Stream A), ForAll P s -> ForAll (fun s' => ForAll P s') s. ``` ```Proof. ``` ```intros A P. ``` ```cofix proof. ``` ```destruct s as (s0, s'). ``` ```intro H. ``` ```apply HereAndFurther. ``` ``` exact H. ``` ``` simpl. ``` ``` apply proof. ``` ``` inversion H. ``` ``` assumption. ``` ```Qed. ``` ```Theorem evt_inv : forall {A} (P Q : Stream A -> Prop) (s : Stream A), ``` ``` ForAll P s -> Exists Q s -> Exists (fun s' => P s' /\ Q s') s. ``` ```Proof. ``` ```induction 2. ``` ``` apply Here. ``` ``` inversion H. ``` ``` intuition. ``` ``` apply Further. ``` ``` apply IHExists. ``` ``` inversion H. ``` ``` assumption. ``` ```Qed. ``` ```CoFixpoint ForAll_apply {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll P s) -> (ForAll (fun s => P s -> Q s) s) -> (ForAll Q s) := ``` ``` fun s always_p always_pq => ``` ``` match always_p, always_pq with ``` ``` | (HereAndFurther p_s always_p'), (HereAndFurther pq_s always_pq') => HereAndFurther s (pq_s p_s) (ForAll_apply (tl s) always_p' always_pq') ``` ``` end. ``` ```CoFixpoint necessitation {A} {P : Stream A -> Prop} (I : forall s, P s) s : ForAll P s := ``` ``` HereAndFurther s (I s) (necessitation I (tl s)). ``` ```Definition concat {A} (prefix : list A) (suffix : Stream A) : Stream A := ``` ``` List.fold_left (fun q t => Cons t q) prefix suffix. ``` ```Theorem eqst_concat : forall {A} pfx (sfx sfx' : Stream A), EqSt sfx sfx' -> EqSt (concat pfx sfx) (concat pfx sfx'). ``` ```Proof. ``` ```induction pfx. ``` ``` auto. ``` ``` simpl. ``` ``` intros. ``` ``` apply IHpfx. ``` ``` apply eqst. ``` ``` reflexivity. ``` ``` exact H. ``` ```Qed. ``` ```Theorem evt_id : forall {A} (s : Stream A), Exists (fun s' => s = s') s. ``` ```Proof. ``` ```intros. ``` ```apply Here. ``` ```reflexivity. ``` ```Qed. ``` ```Theorem evt_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), Exists P s -> Exists P (concat p s). ``` ```Proof. ``` ```induction p. ``` ``` trivial. ``` ``` intros s H. ``` ``` apply (IHp (Cons a s)). ``` ``` apply Further. ``` ``` exact H. ``` ```Qed. ``` ```Theorem inv_concat : forall {A} (P : Stream A -> Prop) p (s : Stream A), ForAll P (concat p s) -> ForAll P s. ``` ```Proof. ``` ```induction p. ``` ``` trivial. ``` ``` simpl. ``` ``` intros s H. ``` ``` generalize (IHp (Cons a s) H). ``` ``` intro H'. ``` ``` inversion H'. ``` ``` assumption. ``` ```Qed. ``` ``` ``` ```CoFixpoint lift {A} (v : A) := Cons v (lift v). ``` ```Lemma hd_lift : forall {A} {v : A}, hd (lift v) = v. ``` ```Proof. ``` ```reflexivity. ``` ```Qed. ``` ```Lemma tl_lift : forall {A} {v : A}, tl (lift v) = lift v. ``` ```Proof. ``` ```reflexivity. ``` ```Qed. ``` ```CoFixpoint apply {A B} : @applyT Stream A B := ``` ``` fun f a => ``` ``` match f, a with ``` ``` | (Cons f0 f'), (Cons a0 a') => Cons (f0 a0) (apply f' a') ``` ``` end. ``` ```Lemma hd_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, hd (apply f a) = (hd f) (hd a). ``` ```Proof. ``` ```destruct f; destruct a. ``` ```reflexivity. ``` ```Qed. ``` ```Lemma tl_apply : forall {A B} {f : Stream (A -> B)} {a : Stream A}, tl (apply f a) = apply (tl f) (tl a). ``` ```Proof. ``` ```destruct f; destruct a. ``` ```reflexivity. ``` ```Qed. ``` ```Lemma cons_apply : forall {A B} {f0 : A -> B} {f' : Stream (A -> B)} {a0 : A} {a' : Stream A}, EqSt (apply (Cons f0 f') (Cons a0 a')) (Cons (f0 a0) (apply f' a')). ``` ```Proof. ``` ```intros. ``` ```apply eqst. ``` ``` reflexivity. ``` ``` apply EqSt_reflex. ``` ```Qed. ``` ```Theorem inv_map : forall {A B} (f : A -> B) P (s : Stream A), ForAll P (apply (lift f) s) -> ForAll (fun s' => P (apply (lift f) s')) s. ``` ```Proof. ``` ```intros A B f P. ``` ```cofix proof. ``` ```destruct s as (s0, s'). ``` ```intro H. ``` ```inversion H. ``` ```apply HereAndFurther. ``` ``` assumption. ``` ``` simpl. ``` ``` apply proof. ``` ``` assumption. ``` ```Qed. ``` ```Theorem map_inv : forall {A B} (f : A -> B) P (s : Stream A), ForAll (fun s' => P (apply (lift f) s')) s -> ForAll P (apply (lift f) s). ``` ```Proof. ``` ```intros A B f P. ``` ```cofix proof. ``` ```destruct s as (s0, s'). ``` ```intro H. ``` ```inversion H. ``` ```apply HereAndFurther. ``` ``` assumption. ``` ``` simpl. ``` ``` apply proof. ``` ``` assumption. ``` ```Qed. ``` ```Theorem evt_map : forall {A B} (f : A -> B) P (s : Stream A), Exists P (apply (lift f) s) -> Exists (fun s' => P (apply (lift f) s')) s. ``` ```Proof. ``` ```intros A B f P s. ``` ```remember (apply (lift f) s) as ss. ``` ```intro H. ``` ```revert s Heqss. ``` ```induction H. ``` ``` intros. ``` ``` apply Here. ``` ``` rewrite <- Heqss. ``` ``` exact H. ``` ``` intros. ``` ``` apply Further. ``` ``` apply (IHExists (tl s)). ``` ``` rewrite <- tl_lift. ``` ``` rewrite <- tl_apply. ``` ``` apply f_equal. ``` ``` exact Heqss. ``` ```Qed. ``` ```Theorem map_evt : forall {A B} (f : A -> B) P (s : Stream A), Exists (fun s' => P (apply (lift f) s')) s -> Exists P (apply (lift f) s). ``` ```Proof. ``` ```intros A B f P s. ``` ```intro H. ``` ```induction H. ``` ``` apply Here. ``` ``` exact H. ``` ``` apply Further. ``` ``` rewrite tl_apply. ``` ``` rewrite tl_lift. ``` ``` exact IHExists. ``` ```Qed. ``` ```Definition zip {A B} (s : Stream A * Stream B) := apply (apply (lift (fun a b => (a, b))) (fst s)) (snd s). ``` ```Lemma zip_fst_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), ``` ``` EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s1 s1'. ``` ```Proof. ``` ```intros A B. ``` ```cofix proof. ``` ```destruct s1; destruct s1'; destruct s2; destruct s2'. ``` ```intro. ``` ```inversion H. ``` ```apply eqst. ``` ``` simpl in H0. ``` ``` simpl in H1. ``` ``` injection H0. ``` ``` intros. ``` ``` subst. ``` ``` reflexivity. ``` ``` eapply proof. ``` ``` apply H1. ``` ```Qed. ``` ```Lemma zip_fst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), ``` ``` zip (s1, s2) = zip (s1', s2') -> s1 = s1'. ``` ```Proof. ``` ```intros. ``` ```apply eqst_eq. ``` ```apply (zip_fst_eqst s1 s1' s2 s2'). ``` ```rewrite H. ``` ```apply EqSt_reflex. ``` ```Qed. ``` ```Lemma zip_snd_eqst : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), ``` ``` EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s2 s2'. ``` ```Proof. ``` ```intros A B. ``` ```cofix proof. ``` ```destruct s1; destruct s1'; destruct s2; destruct s2'. ``` ```intro. ``` ```inversion H. ``` ```apply eqst. ``` ``` simpl in H0. ``` ``` simpl in H1. ``` ``` injection H0. ``` ``` intros. ``` ``` subst. ``` ``` reflexivity. ``` ``` eapply proof. ``` ``` apply H1. ``` ```Qed. ``` ```Lemma zip_snd : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), ``` ``` zip (s1, s2) = zip (s1', s2') -> s2 = s2'. ``` ```Proof. ``` ```intros. ``` ```apply eqst_eq. ``` ```apply (zip_snd_eqst s1 s1' s2 s2'). ``` ```rewrite H. ``` ```apply EqSt_reflex. ``` ```Qed. ``` ```Definition unzip {A B} (s : Stream (A*B)) := (apply (lift (@fst _ _)) s, apply (lift (@snd _ _)) s). ``` ```Lemma fst_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@fst _ _)) (zip (s1, s2))) s1. ``` ```Proof. ``` ```intros A B. ``` ```cofix proof. ``` ```destruct s1; destruct s2. ``` ```apply eqst. ``` ``` reflexivity. ``` ``` apply proof. ``` ```Qed. ``` ```Lemma fst_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@fst _ _)) (zip (s1, s2)) = s1. ``` ```Proof. ``` ```intros. ``` ```apply eqst_eq. ``` ```apply fst_zip_eqst. ``` ```Qed. ``` ```Lemma snd_zip_eqst : forall {A B} (s1 : Stream A) (s2 : Stream B), EqSt (apply (lift (@snd _ _)) (zip (s1, s2))) s2. ``` ```Proof. ``` ```intros A B. ``` ```cofix proof. ``` ```destruct s1; destruct s2. ``` ```apply eqst. ``` ``` reflexivity. ``` ``` apply proof. ``` ```Qed. ``` ```Lemma snd_zip : forall {A B} (s1 : Stream A) (s2 : Stream B), apply (lift (@snd _ _)) (zip (s1, s2)) = s2. ``` ```Proof. ``` ```intros. ``` ```apply eqst_eq. ``` ```apply snd_zip_eqst. ``` ```Qed. ``` ```Lemma zip_unzip_eqst : forall {A B} (s : Stream (A*B)), EqSt (zip (unzip s)) s. ``` ```Proof. ``` ```intros A B. ``` ```cofix proof. ``` ```destruct s. ``` ```apply eqst. ``` ``` simpl. ``` ``` destruct p. ``` ``` reflexivity. ``` ``` simpl. ``` ``` apply proof. ``` ```Qed. ``` ```Lemma zip_unzip : forall {A B} (s : Stream (A*B)), zip (unzip s) = s. ``` ```Proof. ``` ```intros. ``` ```apply eqst_eq. ``` ```apply zip_unzip_eqst. ``` ```Qed. ``` ```(* ``` ```CoInductive transition {A} (T : A -> A -> Prop) : Stream A -> Prop := ``` ```| Tick : forall a0 a1 s'', T a0 a1 -> transition T (Cons a1 s'') -> transition T (Cons a0 (Cons a1 s'')). ``` ```Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : Stream A -> Prop := ``` ``` match k with ``` ``` | 0 => fun s => True ``` ``` | S k' => fun s => (I (hd s) \/ (T (hd s) (hd (tl s)) /\ prefix I T k' (tl s))) ``` ``` end. ``` ```Lemma I_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) k (s : Stream A), I (hd s) -> prefix I T k s. ``` ```Proof. ``` ```destruct k. ``` ``` simpl. ``` ``` trivial. ``` ``` simpl. ``` ``` left. ``` ``` trivial. ``` ```Qed. ``` ```Lemma T_prefix : forall {A} (I : A -> Prop) (T : A -> A -> Prop) k (s : Stream A), T (hd s) (hd (tl s)) -> prefix I T k (tl s) -> prefix I T k s. ``` ```Proof. ``` ```destruct k. ``` ``` simpl. ``` ``` trivial. ``` ``` simpl. ``` ``` right. ``` ``` trivial. ``` ```Qed. ``` ```Lemma prefix_mono_k : forall {A} I T k (s : Stream A), prefix I T (S k) s -> prefix I T k s. ``` ```Proof. ``` ```Qed. ``` ```*) ``` ```CoFixpoint history_rec {A} (past : list A) (s : Stream A) : Stream (list A * A) := ``` ``` match s with ``` ``` | Cons s0 s' => Cons (past, s0) (history_rec (cons s0 past) s') ``` ``` end. ``` ```Definition history {A} (s : Stream A) : Stream (list A * A) := history_rec nil s. ``` ```Theorem eqst_history_rec : forall {A} (pfx : list A) (sfx sfx' : Stream A), ``` ``` EqSt sfx sfx' -> EqSt (history_rec pfx sfx) (history_rec pfx sfx'). ``` ```Proof. ``` ```intros A. ``` ```cofix proof. ``` ```destruct sfx as (sfx0, sfxq). ``` ```destruct sfx' as (sfx0', sfxq'). ``` ```intro H. ``` ```inversion H. ``` ```simpl in H0. ``` ```rewrite H0. ``` ```apply eqst. ``` ``` reflexivity. ``` ``` apply (proof _ sfxq sfxq'). ``` ``` assumption. ``` ```Qed. ``` ```Theorem eqst_history : forall {A} (sfx sfx' : Stream A), ``` ``` EqSt sfx sfx' -> EqSt (history sfx) (history sfx'). ``` ```Proof. ``` ```intros. ``` ```apply eqst_history_rec. ``` ```assumption. ``` ```Qed. ``` ```Theorem unzip_history_rec : forall {A} (pfx : list A) (sfx : Stream A), EqSt (snd (unzip (history_rec pfx sfx))) sfx. ``` ```Proof. ``` ```intro A. ``` ```cofix proof. ``` ```destruct sfx as (sfx0, sfx'). ``` ```apply eqst. ``` ``` reflexivity. ``` ``` apply proof. ``` ```Qed. ``` ```Theorem unzip_history : forall {A} (s : Stream A), EqSt (snd (unzip (history s))) s. ``` ```Proof. ``` ```unfold history. ``` ```intros. ``` ```apply unzip_history_rec. ``` ```Qed. ``` ```Theorem hd_history_rec : forall {A} p (s : Stream A), hd (history_rec p s) = (p, hd s). ``` ```Proof. ``` ```destruct s. ``` ```reflexivity. ``` ```Qed. ``` ```Theorem hd_history : forall {A} (s : Stream A), hd (history s) = (nil, hd s). ``` ```Proof. ``` ```destruct s. ``` ```reflexivity. ``` ```Qed. ``` ```Definition snoc {A} (a : A) (l : list A) := app l (cons a nil). ``` ```Theorem tl_history_rec : forall {A} p (s : Stream A), tl (history_rec p s) = history_rec (cons (hd s) p) (tl s). ``` ```Proof. ``` ```intros. ``` ```destruct s. ``` ```reflexivity. ``` ```Qed. ``` ```Theorem tl_history_rec : forall {A} p (s : Stream A), EqSt (tl (history_rec p s)) (apply (lift (fun pfx_sfx => (app (fst pfx_sfx) (cons (hd s) p), (snd pfx_sfx)))) (history_rec p (tl s))). ``` ```Proof. ``` ```intros. ``` ```Qed. ``` ```Theorem tl_history : forall {A} (s : Stream A), EqSt (tl (history s)) (apply (lift (fun pfx_sfx => (snoc (hd s) (fst pfx_sfx), (snd pfx_sfx)))) (history (tl s))). ``` ```Proof. ``` ```intros. ``` ```Qed. ``` ```CoFixpoint cojoin {A} (s : Stream A) : Stream (Stream A) := ``` ``` match s with ``` ``` | Cons _ s' => Cons s (cojoin s') ``` ``` end. ``` ```(* ``` ```Theorem eqst_cojoin : forall {A} (s s' : Stream A), EqSt s s' -> EqSt (cojoin s) (cojoin s'). ``` ```Proof. ``` ```intros A. ``` ```cofix proof. ``` ```destruct s as (s0, sq). ``` ```destruct s' as (s0', sq'). ``` ```intro H. ``` ```inversion H. ``` ```simpl in H0. ``` ```rewrite H0. ``` ```Qed. ``` ```Theorem inv_history_rec : forall {A} p (s : Stream A), ``` ``` let (fst_s, snd_s) := unzip (history_rec p s) in ForAll (fun s' => EqSt (hd s') (concat p s)) (apply (apply (lift concat) fst_s) (cojoin snd_s)). ``` ```Proof. ``` ```intro A. ``` ```cofix proof. ``` ```destruct s as (s0, s'). ``` ```apply HereAndFurther. ``` ``` apply eqst_concat. ``` ``` apply unzip_history_rec. ``` ``` apply (proof (cons s0 p) s'). ``` ```Qed. ``` ```Theorem inv_history : forall {A} (s : Stream A), ``` ``` let (fst_s, snd_s) := unzip (history s) in ForAll (fun s' => EqSt (hd s') s) (apply (apply (lift concat) fst_s) (cojoin snd_s)). ``` ```Proof. ``` ```intros. ``` ```apply inv_history_rec. ``` ```Qed. ``` ```*) ``` ```Theorem inv_history_rec : forall {A} p (s : Stream A), ``` ``` ForAll (fun s' => EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) (concat p s)) (history_rec p s). ``` ```Proof. ``` ```intro A. ``` ```cofix proof. ``` ```destruct s as (s0, s'). ``` ```apply HereAndFurther. ``` ``` apply eqst_concat. ``` ``` apply unzip_history_rec. ``` ``` apply (proof (cons s0 p) s'). ``` ```Qed. ``` ```Theorem inv_history : forall {A} (s : Stream A), ``` ``` ForAll (fun s' => EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s) (history s). ``` ```Proof. ``` ```intros. ``` ```assert (s = concat nil s). ``` ``` reflexivity. ``` ``` rewrite H. ``` ``` rewrite <- H in |- * at 1. ``` ``` apply inv_history_rec. ``` ```Qed. ``` ```Theorem inv_mono_history_rec : forall {A} (P : Stream A -> Prop) p (s : Stream A), ``` ``` ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s). ``` ```Proof. ``` ```intros. ``` ```apply inv_map. ``` ```generalize (eqst_eq _ _ (unzip_history_rec p s)). ``` ```simpl. ``` ```intro Hs. ``` ```rewrite Hs. ``` ```exact H. ``` ```Qed. ``` ```Theorem inv_mono_history : forall {A} (P : Stream A -> Prop) (s : Stream A), ``` ``` ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s). ``` ```Proof. ``` ```intros. ``` ```apply inv_mono_history_rec. ``` ```assumption. ``` ```Qed. ``` ```Theorem history_rec_mono_inv : forall {A} (P : Stream A -> Prop) p (s : Stream A), ``` ``` ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history_rec p s) -> ForAll P s. ``` ```Proof. ``` ```intros. ``` ```rewrite <- (eqst_eq _ _ (unzip_history_rec p s)). ``` ```apply map_inv. ``` ```exact H. ``` ```Qed. ``` ```Theorem history_mono_inv : forall {A} (P : Stream A -> Prop) (s : Stream A), ``` ``` ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s) -> ForAll P s. ``` ```Proof. ``` ```intros. ``` ```apply history_rec_mono_inv with (p := nil). ``` ```assumption. ``` ```Qed. ``` ```Fixpoint prefix {A} (I : A -> Prop) (T : A -> A -> Prop) (k : nat) : list A -> Prop := ``` ``` match k with ``` ``` | 0 => fun p => True ``` ``` | S k' => fun p => ``` ``` match p with ``` ``` | List.nil => True ``` ``` | List.cons t q => ``` ``` match q with ``` ``` | List.nil => (I t) ``` ``` | List.cons t' q' => (T t' t) /\ (prefix I T k' q) ``` ``` end ``` ``` end ``` ``` end. ``` ```Theorem prefix_mono_k : forall {A} I T k (p : list A), prefix I T (S k) p -> prefix I T k p. ``` ```Proof. ``` ```induction k. ``` ``` simpl. ``` ``` trivial. ``` ``` simpl. ``` ``` intuition. ``` ``` destruct p. ``` ``` trivial. ``` ``` intuition. ``` ``` destruct p. ``` ``` intuition. ``` ``` intuition. ``` ```Qed. ``` ```Theorem prefix_mono : forall {A} (I I' : A -> Prop) (T T' : A -> A -> Prop) k (p : list A), (forall s, I s -> I' s) -> (forall s s', T s s' -> T' s s') -> prefix I T k p -> prefix I' T' k p. ``` ```Proof. ``` ```induction k. ``` ``` trivial. ``` ``` simpl. ``` ``` destruct p. ``` ``` trivial. ``` ``` intros. ``` ``` destruct p. ``` ``` intuition. ``` ``` intuition. ``` ```Qed. ``` ```Theorem kinduction : forall {A} (P : A -> Prop) k (s : Stream A), ``` ``` ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) (history s) ``` ``` -> ForAll (fun s' => P (hd s')) s. ``` ```Proof. ``` ```induction k. ``` ``` simpl. ``` ``` intros. ``` ``` apply history_mono_inv. ``` ``` eapply ForAll_apply. ``` ``` apply H. ``` ``` apply necessitation. ``` ``` intros. ``` ``` rewrite hd_apply. ``` ``` rewrite hd_lift. ``` ``` intuition. ``` ``` intros. ``` ``` apply IHk. ``` ``` eapply ForAll_apply. ``` ``` apply H. ``` ``` apply necessitation. ``` ``` intros. ``` ``` apply H0. ``` ``` simpl. ``` ```Qed. ``` ```Theorem inv_prefix_history_rec : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A), ``` ``` I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) (concat p s) -> ``` ``` forall k, ``` ``` ForAll (fun s' => prefix I T k (fst (hd s'))) (history_rec p s). ``` ```Proof. ``` ```Qed. ``` ```Theorem inv_prefix_history : forall {A} (I : A -> Prop) (T : A -> A -> Prop) (s : Stream A), ``` ``` I (hd s) -> ForAll (fun s' => T (hd s') (hd (tl s'))) s -> ``` ``` forall k, ``` ``` ForAll (fun s' => prefix I T k (fst (hd s'))) (history s). ``` ```Proof. ``` ```intros A I T. ``` ```cofix proof. ``` ```intros. ``` ```Qed. ``` ```Definition _arrow := Cons true (lift false). ``` ```Definition ite {A} (s_if : Stream bool) (s_then s_else : Stream A) := ``` ``` apply (apply (apply (lift (fun (c : bool) (t e : A) => if c then t else e)) s_if) s_then) s_else. ``` ```Lemma hd_ite : forall {A}, forall (c : Stream bool) (t e : Stream A), ``` ``` hd (ite c t e) = if (hd c) then (hd t) else (hd e). ``` ```Proof. ``` ```destruct c; destruct t; destruct e. ``` ```reflexivity. ``` ```Qed. ``` ```Lemma tl_ite : forall {A}, forall (c : Stream bool) (t e : Stream A), ``` ``` tl (ite c t e) = ite (tl c) (tl t) (tl e). ``` ```Proof. ``` ```destruct c; destruct t; destruct e. ``` ```reflexivity. ``` ```Qed. ``` ```Theorem eqst_ite : forall {A}, forall (c1 c2 : Stream bool) (t1 t2 e1 e2 : Stream A), ``` ``` EqSt c1 c2 -> EqSt t1 t2 -> EqSt e1 e2 -> EqSt (ite c1 t1 e1) (ite c2 t2 e2). ``` ```Proof. ``` ```intros. ``` ```apply eqst_apply. ``` ``` apply eqst_apply. ``` ``` apply eqst_apply. ``` ``` apply EqSt_reflex. ``` ``` assumption. ``` ``` assumption. ``` ``` assumption. ``` ```Qed. ``` ```Variable pre : forall {A}, Stream A -> Stream A. ``` ```Axiom pre_spec : forall {A}, forall (s : Stream A), EqSt (tl (pre s)) s. ``` ```Variable when : forall {A}, Stream bool -> Stream A -> Stream A. ``` ```Axiom when_spec : forall {A}, forall (c : Stream bool) (s : Stream A), forall n, hd (Str_nth_tl n c) = true -> hd (Str_nth_tl n (when c s)) = hd (Str_nth_tl n s). ``` ```Require Import Bool. ``` ```Definition bnot (s : Stream bool) := apply (lift negb) s. ``` ```Definition band (s1 s2 : Stream bool) := apply (apply (lift andb) s1) s2. ``` ```Definition bor (s1 s2 : Stream bool) := apply (apply (lift orb) s1) s2. ``` ```Require Import ZArith. ``` ```Definition iplus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 + i2)%Z)) s1) s2. ``` ```Definition iminus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 - i2)%Z)) s1) s2. ``` ```Definition imult (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 * i2)%Z)) s1) s2. ``` ```Definition idiv (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 / i2)%Z)) s1) s2. ``` ```Definition imod (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => Zmod i1 i2)) s1) s2. ``` ```Definition ieq (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Eq => true | _ => false end)) s1) s2. ``` ```Definition ilt (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Lt => true | _ => false end)) s1) s2. ``` ```(* sémantique dénotationnelle de f *) ``` ```Definition denot_f (x cpt y : Stream Z) := ``` ``` (EqSt y (iplus x (lift 1%Z))) /\ (EqSt cpt (iplus (ite _arrow (lift 0%Z) (pre cpt)) (lift 1%Z))). ``` ```(* sémantique axiomatique de f, simplifiée *) ``` ```Definition mem_f := (bool * Z)%type. ``` ```Definition ni_2 (mem : mem_f) := fst mem. ``` ```Definition __f_2 (mem : mem_f) := snd mem. ``` ```Definition init_f (mem : mem_f) := ni_2 mem = true. ``` ```Definition trans_f (x cpt y : Z) (mem_in mem_out : mem_f) := ``` ``` (cpt = ((if bool_dec (ni_2 mem_in) true then 0 else (__f_2 mem_in)) + 1)%Z) ``` ``` /\ (y = (x + 1)%Z) ``` ``` /\ (ni_2 mem_out) = false ``` ``` /\ (__f_2 mem_out) = cpt. ``` ```Definition trans_f' (s s' : (Z * (Z * Z)) * mem_f) := ``` ``` match s, s' with ``` ``` | ((x, (cpt, y)), mem), ((x', (cpt', y')), mem') => trans_f x cpt y mem mem' ``` ``` end. ``` ```Lemma Cons_inj : forall {A}, forall a a' (s s' : Stream A), Cons a s = Cons a' s' -> a = a' /\ s = s'. ``` ```Proof. ``` ```intros. ``` ```injection H. ``` ```intuition. ``` ```Qed. ``` ```Theorem raffinement : forall (x cpt y : Stream Z) (mem : Stream mem_f), ``` ``` (init_f (hd mem) /\ transition trans_f' (zip ((zip (x, (zip (cpt, y)))), mem))) ``` ``` -> ``` ``` denot_f x cpt y. ``` ```Proof. ``` ```intros. ``` ```apply zip_pair. ``` ```revert x cpt y mem H. ``` ```cofix proof. ``` ```intros. ``` ```intros. ``` ```split. ``` ``` revert x cpt y mem H. ``` ``` cofix proof. ``` ``` intros. ``` ``` destruct H. ``` ``` destruct x as (x0, x'); destruct cpt as (cpt0, cpt'); destruct y as (y0, y'). ``` ``` destruct mem as (mem0, mem'). ``` ``` inversion H0. ``` ``` apply eqst. ``` ``` simpl. ``` ``` unfold zip in H1. ``` ``` simpl in H1. ``` ``` generalize (f_equal (@hd _) H1). ``` ``` simpl. ``` ``` intro. ``` ``` subst. ``` ``` generalize (f_equal (@tl _) H1). ``` ``` simpl. ``` ```Qed. ```