proposition: Lemma composeIf_format_correct {S V T} {cache : Cache} {P : CacheDecode -> Prop} {P_invT P_invE : (CacheDecode -> Prop) -> Prop} (P_inv_pf : cache_inv_Property P (fun P => P_invT P /\ P_invE P)) (monoid : Monoid T) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (view : S -> V -> Prop) (ICompb : T -> bool) (formatT formatE : FormatM S T) (decodeT decodeE : DecodeM (V * 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) (ICompb_OKT : forall data bin env xenv ext, Source_Predicate data -> formatT data env ↝ (bin, xenv) -> ICompb (mappend bin ext) = true) (ICompb_OKE : forall data bin env xenv ext, Source_Predicate data -> formatE data env ↝ (bin, xenv) -> ICompb (mappend bin ext) = false) : CorrectDecoder monoid Source_Predicate View_Predicate view (composeIf formatT formatE) (fun (b : T) (env : CacheDecode) => If ICompb b Then decodeT b env Else decodeE b 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. unfold composeIf, Union_Format, Bind2 in com_pf. rewrite unfold_computes in com_pf; destruct_ex. revert H; pattern x; apply IterateBoundedIndex.Iterate_Ensemble_BoundedIndex_equiv; simpl. constructor; intros; [ | constructor; eauto]. - erewrite ICompb_OKT; eauto. eapply (decodeT_pf (proj1 P_inv_pf)) with (ext := ext) in H; eauto. destruct_ex; split_and. simpl; eexists _, _; intuition eauto. unfold composeIf, Union_Format. apply unfold_computes; eexists Fin.F1; simpl; eauto. - intros; erewrite ICompb_OKE; eauto. eapply (decodeE_pf (proj2 P_inv_pf)) with (ext := ext) in H; eauto. destruct_ex; split_and. simpl; eexists _, _; intuition eauto. unfold composeIf, Union_Format. apply unfold_computes; eexists (Fin.FS Fin.F1); simpl; eauto. } { intros. destruct (ICompb t) eqn : IComp_v ; simpl in *. - eapply decodeT_pf in H1; intuition eauto. destruct_ex; intuition; eexists _, _; unfold composeIf; intuition eauto. unfold Union_Format; apply unfold_computes; eexists (Fin.F1); simpl; eauto. - eapply decodeE_pf in H1; intuition eauto. destruct_ex; intuition; eexists _, _; unfold composeIf; intuition eauto. unfold Union_Format; apply unfold_computes; eexists (Fin.FS Fin.F1); simpl; eauto. } Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats