proposition: Lemma refineObserverTrans {oldRep newRep} : forall (AbsR : oldRep -> newRep -> Prop) (dom : list Type) (cod : option Type) (oldObserver : observerType oldRep dom cod) (oldMethod : methodType oldRep dom cod) (newMethod : methodType newRep dom cod), refineObserver eq oldObserver oldMethod -> refineMethod AbsR oldMethod newMethod -> refineObserver AbsR oldObserver newMethod.
proof: Proof. unfold refineObserver; induction dom; simpl. - destruct cod; intros. + setoid_rewrite <- H0; eauto. setoid_rewrite <- H; eauto. repeat setoid_rewrite refineEquiv_bind_bind; f_equiv. intro. repeat setoid_rewrite refineEquiv_bind_unit; simpl. intros v Comp_v; computes_to_inv; subst; repeat computes_to_econstructor. eauto. + setoid_rewrite <- H0; eauto. rewrite <- H by eauto. repeat setoid_rewrite refineEquiv_bind_bind; f_equiv. intro. intros v Comp_v; computes_to_inv; subst; repeat computes_to_econstructor; eauto. - intros. eapply IHdom with (oldObserver := fun r_o => oldObserver r_o d) (oldMethod := fun r_o => oldMethod r_o d) (newMethod := fun r_n => newMethod r_n d); intros; subst; eauto. unfold refineMethod; intros; eapply H; eauto. unfold refineMethod; intros; eauto. Qed.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory