proposition: Lemma CorrectDecodeEncode {S T} {cache : Cache} {monoid : Monoid T} : forall Invariant (FormatSpec : FormatM S T) (encoder : CorrectEncoderFor FormatSpec) (decoder : CorrectDecoderFor Invariant FormatSpec), forall a envE envD b envE', Equiv envE envD -> Invariant a -> snd (proj1_sig decoder) envD -> projT1 encoder a envE = Some (b, envE') -> exists envD', fst (proj1_sig decoder) b envD = Some (a, mempty, envD').
proof: Proof. intros. destruct encoder as [encoder encoder_OK]. destruct decoder as [decoder [Inv [decoder_OK Inv_cd] ] ]; simpl in *. specialize (proj1 (encoder_OK a envE) _ H2); intro. specialize (decoder_OK Inv_cd). destruct decoder_OK as [decoder_OK _]. unfold cache_inv_Property in Inv_cd. eapply decoder_OK with (ext := mempty) in H3; eauto. destruct_ex; intuition. subst; rewrite mempty_right in H4; 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