Commit 77c14c80 authored by Robbert Krebbers's avatar Robbert Krebbers

Seal off definition of Banach's fixpoint.

parent d5ff27dc
Pipeline #370 passed with stage
......@@ -174,20 +174,25 @@ Next Obligation.
- apply (contractive_0 f).
- apply (contractive_S f), IH; auto with omega.
Qed.
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A A)
Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed.
Definition fixpoint {A AiH} f {Hf} := proj1_sig fixpoint_aux A AiH f Hf.
Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
Section fixpoint.
Context {A : cofeT} `{Inhabited A} (f : A A) `{!Contractive f}.
Lemma fixpoint_unfold : fixpoint f f (fixpoint f).
Proof.
apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //.
apply equiv_dist=>n.
rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Qed.
Lemma fixpoint_ne (g : A A) `{!Contractive g} n :
( z, f z {n} g z) fixpoint f {n} fixpoint g.
Proof.
intros Hfg. rewrite /fixpoint
intros Hfg. rewrite fixpoint_eq /fixpoint_def
(conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
rewrite Hfg; apply contractive_S, IH; auto using dist_S.
......@@ -196,7 +201,6 @@ Section fixpoint.
( x, f x g x) fixpoint f fixpoint g.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint.
Global Opaque fixpoint.
(** Function space *)
Record cofeMor (A B : cofeT) : Type := CofeMor {
......
......@@ -117,8 +117,7 @@ Section def.
Definition wp_fix : coPsetC -n> exprC -n> (valC -n> iProp) -n> iProp :=
fixpoint pre_wp_mor.
Lemma wp_fix_unfold E e Φ :
pre_wp_mor wp_fix E e Φ ⊣⊢ wp_fix E e Φ.
Lemma wp_fix_unfold E e Φ : pre_wp_mor wp_fix E e Φ ⊣⊢ wp_fix E e Φ.
Proof. rewrite -fixpoint_unfold. done. Qed.
Lemma wp_fix_sound (E : coPset) (e : expr Λ) (Φ : val Λ -> iProp)
......@@ -131,6 +130,7 @@ Section def.
case EQ: (to_val e)=>[v|].
- rewrite -(of_to_val _ _ EQ) {IH}. constructor. rewrite pvs_eq.
intros rf k Ef σ ???. destruct k; first (exfalso; omega).
apply wp_fix_unfold in Hwp; last done.
edestruct (Hwp rf k Ef σ); eauto with omega; set_solver.
- constructor; first done. intros ???? Hk ??.
apply wp_fix_unfold in Hwp; last done.
......@@ -152,8 +152,7 @@ Section def.
split. rewrite wp_eq /wp_def {1}/uPred_holds.
intros n. revert E e Φ Hproper.
induction n as [n IH] using lt_wf_ind=> E e Φ Hproper r1 Hr1 Hwp.
(* FIXME: This is *slow* *)
apply wp_fix_unfold. { done. }
apply wp_fix_unfold; first done.
intros rf k Ef σ1 ???. split.
- intros ? Hval. destruct Hwp as [??? Hpvs|]; last by destruct (to_val e1).
rewrite pvs_eq in Hpvs.
......@@ -172,5 +171,4 @@ Section def.
apply IH, Hef; first omega; last done.
apply wsat_valid in Hw; last omega. solve_validN.
Qed.
End def.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment