proposition: Lemma sequence_Compose_format_decode_refined_correct' {cache : Cache} {S V1 V2 T : Type} {P : CacheDecode -> Prop} {P_inv1 P_inv2 : (CacheDecode -> Prop) -> Prop} (P_inv_pf : cache_inv_Property P (fun P => P_inv1 P /\ P_inv2 P)) (monoid : Monoid T) (view : S -> V1 -> Prop) (view2 : S -> V2 -> Prop) (Source_Predicate : S -> Prop) (View_Predicate1 : V1 -> Prop) (format1 : FormatM V1 T) (format2 : FormatM S T ) (decode1 : DecodeM (V1 * T) T) (decode_1_OK : cache_inv_Property P P_inv1 -> CorrectDecoder monoid View_Predicate1 View_Predicate1 eq format1 decode1 P format1) (View_Predicate_OK : forall s v, Source_Predicate s -> view s v -> View_Predicate1 v) (decode2 : V1 -> DecodeM (V2 * T) T) (View_Predicate2 : V2 -> Prop) (subformat : FormatM S T) (view_format : FormatM V2 T) (decode2_pf : forall v1 : V1, cache_inv_Property P P_inv2 -> View_Predicate1 v1 -> CorrectRefinedDecoder monoid (fun s => Source_Predicate s /\ view s v1) View_Predicate2 view2 format2 subformat (decode2 v1) P view_format) : CorrectRefinedDecoder monoid Source_Predicate View_Predicate2 view2 (Compose_Format format1 view ++ format2)%format (Compose_Format format1 view ++ subformat)%format (sequence_Decode decode1 decode2) P (Compose_Format format1 (fun _ _ => True) ++ view_format)%format.
proof: Proof. intros. eapply format_decode_correct_alt. 6: apply EquivFormat_reflexive. Focus 6. { eapply injection_decode_correct. - eapply Sequence_refined_decoder_correct. + apply P_inv_pf. + intros; eapply Compose_decode_correct. intros; eapply decode_1_OK; eauto. intros; eapply View_Predicate_OK; eauto. + intros; eapply decode2_pf; eauto. + intros. instantiate (1 := (Projection_Format format1 fst ++ Projection_Format view_format snd)%format). unfold Projection_Format, Compose_Format, sequence_Format, ComposeOpt.compose, Bind2. apply unfold_computes; computes_to_econstructor. apply unfold_computes. simpl; eexists _; intuition eauto. apply unfold_computes; apply H. computes_to_econstructor. apply unfold_computes. simpl; eexists _; intuition eauto. apply unfold_computes; eauto. simpl; eauto. - simpl; intros; split_and; eauto. - simpl; intros; split_and; eauto. - simpl; intros. rewrite unfold_computes in H. split_and. split. + unfold Projection_Format, Compose_Format, sequence_Format, ComposeOpt.compose, Bind2 in *; apply unfold_computes in H0; computes_to_inv. rewrite unfold_computes in H0. rewrite unfold_computes in H0'; destruct_ex; intuition; subst. apply unfold_computes. computes_to_econstructor. apply unfold_computes. eexists _; split; eauto. computes_to_econstructor; eauto. + eauto. } all: try unfold flip, pointwise_relation, impl; intuition eauto using EquivFormat_reflexive. all: try unfold flip, pointwise_relation, impl; intuition eauto using EquivFormat_reflexive. unfold Compose_Decode, sequence_Decode, sequence_Decode'; simpl. destruct (decode1 a a0) as [ [ [? ?] ?] | ]; simpl; eauto. destruct (decode2 v t c)as [ [ [? ?] ?] | ]; simpl; eauto. Qed.
imports: Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Computation.Refinements.General Fiat.Narcissus.BaseFormats