### Profile

 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. ``` ```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 ForAll_reinforce {A} {P Q : (Stream A -> Prop)} : forall s, (ForAll (fun s => P s /\ Q s) s) -> (ForAll Q s). ``` ```Proof. ``` ```intros. ``` ```eapply ForAll_apply. ``` ``` apply H. ``` ``` apply necessitation. ``` ``` intuition. ``` ```Defined. ``` ```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 concat_eqst : forall {A} pfx pfx' (sfx sfx' : Stream A), List.length pfx = List.length pfx' -> EqSt (concat pfx sfx) (concat pfx' sfx') -> pfx = pfx' /\ EqSt sfx sfx'. ``` ```Proof. ``` ```induction pfx. ``` ``` destruct pfx'. ``` ``` intuition. ``` ``` discriminate. ``` ``` destruct pfx'. ``` ``` discriminate. ``` ``` simpl. ``` ``` intros. ``` ``` injection H. ``` ``` clear H; intro H. ``` ``` generalize (IHpfx _ _ _ H H0). ``` ``` destruct 1. ``` ``` inversion H2. ``` ``` simpl in H3. ``` ``` simpl in H4. ``` ``` subst. ``` ``` intuition. ``` ```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. ``` ```Theorem inv_eq_eqst : forall {A} (s s' : Stream A), ``` ``` ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')) -> EqSt s s'. ``` ```Proof. ``` ```intro A. ``` ```cofix proof. ``` ```destruct s as (s0, s'). ``` ```destruct 0 as (t0, t'). ``` ```intro H. ``` ```inversion H. ``` ```apply eqst. ``` ``` assumption. ``` ``` apply proof. ``` ``` assumption. ``` ```Qed. ``` ```Theorem eqst_inv_eq : forall {A} (s s' : Stream A), ``` ``` EqSt s s' -> ForAll (fun ss' => fst (hd ss') = snd (hd ss')) (zip (s, s')). ``` ```Proof. ``` ```intro A. ``` ```cofix proof. ``` ```destruct s as (s0, s'). ``` ```destruct 0 as (t0, t'). ``` ```intro H. ``` ```inversion H. ``` ```apply HereAndFurther. ``` ``` assumption. ``` ``` apply proof. ``` ``` assumption. ``` ```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. ``` ```*) ``` ```Definition History_Spec {A} (s : Stream A) s' := ``` ``` fst (hd (tl s')) = cons (snd (hd s')) (fst (hd s')) ``` ``` /\ EqSt (concat (fst (hd s')) (apply (lift (@snd _ _)) s')) s. ``` ```Theorem history_rec_spec : forall {A} p (s : Stream A), ``` ``` fst (hd (history_rec p s)) = p ``` ``` /\ ForAll (fun s' => History_Spec (concat p s) s') (history_rec p s). ``` ```Proof. ``` ```intros. ``` ```split. ``` ``` destruct s. ``` ``` reflexivity. ``` ``` revert p s. ``` ``` cofix proof. ``` ``` destruct s as (s0, s'). ``` ``` apply HereAndFurther. ``` ``` split. ``` ``` simpl. ``` ``` destruct s'. ``` ``` reflexivity. ``` ``` apply eqst_concat. ``` ``` apply unzip_history_rec. ``` ``` apply (proof (cons s0 p) s'). ``` ```Qed. ``` ```Theorem history_spec : forall {A} (s : Stream A), ``` ``` fst (hd (history s)) = nil ``` ``` /\ ForAll (fun s' => History_Spec s s') (history s). ``` ```Proof. ``` ```intros. ``` ```generalize (history_rec_spec nil s). ``` ```intuition. ``` ```Qed. ``` ```Theorem history_rec_spec_complete : forall {A} p (s : Stream A) ps, ``` ``` fst (hd ps) = p -> ForAll (fun s' => History_Spec (concat p s) s') ps -> EqSt ps (history_rec p s). ``` ```Proof. ``` ```intro A. ``` ```cofix proof. ``` ```intros. ``` ```destruct s as (s0, s'). ``` ```destruct ps as ((p_ps0, s_ps0), ps'). ``` ```simpl in H. ``` ```subst. ``` ```inversion H0. ``` ```unfold History_Spec in H. ``` ```destruct H. ``` ```simpl in H. ``` ```apply eqst. ``` ``` simpl. ``` ``` intros. ``` ``` simpl in H. ``` ``` subst. ``` ``` inversion H0. ``` ``` unfold History_Spec in H. ``` ``` destruct H. ``` ``` simpl. ``` ``` simpl in H2. ``` ``` destruct (concat_eqst _ _ _ _ refl_equal H2). ``` ``` inversion H5. ``` ``` simpl in H6. ``` ``` subst. ``` ``` reflexivity. ``` ``` simpl. ``` ``` apply proof. ``` ``` simpl in H2. ``` ``` destruct (concat_eqst _ _ _ _ refl_equal H2). ``` ``` inversion H4. ``` ``` simpl in H5. ``` ``` subst. ``` ``` assumption. ``` ``` assumption. ``` ```Qed. ``` ```Theorem history_spec_complete : forall {A} (s : Stream A) ps, ``` ``` fst (hd ps) = nil -> ForAll (fun s' => History_Spec s s') ps -> EqSt ps (history s). ``` ```Proof. ``` ```intros. ``` ```apply history_rec_spec_complete. ``` ``` assumption. ``` ``` assumption. ``` ```Qed. ``` ```Theorem inv_snd_history_rec_intro : 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_snd_history_intro : 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_snd_history_rec_intro. ``` ```assumption. ``` ```Qed. ``` ```Theorem inv_snd_history_rec_elim : 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 inv_snd_history_elim : 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 inv_snd_history_rec_elim 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_apply : forall {A} (I I' : A -> Prop) (T T' : A -> A -> Prop) k (p : list A), ``` ``` prefix I T k p -> prefix (fun s => I s -> I' s) (fun s s' => T s s' -> T' s s') k p -> prefix I' T' k p. ``` ```Proof. ``` ```intros A I I' T T'. ``` ```induction k. ``` ``` trivial. ``` ``` simpl. ``` ``` destruct p. ``` ``` trivial. ``` ``` 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. ``` ```intros. ``` ```apply inv_snd_history_elim. ``` ```apply @ForAll_apply with (P := fun s' => P (snd (hd s'))). ``` ``` apply ``` ``` @ForAll_apply ``` ``` with ``` ``` (P := fun s' => ``` ``` prefix (fun st => P st) (fun st st' => P st') k (fst (hd s'))). ``` ``` apply ``` ``` @ForAll_reinforce ``` ``` with ``` ``` (P := ForAll ``` ``` (fun s' : Stream (list A * A) => ``` ``` prefix (fun st : A => P st) (fun _ st' : A => P st') k ``` ``` (fst (hd s')) -> P (snd (hd s')))). ``` ``` apply ``` ``` @ForAll_reinforce ``` ``` with (P := ForAll (fun s' : Stream (list A * A) => History_Spec s s')). ``` ``` eapply ForAll_coind. ``` ``` intro. ``` ``` exact (fun x => x). ``` ``` destruct x as ((p0, s0), ((p1, s1), x'')). ``` ``` simpl. ``` ``` intuition. ``` ``` inversion H1. ``` ``` assumption. ``` ``` inversion H0. ``` ``` assumption. ``` ``` inversion H1. ``` ``` unfold History_Spec in H2. ``` ``` simpl in H2. ``` ``` destruct H2. ``` ``` rewrite H2. ``` ``` destruct k. ``` ``` simpl. ``` ``` trivial. ``` ``` simpl. ``` ``` inversion H0. ``` ``` simpl in H6. ``` ``` destruct p0. ``` ``` intuition. ``` ``` split. ``` ``` simpl in H3. ``` ``` apply H6. ``` ``` exact H3. ``` ``` apply prefix_mono_k. ``` ``` exact H3. ``` ``` simpl. ``` ``` intuition. ``` ``` generalize (history_spec s). ``` ``` intuition. ``` ``` destruct s. ``` ``` simpl. ``` ``` destruct k. ``` ``` simpl. ``` ``` trivial. ``` ``` simpl. ``` ``` trivial. ``` ``` exact H. ``` ``` apply necessitation. ``` ``` destruct s0. ``` ``` simpl. ``` ``` trivial. ``` ```Qed. ``` ```Theorem kinduction' : forall {A} (P : A -> Prop) k ps (s : Stream A), ``` ``` fst (hd ps) = nil ``` ``` -> ForAll (fun s' => History_Spec s s') ps ``` ``` -> ForAll (fun s' => prefix (fun st => P st) (fun st st' => P st') k (fst (hd s')) -> P (snd (hd s'))) ps ``` ``` -> ForAll (fun s' => P (hd s')) s. ``` ```Proof. ``` ```intros. ``` ```rewrite (eqst_eq _ _ (history_spec_complete _ _ H H0)) in H1. ``` ```eapply kinduction. ``` ```apply H1. ``` ```Qed. ``` ```Theorem inv_prefix_history_rec : forall {A} (I : A -> Prop) (T : A -> A -> Prop) p (s : Stream A), ``` ``` ForAll (fun s' => T (hd s') (hd (tl s'))) (concat p s) -> ``` ``` forall k, ``` ``` prefix I T k (cons (hd s) p) -> ``` ``` ForAll (fun s' => prefix I T k (cons (snd (hd s')) (fst (hd s')))) (history_rec p s). ``` ```Proof. ``` ```intros A I T. ``` ```cofix proof. ``` ```intros. ``` ```inversion H. ``` ```destruct s as (s0, s'). ``` ```apply HereAndFurther. ``` ``` assumption. ``` ``` simpl. ``` ``` apply proof. ``` ``` assumption. ``` ``` destruct k; simpl. ``` ``` trivial. ``` ``` split. ``` ``` generalize (inv_concat _ _ _ H). ``` ``` clear H; intro H. ``` ``` inversion H. ``` ``` assumption. ``` ``` apply prefix_mono_k. ``` ``` assumption. ``` ```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 (cons (snd (hd s')) (fst (hd s')))) (history s). ``` ```Proof. ``` ```intros. ``` ```apply inv_prefix_history_rec. ``` ``` assumption. ``` ``` destruct k; simpl. ``` ``` trivial. ``` ``` assumption. ``` ```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. ``` ```destruct k. ``` ``` apply necessitation. ``` ``` simpl. ``` ``` trivial. ``` ``` eapply ForAll_apply. ``` ``` apply (fun i n => inv_prefix_history I T s i n (S (S k))). ``` ``` apply H. ``` ``` apply H0. ``` ``` apply necessitation. ``` ``` destruct s0 as ((p0, s0), s'). ``` ``` simpl. ``` ``` destruct p0. ``` ``` trivial. ``` ``` intuition. ``` ```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. ```