proposition: Lemma itree_family_COFE : COFE itree_family.
proof: Proof. Proof using. apply~ nat_cofe'. typeclass. introv H. exists (itree_diagonal (shifts u)). cuts M: (forall k i u, i <= k -> (forall i j : nat, i < j -> itree_similar_upto (S i) (u i) (u j)) -> itree_similar_upto (S i) (u k) (itree_diagonal u)). intros i. destruct i. simple~. sets u': (shifts u). change (u (S i)) with (u' i). apply M. math. intros i' j' Ri'j'. unfold u', shifts. apply H. math. clears u. induction k using peano_induction; introv Lik Coh. tests: (k = 0). math_rewrite (i = 0). simpl. destruct~ (u 0). unfolds. fold itree_similar_upto. forwards S0: (>> Coh 0 k __). math. simpl in S0. unfold itree_diagonal; fold itree_diagonal. sets_eq <- u0: (u 0). sets_eq <- uk: (u k). destruct u0 as [|t01 t02]; destruct uk as [|tk1 tk2]; auto_false. split. destruct i. simple~. sets u': (itree_left \o shifts u). asserts_rewrite (tk1 = u' (k-1)). unfold u'. unfold compose, shifts, itree_left. math_rewrite (S (k - 1) = k). rewrite~ EQuk. apply H; try math. intros i' j' Li'j'. unfold u'. unfold compose, shifts, itree_left. sets_eq i'': (S i'). sets_eq j'': (S j'). forwards Ssi: (Coh i'' j''). math. simpl in Ssi. destruct (u i''); destruct (u j''); auto_false*. destruct i. simple~. sets u': (itree_right \o shifts u). asserts_rewrite (tk2 = u' (k-1)). unfold u'. unfold compose, shifts. unfold itree_right. math_rewrite (S (k - 1) = k). rewrite~ EQuk. apply H; try math. intros i' j' Li'j'. unfold u'. unfold compose, shifts, itree_left. sets_eq i'': (S i'). sets_eq j'': (S j'). forwards Ssi: (Coh i'' j''). math. simpl in Ssi. destruct (u i''); destruct (u j''); auto_false*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat