proposition: Lemma CorrectEncodeDecode {S T} {cache : Cache} {monoid : Monoid T} : forall Invariant (FormatSpec : FormatM S T) (decoder : CorrectDecoderFor Invariant FormatSpec), forall bs ce cd cd' s ext, Equiv ce cd -> snd (proj1_sig decoder) cd -> fst (proj1_sig decoder) bs cd = Some (s, ext, cd') -> Invariant s /\ exists ce' bs', bs = mappend bs' ext /\ Equiv ce' cd' /\ FormatSpec s ce (bs', ce').
proof: Proof. intros. destruct decoder as [decoder [Inv [decoder_OK Inv_cd] ] ]; simpl in *. specialize (decoder_OK Inv_cd). destruct decoder_OK as [_ decoder_OK]. eapply decoder_OK in H1; eauto. intuition; destruct_ex; 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