[ new ] proofs that various orders are connex (#702)

Author: gallais

CHANGELOG.md

@@ -53,6 +53,8 @@ New modules
 Deprecated features
 -------------------
 
+* Renamed `Relation.Binary.Core`'s `Conn` to `Connex`.
+
 * Renamed a few `-identity` lemmas in `Codata.Stream.Properties` as they were
   proving two streams bisimilar rather than propositionally equal.
   ```agda
@@ -157,6 +159,11 @@ Other minor additions
 
 * Added new proofs to `Data.Nat.Properties`:
   ```agda
+  ≤-<-connex : Connex _≤_ _<_
+  ≥->-connex : Connex _≥_ _>_
+  <-≤-connex : Connex _<_ _≤_
+  >-≥-connex : Connex _>_ _≥_
+
   1+n≢0     : suc n ≢ 0
   <ᵇ⇒<      : T (m <ᵇ n) → m < n
   <⇒<ᵇ      : m < n → T (m <ᵇ n)
@@ -192,7 +199,7 @@ Other minor additions
 
 * Added new proof to `Relation.Binary.PropositionalEquality.Core`:
   ```agda
-  ≢-sym : Symmetric {A = A} _≢_
+  ≢-sym : Symmetric _≢_
   ```
 
 * Added new names, functions and shorthand to `Reflection`:
@@ -232,7 +239,11 @@ Other minor additions
   iΠ[_∶_]_ s a ty   = Π[ s ∶ (iArg a) ] ty
   ```
 
+* Added new proofs to `Relation.Binary.Consequences`:
+  ```agda
+  flip-Connex : Connex P Q → Connex Q P
+  ```
+
 * The relation `_≅_` in `Relation.Binary.HeterogeneousEquality` has
   been generalised so that the types of the two equal elements need not
   be at the same universe level.
-

src/Data/Nat/Properties.agda

@@ -26,6 +26,7 @@ open import Function
 open import Function.Injection using (_↣_)
 open import Level using (0ℓ)
 open import Relation.Binary
+open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary
 open import Relation.Nullary.Decidable using (True; via-injection; map′)
@@ -263,6 +264,20 @@ n≤0⇒n≡0 z≤n = refl
 ≤∧≢⇒< {_} {suc n} (s≤s m≤n) 1+m≢1+n =
   s≤s (≤∧≢⇒< m≤n (1+m≢1+n ∘ cong suc))
 
+≤-<-connex : Connex _≤_ _<_
+≤-<-connex m n with m ≤? n
+... | yes m≤n = inj₁ m≤n
+... | no ¬m≤n = inj₂ (≰⇒> ¬m≤n)
+
+≥->-connex : Connex _≥_ _>_
+≥->-connex = flip ≤-<-connex
+
+<-≤-connex : Connex _<_ _≤_
+<-≤-connex = flip-Connex ≤-<-connex
+
+>-≥-connex : Connex _>_ _≥_
+>-≥-connex = flip-Connex ≥->-connex
+
 ------------------------------------------------------------------------
 -- Relational properties of _<_
 

src/Relation/Binary/Consequences.agda

@@ -13,7 +13,7 @@ open import Relation.Nullary using (yes; no)
 open import Relation.Unary using (∁)
 open import Function using (_∘_; flip)
 open import Data.Maybe.Base using (just; nothing)
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum as Sum using (inj₁; inj₂)
 open import Data.Product using (_,_)
 open import Data.Empty using (⊥-elim)
 
@@ -154,3 +154,10 @@ module _ {a b p q} {A : Set a} {B : Set b }
 
   map-NonEmpty : P ⇒ Q → NonEmpty P → NonEmpty Q
   map-NonEmpty f x = nonEmpty (f (NonEmpty.proof x))
+
+module _ {a b p q} {A : Set a} {B : Set b }
+         {P : REL A B p} {Q : REL B A q}
+         where
+
+  flip-Connex : Connex P Q → Connex Q P
+  flip-Connex f x y = Sum.swap (f y x)

src/Relation/Binary/Core.agda

@@ -113,11 +113,11 @@ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
 
 -- Generalised connex.
 
-Conn : ∀ {a b p q} {A : Set a} {B : Set b} → REL A B p → REL B A q → Set _
-Conn P Q = ∀ x y → P x y ⊎ Q y x
+Connex : ∀ {a b p q} {A : Set a} {B : Set b} → REL A B p → REL B A q → Set _
+Connex P Q = ∀ x y → P x y ⊎ Q y x
 
 Total : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
-Total _∼_ = Conn _∼_ _∼_
+Total _∼_ = Connex _∼_ _∼_
 
 data Tri {a b c} (A : Set a) (B : Set b) (C : Set c) :
          Set (a ⊔ b ⊔ c) where
@@ -194,3 +194,19 @@ record IsEquivalence {a ℓ} {A : Set a}
 
   reflexive : _≡_ ⇒ _≈_
   reflexive ≡-refl = refl
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.1
+
+Conn = Connex
+{-# WARNING_ON_USAGE Conn
+"Warning: Conn was deprecated in v1.1.
+Please use Connex instead."
+#-}