Merge branch 'sigT_equivI-admissible' into 'master'

Prove sigT_equivI is admissible (fix #250)

Closes #250

See merge request iris/iris!280

theories/algebra/ofe.v

@@ -1325,17 +1325,6 @@ Section sigT.
   Definition sigT_dist_proj1 n {x y} : x ≡{n}≡ y → projT1 x = projT1 y := proj1_ex.
   Definition sigT_equiv_proj1 x y : x ≡ y → projT1 x = projT1 y := λ H, proj1_ex (H 0).
 
-  (** [existT] is "non-expansive". *)
-  Lemma existT_ne n {i1 i2} {v1 : P i1} {v2 : P i2} :
-    ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡{n}≡ v2) →
-      existT i1 v1 ≡{n}≡ existT i2 v2.
-  Proof. intros ->; simpl. exists eq_refl => /=. done. Qed.
-
-  Lemma existT_proper {i1 i2} {v1 : P i1} {v2 : P i2} :
-    ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡ v2) →
-      existT i1 v1 ≡ existT i2 v2.
-  Proof. intros eq Heq n. apply (existT_ne n eq), equiv_dist, Heq. Qed.
-
   Definition sigT_ofe_mixin : OfeMixin (sigT P).
   Proof.
     split => // n.
@@ -1353,6 +1342,24 @@ Section sigT.
 
   Canonical Structure sigTO : ofeT := OfeT (sigT P) sigT_ofe_mixin.
 
+  (** [existT] is "non-expansive" — general, dependently-typed statement. *)
+  Lemma existT_ne n {i1 i2} {v1 : P i1} {v2 : P i2} :
+    ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡{n}≡ v2) →
+      existT i1 v1 ≡{n}≡ existT i2 v2.
+  Proof. intros ->; simpl. exists eq_refl => /=. done. Qed.
+
+  Lemma existT_proper {i1 i2} {v1 : P i1} {v2 : P i2} :
+    ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡ v2) →
+      existT i1 v1 ≡ existT i2 v2.
+  Proof. intros eq Heq n. apply (existT_ne n eq), equiv_dist, Heq. Qed.
+
+  (** [existT] is "non-expansive" — non-dependently-typed version. *)
+  Global Instance existT_ne_2 a : NonExpansive (@existT A P a).
+  Proof. move => ??? Heq. apply (existT_ne _ eq_refl Heq). Qed.
+
+  Global Instance existT_proper_2 a : Proper ((≡) ==> (≡)) (@existT A P a).
+  Proof. apply ne_proper, _. Qed.
+
   Implicit Types (c : chain sigTO).
 
   Global Instance sigT_discrete x : Discrete (projT2 x) → Discrete x.

theories/bi/derived_laws_sbi.v

@@ -84,6 +84,25 @@ Qed.
 Lemma sig_equivI {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
 Proof. apply (anti_symm _). apply sig_eq. apply f_equiv, _. Qed.
 
+Section sigT_equivI.
+Import EqNotations.
+
+Lemma sigT_equivI {A : Type} {P : A → ofeT} (x y : sigT P) :
+  x ≡ y ⊣⊢
+  ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
+Proof.
+  apply (anti_symm _).
+  - apply (internal_eq_rewrite' x y (λ y,
+             ∃ eq : projT1 x = projT1 y,
+               rew eq in projT2 x ≡ projT2 y))%I;
+        [| done | exact: (exist_intro' _ _ eq_refl) ].
+    move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
+    apply exist_ne => ?. by rewrite Hab.
+  - apply exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
+    apply f_equiv, _.
+Qed.
+End sigT_equivI.
+
 Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof.
   apply (anti_symm _); auto using fun_ext.