proposition: Lemma Sequence_decode_correct {S V1 V2 : Type} {P : CacheDecode -> Prop} {P_inv1 P_inv2 : (CacheDecode -> Prop) -> Prop} (P_inv_pf : cache_inv_Property P (fun P => P_inv1 P /\ P_inv2 P)) (view1 : S -> V1 -> Prop) (view2 : V1 -> S -> V2 -> Prop) (Source_Predicate : S -> Prop) (View_Predicate2 : V1 -> V2 -> Prop) (View_Predicate1 : V1 -> Prop) (consistency_predicate : V1 -> S -> Prop) (format1 format2 : FormatM S T ) (decode1 : DecodeM (V1 * T) T) (view_format1 : FormatM V1 T) (decode1_pf : cache_inv_Property P P_inv1 -> CorrectDecoder monoid Source_Predicate View_Predicate1 view1 format1 decode1 P view_format1) (consistency_predicate_OK : forall s v1 t1 t2 env xenv xenv', computes_to (format1 s env) (t1, xenv) -> computes_to (view_format1 v1 env) (t2, xenv') -> view1 s v1 -> consistency_predicate v1 s) (decode2 : V1 -> DecodeM (V2 * T) T) (view_format2 : V1 -> FormatM V2 T) (view_format3 : FormatM (V1 * V2) T) (decode2_pf : forall v1 : V1, cache_inv_Property P P_inv2 -> View_Predicate1 v1 -> CorrectDecoder monoid (fun s => Source_Predicate s /\ consistency_predicate v1 s) (View_Predicate2 v1) (view2 v1) format2 (decode2 v1) P (view_format2 v1)) (view_format3_OK : forall v1 t1 env1 xenv1 v2 t2 xenv2, view_format1 v1 env1 (t1, xenv1) -> view_format2 v1 v2 xenv1 (t2, xenv2) -> View_Predicate1 v1 -> view_format3 (v1, v2) env1 (mappend t1 t2, xenv2)) : CorrectDecoder monoid Source_Predicate (fun v1v2 => View_Predicate1 (fst v1v2) /\ View_Predicate2 (fst v1v2) (snd v1v2)) (fun s v1v2 => view1 s (fst v1v2) /\ view2 (fst v1v2) s (snd v1v2)) (format1 ++ format2) (sequence_Decode' decode1 decode2) P view_format3.
proof: Proof. unfold cache_inv_Property, sequence_Decode, sequence_Format, compose in *; split. { intros env env' xenv s t ext ? env_pm pred_pm com_pf. unfold compose, Bind2 in com_pf; computes_to_inv; destruct v; destruct v0. destruct (fun H => proj1 (decode1_pf (proj1 P_inv_pf)) _ _ _ _ _ (mappend t1 ext) env_OK env_pm H com_pf); eauto; destruct_ex; split_and; simpl in *; injections; eauto. unfold sequence_Decode', DecodeBindOpt2, BindOpt. setoid_rewrite <- mappend_assoc; rewrite H0. pose proof (proj2 (decode1_pf H3) _ _ _ _ _ _ env_pm env_OK H0); split_and; destruct_ex; split_and. destruct (fun H => proj1 (decode2_pf x H5 H9) _ _ _ _ _ ext H4 H2 H com_pf'). split; try eassumption. eauto. destruct_ex; split_and. simpl. rewrite H12; eexists _, _; simpl; intuition eauto. apply unfold_computes. rewrite unfold_computes in H1. eapply view_format3_OK; eauto. } { intros ? ? ? ? t; intros. unfold sequence_Decode', DecodeBindOpt2, BindOpt in H1. destruct (decode1 t env') as [ [ [? ?] ? ] | ] eqn : ? ; simpl in *; try discriminate. generalize Heqo; intros Heqo'. eapply (proj2 (decode1_pf (proj1 P_inv_pf))) in Heqo; eauto. split_and; destruct_ex; split_and. subst. destruct (decode2 v0 t0 c) as [ [ [? ?] ? ] | ] eqn : ? ; simpl in *; try discriminate; injections. eapply (proj2 (decode2_pf _ H5 H7)) in Heqo; eauto. destruct Heqo as [? ?]; destruct_ex; split_and; subst. setoid_rewrite mappend_assoc. split; eauto. eexists _, _; repeat split; eauto. apply unfold_computes. eapply view_format3_OK; try eassumption. apply unfold_computes; eassumption. apply unfold_computes; eassumption. } Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.Notations Fiat.Narcissus.Formats.Base.FMapFormat Fiat.Narcissus.Formats.Base.LaxTerminalFormat