proposition: Lemma If_Then_Else_format_correct {A B} {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 B) (predicate predicateT predicateE : A -> Prop) (predicate_rest : A -> B -> Prop) (proj : A -> bool) (ICompb : B -> bool) (formatT : A -> CacheFormat -> Comp (B * CacheFormat)) (decodeT : B -> CacheDecode -> option (A * B * CacheDecode)) (formatE : A -> CacheFormat -> Comp (B * CacheFormat)) (decodeE : B -> CacheDecode -> option (A * B * CacheDecode)) (decodeT_pf : cache_inv_Property P P_invT -> CorrectDecoder cache monoid predicateT predicate_rest formatT decodeT P) (decodeE_pf : cache_inv_Property P P_invE -> CorrectDecoder cache monoid predicateE predicate_rest formatE decodeE P) (ICompb_OKT : forall data bin env xenv ext, predicateT data -> formatT data env ↝ (bin, xenv) -> ICompb (mappend bin ext) = true) (ICompb_OKT' : forall data bin env xenv ext, ICompb bin = true -> decodeT bin env = Some (data, ext, xenv) -> proj data = true) (ICompb_OKE : forall data bin env xenv ext, predicateE data -> formatE data env ↝ (bin, xenv) -> ICompb (mappend bin ext) = false) (ICompb_OKE' : forall data bin env xenv ext, ICompb bin = false -> decodeE bin env = Some (data, ext, xenv) -> proj data = false) (predicateT_OK : forall a, proj a = true -> (predicate a <-> predicateT a)) (predicateE_OK : forall a, proj a = false -> (predicate a <-> predicateE a)) : CorrectDecoder cache monoid (fun a => predicate a) predicate_rest (fun (data : A) (ctx : CacheFormat) => (If (proj data) Then (formatT data ctx) Else (formatE data ctx)) )%comp (fun (b' : B) (env : CacheDecode) => If ICompb b' Then decodeT b' env Else decodeE b' env ) P.
proof: Proof. unfold cache_inv_Property in *; split. { intros env env' xenv data bin ext ? env_pm pred_pm pred_pm_rest com_pf. specialize (predicateT_OK data). specialize (predicateE_OK data). destruct (proj data); simpl in com_pf. - erewrite ICompb_OKT; eauto. simpl; eapply decodeT_pf; intuition eauto. intuition eauto. - erewrite ICompb_OKE; eauto. simpl; eapply decodeE_pf; intuition eauto. intuition eauto. } { intros. destruct (ICompb bin) eqn : IComp_v ; simpl in *. - rewrite (ICompb_OKT' _ _ _ _ _ IComp_v H1). pose proof H1. eapply decodeT_pf in H1; simpl in *; intuition eauto. destruct_ex; eexists _, _; intuition eauto. eapply predicateT_OK; try eassumption. erewrite ICompb_OKT'; eauto. - rewrite (ICompb_OKE' _ _ _ _ _ IComp_v H1). pose proof H1. eapply decodeE_pf in H1; intuition eauto. destruct_ex; eexists _, _; intuition eauto. eapply predicateE_OK; try eassumption. erewrite ICompb_OKE'; eauto. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.Ascii Coq.Strings.String Coq.Numbers.BinNums Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Bedrock.Word Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Automation.Solver Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders