proposition: Lemma refineMethod_eq_sound : forall Dom Cod (cDef refinedCDef : methodType Rep Dom Cod), refineMethod_eq cDef refinedCDef -> let H := refinedCDef in refineMethod eq cDef H.
proof: Proof. unfold refineMethod; simpl; intros; subst. induction Dom; simpl; intros. - destruct Cod; simpl in *. + etransitivity. * apply refine_under_bind; intros. refine pick val (fst a); eauto; simplify with monad laws. destruct a; simpl; finish honing. * simpl; autorewrite with monad laws; eapply H. + etransitivity. * apply refine_under_bind; intros. refine pick val a; eauto; simpl; finish honing. * simpl; autorewrite with monad laws; eapply H. - eapply (IHDom (fun r_n => cDef r_n d) (fun r_n => refinedCDef r_n d)). unfold refineMethod_eq; intros; eapply H. 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.BuildADTRefinements.HoneRepresentation Fiat.ADTRefinement.BuildADTSetoidMorphisms