proposition: Lemma sim_concat s0 s1 t0 t1 (EQ0: sim s0 t0) (EQ1: sim s1 t1) : @sim (concat s0 s1) (concat t0 t1) .
proof: Proof. revert_until s0. revert s0. pcofix CIH. intros. pfold. punfold EQ0. punfold EQ1. inv EQ0. - rewrite ! unfold_concat. cbn. eapply _sim_mon; eauto. intros. pclearbot. left. eapply paco2_mon; eauto. intros. red in PR0. contradict PR0. - rewrite ! unfold_concat. cbn. pclearbot. econstructor; eauto. left. inv EQ1. + admit. + pclearbot. pfold. admit. Abort. Inductive prefixC (R : stream -> stream -> Prop): stream -> stream -> Prop := | prefixC_intro s0 s1 t0 t1 (REL: sim s0 t0) (REL: R s1 t1) : prefixC R (concat s0 s1) (concat t0 t1) . #[export] Hint Constructors prefixC: core. Lemma prefixC_spec simC : prefixC <3= gupaco2 (_sim) (simC) . Proof. gcofix CIH. intros. destruct PR. punfold REL. inv REL. - rewrite ! unfold_concat. cbn. gbase. eauto. - gstep. rewrite ! unfold_concat. cbn. econstructor; eauto. pclearbot. gbase. eauto. Qed.
imports: Paco.paco Program.Tactics RelationClasses Morphisms