proposition: Lemma CorrectDecoder_equiv_CorrectDecoder_id : forall (monoid : Monoid T) (Source_Predicate : S -> Prop) (format : FormatM) encode (correctEncode : CorrectEncoder format encode) (decode : T -> CacheDecode -> option (S * T * CacheDecode)) (decode_inv : CacheDecode -> Prop), (CorrectDecoder_id monoid Source_Predicate format decode decode_inv <-> CorrectDecoder monoid Source_Predicate Source_Predicate eq format decode decode_inv format).
proof: Proof. unfold CorrectDecoder_id, CorrectDecoder; intuition eauto. - generalize H3; intro; eapply H0 in H3; destruct_ex; split_and; eauto. rewrite H5; eexists _, _; intuition eauto. - eapply H0 in H3; destruct_ex; split_and; eauto. rewrite H3; eexists _; subst; 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