proposition: Lemma AlignedDecodeNCharM (addD_O : forall cd, addD cd 0 = cd) {m} : DecodeMEquivAlignedDecodeM (decode_word (sz := m * 8)) (fun numBytes => GetCurrentBytes m).
proof: Proof. induction m. - unfold decode_word; simpl; pose proof (Return_DecodeMEquivAlignedDecodeM WO). eapply DecodeMEquivAlignedDecodeM_trans; intros; try rewrite addD_O; try higher_order_reflexivity. eapply H. - Local Arguments decode_word' : simpl never. Local Arguments plus : simpl never. unfold decode_word; simpl. eapply DecodeMEquivAlignedDecodeM_trans; intros; try eapply AlignedDecodeMEquiv_refl. + eapply AlignedDecodeBindCharM; intros. eapply Bind_DecodeMEquivAlignedDecodeM. eassumption. intros. pose proof (@Return_DecodeMEquivAlignedDecodeM); eapply H. + intros; unfold mult; simpl; rewrite decode_word_plus'; simpl; fold mult; simpl. unfold decode_word. destruct (decode_word' 8 b) as [ [? ?] | ]; simpl; eauto. destruct (decode_word' (m * 8) b0) as [ [? ?] | ]; simpl; eauto. rewrite addD_addD_plus; 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