[ refactor ] do not add irrefl as a parameter to Triple

Author: gallais

src/Data/Integer/Properties.agda

@@ -330,14 +330,17 @@ n≮n {n} = <-irrefl refl
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
-    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤
     <-≤-trans
     ≤-<-trans
+    as Reasoning
     public
-    hiding (step-≈; step-≈˘)
+    hiding (begin-irrefl; step-≈; step-≈˘)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 ------------------------------------------------------------------------
 -- Properties of Positive/NonPositive/Negative/NonNegative and _≤_/_<_
@@ -2601,4 +2604,3 @@ Please use *-cancelˡ-<-nonNeg instead."
 "Warning: *-cancelʳ-<-non-neg was deprecated in v1.5.
 Please use *-cancelʳ-<-nonNeg instead."
 #-}
-

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -254,8 +254,6 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq)
      ≡⟨ P.cong₂ _,_ (lose∘find p) (lose∘find q) ⟩
 
     (p , q) ∎
-    where
-
 
   to∘from : ∀ pq → Any-×⁺ {xs = xs} (Any-×⁻ pq) ≡ pq
   to∘from pq

src/Data/Nat/Properties.agda

@@ -421,14 +421,17 @@ m<n⇒m≤1+n (s≤s (s≤s m<n)) = s≤s (m<n⇒m≤1+n (s≤s m<n))
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
-    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤
     <-transˡ
     <-transʳ
+    as Reasoning
     public
-    hiding (step-≈; step-≈˘)
+    hiding (begin-irrefl; step-≈; step-≈˘)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 open ≤-Reasoning
 

src/Data/Rational/Properties.agda

@@ -433,14 +433,17 @@ p <? q = Dec.map′ *<* drop-*<* ((↥ p ℤ.* ↧ q) ℤ.<? (↥ q ℤ.* ↧ p)
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
-    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤
     <-≤-trans
     ≤-<-trans
+    as Reasoning
     public
-    hiding (step-≈; step-≈˘)
+    hiding (begin-irrefl; step-≈; step-≈˘)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 ------------------------------------------------------------------------
 -- Properties of _/_

src/Data/Rational/Unnormalised/Properties.agda

@@ -393,13 +393,17 @@ p <? q = Dec.map′ *<* drop-*<* (↥ p ℤ.* ↧ q ℤ.<? ↥ q ℤ.* ↧ p)
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
-    <-irrefl
     <-trans
     <-resp-≃
     <⇒≤
     <-≤-trans
     ≤-<-trans
+    as Reasoning
     public
+    hiding (begin-irrefl)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 ------------------------------------------------------------------------
 -- Properties of ↥_/↧_

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda

@@ -30,7 +30,6 @@ open StrictTotalOrder sto renaming (Carrier to Key); open Eq using (_≉_; sym;
 
 import Relation.Binary.Reasoning.StrictPartialOrder as <-Reasoning
 
-
 private
   variable
     v p q : Level

src/Relation/Binary/Reasoning/Base/Triple.agda

@@ -15,7 +15,6 @@ open import Relation.Binary
 module Relation.Binary.Reasoning.Base.Triple {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
   {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} {_<_ : Rel A ℓ₃}
   (isPreorder : IsPreorder _≈_ _≤_)
-  (<-irrefl : Irreflexive _≈_ _<_)
   (<-trans : Transitive _<_) (<-resp-≈ : _<_ Respects₂ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
   (<-≤-trans : Trans _<_ _≤_ _<_) (≤-<-trans : Trans _≤_ _<_ _<_)
   where
@@ -25,7 +24,7 @@ open import Function.Base using (case_of_; id)
 open import Level using (Level; _⊔_; Lift; lift)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
-open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary using (Dec; yes; no; ¬_)
 open import Relation.Nullary.Decidable using (True; toWitness)
 open import Relation.Nullary.Negation using (contradiction)
 
@@ -78,7 +77,7 @@ extractEquality (isEquality x≈y) = x≈y
 -- See `Relation.Binary.Reasoning.Base.Partial` for the design decisions
 -- behind these combinators.
 
-infix  1 begin_ begin-strict_ begin-irrefl_ begin-equality_
+infix  1 begin_ begin-strict_ begin-equality_
 infixr 2 step-< step-≤ step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_
 infix  3 _∎
 
@@ -92,12 +91,21 @@ begin (equals    x≈y) = ≤-reflexive x≈y
 begin-strict_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsStrict? r)} → x < y
 begin-strict_ r {s} = extractStrict (toWitness s)
 
-begin-irrefl_ : ∀ {x} (r : x IsRelatedTo x) → {s : True (IsStrict? r)} → ∀ {a} {A : Set a} → A
-begin-irrefl_ r {s} = contradiction (extractStrict (toWitness s)) (<-irrefl Eq.refl)
-
 begin-equality_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsEquality? r)} → x ≈ y
 begin-equality_ r {s} = extractEquality (toWitness s)
 
+
+begin-irrefl : Irreflexive _≈_ _<_ →
+                ∀ {x} (r : x IsRelatedTo x) {s : True (IsStrict? r)} →
+                ∀ {a} {A : Set a} → A
+begin-irrefl <-irrefl {x} r {s} =  contradiction x<x x≮x where
+
+  x<x : x < x
+  x<x = extractStrict (toWitness s)
+
+  x≮x : ¬ (x < x)
+  x≮x = <-irrefl Eq.refl
+
 -- Step with the strict relation
 
 step-< : ∀ (x : A) {y z} → y IsRelatedTo z → x < y → x IsRelatedTo z

src/Relation/Binary/Reasoning/PartialOrder.agda

@@ -45,22 +45,26 @@ module Relation.Binary.Reasoning.PartialOrder
   {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where
 
 open Poset P
-import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as Strict
+open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_
+  as Strict
+  using (_<_)
 
 ------------------------------------------------------------------------
 -- Re-export contents of base module
 
 open import Relation.Binary.Reasoning.Base.Triple
   isPreorder
-  Strict.<-irrefl
   (Strict.<-trans isPartialOrder)
   (Strict.<-resp-≈ isEquivalence ≤-resp-≈)
   Strict.<⇒≤
   (Strict.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈)
   (Strict.≤-<-trans trans antisym ≤-respˡ-≈)
+  as Reasoning
   public
+  hiding (begin-irrefl)
 
-
+infix 1 begin-irrefl_
+begin-irrefl_ = Reasoning.begin-irrefl Strict.irrefl
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Relation/Binary/Reasoning/StrictPartialOrder.agda

@@ -53,10 +53,14 @@ import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as NonStrict
 
 open import Relation.Binary.Reasoning.Base.Triple
   (NonStrict.isPreorder₂ isStrictPartialOrder)
-  irrefl
   trans
   <-resp-≈
   NonStrict.<⇒≤
   (NonStrict.<-≤-trans trans <-respʳ-≈)
   (NonStrict.≤-<-trans Eq.sym trans <-respˡ-≈)
+  as Reasoning
   public
+  hiding (begin-irrefl)
+
+infix 1 begin-irrefl_
+begin-irrefl_ = Reasoning.begin-irrefl irrefl