### Profile

 1 ```Require Export Streams. ``` ```Require List. ``` ```Require Import Setoid. ``` ```Require Import Relation_Definitions. ``` ```Require Import Program.Wf. ``` ```Require Import Wf_nat. ``` ```Require Import Wellfounded. ``` ```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. ``` ```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. ``` ```Lemma eqst_apply : forall {A B} {f f' : Stream (A -> B)} {a a' : Stream A}, ``` ``` EqSt f f' -> EqSt a a' -> EqSt (apply f a) (apply f' a'). ``` ```Proof. ``` ```intros A B. ``` ```cofix proof. ``` ```intros. ``` ```inversion H. ``` ```inversion H0. ``` ```apply eqst. ``` ``` rewrite hd_apply. ``` ``` rewrite hd_apply. ``` ``` congruence. ``` ``` rewrite tl_apply. ``` ``` rewrite tl_apply. ``` ``` apply proof. ``` ``` assumption. ``` ``` assumption. ``` ```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. ``` ```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. ``` ```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 effective {A : Type} (r : relation A) := ``` ``` forall a1 a2, { r a1 a2 } + { ~ r a1 a2 }. ``` ```Definition lift_hd {A : Type} (r : relation A) : relation (Stream A) := ``` ``` fun s1 => fun s2 => r (hd s1) (hd s2). ``` ```Theorem lift_hd_effective : forall {A : Type} {r : relation A}, ``` ``` effective r -> effective (lift_hd r). ``` ```Proof. ``` ```unfold effective, lift_hd in |- *. ``` ```intros A r H s1 s2. ``` ```destruct s1; destruct s2. ``` ```apply H. ``` ```Defined. ``` ```Section FixedPoint. ``` ```Variable A : Type. ``` ```Variable union : A -> A -> A. ``` ```Variable le : relation A. ``` ```Hypothesis le_mono : forall x y, le x (union x y). ``` ```Hypothesis le_eff : effective le. ``` ```Definition gt x y := le y x /\ ~ le x y. ``` ```Hypothesis gt_wf : well_founded gt. ``` ```Program Fixpoint rec_hd (f : Stream A -> Stream A) (s : Stream A) { wf (lift_hd gt) s } : Stream A := ``` ``` let s' := apply (apply (lift union) s) (f s) in ``` ``` if (lift_hd_effective le_eff s' s) ``` ``` then s' ``` ``` else rec_hd f s'. ``` ```Obligation 1. ``` ```Proof. ``` ```unfold lift_hd. ``` ```rewrite hd_apply. ``` ```rewrite hd_apply. ``` ```rewrite hd_lift. ``` ```unfold gt. ``` ```split. ``` ``` apply le_mono. ``` ``` unfold lift_hd in H. ``` ``` rewrite hd_apply in H. ``` ``` rewrite hd_apply in H. ``` ``` rewrite hd_lift in H. ``` ``` exact H. ``` ```Qed. ``` ```Obligation 2. ``` ```Proof. ``` ```unfold MR. ``` ```apply wf_inverse_image. ``` ```unfold lift_hd. ``` ```apply wf_inverse_image. ``` ```assumption. ``` ```Defined. ``` ```CoFixpoint rec (f : Stream A -> Stream A) (s : Stream A) : Stream A := ``` ``` let s' := rec_hd f s in Cons (hd s') (rec f (tl s')). ``` ```End FixedPoint. ``` ```Arguments gt {A} _ _ _. ``` ```Arguments rec {A} _ _ _ _ _ _ _. ```