proposition: Lemma mixed_fixed_point_generally_consistent : forall I A B {IB:Inhab B} (M:family I B) (E:binary B) (P:A->Prop) (R:binary A) (F:(A->B)->(A->B)) (S:I->A->B->Prop) (f:A->B), COFE M -> wf R -> E = similar M -> mixed_continuous M S -> mixed_contractive M P F R S -> fixed_point (pfun_equiv E P) F f -> (forall i x, P x -> S i x (f x)) -> generally_consistent_partial_fixed_point E F (Build_partial f P).
proof: Proof. Proof using. #[global] Hint Resolve pfun_equiv_equiv similar_equiv. introv IB Cofe WfR SimE. introv Conti Contr Fixf Inva. subst E. split. unfolds. simpl. apply Fixf. intros [f' P'] Fixf'. sets f'': (fun x => if classicT (P' x) then f' x else f x). intros x [Px P'x]. simpls. cuts Ind: (forall p, let (i,x) := p:I*A in P x -> family_sim M i (f x) (f'' x)). intros i. apply~ (trans_inv (f'' x)). apply~ (Ind (i,x)). unfold f''. destruct_if. apply~ refl_inv. clears x. intros p. induction_wf IH: (wf_lexico2 (ofe_wf Cofe) (wf_tclosure WfR)) p. destruct p as [i x]. intros Px. destruct (prop_inv (P' x)) as [P'x|NP'x]; [| unfold f''; destruct_if; apply~ refl_inv ]. apply~ (trans_sym_lr (F f'' x)). apply~ (trans_inv (F f x)). apply~ Fixf. apply~ equiv_refl. applys (proj1 (forall_conj_inv_6 Contr)) Px. intros y j Py Lt. splits. apply~ (IH (j,y)). forwards*: (>> rel_incl_lexico2 I A (family_r M) (family_r M) R (tclosure R) (j,y) (i,x)). auto. applys~ Conti. intros k Rkj. applys (IH (k,y)) Py. destruct Lt as [|[? ?]]. left. apply~ (trans_inv j). subst~. apply~ (Fixf' (Build_partial f'' P)). simpl. intros y P'y. unfold f''. destruct_if~. apply~ refl_inv. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)