complete auth_opened :)

algebra/upred.v

@@ -400,8 +400,8 @@ Lemma exist_elim {A} (P : A → uPred M) Q : (∀ a, P a ⊑ Q) → (∃ a, P a)
 Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
 Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
 Proof. by intros x n ??; simpl. Qed.
-Lemma eq_rewrite {A : cofeT} P (Q : A → uPred M)
-  `{HQ:∀ n, Proper (dist n ==> dist n) Q} a b : P ⊑ (a ≡ b) → P ⊑ Q a → P ⊑ Q b.
+Lemma eq_rewrite {A : cofeT} a b (Q : A → uPred M) P
+  `{HQ:∀ n, Proper (dist n ==> dist n) Q} : P ⊑ (a ≡ b) → P ⊑ Q a → P ⊑ Q b.
 Proof.
   intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
 Qed.
@@ -460,7 +460,7 @@ Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
 Proof. intros ->; apply eq_refl. Qed.
 Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
 Proof.
-  refine (eq_rewrite _ (λ b, b ≡ a)%I a b _ _); auto using eq_refl.
+  apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl.
   intros n; solve_proper.
 Qed.
 
@@ -776,7 +776,7 @@ Qed.
 Lemma always_eq {A:cofeT} (a b : A) : (□ (a ≡ b))%I ≡ (a ≡ b : uPred M)%I.
 Proof.
   apply (anti_symmetric (⊑)); auto using always_elim.
-  refine (eq_rewrite _ (λ b, □ (a ≡ b))%I a b _ _); auto.
+  apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
   { intros n; solve_proper. }
   rewrite -(eq_refl _ True) always_const; auto.
 Qed.

program_logic/auth.v

@@ -40,6 +40,8 @@ Section auth.
     by rewrite always_and_sep_l'.
   Qed.
 
+  Context {Hφ : ∀ n, Proper (dist n ==> dist n) φ}.
+
   Lemma auth_opened a γ :
     (▷auth_inv γ ★ auth_own γ a) ⊑ (▷∃ a', φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
@@ -48,6 +50,13 @@ Section auth.
     rewrite /auth_own [(_ ★ φ _)%I]commutative -associative -own_op.
     rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
     rewrite [∅ ⋅ _]left_id -(exist_intro a').
-  Abort.
+    apply (eq_rewrite b (a ⋅ a')
+              (λ x, φ x ★ own AuthI γ (● x ⋅ ◯ a))%I).
+    { (* TODO this asks for automation. *)
+      move=>n a1 a2 Ha. by rewrite !Ha. }
+    { by rewrite !sep_elim_r. }
+    apply sep_mono; first done.
+    by rewrite sep_elim_l.
+  Qed.
 End auth.