proposition: Lemma refine_AbsMethod' : forall (Dom : list Type) (Cod : option Type) (oldMethod : methodType _ Dom Cod) refinedMeth, refineMethod eq (absMethod (cod := Cod) AbsR oldMethod) refinedMeth -> (forall nr or, AbsR or nr -> refineMethod' AbsR (oldMethod or) (refinedMeth nr)).
proof: Proof. unfold refineMethod; intros; subst. induction Dom; destruct Cod; simpl; intros. - intros v ComputesTo_v; subst. eapply H in ComputesTo_v; eauto. unfold absMethod; simpl in *. computes_to_inv; subst. apply ComputesTo_v in H0; destruct_ex; intuition; subst. destruct x; destruct v0; simpl in *; subst. repeat computes_to_econstructor; eauto. - intros v ComputesTo_v; subst. eapply H in ComputesTo_v; eauto. unfold absMethod; simpl in *. computes_to_inv; subst. apply ComputesTo_v in H0; destruct_ex; intuition; subst. repeat computes_to_econstructor; eauto. - eapply IHDom with (oldMethod := fun r_o => oldMethod r_o d) (refinedMeth := fun r_n => refinedMeth r_n d); intros; eapply H; eauto. - eapply IHDom with (oldMethod := fun r_o => oldMethod r_o d) (refinedMeth := fun r_n => refinedMeth r_n d); intros; eapply H; eauto. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.ADTRefinement.Refinements.HoneRepresentation Fiat.ADTRefinement.BuildADTSetoidMorphisms