proposition: Lemma contract_equ_trans `(c1 : contract i Ω1) `(c2 : contract i Ω2) `(c3 : contract i Ω3) `(is_equ12 : contract_equ c1 c2) `(is_equ23 : contract_equ c2 c3) : contract_equ c1 c3.
proof: Proof. destruct is_equ12 as [f12 g21 isofg12 isogf12 caller_equ12 callee_equ12 witness_equ12]. destruct is_equ23 as [f23 g32 isofg23 isogf23 caller_equ23 callee_equ23 witness_equ23]. apply mk_contract_equ with (f:=fun x => f23 (f12 x)) (g:=fun x => g21 (g32 x)). + setoid_rewrite isofg12. now setoid_rewrite isofg23. + setoid_rewrite isogf23. now setoid_rewrite isogf12. + intros ω1 α p. transitivity (caller_obligation c2 (f12 ω1) p); [ now apply caller_equ12 | now apply caller_equ23 ]. + intros ω1 α p x. transitivity (callee_obligation c2 (f12 ω1) p x); [ now apply callee_equ12 | now apply callee_equ23 ]. + intros ω1 α p x. rewrite <- witness_equ23. assert (equ : f12 (witness_update c1 ω1 p x) = witness_update c2 (f12 ω1) p x) by now rewrite <- witness_equ12. now rewrite equ. Defined.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)