proposition: Lemma refine_CollapseFormatWord (addE_addE_plus : forall ce n m, addE (addE ce n) m = addE ce (n + m)) : forall {sz sz'} (w : word sz) (w' : word sz') format_1 format_2 ce, refine (format_1 ce) (format_word w ce) -> (forall ce, refine (format_2 ce) (format_word w' ce)) -> refine ((format_1 ThenC format_2) ce) ((format_word (combine w' w)) ce).
proof: Proof. intros. etransitivity. instantiate (1 := ((format_word (combine w' w)) ThenC (fun ce => ret (ByteString_id, ce))) ce). rewrite <- CollapseFormatWord; eauto. unfold compose, Bind2; intros. rewrite H; setoid_rewrite H0; setoid_rewrite refineEquiv_bind_bind; repeat setoid_rewrite refineEquiv_bind_unit. simpl. pose proof mempty_right; simpl in *; rewrite H1; reflexivity. unfold compose, Bind2; intros; eauto. repeat setoid_rewrite refineEquiv_bind_unit; simpl. pose proof mempty_right; simpl in *; rewrite H1; 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 Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad