proposition: Lemma option_format_correct' {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)) (Source_Predicate : option S -> Prop) (Some_View_Predicate : VS -> Prop) (None_View_Predicate : VN -> Prop) (viewS : S -> VS -> Prop) (viewN : () -> VN -> Prop) (b' : bool) (predicate := fun a_opt => decides (negb b') (a_opt = None) /\ Source_Predicate a_opt) (format_Some : FormatM S T) (format_None : FormatM () T) (decode_Some : DecodeM (VS * T) T) (decode_None : DecodeM (VN * T) T) (view_format_Some : FormatM VS T) (view_format_None : FormatM VN T) (decode_Some_pf : cache_inv_Property P P_invT -> CorrectDecoder monoid (fun s => Source_Predicate (Some s)) Some_View_Predicate viewS format_Some decode_Some P view_format_Some) (decode_None_pf : cache_inv_Property P P_invE -> CorrectDecoder monoid (fun _ => Source_Predicate None) None_View_Predicate viewN format_None decode_None P view_format_None) : CorrectDecoder monoid predicate (fun v_opt => match v_opt with | inl vs => Some_View_Predicate vs /\ b' = true | inr vn => None_View_Predicate vn /\ b' = false end) (fun s_opt v_opt => match s_opt, v_opt with | Some s, inl vs => viewS s vs | None, inr vn => viewN () vn | _, _ => False end) (format_option format_Some format_None) (option_decode' decode_Some decode_None b') P (fun v_opt => match v_opt with | inl vs => view_format_Some vs | inr vn => view_format_None vn end ).
proof: Proof. unfold cache_inv_Property in *; split. { intros env env' xenv data bin ext ? env_pm pred_pm com_pf. unfold format_option in com_pf; computes_to_inv; unfold option_decode'; destruct data; find_if_inside; unfold predicate in *; simpl in *; intuition; try discriminate. - eapply H3 in com_pf; destruct_ex; subst; intuition eauto; rewrite H6; eauto. subst; eexists _, _; eauto. - eapply H4 in com_pf; destruct_ex; intuition eauto; rewrite H6; eauto. subst; eexists _, _; eauto. } { unfold option_decode'; intros. find_if_inside; simpl in *. - destruct (decode_Some t env') as [ [ [? ?] ?] | ] eqn : ? ; simpl in *; try discriminate; injections; simpl. eapply decode_Some_pf in Heqo; intuition eauto. destruct_ex; split_and; eexists _, _; intuition eauto. - destruct (decode_None t env') as [ [ [? ?] ?] | ] eqn : ? ; simpl in *; try discriminate; injections. eapply decode_None_pf in Heqo; intuition eauto; destruct_ex; intuition eauto; subst. destruct_ex; split_and; eexists _, _; intuition eauto. } Qed.
imports: Fiat.Common Fiat.Computation Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats