proposition: Lemma Bind_Duplicate_DecodeMEquivAlignedDecodeM {A C : Type} (A_decode : DecodeM (A * ByteString) ByteString) (A_decode_aligned : forall {numBytes}, AlignedDecodeM A numBytes) (t : A -> DecodeM (C * ByteString) ByteString) (t' : A -> forall {numBytes}, AlignedDecodeM C numBytes) : DecodeMEquivAlignedDecodeM A_decode (@A_decode_aligned) -> (forall a, DecodeMEquivAlignedDecodeM (t a) (@t' a)) -> DecodeMEquivAlignedDecodeM (fun (b : ByteString) (c : CacheDecode) => `(a, bs, cd') <- A_decode b c; t a b cd') (fun numBytes => BindResetAlignedDecodeM A_decode_aligned (fun a => @t' a numBytes)).
proof: Proof. unfold DecodeMEquivAlignedDecodeM; intros; intuition. - unfold BindResetAlignedDecodeM. rewrite H1. destruct (A_decode_aligned numBytes_hd (Vector.tl v) n cd) as [ [ [? ?] ?] | ]; simpl. + specialize (H0 a); intuition. + reflexivity. - eapply DecodeBindOpt2_inv in H2; destruct_ex; intuition. specialize (H0 x); intuition. eapply H in H4. symmetry in H5; eapply H0 in H5; omega. - destruct (A_decode (build_aligned_ByteString v) cd) as [ [ [? ?] ?] | ] eqn: ?; simpl in *; try discriminate. assert (numBytes b <= n)%nat as nb_le_n. { eapply H in Heqo. unfold build_aligned_ByteString, length_ByteString in Heqo; simpl in Heqo; omega. } unfold BindResetAlignedDecodeM. apply H3 in Heqo; destruct_ex; intuition; subst; destruct_ex. rewrite H4; simpl; eauto. specialize (H0 a); intuition. generalize (build_aligned_ByteString_split' _ _ _ H5); intros; destruct_ex. rewrite H7 in *. apply H8 in H2. assert ((n - (n - numBytes b)) = numBytes b). { rewrite sub_plus; try omega. rewrite H7; auto. } assumption. unfold BindResetAlignedDecodeM; apply H3 in Heqo; rewrite Heqo; reflexivity. - unfold BindResetAlignedDecodeM in H2. destruct (A_decode (build_aligned_ByteString v) cd) as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try eauto. assert (numBytes b <= n)%nat as nb_le_n. { eapply H in Heqo. unfold build_aligned_ByteString, length_ByteString in Heqo; simpl in Heqo; omega. } apply H3 in Heqo; destruct_ex; intuition; subst; destruct_ex. rewrite H4 in H2; simpl in H2; eauto. specialize (H0 a); intuition. generalize (build_aligned_ByteString_split' _ _ _ H5); intros; destruct_ex. rewrite H7 in *. apply H8. assumption. - eapply DecodeBindOpt2_inv in H2; destruct_ex; intuition. assert (numBytes x0 <= n)%nat as nb_le_n. { eapply H in H4. unfold build_aligned_ByteString, length_ByteString in H4; simpl in H4; omega. } eapply H3 in H4. intuition. unfold BindResetAlignedDecodeM; rewrite H2; simpl; destruct_ex; intuition. symmetry in H5. specialize (H0 x); intuition. eapply H8 in H5; intuition. - eapply DecodeBindOpt2_inv in H2; destruct_ex; intuition. eapply H3 in H4; intuition; destruct_ex. setoid_rewrite H4. symmetry in H5. eapply H0 in H5; intuition; destruct_ex. rewrite H5 in H4. rewrite <- H4. eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString