proposition: Lemma weaken_view_pred S T V (cache : Cache) (monoid : Monoid T) (decode_inv : CacheDecode -> Prop) (View_Predicate : V -> Prop) (view : S -> V -> Prop) (format : FormatM S T) decode (Source_Predicate : S -> Prop) (View_Predicate_OK : forall s v, Source_Predicate s -> view s v -> View_Predicate v) : forall x y : V -> CacheFormat -> T * CacheFormat -> Prop, (forall (a : V) (a0 : CacheFormat) (a1 : T * CacheFormat), View_Predicate a -> x a a0 a1 -> y a a0 a1) -> CorrectDecoder monoid Source_Predicate View_Predicate view format decode decode_inv x -> CorrectDecoder monoid Source_Predicate View_Predicate view format decode decode_inv y.
proof: Proof. Local Transparent CorrectDecoder. unfold CorrectDecoder. intuition eauto; intros. - eapply H1 in H4. destruct_ex; split_and. rewrite H5; eexists _, _; intuition eauto. apply unfold_computes; eapply H; eauto. all: eauto. - eapply H2 in H4; intuition eauto. - eapply H2 in H4; intuition eauto. destruct_ex; split_and; subst; eexists _, _; intuition eauto. apply unfold_computes; eapply H; 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