proposition: Lemma AlignedEncoder_extr {S} {cache : Cache} (enc' : EncodeM S ByteString) (enc : forall sz, AlignedEncodeM sz) (enc_OK : EncodeMEquivAlignedEncodeM enc' enc) (enc'_aligned : forall s ce t ce', enc' s ce = Some (t, ce') -> padding t = 0) n n' : forall (t : Vector.t Core.char n) (t' : Vector.t Core.char n') n1 s v ce idx ce', enc _ t n1 s ce = Some (v, idx, ce') -> enc _ (t++t') n1 s ce = Some (v++t', idx, ce').
proof: Proof. intros. edestruct @AlignedEncoder_inv as [n2 [n3 [t1 [t2 [t3 [v2 ?]]]]]]; eauto. destruct_conjs. subst. simpl in *. match goal with | |- enc (?n1 + (?n2 + ?n3) + ?n4) ((?t1 ++ ?t2 ++ ?t3) ++ ?t4) ?a ?b ?c = Some ((?t1' ++ ?t2' ++ ?t3') ++ ?t4', ?d, ?e)=> assert (enc (n1 + (n2 + (n3 + n4))) (t1 ++ t2 ++ (t3 ++ t4)) a b c = Some ((t1' ++ t2' ++ (t3' ++ t4')), d, e)) end. assert (n2 = numBytes (build_aligned_ByteString v2)) as L by eauto. edestruct enc_OK as [? _]. edestruct H0 with (v:=eq_rect _ _ t2 _ L); eauto. clear H0. destruct_conjs. destruct L. simpl in *. rewrite H0. repeat f_equal. apply build_aligned_ByteString_inj. rewrite <- H2. rewrite !build_aligned_ByteString_append. reflexivity. rename n' into n4. revert H0. clear. intros. assert (n1 + (n2 + n3) + n4 = n1 + (n2 + (n3 + n4))) by omega. assert (forall {A} (t1 : Vector.t A n1) (t2 : Vector.t A n2) (t3 : Vector.t A n3) (t4 : Vector.t A n4), t1 ++ t2 ++ t3 ++ t4 = eq_rect _ (Vector.t A) ((t1 ++ t2 ++ t3) ++ t4) _ H) as L. { clear. intros. assert (n2 + n3 + n4 = n2 + (n3 + n4)) by omega. rewrite <- (Vector_append_assoc' _ _ _ _ H0). f_equal. apply Vector_append_assoc. } revert H0. rewrite !L. clear. destruct H. simpl. eauto. 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.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString