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, computes_to (view_format v env) t -> 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: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs