From c8814e31cb53c4054ec20dc4acaeb9fdcdf230d1 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 23 Dec 2017 22:00:40 +0100
Subject: [PATCH] New instances for monpred_car and bi_plainly.

---
 theories/proofmode/monpred.v | 33 +++++++++++++++++++--------------
 1 file changed, 19 insertions(+), 14 deletions(-)

diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 3f6ae721f..a3afd86cc 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -58,10 +58,6 @@ Proof. rewrite /MakeMonPredCar=><-. by unseal. Qed.
 Global Instance make_monPred_car_absorbingly i P 𝓟 :
   MakeMonPredCar i P 𝓟 → MakeMonPredCar i (bi_absorbingly P) (bi_absorbingly 𝓟).
 Proof. rewrite /MakeMonPredCar=><-. by unseal. Qed.
-Global Instance make_monPred_car_plainly i P Φ :
-  (∀ j, MakeMonPredCar j P (Φ j)) →
-  MakeMonPredCar i (bi_plainly P) (∀ j, bi_plainly (Φ j)).
-Proof. rewrite /MakeMonPredCar=>H. unseal. by do 3 f_equiv. Qed.
 Global Instance make_monPred_car_persistently_if i P 𝓟 p :
   MakeMonPredCar i P 𝓟 →
   MakeMonPredCar i (bi_persistently_if p P) (bi_persistently_if p 𝓟).
@@ -251,16 +247,14 @@ Proof.
   rewrite /IntoExist /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
 Qed.
 
-Global Instance from_forall_monPred_car {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
-  FromForall P Φ → (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → FromForall (P i) Ψ.
-Proof.
-  rewrite /FromForall /MakeMonPredCar=><- H. setoid_rewrite <- H. by unseal.
-Qed.
-Global Instance into_forall_monPred_car {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
-  IntoForall P Φ → (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → IntoForall (P i) Ψ.
-Proof.
-  rewrite /IntoForall /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
-Qed.
+Global Instance foram_forall_monPred_car_plainly i P Φ :
+  (∀ i, MakeMonPredCar i P (Φ i)) →
+  FromForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
+Proof. rewrite /FromForall /MakeMonPredCar=>H. unseal. do 3 f_equiv. rewrite H //. Qed.
+Global Instance into_forall_monPred_car_plainly i P Φ :
+  (∀ i, MakeMonPredCar i P (Φ i)) →
+  IntoForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
+Proof. rewrite /IntoForall /MakeMonPredCar=>H. unseal. do 3 f_equiv. rewrite H //. Qed.
 
 Global Instance from_forall_monPred_car_all P (Φ : I → PROP) i :
   (∀ i, MakeMonPredCar i P (Φ i)) → FromForall (monPred_all P i) Φ.
@@ -273,6 +267,17 @@ Proof.
   rewrite /IntoForall /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal.
 Qed.
 
+Global Instance from_forall_monPred_car {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
+  FromForall P Φ → (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → FromForall (P i) Ψ.
+Proof.
+  rewrite /FromForall /MakeMonPredCar=><- H. setoid_rewrite <- H. by unseal.
+Qed.
+Global Instance into_forall_monPred_car {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
+  IntoForall P Φ → (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → IntoForall (P i) Ψ.
+Proof.
+  rewrite /IntoForall /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
+Qed.
+
 (* FIXME : there are two good ways to frame under a call to
    monPred_car. This may cause some backtracking in the typeclass
    search, and hence performance issues. *)
-- 
GitLab