proposition: Lemma FixFunMod_fix_partial_inv : forall A (R:binary A) (P:A->Prop) B (S:A->B->Prop) {IB:Inhab B} (F:(A->B)->(A->B)) (E:binary B) (f:A->B), f = FixFunMod E F -> equiv E -> (forall x, pred_compatible E (S x)) -> wf R -> rec_contractive E P F R S -> (forall x, P x -> E (f x) (F f x)) /\ (forall x, P x -> S x (f x)).
proof: Proof. Proof using. introv Deff Equiv Comp Wfr Contr. unfolds FixFunMod, Fix. epsilon g. forwards* [g Opt]: (@optimal_fixed_point_exists _ _ _ E F). exists g. apply~ Fix_prop_of_optimal. intros [Fixg Bestg]. subst f. forwards~ (f&Fixf&Inv): (@rec_fixed_point _ _ _ F R P S E). lets Fixf': Fixf. rewrite partial_fixed_point_definitions in Fixf'. lets [ED MG]: (Bestg _ Fixf'). forwards [Dom Equ]: ED. eapply rec_fixed_point_generally_consistent with (R:=R); eauto. clear ED. simpls. split; introv Px. apply~ Fixf. apply* Comp. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)