proposition: Lemma injection_decode_correct {S V V' T} {cache : Cache} {P : CacheDecode -> Prop} {monoid : Monoid T} (inj : V -> V') (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (View'_Predicate : V' -> Prop) (format : FormatM S T) (view : S -> V -> Prop) (view' : S -> V' -> Prop) (view_format : FormatM V T) (view'_format : FormatM V' T) (decode_V : DecodeM (V * T) T) (decode_V_OK : CorrectDecoder monoid Source_Predicate View_Predicate view format decode_V P view_format) (view'_OK : forall s v, Source_Predicate s -> view s v -> view' s (inj v)) (View'_Predicate_OK : forall v, View_Predicate v -> View'_Predicate (inj v)) (view'_format_OK : forall v env t env' xenv' t', Equiv env env' -> P env' -> Equiv (snd t) xenv' -> decode_V (mappend (fst t) t') env' = Some (v, t', xenv') -> computes_to (view_format v env) t -> View_Predicate v -> computes_to (view'_format (inj v) env) t ) : CorrectDecoder monoid Source_Predicate View'_Predicate view' format (Compose_Decode decode_V (fun s => (inj (fst s), snd s))) P view'_format.
proof: Proof. eapply (injection_decode_correct' (fun v => Some (inj v))); intuition eauto; injections; intuition eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.InternetChecksum Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats Bedrock.Word