diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index a6721f962998caf64bc0b2204dd6b2848e49f3f0..89df57d6bc9eb93ab43cf47c2cb4dd758fbb3f1a 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -246,6 +246,46 @@ Ltac f_contractive := Ltac solve_contractive := solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]). +(** Limit preserving predicates *) +Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop := + limit_preserving (c : chain A) : (∀ n, P (c n)) → P (compl c). +Hint Mode LimitPreserving + + ! : typeclass_instances. + +Section limit_preserving. + Context `{Cofe A}. + (* These are not instances as they will never fire automatically... + but they can still be helpful in proving things to be limit preserving. *) + + Lemma limit_preserving_ext (P Q : A → Prop) : + (∀ x, P x ↔ Q x) → LimitPreserving P → LimitPreserving Q. + Proof. intros HP Hlimit c ?. apply HP, Hlimit=> n; by apply HP. Qed. + + Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _, P). + Proof. intros c HP. apply (HP 0). Qed. + + Lemma limit_preserving_timeless (P : A → Prop) : + Proper (dist 0 ==> impl) P → LimitPreserving P. + Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed. + + Lemma limit_preserving_and (P1 P2 : A → Prop) : + LimitPreserving P1 → LimitPreserving P2 → + LimitPreserving (λ x, P1 x ∧ P2 x). + Proof. intros Hlim1 Hlim2 c Hc. split. apply Hlim1, Hc. apply Hlim2, Hc. Qed. + + Lemma limit_preserving_impl (P1 P2 : A → Prop) : + Proper (dist 0 ==> impl) P1 → LimitPreserving P2 → + LimitPreserving (λ x, P1 x → P2 x). + Proof. + intros Hlim1 Hlim2 c Hc HP1. apply Hlim2=> n; apply Hc. + eapply Hlim1, HP1. apply dist_le with n; last lia. apply (conv_compl n). + Qed. + + Lemma limit_preserving_forall {B} (P : B → A → Prop) : + (∀ y, LimitPreserving (P y)) → + LimitPreserving (λ x, ∀ y, P y x). + Proof. intros Hlim c Hc y. by apply Hlim. Qed. +End limit_preserving. + (** Fixpoint *) Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A) `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. @@ -294,22 +334,23 @@ Section fixpoint. Lemma fixpoint_ind (P : A → Prop) : Proper ((≡) ==> impl) P → (∃ x, P x) → (∀ x, P x → P (f x)) → - (∀ (c : chain A), (∀ n, P (c n)) → P (compl c)) → + LimitPreserving P → P (fixpoint f). Proof. intros ? [x Hx] Hincr Hlim. set (chcar i := Nat.iter (S i) f x). assert (Hcauch : ∀ n i : nat, n ≤ i → chcar i ≡{n}≡ chcar n). - { intros n. induction n as [|n IH]=> -[|i] //= ?; try omega. - - apply (contractive_0 f). - - apply (contractive_S f), IH; auto with omega. } + { intros n. rewrite /chcar. induction n as [|n IH]=> -[|i] //=; + eauto using contractive_0, contractive_S with omega. } set (fp2 := compl {| chain_cauchy := Hcauch |}). - rewrite -(fixpoint_unique fp2); first by apply Hlim; induction n; apply Hincr. - apply equiv_dist=>n. - rewrite /fp2 (conv_compl n) /= /chcar. - induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. + assert (f fp2 ≡ fp2). + { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar. + induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. } + rewrite -(fixpoint_unique fp2) //. + apply Hlim=> n /=. by apply nat_iter_ind. Qed. End fixpoint. + (** Fixpoint of f when f^k is contractive. **) Definition fixpointK `{Cofe A, Inhabited A} k (f : A → A) `{!Contractive (Nat.iter k f)} := fixpoint (Nat.iter k f). @@ -374,11 +415,11 @@ Section fixpointK. Lemma fixpointK_ind (P : A → Prop) : Proper ((≡) ==> impl) P → (∃ x, P x) → (∀ x, P x → P (f x)) → - (∀ (c : chain A), (∀ n, P (c n)) → P (compl c)) → + LimitPreserving P → P (fixpointK k f). Proof. - intros ? Hst Hincr Hlim. rewrite /fixpointK. eapply fixpoint_ind; [done..| |done]. - clear- Hincr. intros. induction k; first done. simpl. auto. + intros. rewrite /fixpointK. apply fixpoint_ind; eauto. + intros; apply nat_iter_ind; auto. Qed. End fixpointK. @@ -1104,33 +1145,6 @@ Proof. destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg. Qed. -(** Limit preserving predicates *) -Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop := - limit_preserving (c : chain A) : (∀ n, P (c n)) → P (compl c). -Hint Mode LimitPreserving + + ! : typeclass_instances. - -Section limit_preserving. - Context {A : ofeT} `{!Cofe A}. - (* These are not instances as they will never fire automatically... - but they can still be helpful in proving things to be limit preserving. *) - - Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _, P). - Proof. intros c HP. apply (HP 0). Qed. - - Lemma limit_preserving_timeless (P : A → Prop) : - Proper (dist 0 ==> impl) P → LimitPreserving P. - Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed. - - Lemma limit_preserving_and (P1 P2 : A → Prop) : - LimitPreserving P1 → LimitPreserving P2 → - LimitPreserving (λ x, P1 x ∧ P2 x). - Proof. - intros Hlim1 Hlim2 c Hc. split. - - apply Hlim1, Hc. - - apply Hlim2, Hc. - Qed. -End limit_preserving. - (** Constructing isomorphic OFEs *) Lemma iso_ofe_mixin {A : ofeT} `{Equiv B, Dist B} (g : B → A) (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2) @@ -1161,6 +1175,14 @@ Section iso_cofe_subtype. Qed. End iso_cofe_subtype. +Lemma iso_cofe_subtype' {A B : ofeT} `{Cofe A} + (P : A → Prop) (f : ∀ x, P x → B) (g : B → A) + (Pg : ∀ y, P (g y)) + (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) + (gf : ∀ x Hx, g (f x Hx) ≡ x) + (Hlimit : LimitPreserving P) : Cofe B. +Proof. apply: (iso_cofe_subtype P f g)=> // c. apply Hlimit=> ?; apply Pg. Qed. + Definition iso_cofe {A B : ofeT} `{Cofe A} (f : A → B) (g : B → A) (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) (gf : ∀ x, g (f x) ≡ x) : Cofe B. @@ -1190,11 +1212,7 @@ Section sigma. Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin. Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigC. - Proof. - apply: (iso_cofe_subtype P (exist P) proj1_sig). - - done. - - intros c. apply limit_preserving=> n. apply proj2_sig. - Qed. + Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed. Global Instance sig_timeless (x : sig P) : Timeless (`x) → Timeless x. Proof. intros ? y. rewrite sig_dist_alt sig_equiv_alt. apply (timeless _). Qed. diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v index 387a0936245f92440945db75152c8f753055eb14..b84f6af05ae633393147529fdaddd7e70ab412f5 100644 --- a/theories/base_logic/derived.v +++ b/theories/base_logic/derived.v @@ -816,6 +816,9 @@ Proof. destruct mx; apply _. Qed. (* Derived lemmas for persistence *) Global Instance PersistentP_proper : Proper ((≡) ==> iff) (@PersistentP M). Proof. solve_proper. Qed. +Global Instance limit_preserving_PersistentP {A:ofeT} `{Cofe A} (Φ : A → uPred M) : + NonExpansive Φ → LimitPreserving (λ x, PersistentP (Φ x)). +Proof. intros. apply limit_preserving_entails; solve_proper. Qed. Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P. Proof. apply (anti_symm (⊢)); auto using always_elim. Qed. diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v index 45fdacf7ec84c275077e24be7a9d2f2533f8ec31..52ac2d274ef5a1939aa29c26e9b0d77db7d611e8 100644 --- a/theories/base_logic/upred.v +++ b/theories/base_logic/upred.v @@ -149,13 +149,13 @@ Section entails. Context {M : ucmraT}. Implicit Types P Q : uPred M. -Global Instance: PreOrder (@uPred_entails M). +Global Instance entails_po : PreOrder (@uPred_entails M). Proof. split. - by intros P; split=> x i. - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP. Qed. -Global Instance: AntiSymm (⊣⊢) (@uPred_entails M). +Global Instance entails_anti_sym : AntiSymm (⊣⊢) (@uPred_entails M). Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed. Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P). @@ -179,28 +179,15 @@ Proof. by intros ->. Qed. Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R). Proof. by intros ? <-. Qed. -Lemma entails_lim (P Q : chain (uPredC M)) : - (∀ n, P n ⊢ Q n) → compl P ⊢ compl Q. +Lemma entails_lim (cP cQ : chain (uPredC M)) : + (∀ n, cP n ⊢ cQ n) → compl cP ⊢ compl cQ. Proof. - intros Hlim. split. intros n m Hval HP. + intros Hlim; split=> n m ? HP. eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl. Qed. -Lemma entails_lim' {T : ofeT} `{Cofe T} (P Q : T → uPredC M) - `{!NonExpansive P} `{!NonExpansive Q} (c : chain T) : - (∀ n, P (c n) ⊢ Q (c n)) → P (compl c) ⊢ Q (compl c). -Proof. - set (cP := chain_map P c). set (cQ := chain_map Q c). - rewrite -!compl_chain_map=>HPQ. exact: entails_lim. -Qed. - +Lemma limit_preserving_entails `{Cofe A} (Φ Ψ : A → uPred M) : + NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢ Ψ x). +Proof. intros HΦ HΨ c Hc. rewrite -!compl_chain_map /=. by apply entails_lim. Qed. End entails. - -Ltac entails_lim c := - pattern (compl c); - match goal with - | |- (λ o, ?P ⊢ ?Q) ?x => change (((λ o, P) x) ⊢ (λ o, Q) x) - end; - apply entails_lim'. - End uPred.