proposition: Lemma Compose_decode_correct {S V T} {cache : Cache} {P : CacheDecode -> Prop} {monoid : Monoid T} (view : S -> V -> Prop) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (format : FormatM V T) (view_format : FormatM V T) (decode_V : DecodeM (V * T) T) (decode_V_OK : CorrectDecoder monoid View_Predicate View_Predicate eq format decode_V P view_format) (View_Predicate_OK : forall s v, view s v -> Source_Predicate s -> View_Predicate v) : CorrectDecoder monoid Source_Predicate View_Predicate view (Compose_Format format view) decode_V P view_format.
proof: Proof. unfold CorrectDecoder, Projection_Format, Compose_Format; split; intros. { rewrite @unfold_computes in H1; destruct_ex; intuition. apply proj1 in decode_V_OK; eapply decode_V_OK with (ext := ext) in H2; eauto. destruct_ex; intuition; subst; eauto. eexists _, _; intuition eauto. } { apply proj2 in decode_V_OK; eapply decode_V_OK in H1; clear decode_V_OK; eauto. } Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs