proposition: Lemma CorrectDecoderStrengthenFormat : forall (monoid : Monoid T) {V} (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (view : S -> V -> Prop) (format : S -> CacheFormat -> Comp (T * CacheFormat)) (decode : T -> CacheDecode -> option (V * T * CacheDecode)) (decode_inv : CacheDecode -> Prop) (Source_Predicate_dec : forall a, {Source_Predicate a} + {~ Source_Predicate a}) view_format , CorrectDecoder monoid Source_Predicate View_Predicate view format decode decode_inv view_format -> CorrectDecoder monoid Source_Predicate View_Predicate view (fun a s b => (format a s ∋ b) /\ Source_Predicate a) decode decode_inv view_format.
proof: Proof. intros; destruct H as [? ? ]; unfold CorrectDecoder; split; intros. - eapply H; eauto. apply (proj1 H3). - eapply H0 in H3; intuition eauto. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache