proposition: Lemma AlignedDecodeListM {A C : Type} (A_decode : DecodeM (A * _) ByteString) (A_decode_align : forall {m}, AlignedDecodeM A m) (n : nat) : forall (t : list A -> DecodeM (C * _) ByteString) (t' : list A -> forall {numBytes}, AlignedDecodeM C numBytes), (DecodeMEquivAlignedDecodeM A_decode (@A_decode_align)) -> (forall b, DecodeMEquivAlignedDecodeM (t b) (@t' b)) -> DecodeMEquivAlignedDecodeM (fun v cd => `(l, bs, cd') <- decode_list A_decode n v cd; t l bs cd') (fun numBytes => l <- ListAlignedDecodeM (@A_decode_align) n; t' l)%AlignedDecodeM%list.
proof: Proof. induction n; simpl; intros; eauto. eapply DecodeMEquivAlignedDecodeM_trans; simpl; intros. 2: reflexivity. 2: apply AlignedDecodeMEquiv_sym; etransitivity; [apply ReturnAlignedDecodeM_LeftUnit; reflexivity | reflexivity ]. eauto. eapply DecodeMEquivAlignedDecodeM_trans; simpl; intros. 2: set_evars; erewrite !DecodeBindOpt2_assoc; subst_evars; higher_order_reflexivity. 2: apply AlignedDecodeMEquiv_sym; etransitivity; [apply BindAlignedDecodeM_assoc; reflexivity | higher_order_reflexivity ]. simpl. eapply Bind_DecodeMEquivAlignedDecodeM; intros. eauto. eapply DecodeMEquivAlignedDecodeM_trans; simpl; intros. 2: set_evars; erewrite !DecodeBindOpt2_assoc; subst_evars; higher_order_reflexivity. 2: apply AlignedDecodeMEquiv_sym; etransitivity; [apply BindAlignedDecodeM_assoc; reflexivity | higher_order_reflexivity ]. simpl. eapply IHn; eauto. intros. eapply DecodeMEquivAlignedDecodeM_trans; simpl; intros. 2: higher_order_reflexivity. 2: apply AlignedDecodeMEquiv_sym; etransitivity; [eapply ReturnAlignedDecodeM_LeftUnit | higher_order_reflexivity]. eapply H0. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BaseFormats Bedrock.Word