proposition: Lemma AlignedFormatListDoneC {A} (A_OK : A -> Prop) format_A (encode_An : A -> CacheFormat -> nat) (encode_A1 : forall a ce, t (word 8) (encode_An a ce)) (encode_A2 : A -> CacheFormat -> CacheFormat) : forall (l : list A) ce, (forall (a : A) (ce : CacheFormat), A_OK a -> refine (format_A a ce) (ret (build_aligned_ByteString (encode_A1 a ce), encode_A2 a ce))) -> (forall a : A, In a l -> A_OK a) -> refine (((format_list format_A l) DoneC) ce) (ret (build_aligned_ByteString (projT2 (fst (align_format_list (fun a ce => (existT _ _ (encode_A1 a ce), encode_A2 a ce)) l ce))), let (v, ce'') := align_format_list (fun a ce => (existT _ _ (encode_A1 a ce), encode_A2 a ce)) l ce in ce'')).
proof: Proof. intros. etransitivity. eapply AlignedFormatDoneC. rewrite (optimize_align_format_list A_OK format_A (fun a ce => (existT _ _ (encode_A1 a ce), encode_A2 a ce))); try eassumption. match goal with |- context [let (v, c) := ?z in ret (@?b v c)] => rewrite (zeta_inside_ret z _) end. rewrite zeta_to_fst; simpl. instantiate (2 := fun ce => fst (_ ce)). instantiate (1 := fun ce => snd (_ ce)). simpl; reflexivity. intros; rewrite zeta_to_fst; simpl; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BaseFormats Bedrock.Word