fixpoint for chains in the transfinite setting

theories/algebra/ofe.v

@@ -412,15 +412,76 @@ End bounded_limit_preserving.
 (** Fixpoint *)
 Section fixpoint.
 
-  Context {I: indexT} `{Cofe I A}.
+  Context {I: indexT} `{Cofe I A} (f: A → A) `{Contractive f}.
+
+  Record fp_chain α := mkfpchain
+    {
+      ch :> bchain A α;
+      is_fp: dist_later α (f (bcompl ch)) (bcompl ch)
+    }.
+
+
+  Program Definition cast {α} (c: fp_chain α) β (Hβ: β ⪯ α) : fp_chain β :=
+    mkfpchain β (mkbchain _ _ _ (λ γ Hγ, c γ _) _) _.
+  Next Obligation.
+    eauto using index_rel_trans_l.
+  Qed.
+  Next Obligation.
+    intros α c β Hβ γ1 γ2 Hγ Hγ1 Hγ2; simpl. rewrite bchain_cauchy'; eauto.
+  Qed.
+  Next Obligation.
+    intros α c β Hβ γ Hγ; simpl. unshelve rewrite !bchain_conv_bcompl; simpl; eauto.
+    rewrite -bchain_conv_bcompl. eapply is_fp; eauto using index_rel_trans_l.
+  Qed.
+
+  Lemma fp_chain_unique α (c: fp_chain α) β (Hβ: β ⪯ α) (d: fp_chain β) :
+    dist_later β (bcompl c) (bcompl d).
+  Proof using A Contractive0 H I f.
+    revert Hβ d. induction (index_rel_wf I β) as [β _ IH]. intros Hβ d γ Hγ.
+    rewrite -(is_fp _ d γ Hγ). rewrite -(is_fp _ c γ _); eauto using index_rel_trans_l.
+    eapply contractive_mono; eauto.
+    intros δ Hδ. assert (γ ⪯ β) as Hγβ by eauto. transitivity (bcompl (cast d γ Hγβ)).
+    apply IH; eauto using index_rel_trans_l.
+    unshelve rewrite !bchain_conv_bcompl; eauto using index_rel_trans_l.
+    simpl. by eapply bchain_cauchy'.
+  Qed.
+
+
+  Program Definition fpc : ∀ (α: I), fp_chain α :=
+    Fix (index_rel_wf I) (fp_chain)
+   (λ β Hβ, mkfpchain β (mkbchain I A β (λ γ Hγ, f (bcompl (Hβ γ Hγ))) _) _).
+  Next Obligation.
+    intros  α Hα β1 β2 Hβ Hβ1 Hβ2; simpl.
+    apply contractive_mono; eauto. apply fp_chain_unique; eauto using is_fp.
+  Qed.
+  Next Obligation.
+    intros β Hβ γ Hγ; simpl. unshelve rewrite bchain_conv_bcompl; simpl; eauto.
+    apply contractive_mono; eauto. intros δ Hδ. by apply is_fp.
+  Qed.
 
 
-  Program Definition bfpc (f: A → A) `{C: Contractive f} (α: I) : bchain A α :=
-    Fix (index_rel_wf I) (bchain A) (λ β Hβ, mkbchain I A β (λ γ Hγ, f (bcompl (Hβ γ Hγ))) _) α.
+  Program Definition fpc_chain: chain A := mkchain _ _ (λ α, f (bcompl (fpc α))) _.
   Next Obligation.
-    intros f C _ β Hβ γ1 γ2 Hγ Hγ1 Hγ2; simpl. apply C.
-    intros δ Hδ. unshelve rewrite !(bchain_conv_bcompl); eauto using index_rel_trans_l.
-  Abort.
+    intros β α Hαβ; simpl. apply contractive_mono; eauto.
+      by apply fp_chain_unique.
+  Qed.
+
+
+  Program Definition fixpoint_def  : A := compl fpc_chain.
+  Definition fixpoint_aux : seal (@fixpoint_def). by eexists. Qed.
+  Definition fixpoint := fixpoint_aux.(unseal).
+  Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
+
+  Lemma fixpoint_unfold :
+    fixpoint ≡ f (fixpoint).
+  Proof.
+    apply equiv_dist=>α.
+    rewrite fixpoint_eq /fixpoint_def; cbn.
+    erewrite !conv_compl. unfold fpc_chain; simpl.
+    eapply contractive_mono; eauto. intros β Hβ.
+    symmetry. by eapply is_fp.
+  Qed.
+  
 
   (*
   Definition fpc (f : A → A) : I → A :=