From f7bbaa2c319188f44935c21080bd8701e08c47c5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 31 Jan 2016 23:27:43 +0100
Subject: [PATCH] Some simplifications to logic.v.

---
 iris/ownership.v |  2 +-
 modures/logic.v  | 65 ++++++++----------------------------------------
 2 files changed, 12 insertions(+), 55 deletions(-)

diff --git a/iris/ownership.v b/iris/ownership.v
index 98bfc9721..2e2c1c3a3 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -56,7 +56,7 @@ Qed.
 Lemma ownG_valid m : (ownG m) âŠ‘ (âœ“ m).
 Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
 Lemma ownG_valid_r m : (ownG m) âŠ‘ (ownG m â˜… âœ“ m).
-Proof. apply uPred.always_entails_r', ownG_valid; by apply _. Qed.
+Proof. apply (uPred.always_entails_r' _ _), ownG_valid. Qed.
 Global Instance ownG_timeless m : Timeless m â†’ TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 
diff --git a/modures/logic.v b/modures/logic.v
index 1a8a4c12e..feaf66ebb 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -55,14 +55,10 @@ Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.
 
 Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x :
   P1 ={n}= P2 â†’ âœ“{n} x â†’ P1 n x â†’ P2 n x.
-Proof.
-  intros HP ?. apply HP; by auto.
-Qed.
+Proof. intros HP ?; apply HP; auto. Qed.
 Lemma uPred_weaken' {M} (P : uPred M) x1 x2 n1 n2 :
   x1 â‰¼ x2 â†’ n2 â‰¤ n1 â†’ âœ“{n2} x2 â†’ P n1 x1 â†’ P n2 x2.
-Proof.
-  intros; eauto using uPred_weaken.
-Qed.
+Proof. eauto using uPred_weaken. Qed.
 
 (** functor *)
 Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
@@ -445,27 +441,14 @@ Proof. intros; apply impl_elim with Q; auto. Qed.
 Lemma impl_elim_r' P Q R : Q âŠ‘ (P â†’ R) â†’ (P âˆ§ Q) âŠ‘ R.
 Proof. intros; apply impl_elim with P; auto. Qed.
 Lemma impl_entails P Q : True âŠ‘ (P â†’ Q) â†’ P âŠ‘ Q.
-Proof.
-  intros H; eapply impl_elim; last reflexivity. rewrite -H.
-  by apply True_intro.
-Qed.
+Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
 Lemma entails_impl P Q : (P âŠ‘ Q) â†’ True âŠ‘ (P â†’ Q).
-Proof.
-  intros H; apply impl_intro_l. by rewrite -H and_elim_l.
-Qed.
+Proof. auto using impl_intro_l. Qed.
 
-Lemma const_intro_l Ï† Q R :
-  Ï† â†’ (â– Ï† âˆ§ Q) âŠ‘ R â†’ Q âŠ‘ R.
-Proof.
-  intros ? <-. apply and_intro; last done.
-  by apply const_intro.
-Qed.
+Lemma const_intro_l Ï† Q R : Ï† â†’ (â– Ï† âˆ§ Q) âŠ‘ R â†’ Q âŠ‘ R.
+Proof. intros ? <-; auto using const_intro. Qed.
 Lemma const_intro_r Ï† Q R : Ï† â†’ (Q âˆ§ â– Ï†) âŠ‘ R â†’ Q âŠ‘ R.
-Proof.
-  (* FIXME RJ: Why does this not work? rewrite (commutative uPred_and Q (â– Ï†)%I). *)
-  intros ? <-. apply and_intro; first done.
-  by apply const_intro.
-Qed.
+Proof. intros ? <-; auto using const_intro. Qed.
 Lemma const_elim_l Ï† Q R : (Ï† â†’ Q âŠ‘ R) â†’ (â–  Ï† âˆ§ Q) âŠ‘ R.
 Proof. intros; apply const_elim with Ï†; eauto. Qed.
 Lemma const_elim_r Ï† Q R : (Ï† â†’ Q âŠ‘ R) â†’ (Q âˆ§ â–  Ï†) âŠ‘ R.
@@ -617,15 +600,9 @@ Lemma sep_elim_r' P Q R : Q âŠ‘ R â†’ (P â˜… Q) âŠ‘ R.
 Proof. intros ->; apply sep_elim_r. Qed.
 Hint Resolve sep_elim_l' sep_elim_r'.
 Lemma sep_intro_True_l P Q R : True âŠ‘ P â†’ R âŠ‘ Q â†’ R âŠ‘ (P â˜… Q).
-Proof.
-  intros HP HQ. etransitivity; last (eapply sep_mono; eassumption).
-  by rewrite left_id.
-Qed.
+Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
 Lemma sep_intro_True_r P Q R : R âŠ‘ P â†’ True âŠ‘ Q â†’ R âŠ‘ (P â˜… Q).
-Proof.
-  intros HP HQ. etransitivity; last (eapply sep_mono; eassumption).
-  by rewrite right_id.
-Qed.
+Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
 Lemma wand_intro_l P Q R : (Q â˜… P) âŠ‘ R â†’ P âŠ‘ (Q -â˜… R).
 Proof. rewrite (commutative _); apply wand_intro_r. Qed.
 Lemma wand_elim_r P Q : (P â˜… (P -â˜… Q)) âŠ‘ Q.
@@ -787,26 +764,10 @@ Proof.
   apply always_intro, impl_intro_r.
   by rewrite always_and_sep_l always_elim wand_elim_l.
 Qed.
-Lemma always_impl_l P Q : (P â†’ â–¡ Q) âŠ‘ (P â†’ â–¡ Q â˜… P).
-Proof.
-  rewrite -always_and_sep_l. apply impl_intro_l, and_intro.
-  - by rewrite impl_elim_r.
-  - by rewrite and_elim_l.
-Qed.
-Lemma always_impl_r P Q : (P â†’ â–¡ Q) âŠ‘ (P â†’ P â˜… â–¡ Q).
-Proof.
-  by rewrite commutative always_impl_l.
-Qed.
 Lemma always_entails_l P Q : (P âŠ‘ â–¡ Q) â†’ P âŠ‘ (â–¡ Q â˜… P).
-Proof.
-  intros H. apply impl_entails. rewrite -always_impl_l.
-  by apply entails_impl.
-Qed.
+Proof. intros; rewrite -always_and_sep_l; auto. Qed.
 Lemma always_entails_r P Q : (P âŠ‘ â–¡ Q) â†’ P âŠ‘ (P â˜… â–¡ Q).
-Proof.
-  intros H. apply impl_entails. rewrite -always_impl_r.
-  by apply entails_impl.
-Qed.
+Proof. intros; rewrite -always_and_sep_r; auto. Qed.
 
 (* Own *)
 Lemma own_op (a1 a2 : M) :
@@ -979,10 +940,6 @@ Lemma always_and_sep_r' P Q `{!AlwaysStable Q} : (P âˆ§ Q)%I â‰¡ (P â˜… Q)%I.
 Proof. by rewrite -(always_always Q) always_and_sep_r. Qed.
 Lemma always_sep_dup' P `{!AlwaysStable P} : P â‰¡ (P â˜… P)%I.
 Proof. by rewrite -(always_always P) -always_sep_dup. Qed.
-Lemma always_impl_l' P Q `{!AlwaysStable Q} : (P â†’ Q) âŠ‘ (P â†’ Q â˜… P).
-Proof. by rewrite -(always_always Q) always_impl_l. Qed.
-Lemma always_impl_r' P Q `{!AlwaysStable Q} : (P â†’ Q) âŠ‘ (P â†’ P â˜… Q).
-Proof. by rewrite -(always_always Q) always_impl_r. Qed.
 Lemma always_entails_l' P Q `{!AlwaysStable Q} : (P âŠ‘ Q) â†’ P âŠ‘ (Q â˜… P).
 Proof. by rewrite -(always_always Q); apply always_entails_l. Qed.
 Lemma always_entails_r' P Q `{!AlwaysStable Q} : (P âŠ‘ Q) â†’ P âŠ‘ (P â˜… Q).
-- 
GitLab