proposition: Lemma Sequence_refined_decoder_correct {S V1 V2 T : Type} {monoid : Monoid T} {cache : Cache} {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) (format1 format2 subformat : 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) (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 -> CorrectRefinedDecoder monoid (fun s => Source_Predicate s /\ view1 s v1) (View_Predicate2 v1) (view2 v1) format2 subformat (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)) : CorrectRefinedDecoder 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) (format1 ++ subformat) (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 ComposeOpt.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. simpl. 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. rewrite unfold_computes in H13; split_and. split. eapply view_format3_OK; eauto. intros. simpl. unfold ComposeOpt.compose, Bind2 in H19; computes_to_inv; simpl in *; injections; destruct v; destruct v0; simpl in *. eapply (proj1 H15) in H19. rewrite mappend_assoc in H0; rewrite <- H21 in H0. rewrite <- mappend_assoc in H0. rewrite H0 in H19; destruct_ex; split_and. injections; eauto. split; eauto. all: eauto. eapply decode2_pf in H19'; split_and; destruct_ex; split_and. rewrite <- H26 in H24. rewrite H12 in H24. injections; intuition eauto. all: 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. generalize Heqo as Heqo''; intro. eapply (proj2 (decode2_pf _ H5 H7)) in Heqo; eauto. destruct Heqo as [? ?]; destruct_ex; split_and; subst. setoid_rewrite mappend_assoc. split; eauto. eexists _, _; split; eauto. apply unfold_computes; split. eapply view_format3_OK; try eassumption. apply unfold_computes; eassumption. rewrite unfold_computes in H8. apply unfold_computes; intuition eauto. intros; unfold ComposeOpt.compose, Bind2 in H11; computes_to_inv; simpl in *; injections; destruct v; destruct v2; simpl in *. eapply (proj1 (decode1_pf _)) in H11. rewrite mappend_assoc in Heqo'; rewrite <- H14 in Heqo'. rewrite <- mappend_assoc in Heqo'. rewrite Heqo' in H11; destruct_ex; split_and. injections; eauto. all: eauto. eapply decode2_pf in H11'; split_and; destruct_ex; split_and. rewrite H19 in Heqo''. rewrite Heqo'' in H17. injections; intuition eauto. all: eauto. } Unshelve. eauto. 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