proposition: Lemma decode_None : forall (monoid : Monoid T) (Source_Predicate : S -> Prop) (format : S -> CacheFormat -> Comp (T * CacheFormat)) (decode : T -> CacheDecode -> option (S * T * CacheDecode)) (decode_inv : CacheDecode -> Prop) (Source_Predicate_dec : forall a, {Source_Predicate a} + {~ Source_Predicate a}), CorrectDecoder monoid Source_Predicate Source_Predicate eq format decode decode_inv format -> forall b env' env, Equiv env env' -> decode b env' = None -> decode_inv env' -> forall s, ~ Source_Predicate s \/ ~ exists xenv, format s env ∋ (b, xenv).
proof: Proof. intros. destruct (Source_Predicate_dec s); try (solve [intuition]). right. intros [? ?]. destruct ((proj1 H) env env' _ s _ mempty H2 H0 s0 H3); intuition; destruct_ex; intuition. rewrite mempty_right in H5; congruence. 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