diff --git a/algebra/cofe.v b/algebra/cofe.v index 14941ef145361311a8c073813fe251ff0ec0a636..dfd10fcbdabe7d1f75e71864072911f05bdc0143 100644 --- a/algebra/cofe.v +++ b/algebra/cofe.v @@ -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 { diff --git a/program_logic/weakestpre_fix.v b/program_logic/weakestpre_fix.v index f6f623ccfd9a0514d2f82f290283a2ac6de342c9..d662d66214073b9e68ae1407cb4b0a6f5f6ae547 100644 --- a/program_logic/weakestpre_fix.v +++ b/program_logic/weakestpre_fix.v @@ -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.