proposition: Lemma correct_component_derives_compliant_semantics `{MayProvide jx j} `(c : component i jx) `(ci : contract i Ωi) `(cj : contract j Ωj) (pred : Ωi -> Ωj -> Prop) (correct : correct_component c ci cj pred) (ωi : Ωi) (ωj : Ωj) (inv : pred ωi ωj) (sem : semantics jx) (comp : compliant_semantics cj ωj sem) : compliant_semantics ci ωi (derive_semantics c sem).
proof: Proof. rewrite derive_semantics_equ. revert ωi ωj inv sem comp. cofix correct_component_derives_compliant_semantics. intros ωi ωj inv sem comp. unfold correct_component in correct. specialize (correct ωi ωj inv). constructor; intros a e req; specialize (correct a e req); destruct correct as [trust run]. + eapply run. cbn. ++ rewrite instrument_to_state_eval_morphism with (c0 := cj) (ω := ωj). now apply instrument_satisfies_hoare. + eapply correct_component_derives_compliant_semantics. ++ apply run. cbn. erewrite instrument_to_state_eval_morphism. apply instrument_satisfies_hoare. +++ exact comp. +++ exact trust. ++ erewrite instrument_to_state_exec_morphism. apply instrument_preserves_compliance. +++ exact comp. +++ apply trust. Qed.
imports: ExtLib(StateMonad) FreeSpec.Core(Contract HoareFacts SemanticsFacts InstrumentFacts)