proposition: Lemma composeIf_subformat_correct_low {S T} {cache : Cache} {P : CacheDecode -> Prop} {monoid : Monoid T} {richmonoid : RichMonoidOpt monoid} (Source_Predicate : S -> Prop) (formatT formatE : FormatM S T) (subformat : FormatM S T) (decodeB : DecodeM (bool * T) T) (decodeB_OK : forall env env' xenv s t ext, P env' -> Equiv env env' -> Source_Predicate s -> subformat s env ∋ (t, xenv) -> exists v xenv', decodeB (mappend t ext) env' = Some (v, ext, xenv') /\ Equiv xenv xenv' /\ P xenv') (decodeB_OK' : forall env env' xenv' v t t', Equiv env env' -> P env' -> decodeB t env' = Some (v, t', xenv') -> P xenv' /\ exists t'' xenv, (forall s t1 xenv, Source_Predicate s -> (formatT s env ∋ (mappend t'' t1, xenv) -> v = true) /\ (formatE s env ∋ (mappend t'' t1, xenv) -> v = false)) /\ t = mappend t'' t' /\ Equiv xenv xenv') : 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))).
proof: Proof. split; intros. { edestruct decodeB_OK; eauto. destruct_conjs. eexists _, _; intuition eauto. rewrite unfold_computes; repeat split; simpl; intros; rewrite <- unfold_computes in H7; edestruct decodeB_OK' with (env:=env); eauto; destruct_conjs; apply mappend_inj in H12; subst; eapply H11; eauto. } { edestruct decodeB_OK' with (env:=env); eauto. destruct_conjs. subst. intuition eauto. eexists _, _. rewrite unfold_computes; simpl. intuition eauto 1; rewrite <- unfold_computes in H8; eapply H5; eauto. } Qed.
imports: Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations Fiat.Narcissus.BaseFormats