proposition: Lemma CollapseFormatWord : forall {sz sz'} (w : word sz) (w' : word sz') k ce, refine (((format_word w) ThenC (format_word w') ThenC k) ce) (((format_word (combine w' w)) ThenC k) ce).
proof: Proof. intros; unfold compose, format_word, Bind2. autorewrite with monad laws. simpl; rewrite addE_addE_plus. rewrite Plus.plus_comm; f_equiv; intro. rewrite mappend_assoc. destruct a; simpl. f_equiv; f_equiv; f_equiv. revert sz' w'; induction w; simpl; intros. - rewrite mempty_left. generalize mempty; clear; induction w'; intros. + reflexivity. + simpl; rewrite IHw'; reflexivity. - rewrite !enqueue_opt_format_word. replace (encode_word' (sz' + S n) (combine w' (WS b0 w)) mempty) with (encode_word' (S sz' + n) (combine (SW_word b0 w') w) mempty). + rewrite <- IHw. simpl; rewrite format_word_S. rewrite <- mappend_assoc, word_split_tl_SW_word, word_split_hd_SW_word. f_equal. clear; induction w'. * simpl; rewrite mempty_right; reflexivity. * simpl; rewrite !enqueue_opt_format_word. rewrite <- IHw'. rewrite mappend_assoc; reflexivity. + clear; revert n w; induction w'; intros. * simpl; eauto. * simpl; rewrite <- IHw'; reflexivity. 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