Added P-resp⟶¬P-resp

agda · Jul 3, 2017 · 22ed935 · 22ed935
1 parent e825415
commit 22ed935
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -460,6 +460,11 @@ Backwards compatible changes
   All₂-concat⁻ : All₂ _~_ (concat xss) (concat yss) → All₂ (All₂ _~_) xss yss
   ```
 
+* Added proofs to `Relation.Binary.Consequences`
+  ```agda
+  P-resp⟶¬P-resp : Symmetric _≈_ → P Respects _≈_ → (¬_ ∘ P) Respects _≈_
+  ```
+
 Version 0.13
 ============
 

diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
@@ -114,6 +114,11 @@ trans∧tri⟶resp≈ {_≈_ = _≈_} {_<_} sym trans <-trans tri =
   ... | tri≈ _ y≈z _ = ⊥-elim (tri⟶irr tri (trans x≈y y≈z) x<z)
   ... | tri> _ _ z<y = ⊥-elim (tri⟶irr tri x≈y (<-trans x<z z<y))
 
+P-resp⟶¬P-resp :
+  ∀ {a p ℓ} {A : Set a} {_≈_ : Rel A ℓ} {P : A → Set p} →
+  Symmetric _≈_ → P Respects _≈_ → (¬_ ∘ P) Respects _≈_
+P-resp⟶¬P-resp sym resp x≈y ¬Px Py = ¬Px (resp (sym x≈y) Py)
+
 tri⟶dec≈ :
   ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} →
   Trichotomous _≈_ _<_ → Decidable _≈_