Decidable: inequality instances + syntactic sugar

Class/Decidable/Core.agda

@@ -37,26 +37,41 @@ _⁇³ = _⁇ ³
 
 module _ {A : Type ℓ} where
 
-  dec¹ : {P : Pred A ℓ′} → ⦃ P ⁇¹ ⦄ → Decidable¹ P
-  dec¹ _ = dec
+  module _ {P : Pred A ℓ′} where
+
+    dec¹ : ⦃ P ⁇¹ ⦄ → Decidable¹ P
+    dec¹ _ = dec
+
+    ⁇¹_ : Decidable¹ P → P ⁇¹
+    ⁇¹ p? = ⁇ (p? _)
 
   ¿_¿¹ : (P : Pred A ℓ′) → ⦃ P ⁇¹ ⦄ → Decidable¹ P
   ¿ _ ¿¹ = dec¹
 
 module _ {A B : Type ℓ} where
 
-  dec² : {_~_ : REL A B ℓ′} → ⦃ _~_ ⁇² ⦄ → Decidable² _~_
-  dec² _ _ = dec
+  module _ {R : REL A B ℓ′} where
+
+    dec² : ⦃ R ⁇² ⦄ → Decidable² R
+    dec² _ _ = dec
 
-  ¿_¿² : (_~_ : REL A B ℓ′) → ⦃ _~_ ⁇² ⦄ → Decidable² _~_
+    ⁇²_ : Decidable² R → R ⁇²
+    ⁇² p? = ⁇ (p? _ _)
+
+  ¿_¿² : (R : REL A B ℓ′) → ⦃ R ⁇² ⦄ → Decidable² R
   ¿ _ ¿² = dec²
 
 module _ {A B C : Type ℓ} where
 
-  dec³ : {_~_~_ : 3REL A B C ℓ′} → ⦃ _~_~_ ⁇³ ⦄ → Decidable³ _~_~_
-  dec³ _ _ _ = dec
+  module _ {R : 3REL A B C ℓ′} where
+
+    dec³ : ⦃ R ⁇³ ⦄ → Decidable³ R
+    dec³ _ _ _ = dec
+
+    ⁇³_ : Decidable³ R → R ⁇³
+    ⁇³_ p? = ⁇ (p? _ _ _)
 
-  ¿_¿³ : (_~_~_ : 3REL A B C ℓ′) → ⦃ _~_~_ ⁇³ ⦄ → Decidable³ _~_~_
+  ¿_¿³ : (R : 3REL A B C ℓ′) → ⦃ R ⁇³ ⦄ → Decidable³ R
   ¿ _ ¿³ = dec³
 
 infix -100 auto∶_

Class/Decidable/Instances.agda

@@ -12,6 +12,13 @@ private variable
   R : Rel A ℓ
 
 instance
+
+  -- ** deriving from DecEq
+  DecEq⇒Dec : ⦃ DecEq A ⦄ → _≡_ {A = A} ⁇²
+  DecEq⇒Dec = ⁇² _≟_
+
+  -- ** basic type formers
+
   Dec-⊥ : ⊥ ⁇
   Dec-⊥ .dec = no λ()
 
@@ -23,53 +30,65 @@ instance
   Dec-→ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A → B) ⁇
   Dec-→ .dec = dec D.→-dec dec
 
+  -- ** products
+
   Dec-× : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A × B) ⁇
   Dec-× .dec = dec D.×-dec dec
 
+  -- ** sums
+
   Dec-⊎ : ⦃ A ⁇ ⦄ → ⦃ B ⁇ ⦄ → (A ⊎ B) ⁇
   Dec-⊎ .dec = dec D.⊎-dec dec
 
-  DecEq⇒Dec : ⦃ DecEq A ⦄ → _≡_ {A = A} ⁇²
-  DecEq⇒Dec .dec = _ ≟ _
+  import Data.Sum.Relation.Unary.All as ⊎; open ⊎ using (inj₁; inj₂)
+  open import Relation.Nullary.Decidable using () renaming (map′ to mapDec)
+
+  Dec-⊎All : ⦃ P ⁇¹ ⦄ → ⦃ Q ⁇¹ ⦄ → ⊎.All P Q ⁇¹
+  Dec-⊎All {P = P} {Q = Q} {x = inj₁ x} .dec = mapDec inj₁ inj₁˘ ¿ P x ¿
+    where inj₁˘ : ⊎.All P Q (inj₁ x) → P x
+          inj₁˘ (inj₁ x) = x
+  Dec-⊎All {P = P} {Q = Q} {x = inj₂ y} .dec = mapDec inj₂ inj₂˘ ¿ Q y ¿
+    where inj₂˘ : ⊎.All P Q (inj₂ x) → Q x
+          inj₂˘ (inj₂ x) = x
 
   import Data.Bool as 𝔹
 
   Dec-T : T ⁇¹
-  Dec-T .dec = 𝔹.T? _
+  Dec-T = ⁇¹ 𝔹.T?
 
   import Data.List.Relation.Unary.All as L
   import Data.List.Relation.Unary.Any as L
 
   Dec-All : ⦃ P ⁇¹ ⦄ → L.All P ⁇¹
-  Dec-All .dec = L.all? dec¹ _
+  Dec-All = ⁇¹ L.all? dec¹
 
   Dec-Any : ⦃ P ⁇¹ ⦄ → L.Any P ⁇¹
-  Dec-Any .dec = L.any? dec¹ _
+  Dec-Any = ⁇¹ L.any? dec¹
 
   import Data.List.Relation.Unary.AllPairs as AP
 
   Dec-AllPairs : ⦃ R ⁇² ⦄ → AP.AllPairs R ⁇¹
-  Dec-AllPairs .dec = AP.allPairs? dec² _
+  Dec-AllPairs = ⁇¹ AP.allPairs? dec²
 
   open import Data.Vec as V
   open import Data.Vec.Relation.Unary.All as V
   open import Data.Vec.Relation.Unary.Any as V
 
   Dec-VAll : ⦃ P ⁇¹ ⦄ → V.All P {n} ⁇¹
-  Dec-VAll .dec = V.all? dec¹ _
+  Dec-VAll = ⁇¹ V.all? dec¹
 
   Dec-VAny : ⦃ P ⁇¹ ⦄ → V.Any P {n} ⁇¹
-  Dec-VAny .dec = V.any? dec¹ _
+  Dec-VAny = ⁇¹ V.any? dec¹
 
   import Data.Maybe as M
   import Data.Maybe.Relation.Unary.All as M renaming (dec to all?)
   import Data.Maybe.Relation.Unary.Any as M renaming (dec to any?)
 
   Dec-MAll : ⦃ P ⁇¹ ⦄ → M.All P ⁇¹
-  Dec-MAll .dec = M.all? dec¹ _
+  Dec-MAll = ⁇¹ M.all? dec¹
 
   Dec-MAny : ⦃ P ⁇¹ ⦄ → M.Any P ⁇¹
-  Dec-MAny .dec = M.any? dec¹ _
+  Dec-MAny = ⁇¹ M.any? dec¹
 
   Dec-Is-just : M.Is-just {A = A} ⁇¹
   Dec-Is-just {x = x} .dec with x
@@ -81,13 +100,14 @@ instance
   ... | just _  = no λ where (M.just ())
   ... | nothing = yes M.nothing
 
-  import Data.Sum.Relation.Unary.All as ⊎; open ⊎ using (inj₁; inj₂)
-  open import Relation.Nullary.Decidable using () renaming (map′ to mapDec)
+  -- ** inequalities
 
-  Dec-⊎All : ⦃ P ⁇¹ ⦄ → ⦃ Q ⁇¹ ⦄ → ⊎.All P Q ⁇¹
-  Dec-⊎All {P = P} {Q = Q} {x = inj₁ x} .dec = mapDec inj₁ inj₁˘ ¿ P x ¿
-    where inj₁˘ : ⊎.All P Q (inj₁ x) → P x
-          inj₁˘ (inj₁ x) = x
-  Dec-⊎All {P = P} {Q = Q} {x = inj₂ y} .dec = mapDec inj₂ inj₂˘ ¿ Q y ¿
-    where inj₂˘ : ⊎.All P Q (inj₂ x) → Q x
-          inj₂˘ (inj₂ x) = x
+  import Data.Nat.Properties as ℕ
+
+  ℕ-Dec-≤ = ⁇² ℕ._≤?_
+  ℕ-Dec-< = ⁇² ℕ._<?_
+
+  import Data.Integer.Properties as ℤ
+
+  ℤ-Dec-≤ = ⁇² ℤ._≤?_
+  ℤ-Dec-< = ⁇² ℤ._<?_

Test/Decidable.agda

@@ -5,9 +5,17 @@ open import Class.Prelude
 open import Class.Decidable
 open import Class.DecEq
 
+import Data.Nat as ℕ
+_ = ℕ._≤_ ⁇² ∋ it
+_ = ℕ._<_ ⁇² ∋ it
+
+import Data.Integer as ℤ
+_ = ℤ._≤_ ⁇² ∋ it
+_ = ℤ._<_ ⁇² ∋ it
+
 open import Data.List.Membership.Propositional using (_∈_; _∉_)
 
-private 0⋯2 = List ℕ ∋ 0 ∷ 1 ∷ 2 ∷ []
+0⋯2 = List ℕ ∋ 0 ∷ 1 ∷ 2 ∷ []
 
 _ = 1 ∈ 0⋯2
   ∋ auto