proposition: Lemma AlignedDecode_CollapseWord' {A B} : forall (ResultT : Type) (sz sz' : nat) aligned_decoder (decode_A : DecodeM (A * _) ByteString) (decode_B : DecodeM (B * _) ByteString) (f : word sz -> A) (f' : word sz' -> B) (k : A -> B -> _ -> CacheDecode -> option (ResultT * _ * CacheDecode)), DecodeMEquivAlignedDecodeM (fun bs cd => `(w, b', cd') <- decode_word bs cd; k (f (split1' sz sz' w)) (f' (split2' sz sz' w)) b' cd') aligned_decoder -> (forall bs cd, Ifopt (decode_word (sz := sz) bs cd) as a Then Some (f (fst (fst a)), (snd (fst a)), snd a) Else None = decode_A bs cd) -> (forall bs cd, Ifopt (decode_word (sz := sz') bs cd) as a Then Some (f' (fst (fst a)), (snd (fst a)), snd a) Else None = decode_B bs cd) -> DecodeMEquivAlignedDecodeM (fun bs cd => `(a, b', cd') <- decode_A bs cd; `(b, b'0, cd'0) <- decode_B b' cd'; k a b b'0 cd'0) aligned_decoder.
proof: Proof. intros; eapply DecodeMEquivAlignedDecodeM_trans; eauto; intros; simpl; try reflexivity. setoid_rewrite <- H0. rewrite <- (fun H => CollapseWord H sz sz' b cd (fun w w' => k (f w) (f' w'))) by eauto. destruct (decode_word b cd) as [ [ [? ?] ?] | ]; simpl; eauto. rewrite <- H1. destruct (decode_word b0 c) as [ [ [? ?] ?] | ]; simpl; 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