proposition: Lemma refine_LeastFixedPoint {fDom : list Type} {fCod : Type} (fDef fDef' : funType fDom fCod -> funType fDom fCod) : respectful (@refineFun fDom fCod) (@refineFun fDom fCod) 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 (LeastFixedPoint fDef) (LeastFixedPoint fDef').
proof: Proof. unfold LeastFixedPoint, respectful; intros. destruct (sup_lub (postfixed_point fDef)) as [? ?]; destruct (sup_lub (postfixed_point fDef')) as [? ?]; simpl in *. etransitivity. - pose proof (proj1 (Is_GreatestFixedPoint (O := @funDefOps fDom fCod) _ (fDef_monotone))); etransitivity. apply H4. eapply H; reflexivity. - eapply (H2 (fDef' (refineFun_sup (postfixed_point fDef)))). eapply fDef'_monotone. etransitivity. pose proof (proj1 (Is_GreatestFixedPoint (O := @funDefOps fDom fCod) _ (fDef_monotone))); eapply H4. eapply H; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Sets.Ensembles Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Classes.SetoidTactics Fiat.Computation Fiat.Computation.SetoidMorphisms Coq.Logic.FunctionalExtensionality