proposition: Lemma format_words' {n m} (addE_addE_plus : forall ce n m, addE (addE ce n) m = addE ce (n + m)) : forall (w : word (n + m)) ce, refine (format_word (monoidUnit := ByteString_QueueMonoidOpt) w ce) ((format_word (monoidUnit := ByteString_QueueMonoidOpt) (split1' _ _ w) ThenC (format_word (monoidUnit := ByteString_QueueMonoidOpt) (split2' _ _ w))) ce).
proof: Proof. induction n. - unfold compose; simpl; intros. unfold format_word at 2; simpl. autorewrite with monad laws. simpl; rewrite addE_addE_plus. pose proof mempty_left as H'; simpl in H'; rewrite H'. reflexivity. - unfold plus; fold plus; simpl; intros. rewrite (word_split_SW w) at 1. rewrite format_SW_word. unfold compose, Bind2. rewrite (IHn (word_split_tl w) (addE ce 1)). unfold compose, Bind2. unfold format_word; autorewrite with monad laws. simpl. rewrite format_word_S. pose proof mappend_assoc as H'; simpl in H'. rewrite !H'. rewrite !addE_addE_plus; simpl. f_equiv. f_equiv. f_equiv. rewrite !word_split_hd_SW_word, !word_split_tl_SW_word. fold plus. clear; generalize (split1' n m (word_split_tl w)) (ByteString_enqueue (word_split_hd w) ByteString_id). induction w0; simpl in *. + intros; pose proof (mempty_right b) as H; simpl in H; rewrite H; eauto. + intros. rewrite <- (IHw0 (wtl w) b0). pose proof enqueue_mappend_opt as H'''; simpl in H'''. rewrite <- H'''; eauto. + eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad