proposition: Lemma AlignedDecodeBind2CharM {C : Type} (t : word 16 -> DecodeM (C * ByteString) ByteString) (t' : word 16 -> forall {numBytes}, AlignedDecodeM C numBytes) : (forall b, DecodeMEquivAlignedDecodeM (t b) (@t' b)) -> DecodeMEquivAlignedDecodeM (fun v cd => `(a, b0, cd') <- decode_word (monoidUnit := ByteString_QueueMonoidOpt) (sz := 16) v cd; t a b0 cd') (fun numBytes => b <- GetCurrentByte; b' <- GetCurrentByte; w <- return (Core.append_word b' b); t' w).
proof: Proof. intros; eapply DecodeMEquivAlignedDecodeM_trans with (bit_decoder1 := (fun (v : ByteString) (cd : CacheDecode) => `(w1, bs, cd') <- decode_word (sz := 8) v cd; `(w2, bs, cd') <- decode_word (sz := 8) bs cd'; t (Core.append_word w2 w1) bs cd')). eapply AlignedDecodeBindCharM; intros. eapply AlignedDecodeBindCharM; intros. eapply DecodeMEquivAlignedDecodeM_trans. eapply (H _). intros; reflexivity. intros; higher_order_reflexivity. intros. unfold decode_word. rewrite (decode_word_plus' 8 8). unfold DecodeBindOpt2, DecodeBindOpt, BindOpt, If_Opt_Then_Else. destruct (decode_word' 8 b) as [ [? ?] | ]; eauto. destruct (decode_word' 8 b0) as [ [? ?] | ]; eauto. rewrite <- eq_rect_eq_dec; eauto using eq_nat_dec. rewrite addD_addD_plus; reflexivity. intros; 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