proposition: Lemma ExtractViewFrom {S V T} : forall (cache : Cache) (monoid : Monoid T) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (view : S -> V -> Prop) (View_Format : FormatM V T) (decode_inv : CacheDecode -> Prop) (v : V) (v_OK : View_Predicate v), (forall s', Source_Predicate s' -> view s' v) -> (forall env, View_Format v env ∋ (mempty, env)) -> CorrectDecoder monoid Source_Predicate View_Predicate view empty_Format (fun t' ctxD => Some (v, t', ctxD)) decode_inv View_Format.
proof: Proof. unfold CorrectDecoder; split; intros. - eexists v, env'; pose proof (H _ H2); subst. unfold empty_Format in H3; computes_to_inv; injections. intuition eauto. rewrite mempty_left; eauto. - injections. intuition eauto. eexists mempty, _; intuition eauto. rewrite mempty_left; reflexivity. Qed.
imports: Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Computation.Refinements.General Fiat.Narcissus.BaseFormats