proposition: Lemma AlignedDecodeUnusedCharM : DecodeMEquivAlignedDecodeM (decode_unused_word (sz := 8)) (fun numBytes => SkipCurrentByte).
proof: Proof. unfold DecodeMEquivAlignedDecodeM, BindAlignedDecodeM, DecodeBindOpt2, BindOpt, Compose_Decode; intros; unfold WordOpt.decode_word, Compose_Decode. split; [ | split ]; intros. - pattern numBytes_hd, v; eapply Vector.caseS; simpl; intros. unfold SkipCurrentByte, nth_opt; simpl. destruct (Vector_nth_opt t n); simpl; eauto. - unfold decode_unused_word, Compose_Decode, decode_word in H. destruct (decode_word' 8 b) as [ [? ?] | ] eqn: ?; simpl in H; try discriminate. injections. eapply decode_word'_lt in Heqo; unfold le_B, bin_measure in Heqo; simpl in Heqo. unfold lt_B in Heqo; simpl in Heqo. injections; omega. - destruct v. + simpl; intuition; discriminate. + rewrite aligned_decode_unused_char_eq'; simpl; intuition. * discriminate. * unfold GetCurrentByte in H; simpl in H; discriminate. * unfold SkipCurrentByte; injections; simpl. clear; induction n; simpl; eauto. * injections. replace (match numBytes (build_aligned_ByteString v) with | 0 => S n | S l => n - l end) with 1 by (unfold numBytes; simpl; clear; induction n; omega). setoid_rewrite <- build_aligned_ByteString_append. eexists (Vector.cons _ h _ (@Vector.nil _)); 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