proposition: Lemma CollapseWord'' {ResultT} : forall sz' sz (b : B) (cd : CacheDecode) (k : _ -> _ -> _ -> _ -> option (ResultT * B * CacheDecode)), (`(w, b', cd') <- decode_word (sz:=sz) b cd; `(w', b', cd') <- decode_word (sz:=sz') b' cd'; k w w' b' cd') = (`(w , b', cd') <- decode_word (sz:=sz' + sz) b cd; k (split2 sz' sz w) (split1 sz' sz w) b' cd').
proof: Proof. intros; rewrite CollapseWord'. replace (decode_word (sz:=sz' + sz) b cd) with (eq_rect _ (fun n => option (word n * B * _)) (decode_word (sz:=sz + sz') b cd) _ (trans_plus_comm _ _)). - destruct (decode_word b cd) as [ [ [? ?] ?] | ]; simpl. + revert w; rewrite (trans_plus_comm sz sz'); simpl; eauto. + rewrite (trans_plus_comm sz sz'); simpl; eauto. - rewrite (trans_plus_comm sz sz'); simpl; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word