proposition: Lemma AlignedDecode2Char {C} {numBytes} : forall (v : ByteBuffer.t (S (S numBytes))) (t : (word 16 * ByteString * CacheDecode) -> C) (e : C) cd, (Ifopt (decode_word (monoidUnit := ByteString_QueueMonoidOpt) (sz := 16) (build_aligned_ByteString v) cd) as w Then t w Else e) = Let n := Core.append_word (Vector.nth v (Fin.FS Fin.F1)) (Vector.nth v Fin.F1) in t (n, build_aligned_ByteString (snd (Vector_split 2 _ v)), addD cd 16).
proof: Proof. unfold LetIn; intros. unfold decode_word, WordOpt.decode_word. match goal with |- context[Ifopt ?Z as _ Then _ Else _] => replace Z with (let (v', v'') := Vector_split 2 numBytes v in Some (VectorByteToWord v', build_aligned_ByteString v'')) by (symmetry; apply (@aligned_decode_char_eq' _ 1 v)) end. unfold Vector_split, If_Opt_Then_Else, If_Opt_Then_Else. f_equal. rewrite !Vector_nth_tl, !Vector_nth_hd. erewrite VectorByteToWord_cons. rewrite <- !Eqdep_dec.eq_rect_eq_dec; eauto using Peano_dec.eq_nat_dec. f_equal. erewrite VectorByteToWord_cons. rewrite <- !Eqdep_dec.eq_rect_eq_dec; eauto using Peano_dec.eq_nat_dec. Unshelve. omega. omega. 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 Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad