proposition: Lemma refineADT_BuildADT_ReplaceMethod (Rep : Type) {n n'} (consSigs : Vector.t consSig n) (methSigs : Vector.t methSig n') (consDefs : ilist (B := @consDef Rep) consSigs) (methDefs : ilist (B := @methDef Rep) methSigs) (idx : @Fin.t n') (newDef : methDef (Vector.nth methSigs idx)) AbsR (AbsR_reflexive_constructor : forall consIdx, refineConstructor AbsR (getConsDef consDefs consIdx) (getConsDef consDefs consIdx)) (AbsR_reflexive_method : forall methIdx, refineMethod AbsR (getMethDef methDefs methIdx) (getMethDef methDefs methIdx)) : refineMethod AbsR (methBody (ith methDefs idx)) (methBody newDef) -> refineADT (BuildADT consDefs methDefs) (ADTReplaceMethDef consDefs methDefs idx newDef).
proof: Proof. intros; eapply refineADT_BuildADT_Rep with (AbsR := AbsR); trivial. intros; unfold getMethDef. unfold replaceMethDef. destruct (fin_eq_dec methIdx idx); subst. rewrite ith_replace_Index_eq; eauto. rewrite ith_replace_Index_neq; eauto. Qed.
imports: Coq.Lists.List Coq.Arith.Arith Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADT.ComputationalADT Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildComputationalADT Fiat.ADTNotation.BuildADTReplaceMethods Fiat.ADTRefinement.Core Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.BuildADTSetoidMorphisms Coq.Strings.String