proposition: Lemma composeIf_format_correct' {S V T} {cache : Cache} {P : CacheDecode -> Prop} {P_invT P_invE P_invS: (CacheDecode -> Prop) -> Prop} (P_inv_pf : cache_inv_Property P (fun P => P_invT P /\ P_invE P /\ P_invS P)) (monoid : Monoid T) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (view : S -> V -> Prop) (formatT formatE : FormatM S T) (subformat : FormatM S T) (decodeT decodeE : DecodeM (V * T) T) (decodeB : DecodeM (bool * T) T) (view_formatT view_formatE : FormatM V T) (decodeT_pf : cache_inv_Property P P_invT -> CorrectDecoder monoid Source_Predicate View_Predicate view formatT decodeT P view_formatT) (decodeE_pf : cache_inv_Property P P_invE -> CorrectDecoder monoid Source_Predicate View_Predicate view formatE decodeE P view_formatE) (decodeB_pf : cache_inv_Property P P_invS -> CorrectRefinedDecoder monoid Source_Predicate (fun bs => True) (fun s bs => True) (composeIf formatT formatE) subformat decodeB P (fun bs env t => (forall s t' env', Source_Predicate s -> (formatT s env (mappend (fst t) t', env') -> bs = true) /\ (formatE s env (mappend (fst t) t', env') -> bs = false))) /\ Prefix_Format _ (composeIf formatT formatE) subformat) : CorrectDecoder monoid Source_Predicate View_Predicate view (composeIf formatT formatE) (fun (t : T) (env : CacheDecode) => `(b, _, _) <- decodeB t env; If b Then decodeT t env Else decodeE t env ) P (composeIf view_formatT view_formatE).
proof: Proof. unfold cache_inv_Property in *; split. { intros env env' xenv data bin ext ? env_pm pred_pm com_pf. generalize com_pf; intro. subst. unfold composeIf, Union_Format, Bind2 in com_pf0. rewrite unfold_computes in com_pf0; destruct_ex. revert H; pattern x; apply IterateBoundedIndex.Iterate_Ensemble_BoundedIndex_equiv; simpl. constructor; intros; [ | constructor; eauto]. - eapply (proj2 (decodeB_pf (proj2 (proj2 P_inv_pf)))) in com_pf; eauto; destruct_ex; split_and; intros. subst. eapply H0 in H2; eauto. destruct_ex; split_and. rewrite <- mappend_assoc. rewrite H2; simpl. rewrite unfold_computes in H5. rewrite (proj1 (proj1 H5 _ _ _ pred_pm) H); simpl. eapply decodeT_pf in H; destruct_ex; split_and. rewrite mappend_assoc. rewrite H9; eexists _, _; intuition eauto. unfold composeIf, Union_Format; apply unfold_computes; exists Fin.F1; simpl; eauto. eauto. eauto. eauto. eauto. - eapply (proj2 (decodeB_pf (proj2 (proj2 P_inv_pf)))) in com_pf; eauto; destruct_ex; split_and; intros. subst. eapply H in H1; eauto. destruct_ex; split_and. rewrite <- mappend_assoc. rewrite H1; simpl. rewrite unfold_computes in H7. rewrite (proj2 (proj1 H7 _ _ _ pred_pm) H4); simpl. eapply decodeE_pf in H4; destruct_ex; split_and. rewrite mappend_assoc. rewrite H9; eexists _, _; intuition eauto. unfold composeIf, Union_Format; apply unfold_computes; exists (Fin.FS Fin.F1); simpl; eauto. eauto. eauto. eauto. eauto. } { intros. destruct (decodeB t env') as [ [ [? ?] ? ] | ] eqn: ? ; simpl in *; try discriminate. destruct b; simpl in *. - eapply decodeT_pf in H1. split_and; destruct_ex; intuition eauto; subst. eexists _, _; intuition eauto. unfold composeIf, Union_Format; apply unfold_computes; exists Fin.F1; simpl; eauto. intuition. eauto. intuition. - eapply decodeE_pf in H1. split_and; destruct_ex; intuition eauto; subst. eexists _, _; intuition eauto. unfold composeIf, Union_Format; apply unfold_computes; exists (Fin.FS Fin.F1); simpl; eauto. intuition. eauto. intuition. } Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats