proposition: Theorem cofe_explicit_fixed_point : forall I (A:Type) {IA:Inhab A} (M:family I A) (F:A->A) (Q:I->A->Prop) (Cofe: COFE M), continuous M Q -> contractive M F Q -> let x := build_fixed_point F Cofe in unique_fixed_point (similar M) F x /\ (forall i, Q i x).
proof: Proof. Proof using. introv Conti Contr. sets predecessor: (inverse (family_r M)). unfold build_fixed_point. sets V: (fun i v' => F (local_limit_dep M i v')). sets v: (fix_dep V (ofe_wf Cofe)). asserts Fixv: (forall i, v i = V i (fun j _ => v j)). apply fix_dep_eq. intros x v1 v2 H. unfold V. fequals. apply epsilon_eq. intros i. iff N; intros j; specializes N j; destruct (classicT (family_r M j x)); congruence. asserts Coh: (forall i j, family_r M j i -> locally_coherent M i v -> locally_coherent M j v -> (forall k, family_r M k i -> Q k (v k)) -> family_sim M j (v j) (v i)). intros i j Rji Cohi Cohj Qk. do 2 rewrite Fixv. unfold V. forwards* (l1&El1&L1): (>> (@local_limit_dep_name I) j). forwards* (l2&El2&L2): (>> (@local_limit_dep_name I) i). rewrite El1. rewrite El2. clear El1 El2. apply (proj1 (forall_conj_inv_4 Contr)). intros k Rkj. asserts Rkj': (family_r M k i). apply* ofe_trans. splits. applys~ (trans_sym_rl (v k)). applys~ (Conti (predecessor j) v). intros. apply Qk. applys* trans_inv. applys~ (Conti (predecessor i) v). asserts LocCohQv: (forall i, locally_coherent M i v /\ Q i (v i)). intros i. induction_wf IH: (ofe_wf Cofe) i. lets [IH1 IH2]: (forall_conj_inv_2 IH). clear IH. logic (forall (U V : Prop), U -> (U -> V) -> U /\ V). intros j' j Rij' Rij Rjj'. unfolds inverse. apply~ Coh. intros k Rkj'. apply IH2. apply* trans_inv. introv Cohi. rewrite Fixv. unfold V. forwards* (l&El&L): (>> (@local_limit_dep_name I) i). rewrite El. clear El. applys~ (contractive_to_invariant Cofe Contr). introv Rji. applys~ (Conti (predecessor i) v). lets LocCohv Qv: (forall_conj_inv_1 LocCohQv). clear LocCohQv. asserts Cohv: (globally_coherent M v). intros_all. apply~ Coh. epsilon l. apply~ cofe_complete. intros L. split. unfolds. logic (forall P Q : Prop, P -> (P -> Q) -> P /\ Q). intros l' Sim' i. applys~ (trans_sym_rl l). applys~ (trans_sym_rl (v i)). rewrite Fixv. unfold V. applys (proj1 (forall_conj_inv_4 Contr)). intros j Rji. splits. applys~ (trans_sym_rl l). applys~ (trans_sym_rl (v j)). applys~ local_limit_dep_inv. forwards* (l1&El1&L1): (>> (@local_limit_dep_name I) i). rewrite El1. clear El1. applys~ (Conti (predecessor i) v). applys~ (Conti pred_true v). intros k _. applys~ (trans_inv l). intros Fixl l' Fixl'. unfold fixed_point in Fixl, Fixl'. specializes Fixl l __. intros j. apply~ refl_inv. apply~ sym_inv. intros i. induction_wf IH: (ofe_wf Cofe) i. applys~ (@trans_inv _ (F l)). apply~ sym_inv. applys~ (@trans_sym_lr _ (F l')). apply Fixl'. intros j. apply* refl_inv. apply (proj1 (forall_conj_inv_4 Contr)). intros j Rji. splits. apply~ IH. applys~ (Conti pred_true v). applys~ (Conti (predecessor i) v). intros k Rki. apply~ (@trans_inv _ l). intros i. applys~ (Conti pred_true v). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)