proposition: Lemma AlignedEncoder_extl {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) : forall n (t : Vector.t Core.char n) n1 s ce v ce', enc _ t 0 s ce = Some (v, n1, ce') -> forall idx (t1 : Vector.t Core.char idx), enc _ (t1++t) idx s ce = Some (t1++v, idx+n1, ce').
proof: Proof. intros. match goal with | |- ?a = _ => destruct a eqn:? end. destruct_conjs. edestruct @AlignedEncoder_inv2 as [n2 [n3 [t2 [t23 [v23 ?]]]]]; try apply Heqo; eauto. destruct_conjs. assert (n2 + n3 = n) as L by omega. destruct L. rewrite <- Eqdep_dec.eq_rect_eq_dec in H3 by (apply Nat.eq_dec). rewrite <- Eqdep_dec.eq_rect_eq_dec in H4 by (apply Nat.eq_dec). subst. apply Vector_append_inj in H3. destruct_conjs. subst. edestruct @AlignedEncoder_some_inv; try apply H; eauto. edestruct @AlignedEncoder_some_inv; try apply H1; eauto. substss. injections. eauto. exfalso. edestruct @AlignedEncoder_some_inv; try apply H; eauto. eapply AlignedEncoder_none_inv in Heqo; eauto. eapply AlignedEncoder_sz_destruct' in H; eauto. omega. 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