proposition: Lemma AlignedDecodeNatM {C : Set} (t : nat -> DecodeM (C * _) ByteString) (t' : nat -> forall {numBytes}, AlignedDecodeM C numBytes) : (forall b, DecodeMEquivAlignedDecodeM (t b) (@t' b)) -> DecodeMEquivAlignedDecodeM (fun v cd => `(a, b0, cd') <- decode_nat (monoidUnit := ByteString_QueueMonoidOpt) 8 v cd; t a b0 cd') (fun numBytes => b <- GetCurrentByte; n <- return (wordToNat b); t' n).
proof: Proof. replace (fun (v : ByteString) (cd : CacheDecode) => `(a, b0, cd') <- decode_nat 8 v cd; t a b0 cd') with (fun (v : ByteString) (cd : CacheDecode) => `(w, b, cd') <- decode_word (sz := 8) v cd; t (wordToNat w) b cd'); intros. eapply AlignedDecodeBindCharM; intros. replace (fun numBytes : nat => n <- return (wordToNat b); t' n numBytes) with (fun numBytes : nat => t' (wordToNat b) numBytes). eapply H. unfold BindAlignedDecodeM, ReturnAlignedDecodeM; simpl. repeat (apply functional_extensionality_dep; intros); reflexivity. repeat (apply functional_extensionality_dep; intros). unfold decode_nat, DecodeBindOpt2; intros. rewrite BindOpt_assoc; f_equal. repeat (apply functional_extensionality_dep; intros). unfold BindOpt. destruct x1; destruct p; simpl. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad 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.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word