Strict and non-strict transitive property names

CHANGELOG.md

@@ -1195,6 +1195,9 @@ Deprecated names
   been made consistent so that `m`, `n` always refer to naturals and
   `i` and `j` always refer to integers:
   ```
+  ≤-<-trans  ↦  ≤-<-transˡ
+  <-≤-trans  ↦  <-≤-transʳ
+
   ≤-steps        ↦  i≤j⇒i≤k+j
   ≤-step         ↦  i≤j⇒i≤1+j
 
@@ -1224,7 +1227,7 @@ Deprecated names
   m<n⇒m≤pred[n]  ↦  i<j⇒i≤pred[j]
   -1*n≡-n        ↦  -1*i≡-i
   m*n≡0⇒m≡0∨n≡0  ↦  i*j≡0⇒i≡0∨j≡0
-  ∣m*n∣≡∣m∣*∣n∣     ↦  ∣i*j∣≡∣i∣*∣j∣
+  ∣m*n∣≡∣m∣*∣n∣  ↦  ∣i*j∣≡∣i∣*∣j∣
   m≤m+n          ↦  i≤i+j
   n≤m+n          ↦  i≤j+i
   m-n≤m          ↦  i≤i-j
@@ -1319,6 +1322,9 @@ Deprecated names
   ≤-stepsˡ        ↦  m≤n⇒m≤o+n
   ≤-stepsʳ        ↦  m≤n⇒m≤n+o
   <-step          ↦  m<n⇒m<1+n
+
+  <-transʳ        ↦  ≤-<-transˡ
+  <-transˡ        ↦  <-≤-transʳ
   ```
 
 * In `Data.Rational.Unnormalised.Properties`:
@@ -2919,6 +2925,9 @@ Other minor changes
 
 * Added new definitions in `Relation.Binary.Definitions`:
   ```
+  RightTrans R S = Trans R S R
+  LeftTrans  S R = Trans S R R
+
   Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y)
   Tight    _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y)
 

src/Data/Integer/Properties.agda

@@ -33,7 +33,7 @@ open import Relation.Binary.Bundles using
 open import Relation.Binary.Structures
   using (IsPreorder; IsTotalPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
 open import Relation.Binary.Definitions
-  using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>)
+  using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri<; tri>)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary using (yes; no; ¬_)
 import Relation.Nullary.Reflects as Reflects
@@ -276,20 +276,20 @@ drop‿-<- (-<- n<m) = n<m
 <-asym (-<- n<m) = ℕ.<-asym n<m ∘ drop‿-<-
 <-asym (+<+ m<n) = ℕ.<-asym m<n ∘ drop‿+<+
 
-≤-<-trans : Trans _≤_ _<_ _<_
-≤-<-trans (-≤- n≤m) (-<- o<n) = -<- (ℕ.<-transˡ o<n n≤m)
-≤-<-trans (-≤- n≤m) -<+       = -<+
-≤-<-trans -≤+       (+<+ m<o) = -<+
-≤-<-trans (+≤+ m≤n) (+<+ n<o) = +<+ (ℕ.<-transʳ m≤n n<o)
+≤-<-transˡ : LeftTrans _≤_ _<_
+≤-<-transˡ (-≤- n≤m) (-<- o<n) = -<- (ℕ.<-≤-transʳ o<n n≤m)
+≤-<-transˡ (-≤- n≤m) -<+       = -<+
+≤-<-transˡ -≤+       (+<+ m<o) = -<+
+≤-<-transˡ (+≤+ m≤n) (+<+ n<o) = +<+ (ℕ.≤-<-transˡ m≤n n<o)
 
-<-≤-trans : Trans _<_ _≤_ _<_
-<-≤-trans (-<- n<m) (-≤- o≤n) = -<- (ℕ.<-transʳ o≤n n<m)
-<-≤-trans (-<- n<m) -≤+       = -<+
-<-≤-trans -<+       (+≤+ m≤n) = -<+
-<-≤-trans (+<+ m<n) (+≤+ n≤o) = +<+ (ℕ.<-transˡ m<n n≤o)
+<-≤-transʳ : RightTrans _<_ _≤_
+<-≤-transʳ (-<- n<m) (-≤- o≤n) = -<- (ℕ.≤-<-transˡ o≤n n<m)
+<-≤-transʳ (-<- n<m) -≤+       = -<+
+<-≤-transʳ -<+       (+≤+ m≤n) = -<+
+<-≤-transʳ (+<+ m<n) (+≤+ n≤o) = +<+ (ℕ.<-≤-transʳ m<n n≤o)
 
 <-trans : Transitive _<_
-<-trans m<n n<p = ≤-<-trans (<⇒≤ m<n) n<p
+<-trans m<n n<p = ≤-<-transˡ (<⇒≤ m<n) n<p
 
 <-cmp : Trichotomous _≡_ _<_
 <-cmp +0       +0       = tri≈ +≮0 refl +≮0
@@ -368,8 +368,8 @@ module ≤-Reasoning where
     <-trans
     (resp₂ _<_)
     <⇒≤
-    <-≤-trans
-    ≤-<-trans
+    <-≤-transʳ
+    ≤-<-transˡ
     public
     hiding (step-≈; step-≈˘)
 
@@ -613,7 +613,7 @@ n⊖n≡0 n with n ℕ.<ᵇ n in leq
 
 ⊖-≥ : m ℕ.≥ n → m ⊖ n ≡ + (m ∸ n)
 ⊖-≥ {m} {n} p with m ℕ.<ᵇ n | Reflects.invert (ℕ.<ᵇ-reflects-< m n)
-... | true  | q = contradiction (ℕ.<-transʳ p q) (ℕ.<-irrefl refl)
+... | true  | q = contradiction (ℕ.≤-<-transˡ p q) (ℕ.<-irrefl refl)
 ... | false | q = refl
 
 ≤-⊖ : m ℕ.≤ n → n ⊖ m ≡ + (n ∸ m)
@@ -697,7 +697,7 @@ m⊖n≤m (suc m) (suc n) = begin
   +[1+ m ]      ∎ where open ≤-Reasoning
 
 m⊖n<1+m : ∀ m n → m ⊖ n < +[1+ m ]
-m⊖n<1+m m n = ≤-<-trans (m⊖n≤m m n) (+<+ (ℕ.m<n+m m z<s))
+m⊖n<1+m m n = ≤-<-transˡ (m⊖n≤m m n) (+<+ (ℕ.m<n+m m z<s))
 
 m⊖1+n<m : ∀ m n .{{_ : ℕ.NonZero n}} → m ⊖ n < + m
 m⊖1+n<m zero    (suc n) = -<+
@@ -1053,10 +1053,10 @@ i≤i+j i j rewrite +-comm i j = i≤j+i i j
 
 +-monoʳ-< : ∀ i → (_+_ i) Preserves _<_ ⟶ _<_
 +-monoʳ-< (+ n)    {_} {_}   (-<- o<m) = ⊖-monoʳ->-< n (s<s o<m)
-+-monoʳ-< (+ n)    {_} {_}   -<+       = <-≤-trans (m⊖1+n<m n _) (+≤+ (ℕ.m≤m+n n _))
++-monoʳ-< (+ n)    {_} {_}   -<+       = <-≤-transʳ (m⊖1+n<m n _) (+≤+ (ℕ.m≤m+n n _))
 +-monoʳ-< (+ n)    {_} {_}   (+<+ m<o) = +<+ (ℕ.+-monoʳ-< n m<o)
 +-monoʳ-< -[1+ n ] {_} {_}   (-<- o<m) = -<- (ℕ.+-monoʳ-< (suc n) o<m)
-+-monoʳ-< -[1+ n ] {_} {+ o} -<+       = <-≤-trans (-<- (ℕ.m≤m+n (suc n) _)) (-[1+m]≤n⊖m+1 n o)
++-monoʳ-< -[1+ n ] {_} {+ o} -<+       = <-≤-transʳ (-<- (ℕ.m≤m+n (suc n) _)) (-[1+m]≤n⊖m+1 n o)
 +-monoʳ-< -[1+ n ] {_} {_}   (+<+ m<o) = ⊖-monoˡ-< (suc n) m<o
 
 +-monoˡ-< : ∀ i → (_+ i) Preserves _<_ ⟶ _<_
@@ -1070,10 +1070,10 @@ i≤i+j i j rewrite +-comm i j = i≤j+i i j
   where open ≤-Reasoning
 
 +-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
-+-mono-≤-< {i} {j} {k} i≤j j<k = ≤-<-trans (+-monoˡ-≤ k i≤j) (+-monoʳ-< j j<k)
++-mono-≤-< {i} {j} {k} i≤j j<k = ≤-<-transˡ (+-monoˡ-≤ k i≤j) (+-monoʳ-< j j<k)
 
 +-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
-+-mono-<-≤ {i} {j} {k} i<j j≤k = <-≤-trans (+-monoˡ-< k i<j) (+-monoʳ-≤ j j≤k)
++-mono-<-≤ {i} {j} {k} i<j j≤k = <-≤-transʳ (+-monoˡ-< k i<j) (+-monoʳ-≤ j j≤k)
 
 ------------------------------------------------------------------------
 -- Properties of _-_
@@ -1281,8 +1281,8 @@ minus-suc m n = begin
   pred (m - + n)     ∎ where open ≡-Reasoning
 
 i≤pred[j]⇒i<j : i ≤ pred j → i < j
-i≤pred[j]⇒i<j {_} { + n}      leq = ≤-<-trans leq (m⊖1+n<m n 1)
-i≤pred[j]⇒i<j {_} { -[1+ n ]} leq = ≤-<-trans leq (-<- ℕ.≤-refl)
+i≤pred[j]⇒i<j {_} { + n}      leq = ≤-<-transˡ leq (m⊖1+n<m n 1)
+i≤pred[j]⇒i<j {_} { -[1+ n ]} leq = ≤-<-transˡ leq (-<- ℕ.≤-refl)
 
 i<j⇒i≤pred[j] : i < j → i ≤ pred j
 i<j⇒i≤pred[j] {_} { +0}       -<+       = -≤- z≤n
@@ -2394,3 +2394,14 @@ Please use +-0-isAbelianGroup instead."
 {- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -}
 open Data.Integer.Base public
   using (*-rawMagma; *-1-rawMonoid)
+
+≤-<-trans = ≤-<-transˡ
+{-# WARNING_ON_USAGE ≤-<-trans
+"Warning: ≤-<-trans was deprecated in v2.0. Please use ≤-<-transˡ instead. "
+#-}
+
+<-≤-trans = <-≤-transʳ
+{-# WARNING_ON_USAGE <-≤-trans
+"Warning: <-≤-trans was deprecated in v2.0. Please use <-≤-transʳ instead. "
+#-}
+

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -119,7 +119,7 @@ Unique-resp-↭ = AllPairs-resp-↭ (_∘ ≈-sym) ≉-resp₂
 0<steps (prep eq xs↭ys)      = m<n⇒m<1+n (0<steps xs↭ys)
 0<steps (swap eq₁ eq₂ xs↭ys) = m<n⇒m<1+n (0<steps xs↭ys)
 0<steps (trans xs↭ys xs↭ys₁) =
-  <-transˡ (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁))
+  <-≤-transʳ (0<steps xs↭ys) (m≤m+n (steps xs↭ys) (steps xs↭ys₁))
 
 steps-respˡ : ∀ {xs ys zs} (ys≋xs : ys ≋ xs) (ys↭zs : ys ↭ zs) →
               steps (↭-respˡ-≋ ys≋xs ys↭zs) ≡ steps ys↭zs

src/Data/Nat/Coprimality.agda

@@ -146,4 +146,4 @@ prime⇒coprime (suc (suc _)) p _ _ _ {0} (0∣m , _) =
 prime⇒coprime (suc (suc _)) _ _ _ _ {1} _         = refl
 prime⇒coprime (suc (suc _)) p (suc _) _ n<m {(suc (suc _))} (d∣m , d∣n) =
   contradiction d∣m (p 2≤d d<m)
-  where 2≤d = s≤s (s≤s z≤n); d<m = <-transˡ (s≤s (∣⇒≤ d∣n)) n<m
+  where 2≤d = s≤s (s≤s z≤n); d<m = <-≤-transʳ (s≤s (∣⇒≤ d∣n)) n<m

src/Data/Nat/DivMod.agda

@@ -24,6 +24,10 @@ open import Relation.Nullary.Decidable using (False; toWitnessFalse)
 
 open ≤-Reasoning
 
+private
+  variable
+    m n o p : ℕ
+
 ------------------------------------------------------------------------
 -- Definitions
 
@@ -46,10 +50,10 @@ m%n≡m∸m/n*n m n = begin-equality
 ------------------------------------------------------------------------
 -- Properties of _%_
 
-%-congˡ : ∀ {m n o} .⦃ _ : NonZero o ⦄ → m ≡ n → m % o ≡ n % o
+%-congˡ : .⦃ _ : NonZero o ⦄ → m ≡ n → m % o ≡ n % o
 %-congˡ refl = refl
 
-%-congʳ : ∀ {m n o} .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ≡ n →
+%-congʳ : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ≡ n →
           o % m ≡ o % n
 %-congʳ refl = refl
 
@@ -73,7 +77,7 @@ m%n%n≡m%n m (suc n-1) = modₕ-idem 0 m n-1
   (m + n)           % n ≡⟨ [m+n]%n≡m%n m n ⟩
   m                 % n ∎
 
-m≤n⇒[n∸m]%m≡n%m : ∀ {m n} .⦃ _ : NonZero m ⦄ → m ≤ n →
+m≤n⇒[n∸m]%m≡n%m : .⦃ _ : NonZero m ⦄ → m ≤ n →
                   (n ∸ m) % m ≡ n % m
 m≤n⇒[n∸m]%m≡n%m {m} {n} m≤n = begin-equality
   (n ∸ m) % m     ≡˘⟨ [m+n]%n≡m%n (n ∸ m) m ⟩
@@ -119,12 +123,12 @@ m%n≤n m n = <⇒≤ (m%n<n m n)
 m%n≤m : ∀ m n .{{_ : NonZero n}} → m % n ≤ m
 m%n≤m m (suc n-1) = a[modₕ]n≤a 0 m n-1
 
-m≤n⇒m%n≡m : ∀ {m n} → m ≤ n → m % suc n ≡ m
+m≤n⇒m%n≡m : m ≤ n → m % suc n ≡ m
 m≤n⇒m%n≡m {m} {n} m≤n with ≤⇒≤″ m≤n
 ... | less-than-or-equal {k} refl = a≤n⇒a[modₕ]n≡a 0 (m + k) m k
 
 m<n⇒m%n≡m : ∀ {m n} .⦃ _ : NonZero n ⦄ → m < n → m % n ≡ m
-m<n⇒m%n≡m {m} {suc n} m<n = m≤n⇒m%n≡m (<⇒≤pred m<n)
+m<n⇒m%n≡m {m} {n = suc _} m<n = m≤n⇒m%n≡m (<⇒≤pred m<n)
 
 %-pred-≡0 : ∀ {m n} .{{_ : NonZero n}} → (suc m % n) ≡ 0 → (m % n) ≡ n ∸ 1
 %-pred-≡0 {m} {suc n-1} eq = a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 0 n-1 m eq
@@ -182,11 +186,11 @@ m<[1+n%d]⇒m≤[n%d] {m} n (suc d-1) = k<1+a[modₕ]n⇒k≤a[modₕ]n 0 m n d-
 ------------------------------------------------------------------------
 -- Properties of _/_
 
-/-congˡ : ∀ {m n o : ℕ} .{{_ : NonZero o}} →
+/-congˡ :  .{{_ : NonZero o}} →
           m ≡ n → m / o ≡ n / o
 /-congˡ refl = refl
 
-/-congʳ : ∀ {m n o : ℕ} .{{_ : NonZero n}} .{{_ : NonZero o}} →
+/-congʳ : .{{_ : NonZero n}} .{{_ : NonZero o}} →
           n ≡ o → m / n ≡ m / o
 /-congʳ refl = refl
 
@@ -205,7 +209,7 @@ m*n/n≡m m (suc n-1) = a*n[divₕ]n≡a 0 m n-1
 m/n*n≡m : ∀ {m n} .{{_ : NonZero n}} → n ∣ m → m / n * n ≡ m
 m/n*n≡m {_} {n@(suc _)} (divides-refl q) = cong (_* n) (m*n/n≡m q n)
 
-m*[n/m]≡n : ∀ {m n} .{{_ : NonZero m}} → m ∣ n → m * (n / m) ≡ n
+m*[n/m]≡n : .{{_ : NonZero m}} → m ∣ n → m * (n / m) ≡ n
 m*[n/m]≡n {m} m∣n = trans (*-comm m (_ / m)) (m/n*n≡m m∣n)
 
 m/n*n≤m : ∀ m n .{{_ : NonZero n}} → (m / n) * n ≤ m
@@ -227,11 +231,11 @@ m/n<m m n n≥2 = *-cancelʳ-< _ (m / n) m (begin-strict
   m           <⟨ m<m*n m n n≥2 ⟩
   m * n       ∎)
 
-/-mono-≤ : ∀ {m n o p} .{{_ : NonZero o}} .{{_ : NonZero p}} →
+/-mono-≤ : .{{_ : NonZero o}} .{{_ : NonZero p}} →
            m ≤ n → o ≥ p → m / o ≤ n / p
 /-mono-≤ m≤n (s≤s o≥p) = divₕ-mono-≤ 0 m≤n o≥p
 
-/-monoˡ-≤ : ∀ {m n} o .{{_ : NonZero o}} → m ≤ n → m / o ≤ n / o
+/-monoˡ-≤ : ∀ o .{{_ : NonZero o}} → m ≤ n → m / o ≤ n / o
 /-monoˡ-≤ o m≤n = /-mono-≤ m≤n (≤-refl {o})
 
 /-monoʳ-≤ : ∀ m {n o} .{{_ : NonZero n}} .{{_ : NonZero o}} →
@@ -330,7 +334,7 @@ m<n*o⇒m/o<n {m} {suc n} {o} m<n*o with m <? o
 [m∸n]/n≡m/n∸1 : ∀ m n .⦃ _ : NonZero n ⦄ → (m ∸ n) / n ≡ pred (m / n)
 [m∸n]/n≡m/n∸1 m n with m <? n
 ... | yes m<n = begin-equality
-  (m ∸ n) / n  ≡⟨ m<n⇒m/n≡0 (<-transʳ (m∸n≤m m n) m<n) ⟩
+  (m ∸ n) / n  ≡⟨ m<n⇒m/n≡0 (≤-<-transˡ (m∸n≤m m n) m<n) ⟩
   0            ≡⟨⟩
   0 ∸ 1        ≡˘⟨ cong (_∸ 1) (m<n⇒m/n≡0 m<n) ⟩
   m / n ∸ 1    ≡⟨⟩

src/Data/Nat/DivMod/Core.agda

@@ -154,14 +154,14 @@ private
   divₕ-offsetEq d (suc n) zero    zero    j≤d k≤d (inj₂′ (refl , _)) =
     divₕ-offsetEq d n d d ≤-refl ≤-refl (inj₂′ (refl , a[modₕ]n<n 0 n d , ≤-refl))
   divₕ-offsetEq d (suc n) zero    zero    j≤d k≤d (inj₃ (_ , 0<mod , mod≤0)) =
-    contradiction (<-transˡ 0<mod mod≤0) λ()
+    contradiction (<-≤-transʳ 0<mod mod≤0) λ()
   -- (0 , suc) cases
   divₕ-offsetEq d (suc n) zero (suc k)    j≤d k≤d (inj₁  (refl , _ , 1+k<mod)) =
     divₕ-offsetEq d n d k ≤-refl (<⇒≤ k≤d) (inj₃ (refl , k<1+a[modₕ]n⇒k≤a[modₕ]n 0 (suc k) n d 1+k<mod , a[modₕ]n<n 0 n d))
   divₕ-offsetEq d (suc n) zero (suc k)    j≤d k≤d (inj₂′ (refl , mod≤0 , _)) =
     divₕ-offsetEq d n d k ≤-refl (<⇒≤ k≤d) (inj₃ (refl , subst (k <_) (sym (a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 0 d n (n≤0⇒n≡0 mod≤0))) k≤d , a[modₕ]n<n 0 n d))
   divₕ-offsetEq d (suc n) zero (suc k)    j≤d k≤d (inj₃  (_ , 1+k<mod , mod≤0)) =
-    contradiction (<-transˡ 1+k<mod mod≤0) λ()
+    contradiction (<-≤-transʳ 1+k<mod mod≤0) λ()
   -- (suc , 0) cases
   divₕ-offsetEq d (suc n) (suc j) zero j≤d k≤d (inj₁  (_ , () , _))
   divₕ-offsetEq d (suc n) (suc j) zero j≤d k≤d (inj₂′ (_ , _ , ()))
@@ -174,7 +174,7 @@ private
   ... | yes mod≡0 = divₕ-offsetEq d n j k (<⇒≤ j≤d) (<⇒≤ k≤d) (inj₁ (eq , j≤k , subst (k <_) (sym (a+1[modₕ]n≡0⇒a[modₕ]n≡n-1 0 d n mod≡0)) k≤d))
   ... | no  mod≢0 = divₕ-offsetEq d n j k (<⇒≤ j≤d) (<⇒≤ k≤d) (inj₂′ (eq , 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 j n d (n≢0⇒n>0 mod≢0) mod≤1+j , j≤k))
   divₕ-offsetEq d (suc n) (suc j) (suc k) j≤d k≤d (inj₃  (eq , k<mod , mod≤1+j)) =
-    divₕ-offsetEq d n j k (<⇒≤ j≤d) (<⇒≤ k≤d) (inj₃ (eq , k<1+a[modₕ]n⇒k≤a[modₕ]n 0 (suc k) n d k<mod , 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 j n d (<-transʳ z≤n k<mod) mod≤1+j))
+    divₕ-offsetEq d n j k (<⇒≤ j≤d) (<⇒≤ k≤d) (inj₃ (eq , k<1+a[modₕ]n⇒k≤a[modₕ]n 0 (suc k) n d k<mod , 1+a[modₕ]n≤1+k⇒a[modₕ]n≤k 0 j n d (≤-<-transˡ z≤n k<mod) mod≤1+j))
 
 ------------------------------------------------------------------------
 -- Lemmas for divₕ that also have an interpretation for _/_