More LimitPreserving stuff.

Now, we never need to unfold LimitPreserving in LambdaRust, and hence
the entails_lim tactic is no longer needed.

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.

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.

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.