proposition: Corollary CorrectDecoderEmpty {S T} : forall (cache : Cache) (monoid : Monoid T) (Source_Predicate : S -> Prop) (decode_inv : CacheDecode -> Prop) (s : S) (b : bool), (forall s', Source_Predicate s' -> s' = s) -> decides b (Source_Predicate s) -> CorrectDecoder monoid Source_Predicate Source_Predicate eq empty_Format (fun t' ctxD => if b then Some (s, t', ctxD) else None) decode_inv empty_Format.
proof: Proof. intros. find_if_inside. - eapply ExtractViewFrom; eauto; unfold empty_Format; eauto. - unfold CorrectDecoder, empty_Format; split; intros. + exfalso; eapply H0. rewrite <- (H _ H2); eassumption. + discriminate. 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