proposition: Lemma cMethods_AbsR {Sig} {spec : ADT Sig} (impl : FullySharpened spec) midx (r_o : Rep spec) (r_n : cRep (projT1 impl)) (Abs : AbsR (projT2 impl) r_o r_n) : @Lift_Method2P _ _ _ _ (fun _ Meth cMeth => exists r_o', computes_to Meth (r_o', (snd cMeth)) /\ AbsR (projT2 impl) r_o' (fst cMeth)) (fun Meth cMeth => exists r_o', computes_to Meth (r_o') /\ AbsR (projT2 impl) r_o' cMeth) (Methods spec midx r_o) (cMethods (projT1 impl) midx r_n).
proof: Proof. simpl in *. generalize (ADTRefinementPreservesMethods (projT2 impl) midx _ _ Abs). intro. eapply Lift_Method2P_ind with (P'' := fun dom cod meth (cMeth : cMethodType' _ dom cod) => refineMethod' (AbsR (projT2 impl)) meth (LiftcMethod' _ dom cod cMeth)) ; simpl; intros; eauto. - revert H0; clear; destruct (MethodDomCod Sig midx) as [? [? |] ]; simpl; intros; specialize (H0 _ (ReturnComputes _)); computes_to_inv; subst; eexists; split; simpl; try destruct v; simpl; eauto. simpl; eauto. Qed.
imports: Coq.Lists.List Coq.Strings.String Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.ADT.Core Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms