decidable equality

Data.agda

@@ -1,5 +1,7 @@
 module OTT.Data where
 
+open import OTT.Data.Lift  public
+open import OTT.Data.Fin   public
 open import OTT.Data.Maybe public
 open import OTT.Data.Sum   public
 open import OTT.Data.W     public

Lib/PartDec.agda → Lib/Decidable.agda

@@ -1,4 +1,8 @@
-module OTT.Lib.PartDec where
+module OTT.Lib.Decidable where
+
+open import Relation.Nullary public
+open import Relation.Nullary.Decidable public
+open import Relation.Binary using (Decidable) public
 
 open import Function
 open import Relation.Nullary
@@ -12,59 +16,37 @@ infix  3  _#_
 
 _% = _∘_
 
-data PartDec {α} (A : Set α) : Set α where
-  yes  : A   -> PartDec A
-  no   : ¬ A -> PartDec A
-  none : PartDec A
-
-PartDecidable : ∀ {α} {A : Set α} -> (A -> A -> Set α) -> Set α
-PartDecidable _~_ = ∀ x y -> PartDec (x ~ y)
-
-IsPartSet : ∀ {α} -> Set α -> Set α
-IsPartSet A = PartDecidable {A = A} _≡_
+IsSet : ∀ {α} -> Set α -> Set α
+IsSet A = Decidable {A = A} _≡_
 
 _#_ : ∀ {α} {A : Set α} -> A -> A -> Set α
-x # y = PartDec (x ≡ y)
+x # y = Dec (x ≡ y)
 
-delim : ∀ {α π} {A : Set α} {P : PartDec A -> Set π}
-      -> (∀ x -> P (yes x)) -> (∀ c -> P (no c)) -> P none -> (d : PartDec A) -> P d
-delim f g z (yes x) = f x
-delim f g z (no  c) = g c
-delim f g z  none   = z
+delim : ∀ {α π} {A : Set α} {P : Dec A -> Set π}
+      -> (∀ x -> P (yes x)) -> (∀ c -> P (no c)) -> (d : Dec A) -> P d
+delim f g (yes x) = f x
+delim f g (no  c) = g c
 
-drec : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> (¬ A -> B) -> B -> PartDec A -> B
+drec : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> (¬ A -> B) -> Dec A -> B
 drec = delim
 
-dbind : ∀ {α β} {A : Set α} {B : Set β}
-      -> (A -> PartDec B) -> (¬ A -> PartDec B) -> PartDec A -> PartDec B
-dbind f g = drec f g none
-
-dmap : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> (¬ A -> ¬ B) -> PartDec A -> PartDec B
-dmap f g = dbind (yes ∘ f) (no ∘ g)
+dmap : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> (¬ A -> ¬ B) -> Dec A -> Dec B
+dmap f g = drec (yes ∘ f) (no ∘ g)
 
 sumM2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
-      -> (A -> PartDec C)
-      -> (B -> PartDec C)
-      -> (¬ A -> ¬ B -> PartDec C)
-      -> PartDec A -> PartDec B
-      -> PartDec C
-sumM2 f g h d e = dbind f (λ c -> dbind g (h c) e) d
+      -> (A -> Dec C) -> (B -> Dec C) -> (¬ A -> ¬ B -> Dec C) -> Dec A -> Dec B -> Dec C
+sumM2 f g h d e = drec f (λ c -> drec g (h c) e) d
 
 prodM2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
-       -> (A -> B -> PartDec C)
-       -> (¬ A -> PartDec C)
-       -> (¬ B -> PartDec C)
-       -> PartDec A
-       -> PartDec B
-       -> PartDec C
-prodM2 h f g d e = dbind (λ x -> dbind (h x) g e) f d
+       -> (A -> B -> Dec C) -> (¬ A -> Dec C) -> (¬ B -> Dec C) -> Dec A -> Dec B -> Dec C
+prodM2 h f g d e = drec (λ x -> drec (h x) g e) f d
 
 sumF2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
-     -> (A -> C) -> (B -> C) -> (¬ A -> ¬ B -> ¬ C) -> PartDec A -> PartDec B -> PartDec C
+      -> (A -> C) -> (B -> C) -> (¬ A -> ¬ B -> ¬ C) -> Dec A -> Dec B -> Dec C
 sumF2 f g h = sumM2 (yes ∘ f) (yes ∘ g) (no % ∘ h) 
 
 prodF2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
-       -> (A -> B -> C) -> (¬ A -> ¬ C) -> (¬ B -> ¬ C) -> PartDec A -> PartDec B -> PartDec C
+       -> (A -> B -> C) -> (¬ A -> ¬ C) -> (¬ B -> ¬ C) -> Dec A -> Dec B -> Dec C
 prodF2 h f g = prodM2 (yes % ∘ h) (no ∘ f) (no ∘ g) 
 
 dcong : ∀ {α β} {A : Set α} {B : Set β} {x y}
@@ -87,8 +69,3 @@ dhcong₂ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {x₁ x
         -> f x₁ y₁ # f x₂ y₂
 dhcong₂ f inj (yes refl) q = dcong (f _) (homo ∘ inj) (q _)
 dhcong₂ f inj (no c)     q = no (c ∘ inds ∘ inj)
-dhcong₂ f inj  none      q = none
-
-decToPartDec : ∀ {α} {A : Set α} -> Dec A -> PartDec A
-decToPartDec (yes x) = yes x
-decToPartDec (no  c) = no  c

Prelude.agda

@@ -12,7 +12,7 @@ open import Data.Maybe.Base using (Maybe; nothing; just) public
 open import Data.Product hiding (,_) renaming (map to pmap) public
 
 open import OTT.Lib.HeteroIndexed public
-open import OTT.Lib.PartDec public
+open import OTT.Lib.Decidable public
 
 open import Relation.Nullary
 open import Relation.Binary

Property/Eq.agda

@@ -7,7 +7,7 @@ import Data.Nat.Base as Nat
 
 open import OTT.Main
 
-infix 4 _≟_ _≟ᵈ_
+infix 4 _≟_
 
 -- TODO?
 module _ where
@@ -34,7 +34,8 @@ module _ where
     go (suc (suc n))  nothing (x , xs) = x
     go (suc (suc n)) (just e) (x , xs) = go (suc n) e xs
 
--- We could compare functions with a finite domain for equality.
+-- We could compare functions with a finite domain for equality,
+-- but then equality can't be `_≡_`.
 mutual
   SemEq : ∀ {i a} {α : Level a} {I : Type i} -> Desc I α -> Set
   SemEq (var i) = ⊤
@@ -49,14 +50,11 @@ mutual
   Eq : ∀ {a} {α : Level a} -> Univ α -> Set
   Eq  bot       = ⊤
   Eq  top       = ⊤
-  Eq (α ≡ˢˡ β)  = ⊥
   Eq  nat       = ⊤
   Eq (enum n)   = ⊤
-  Eq (univ α)   = ⊥
   Eq (σ A B)    = Eq A × Pi A λ x -> Eq (B x)
-  Eq (π A B)    = ⊥
-  Eq (desc I α) = Eq I
   Eq (imu D j)  = ExtendEq D
+  Eq  _         = ⊥
 
   -- Should there be a separate type class for `imu`?
   -- Is there any reason to bother with `desc`?
@@ -82,53 +80,40 @@ apply {A = imu _ _ } y x = y
 
 {-# TERMINATING #-}
 mutual
-  _≟ᵈ_ : ∀ {i a} {α : Level a} {I : Type i} {{eqI : Eq I}} -> IsPartSet (Desc I α)
-  var i₁    ≟ᵈ var i₂    = dcong var var-inj (i₁ ≟ i₂)
-  π A₁ D₁   ≟ᵈ π A₂ D₂   = none -- The only undecidable part.
-  (D₁ ⊛ E₁) ≟ᵈ (D₂ ⊛ E₂) = dcong₂ _⊛_ ⊛-inj (D₁ ≟ᵈ D₂) (E₁ ≟ᵈ E₂)
-  var _     ≟ᵈ π _ _     = no λ()
-  var _     ≟ᵈ (_ ⊛ _)   = no λ()
-  π _ _     ≟ᵈ var _     = no λ()
-  π _ _     ≟ᵈ (_ ⊛ _)   = no λ()
-  (_ ⊛ _)   ≟ᵈ var _     = no λ()
-  (_ ⊛ _)   ≟ᵈ π _ _     = no λ()
-
   decSem : ∀ {i a p} {α : Level a} {φ : Level p} {I : Type i}
              {F : ⟦ I ⟧ -> Univ φ} {{eqF : ∀ {i} -> Eq (F i)}}
-         -> (D : Desc I α) {{eqD : SemEq D}} -> IsPartSet (⟦ D ⟧ᵈ ⟦ F ⟧ᵒ)
+         -> (D : Desc I α) {{eqD : SemEq D}} -> IsSet (⟦ D ⟧ᵈ ⟦ F ⟧ᵒ)
   decSem (var i)                x₁        x₂       = x₁ ≟ x₂ 
   decSem (π A D) {{()}}
   decSem (D ⊛ E) {{eqD , eqE}} (s₁ , t₁) (s₂ , t₂) =
     decSem D {{eqD}} s₁ s₂ <,>ᵈ decSem E {{eqE}} t₁ t₂
 
   decExtend : ∀ {i a p} {α : Level a} {φ : Level p} {I : Type i} {j}
                 {F : ⟦ I ⟧ -> Univ φ} {{eqF : ∀ {i} -> Eq (F i)}}
-            -> (D : Desc I α) {{eqD : ExtendEq D}} -> IsPartSet (Extend D ⟦ F ⟧ᵒ j)
+            -> (D : Desc I α) {{eqD : ExtendEq D}} -> IsSet (Extend D ⟦ F ⟧ᵒ j)
   decExtend (var i)                q₁        q₂       = yes contr
   decExtend (π A D) {{eqA , eqD}} (x₁ , e₁) (x₂ , e₂) =
     _≟_ {{eqA}} x₁ x₂ <,>ᵈᵒ decExtend (D x₁) {{apply eqD x₁}} e₁
   decExtend (D ⊛ E) {{eqD , eqE}} (s₁ , e₁) (s₂ , e₂) =
     decSem D {{eqD}} s₁ s₂ <,>ᵈ decExtend E {{eqE}} e₁ e₂
 
-  _≟_ : ∀ {a} {α : Level a} {A : Univ α} {{eqA : Eq A}} -> IsPartSet ⟦ A ⟧
+  _≟_ : ∀ {a} {α : Level a} {A : Univ α} {{eqA : Eq A}} -> IsSet ⟦ A ⟧
   _≟_ {A = bot     }                ()        ()
   _≟_ {A = top     }                tt        tt       = yes prefl
   _≟_ {A = α ≡ˢˡ β } {{()}}
-  _≟_ {A = nat     }                n₁        n₂       = decToPartDec (n₁ Nat.≟ n₂)
-  _≟_ {A = enum n  }               (tag e₁)  (tag e₂)  =
-    dcong tag tag-inj (decToPartDec (decEnum n e₁ e₂))
+  _≟_ {A = nat     }                n₁        n₂       = n₁ Nat.≟ n₂
+  _≟_ {A = enum n  }               (tag e₁)  (tag e₂)  = dcong tag tag-inj (decEnum n e₁ e₂)
   _≟_ {A = univ α  } {{()}}
   _≟_ {A = σ A B   } {{eqA , eqB}} (x₁ , y₁) (x₂ , y₂) =
     _≟_ {{eqA}} x₁ x₂ <,>ᵈᵒ _≟_ {{apply eqB x₁}} y₁
   _≟_ {A = π A B   } {{()}}
-  _≟_ {A = desc I α}                D₁        D₂       = D₁ ≟ᵈ D₂
+  _≟_ {A = desc I α} {{()}}
   _≟_ {A = imu D j }               (node e₁) (node e₂) = dcong node node-inj (decExtend D e₁ e₂)
 
 private
   module Test where
     open import OTT.Data.Fin
     open import OTT.Data.Sum
-    open import OTT.Data.List
 
     ns₁ : List (list nat ⊕ σ nat fin)
     ns₁ = inj₁ (1 ∷ 4 ∷ []) ∷ inj₂ (3 , fsuc fzero) ∷ inj₂ (2 , fzero) ∷ []

readme.md

@@ -188,6 +188,20 @@ elimW : ∀ {a b π} {α : Level a} {β : Level b} {A : Univ α} {B : ⟦ A ⟧
 elimW P h (sup x g) = h (λ y -> elimW P h (g y))
 ```
 
+An example of generic programming can be found in the `Property/Eq.agda` module which defines this operator:
+
+`_≟_ : ∀ {a} {α : Level a} {A : Univ α} {{eqA : Eq A}} -> (x y : ⟦ A ⟧) -> Dec (x ≡ y)`
+
+It can handle numbers, finite sets, sums, products, lists and many other data types. An example:
+
+```
+ns : List (list nat ⊕ σ nat fin)
+ns = inj₁ (1 ∷ 4 ∷ []) ∷ inj₂ (3 , fsuc fzero) ∷ inj₂ (2 , fzero) ∷ []
+
+test : (ns ≟ ns) ≡ yes prefl
+test = prefl
+```
+
 There is [an alternative encoding](https://github.com/effectfully/random-stuff/blob/master/IRDesc.agda) in terms of proper propositional descriptions (see [6]), which is a slightly modified version of [7]. It's more standard, more powerful (it's able to express induction-recursion), but also significantly more complicated: data types must be defined mutually with coercions (or maybe we can to use a parametrised module like in the model, but it still doesn't look nice), which results in a giant mutual block. I didn't try to define equality and coercions for descriptions, but I suspect it's much harder than how it's now. I'll go with the current simple approach.
 
 ## Not implemented