[Refractor] contradiction over ⊥-elim in Data.*.Relation.Binary.Lex.* (#2671)

* [Refractor] contradiction over ⊥-elim in

* Modification

* remove of useless import and replacing tt with _

* add open import Data.Empty using (⊥; ⊥-elim)

Author: jmougeot

src/Data/List/Relation/Binary/Lex/Core.agda

@@ -8,13 +8,13 @@
 
 module Data.List.Relation.Binary.Lex.Core where
 
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Unit.Base using (⊤; tt)
+open import Data.Empty using (⊥)
+open import Data.Unit.Base using (⊤)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Data.List.Base using (List; []; _∷_)
 open import Function.Base using (_∘_; flip; id)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.Core using (Rel)
 open import Data.List.Relation.Binary.Pointwise.Base
    using (Pointwise; []; _∷_; head; tail)

src/Data/List/Relation/Binary/Lex/Strict.agda

@@ -11,8 +11,6 @@
 
 module Data.List.Relation.Binary.Lex.Strict where
 
-open import Data.Empty using (⊥)
-open import Data.Unit.Base using (⊤; tt)
 open import Function.Base using (_∘_; id)
 open import Data.Product.Base using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
@@ -146,7 +144,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
 
   ≤-reflexive : (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
                 Pointwise _≈_ ⇒ Lex-≤ _≈_ _≺_
-  ≤-reflexive _≈_ _≺_ []            = base tt
+  ≤-reflexive _≈_ _≺_ []            = base _
   ≤-reflexive _≈_ _≺_ (x≈y ∷ xs≈ys) =
     next x≈y (≤-reflexive _≈_ _≺_ xs≈ys)
 
@@ -168,7 +166,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     -- the following lemma.
 
     ≤-total : Symmetric _≈_ → Trichotomous _≈_ _≺_ → Total _≤_
-    ≤-total _   _   []       []       = inj₁ (base tt)
+    ≤-total _   _   []       []       = inj₁ (base _)
     ≤-total _   _   []       (x ∷ xs) = inj₁ halt
     ≤-total _   _   (x ∷ xs) []       = inj₂ halt
     ≤-total sym tri (x ∷ xs) (y ∷ ys) with tri x y
@@ -179,7 +177,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ...   | inj₂ ys≲xs = inj₂ (next (sym x≈y) ys≲xs)
 
     ≤-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _≤_
-    ≤-decidable = Core.decidable (yes tt)
+    ≤-decidable = Core.decidable (yes _)
 
     ≤-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   _≤_ Respects₂ _≋_

src/Data/Vec/Relation/Binary/Lex/Core.agda

@@ -8,7 +8,6 @@
 
 module Data.Vec.Relation.Binary.Lex.Core {a} {A : Set a} where
 
-open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; suc)
 import Data.Nat.Properties as ℕ using (_≟_; ≡-irrelevant)
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
@@ -27,7 +26,7 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; cong)
 import Relation.Nullary as Nullary
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_)
-open import Relation.Nullary.Negation
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
   variable
@@ -114,9 +113,9 @@ module _ {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
 
     antisym : ∀ {n} → Antisymmetric (_≋_ {n}) (_<ₗₑₓ_)
     antisym (base _)         (base _)         = []
-    antisym (this x≺y m≡n)   (this y≺x n≡m)   = ⊥-elim (≺-asym x≺y y≺x)
-    antisym (this x≺y m≡n)   (next y≈x ys<xs) = ⊥-elim (≺-irrefl (≈-sym y≈x) x≺y)
-    antisym (next x≈y xs<ys) (this y≺x m≡n)   = ⊥-elim (≺-irrefl (≈-sym x≈y) y≺x)
+    antisym (this x≺y m≡n)   (this y≺x n≡m)   = contradiction y≺x (≺-asym x≺y)
+    antisym (this x≺y m≡n)   (next y≈x ys<xs) = contradiction x≺y (≺-irrefl (≈-sym y≈x))
+    antisym (next x≈y xs<ys) (this y≺x m≡n)   = contradiction y≺x (≺-irrefl (≈-sym x≈y))
     antisym (next x≈y xs<ys) (next y≈x ys<xs) = x≈y ∷ (antisym xs<ys ys<xs)
 
   module _ (≈-equiv : IsPartialEquivalence _≈_) (open IsPartialEquivalence ≈-equiv) where

src/Data/Vec/Relation/Binary/Lex/Strict.agda

@@ -23,7 +23,7 @@ open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
   using (Pointwise; []; _∷_; head; tail)
 open import Function.Base using (id; _on_; _∘_)
 open import Induction.WellFounded
-open import Relation.Nullary using (yes; no; ¬_)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder
@@ -39,7 +39,8 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Binary.Construct.On as On using (wellFounded)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-open import Level using (Level; _⊔_)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
   variable
@@ -139,7 +140,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     where
 
     <-wellFounded : ∀ {n} → WellFounded (_<_ {n})
-    <-wellFounded {0}     [] = acc λ ys<[] → ⊥-elim (xs≮[] ys<[])
+    <-wellFounded {0}     [] = acc λ ys<[] → contradiction ys<[] xs≮[]
 
     <-wellFounded {suc n} xs = Subrelation.wellFounded <⇒uncons-Lex uncons-Lex-wellFounded xs
       where