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 (split1' sz sz' w) (split2' sz sz' w) b' cd').
proof: Proof. unfold decode_word; repeat setoid_rewrite If_Opt_Then_Else_DecodeBindOpt; simpl. induction sz; simpl; intros. - rewrite !If_Opt_Then_Else_DecodeBindOpt; simpl. rewrite addD_addD_plus; reflexivity. - destruct (dequeue_opt b) as [ [? ?] | ]; simpl; eauto. pose proof (IHsz sz' b1 (addD cd 1) (fun w => k (SW_word b0 w))). destruct (decode_word' sz b1) as [ [? ?] | ]; simpl in *. + rewrite !If_Opt_Then_Else_DecodeBindOpt; rewrite !If_Opt_Then_Else_DecodeBindOpt in H; simpl in *; rewrite !addD_addD_plus in H; rewrite !addD_addD_plus; simpl in *. rewrite H. destruct (decode_word' (sz + sz') b1) as [ [? ?] | ]; simpl; eauto. repeat f_equal; clear. * induction sz; simpl in *. induction sz'; simpl in *; try shatter_word w0; simpl; eauto. pose proof (shatter_word_S w0); destruct_ex; subst; simpl; eauto. pose proof (shatter_word_S w0); destruct_ex; subst; simpl; eauto. * induction sz; simpl in *. induction sz'; simpl in *; try shatter_word w0; simpl; eauto. pose proof (shatter_word_S w0); destruct_ex; subst; simpl; f_equal; eauto. pose proof (shatter_word_S w0); destruct_ex; subst; simpl; f_equal; eauto. * induction sz; simpl in *. induction sz'; simpl in *; try shatter_word w0; simpl; eauto. pose proof (shatter_word_S w0); destruct_ex; subst; simpl; f_equal; eauto. pose proof (shatter_word_S w0); destruct_ex; subst; simpl; f_equal; eauto. + destruct (decode_word' (sz + sz') b1) as [ [? ?] | ]; simpl in *; eauto. rewrite addD_addD_plus in H; simpl in *. rewrite H; repeat f_equal; clear. * induction sz; simpl in *. induction sz'; simpl in *; try shatter_word w; simpl; eauto. pose proof (shatter_word_S w); destruct_ex; subst; simpl; eauto. pose proof (shatter_word_S w); destruct_ex; subst; simpl; eauto. * induction sz; simpl in *. induction sz'; simpl in *; try shatter_word w; simpl; eauto. pose proof (shatter_word_S w); destruct_ex; subst; simpl; f_equal; eauto. pose proof (shatter_word_S w); destruct_ex; subst; simpl; f_equal; eauto. * induction sz; simpl in *. induction sz'; simpl in *; try shatter_word w; simpl; eauto. pose proof (shatter_word_S w); destruct_ex; subst; simpl; f_equal; eauto. pose proof (shatter_word_S w); destruct_ex; subst; simpl; f_equal; eauto. 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