proposition: Lemma optimal_fixed_point_exists : forall A B {I:Inhab B} (E:binary B) (F:(A->B)->(A->B)), equiv E -> exists (f:A-->B), optimal_fixed_point E F f.
proof: Proof. Proof using. introv I Equiv. sets S: (generally_consistent_partial_fixed_point E F). forwards~ (f&[Upf Lubf]&Fixf): (@lub_of_consistent_set _ _ _ E F S). intros f f' [Pf Cf] [Pf' Cf']. auto. intros f [Pf Cf]. auto. exists f. split~. split~. intros g Fixg. sets S': (fun x => S x \/ (x = g)). forwards~ (h&[Uph Lubh]&Fixh): (@lub_of_consistent_set _ _ _ E F S'). intros f1 f2 [[Pf1 Cf1]|G1] [[Pf2 Cf2]|G2]; subst~. intros_all. apply~ sym_inv. apply~ Cf2. unfolds* pred_and. intros_all. apply~ refl_inv. intros f1 [[Pf1 Cf1]|G1]; subst~. asserts Dfh Efh: (extends E f h). apply Lubf. intros f' Sf'. apply~ Uph. asserts Dgh Egh: (extends E g h). apply~ Uph. intros x [Dfx Dgx]. apply~ (trans_sym_lr (h x)). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)