proposition: Lemma refine_LeastFixedPoint_AbsR {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} (fDef : funType (oldRep :: fDom) (oldRep * fCod) -> funType (oldRep :: fDom) (oldRep * fCod)) (fDef' : funType (newRep :: fDom) (newRep * fCod) -> funType (newRep :: fDom) (newRep * fCod)) : respectful_hetero (funType (oldRep :: fDom) (oldRep * fCod)) (funType (newRep :: fDom) (newRep * fCod)) (fun _ => funType (oldRep :: fDom) (oldRep * fCod)) (fun _ => funType (newRep :: fDom) (newRep * fCod)) (fun f f' => @refineFun_AbsR _ _ AbsR fDom fCod f f') (fun rec rec' f f' => @refineFun_AbsR _ _ AbsR fDom fCod f f') fDef fDef' -> forall (fDef_monotone : forall rec rec', refineFun rec rec' -> refineFun (fDef rec) (fDef rec')) (fDef'_monotone : forall rec rec', refineFun rec rec' -> refineFun (fDef' rec) (fDef' rec')), refineFun_AbsR AbsR (LeastFixedPoint fDef) (LeastFixedPoint fDef').
proof: Proof. unfold LeastFixedPoint, respectful_hetero; intros. unfold refineFun_AbsR; intros; simpl; eapply refineFun_AbsR'_trans. pose proof (proj1 (Is_GreatestFixedPoint (O := @funDefOps (oldRep :: fDom) (oldRep * fCod)) _ (fDef_monotone))). simpl in *; rewrite H1; reflexivity. eapply refineFun_AbsR_trans'; eauto; [ | eapply H; eapply refineFunAbsR_domcod_old_to_new ]. pose proof (proj2 (Is_GreatestFixedPoint (O := @funDefOps (newRep :: fDom) (newRep * fCod)) _ (fDef'_monotone))). rewrite <- H1. eapply fDef'_monotone. eapply (GreatestFixedPoint_ind (O := @funDefOps (newRep :: fDom) (newRep * fCod))). simpl. eapply refineFun_To_refineFunAbsR. eapply refineFun_AbsR_trans; eauto. pose proof (proj1 (Is_GreatestFixedPoint (O := @funDefOps (oldRep :: fDom) (oldRep * fCod)) _ (fDef_monotone))). eapply H2. eapply H. eapply refineFun_To_refineFunAbsR. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT Fiat.ADTNotation Fiat.Computation.FixComp Coq.ZArith.ZArith Coq.Arith.PeanoNat Fiat.Common.Frame Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements