proposition: Lemma A_decode_aligned_shift {A : Type} (A_decode_aligned : forall {numBytes}, AlignedDecodeM A numBytes) : (forall (numBytes_hd n : nat) (v : Vector.t char (S numBytes_hd)) (cd : CacheDecode), @A_decode_aligned (S numBytes_hd) v (S n) cd = (Ifopt @A_decode_aligned numBytes_hd (Vector.tl v) n cd as a0 Then Some (fst (fst a0), S (snd (fst a0)), snd a0) Else None)) -> forall (numBytes_hd numBytes_tl : nat) (v : Vector.t char (numBytes_hd + numBytes_tl)) (cd : CacheDecode), @A_decode_aligned _ v numBytes_hd cd = (Ifopt @A_decode_aligned _ (snd (Vector_split _ _ v)) 0 cd as a0 Then Some (fst (fst a0), numBytes_hd + (snd (fst a0)), snd a0) Else None).
proof: Proof. induction numBytes_hd; simpl; intros. - destruct ( A_decode_aligned numBytes_tl v 0 cd) as [ [ [? ?] ?] | ]; reflexivity. - rewrite H. rewrite IHnumBytes_hd; destruct (Vector_split numBytes_hd numBytes_tl (Vector.tl v)) eqn: ?; simpl. match goal with |- context [Vector_split ?m ?n ?v] => replace (Vector_split m n v) with (t, t0) end; simpl. destruct (A_decode_aligned numBytes_tl t0 0 cd); simpl; reflexivity. rewrite <- Heqp; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString