proposition: Lemma AlignedDecodeBindOption {S S' : Type} (decode_Some : DecodeM (S * _) ByteString) (decode_None : DecodeM (() * _) ByteString) (aligned_decode_Some : forall numBytes, AlignedDecodeM S numBytes) (aligned_decode_None : forall numBytes, AlignedDecodeM () numBytes) (t : option S -> DecodeM (S' * _) ByteString) (t' : option S -> forall {numBytes}, AlignedDecodeM S' numBytes) b' : (DecodeMEquivAlignedDecodeM decode_Some aligned_decode_Some) -> (DecodeMEquivAlignedDecodeM decode_None aligned_decode_None) -> (forall s_opt, DecodeMEquivAlignedDecodeM (t s_opt) (@t' s_opt)) -> DecodeMEquivAlignedDecodeM (fun v cd => `(a, b0, cd') <- Option.option_decode _ decode_Some decode_None b' v cd ; t a b0 cd') (fun numBytes => a <- aligned_option_decode aligned_decode_Some aligned_decode_None b'; t' a)%AlignedDecodeM.
proof: Proof. intros. destruct b'; simpl; eapply Bind_DecodeMEquivAlignedDecodeM; eauto. - unfold DecodeMEquivAlignedDecodeM; split; intros. { unfold aligned_option_decode; simpl. destruct H. rewrite H. destruct (aligned_decode_Some numBytes_hd (Vector.tl v) n cd) as [ [ [? ?] ] | ]; simpl; eauto. } split; intros. { destruct (decode_Some b cd) as [ [ [? ?] ?] | ] eqn: ? ; try discriminate. injections. eapply H; eauto. } split; intros. unfold aligned_option_decode; simpl. split; intros. { destruct (decode_Some (build_aligned_ByteString v) cd) as [ [ [? ?] ] | ] eqn: ?; simpl; try discriminate. eapply H in Heqo. rewrite Heqo; eauto. } { destruct (aligned_decode_Some n v 0 cd) as [ [ [? ?] ] | ] eqn: ?; simpl; try discriminate. eapply H in Heqo; rewrite Heqo; reflexivity. } split. { destruct (decode_Some (build_aligned_ByteString v) cd) as [ [ [? ?] ] | ] eqn: ?; simpl; try discriminate. eapply H in Heqo; destruct Heqo. rewrite H3. injections; reflexivity. } { destruct (decode_Some (build_aligned_ByteString v) cd) as [ [ [? ?] ] | ] eqn: ?; simpl; try discriminate. eapply H in Heqo; destruct Heqo. destruct H4. injections; eauto. } - unfold DecodeMEquivAlignedDecodeM; split; intros. { unfold aligned_option_decode; simpl. destruct H0; rewrite H0. destruct (aligned_decode_None numBytes_hd (Vector.tl v) n cd) as [ [ [? ?] ] | ]; simpl; eauto. } split; intros. { destruct (decode_None b cd) as [ [ [? ?] ?] | ] eqn: ? ; try discriminate. injections. eapply H0; eauto. } split; intros. unfold aligned_option_decode; simpl. split; intros. { destruct (decode_None (build_aligned_ByteString v) cd) as [ [ [? ?] ] | ] eqn: ?; simpl; try discriminate. eapply H0 in Heqo. rewrite Heqo; eauto. } { destruct (aligned_decode_None n v 0 cd) as [ [ [? ?] ] | ] eqn: ?; simpl; try discriminate. eapply H0 in Heqo; rewrite Heqo; reflexivity. } split. { destruct (decode_None (build_aligned_ByteString v) cd) as [ [ [? ?] ] | ] eqn: ?; simpl; try discriminate. eapply H0 in Heqo; destruct Heqo. rewrite H3. injections; reflexivity. } { destruct (decode_None (build_aligned_ByteString v) cd) as [ [ [? ?] ] | ] eqn: ?; simpl; try discriminate. eapply H0 in Heqo; destruct Heqo. destruct H4. injections; eauto. } 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