From 7fe3cfc470f66f8ec22078d687284bb385a0625e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Jan 2016 14:37:30 +0100
Subject: [PATCH] Fix inconsistent lemmas for conjunction/disjunction.

---
 modures/logic.v | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

diff --git a/modures/logic.v b/modures/logic.v
index 5417e2a36..0db9edcd1 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -332,10 +332,10 @@ Lemma and_elim_r P Q : (P âˆ§ Q)%I âŠ† Q.
 Proof. by intros x n ? [??]. Qed.
 Lemma and_intro P Q R : P âŠ† Q â†’ P âŠ† R â†’ P âŠ† (Q âˆ§ R)%I.
 Proof. intros HQ HR x n ??; split; auto. Qed.
-Lemma or_intro_l P Q R : P âŠ† Q â†’ P âŠ† (Q âˆ¨ R)%I.
-Proof. intros HQ x n ??; left; auto. Qed.
-Lemma or_intro_r P Q R : P âŠ† R â†’ P âŠ† (Q âˆ¨ R)%I.
-Proof. intros HR x n ??; right; auto. Qed.
+Lemma or_intro_l P Q : P âŠ† (P âˆ¨ Q)%I.
+Proof. intros x n ??; left; auto. Qed.
+Lemma or_intro_r P Q : Q âŠ† (P âˆ¨ Q)%I.
+Proof. intros x n ??; right; auto. Qed.
 Lemma or_elim R P Q : P âŠ† R â†’ Q âŠ† R â†’ (P âˆ¨ Q)%I âŠ† R.
 Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
 Lemma impl_intro P Q R : (R âˆ§ P)%I âŠ† Q â†’ R âŠ† (P â†’ Q)%I.
@@ -375,8 +375,14 @@ Lemma and_elim_l' P Q R : P âŠ† R â†’ (P âˆ§ Q)%I âŠ† R.
 Proof. by rewrite and_elim_l. Qed.
 Lemma and_elim_r' P Q R : Q âŠ† R â†’ (P âˆ§ Q)%I âŠ† R.
 Proof. by rewrite and_elim_r. Qed.
-
-Hint Resolve or_elim or_intro_l or_intro_r.
+Lemma or_intro_l' P Q R : P âŠ† Q â†’ P âŠ† (Q âˆ¨ R)%I.
+Proof. intros ->; apply or_intro_l. Qed.
+Lemma or_intro_r' P Q R : P âŠ† R â†’ P âŠ† (Q âˆ¨ R)%I.
+Proof. intros ->; apply or_intro_r. Qed.
+Lemma exist_intro' P `(Q : A â†’ uPred M) a : P âŠ† Q a â†’ P âŠ† (âˆƒ a, Q a)%I.
+Proof. intros ->; apply exist_intro. Qed.
+
+Hint Resolve or_elim or_intro_l' or_intro_r'.
 Hint Resolve and_intro and_elim_l' and_elim_r'.
 Hint Immediate True_intro False_elim.
 
@@ -523,11 +529,15 @@ Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
 
 Global Instance sep_True : RightId (â‰¡) True%I (@uPred_sep M).
 Proof. by intros P; rewrite (commutative _), (left_id _ _). Qed.
-Lemma sep_elim_l P Q R : P âŠ† R â†’ (P â˜… Q)%I âŠ† R.
-Proof. by intros HR; rewrite <-(right_id _ (â˜…) R)%I, HR, (True_intro Q). Qed.
+Lemma sep_elim_l P Q : (P â˜… Q)%I âŠ† P.
+Proof. by rewrite (True_intro Q), (right_id _ _). Qed.
 Lemma sep_elim_r P Q : (P â˜… Q)%I âŠ† Q.
 Proof. by rewrite (commutative (â˜…))%I; apply sep_elim_l. Qed.
-Hint Resolve sep_elim_l sep_elim_r.
+Lemma sep_elim_l' P Q R : P âŠ† R â†’ (P â˜… Q)%I âŠ† R.
+Proof. intros ->; apply sep_elim_l. Qed.
+Lemma sep_elim_r' P Q R : Q âŠ† R â†’ (P â˜… Q)%I âŠ† R.
+Proof. intros ->; apply sep_elim_r. Qed.
+Hint Resolve sep_elim_l' sep_elim_r'.
 Lemma sep_and P Q : (P â˜… Q)%I âŠ† (P âˆ§ Q)%I.
 Proof. auto. Qed.
 Global Instance sep_False : LeftAbsorb (â‰¡) False%I (@uPred_sep M).
-- 
GitLab