proposition: Lemma CollapseCorrectAlignedEncoderFormatWord' {S : Type} (addE_addE_plus : forall ce n m, addE (addE ce n) m = addE ce (n + m)) : forall {sz sz'} (f : S -> word sz) (f' : S -> word sz') k encoder, CorrectAlignedEncoder (Projection_Format format_word f ++ Projection_Format format_word f' ++ k) encoder -> CorrectAlignedEncoder (Projection_Format format_word (fun s => combine (f' s) (f s)) ++ k) encoder.
proof: Proof. intros; eapply refine_CorrectAlignedEncoder; eauto. intros. rewrite !refine_sequence_Format. unfold compose, Bind2. rewrite !refine_Projection_Format. pose proof CollapseFormatWord'. unfold compose, Bind2 in H. rewrite H; eauto. split. - f_equiv; intro. rewrite !refine_sequence_Format. simpl. unfold compose, Bind2. simplify with monad laws. rewrite !refine_Projection_Format. setoid_rewrite refineEquiv_bind_bind. f_equiv; intro. setoid_rewrite refineEquiv_bind_bind. f_equiv; intro. setoid_rewrite refineEquiv_bind_unit. reflexivity. - intros. intro. simpl. apply refine_sequence_Format in H1. unfold compose, Bind2 in H1. computes_to_inv. apply refine_Projection_Format in H1. unfold format_word in *. computes_to_inv; subst. simpl in *. eapply H0. unfold sequence_Format, compose, Bind2. computes_to_econstructor. apply refine_Projection_Format. eauto. computes_to_econstructor; eauto. simpl. computes_to_econstructor; eauto. apply refine_Projection_Format. eauto. computes_to_econstructor; eauto. simpl. rewrite addE_addE_plus; rewrite plus_comm; eauto. Defined.
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