proposition: Lemma refine_CollapseFormatWord' (addE_addE_plus : forall ce n m, addE (addE ce n) m = addE ce (n + m)) {S} : forall {sz sz'} (f : S -> word sz) (f' : S -> word sz') (format_1 format_2 : FormatM S _), (forall s env, refine (format_1 s env) (Projection_Format format_word f s env)) -> (forall s env, refine (format_2 s env) (Projection_Format format_word f' s env)) -> (forall s env, refine ((format_1 ++ format_2) s env) (Projection_Format format_word (fun s => combine (f' s) (f s)) s env)).
proof: Proof. intros. unfold sequence_Format, compose, Projection_Format, Compose_Format, Bind2. rewrite H; setoid_rewrite H0. intros ? ?. rewrite unfold_computes in H1. destruct_ex; intuition; subst. pose proof (CollapseFormatWord (sz' := sz') (sz := sz) addE_addE_plus (f s) (f' s) (fun ce => ret (ByteString_id, ce)) env); eauto. unfold compose in H1. unfold Bind2 in H1. repeat setoid_rewrite refineEquiv_bind_unit in H1. simpl in H1. unfold format_word in H2. pose proof mempty_right. simpl in H3. rewrite !H3 in H1. eapply H1 in H2. computes_to_inv; subst. computes_to_econstructor. unfold Projection_Format, Compose_Format; apply unfold_computes; eexists; intuition eauto. unfold format_word; computes_to_econstructor. computes_to_econstructor. unfold Projection_Format, Compose_Format; apply unfold_computes; eexists; intuition eauto. unfold format_word; computes_to_econstructor. simpl. 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