proposition: Lemma CollapseEnumWord {ResultT} : forall sz' sz n (b : B) (tb : Vector.t (word sz) (S n)) (cd : CacheDecode) (k : _ -> _ -> _ -> _ -> option (ResultT * B * CacheDecode)), (`(w, b', cd') <- decode_enum (sz:=sz) tb 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; Ifopt (word_indexed (split2 sz' sz w) tb) as idx Then k idx (split1 sz' sz w) b' cd' Else None).
proof: Proof. intros. unfold decode_enum. rewrite <- CollapseWord'' with (b0 := b) (cd0 := cd) (k0 := fun w1 w2 b cd => Ifopt (word_indexed w1 tb) as idx Then k idx w2 b cd Else None). unfold decode_word; repeat setoid_rewrite If_Opt_Then_Else_DecodeBindOpt; simpl. destruct (decode_word' sz b) as [ [? ?] | ] eqn: ?; simpl; eauto. destruct (word_indexed w tb) as [ ? | ] eqn: ?; simpl; eauto. destruct (decode_word' sz' b0) as [ [? ?] | ] eqn: ?; simpl; 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