### Profile

Statistics
| Branch: | Tag: | Revision:

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

 1 ```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. ``` ```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 eqst_apply : forall {A B}, forall (f1 f2 : Stream (A -> B)), forall (a1 a2 : Stream A), ``` ``` EqSt f1 f2 -> EqSt a1 a2 -> EqSt (apply f1 a1) (apply f2 a2). ``` ```Proof. ``` ```intros A B. ``` ```cofix Hcoind. ``` ```destruct f1 as (vf1, f1'). ``` ```destruct f2 as (vf2, f2'). ``` ```destruct a1 as (va1, a1'). ``` ```destruct a2 as (va2, a2'). ``` ```intros Hf Ha. ``` ```destruct Hf. ``` ```destruct Ha. ``` ```apply eqst. ``` ``` simpl. ``` ``` simpl in H. ``` ``` simpl in H0. ``` ``` subst. ``` ``` reflexivity. ``` ``` apply Hcoind. ``` ``` exact Hf. ``` ``` exact Ha. ``` ```Qed. ``` ```Definition zip {A B} (s : Stream A * Stream B) := apply (apply (lift (fun a b => (a, b))) (fst s)) (snd s). ``` ```Lemma eqst_zip : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), ``` ``` EqSt s1 s1' -> EqSt s2 s2' -> EqSt (zip (s1, s2)) (zip (s1', s2')). ``` ```Proof. ``` ```intros A B. ``` ```cofix proof. ``` ```intros. ``` ```destruct s1; destruct s1'; destruct s2; destruct s2'. ``` ```apply eqst. ``` ``` simpl. ``` ``` inversion H. ``` ``` inversion H0. ``` ``` simpl in H1. ``` ``` simpl in H3. ``` ``` subst. ``` ``` reflexivity. ``` ``` apply proof. ``` ``` inversion H. ``` ``` exact H2. ``` ``` inversion H0. ``` ``` exact H2. ``` ```Qed. ``` ```Lemma zip_fst : 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_snd : 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_pair : forall {A B}, forall (s1 s1' : Stream A) (s2 s2' : Stream B), ``` ``` EqSt (zip (s1, s2)) (zip (s1', s2')) -> EqSt s1 s1' /\ EqSt s2 s2'. ``` ```Proof. ``` ```intros. ``` ```split. ``` ``` eapply zip_fst. ``` ``` apply H. ``` ``` eapply zip_snd. ``` ``` apply H. ``` ```Qed. ``` ```Definition unzip {A B} (s : Stream (A*B)) := (apply (lift (@fst _ _)) s, apply (lift (@snd _ _)) s). ``` ```Lemma fst_unzip_zip : 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 snd_unzip_zip : 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 zip_unzip : 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. ``` ```(* ``` ```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. ``` ```*) ``` ```Theorem eqst_ForAll : forall {A} {P : Stream A -> Prop}, (forall s s', EqSt s s' -> P s -> P s') -> forall {s s'}, EqSt s s' -> ForAll P s -> ForAll P s'. ``` ```Proof. ``` ```intros A P HP. ``` ```cofix proof. ``` ```destruct s as (s0, sq). ``` ```destruct s' as (s0', sq'). ``` ```intros Heq H. ``` ```inversion H. ``` ```apply HereAndFurther. ``` ``` exact (HP _ _ Heq H0). ``` ``` apply (proof sq sq'). ``` ``` inversion Heq. ``` ``` assumption. ``` ``` 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)). ``` ```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. ``` ```Definition concat {A} (prefix : list A) (suffix : Stream A) : Stream A := ``` ``` List.fold_left (fun q t => Cons t q) prefix suffix. ``` ```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 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 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. ``` ```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. ``` ```admit. ``` ```(*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 : forall {A} (P : Stream A -> Prop) (s : Stream A), ``` ``` ForAll P s -> ForAll (fun s' => P (apply (lift (@snd _ _)) s')) (history s). ``` ```Proof. ``` ```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 => (I t) \/ ``` ``` match q with ``` ``` | List.nil => False ``` ``` | List.cons t' q' => (T t t') /\ (prefix I T k' q) ``` ``` end ``` ``` end ``` ``` end. ``` ```Theorem inv_prefix : 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. ``` ```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. ```