From 54661db8c41fea319063ee4bdcb2edf2158d1c32 Mon Sep 17 00:00:00 2001 From: effectfully Date: Sun, 12 Jun 2016 08:16:53 +0300 Subject: [PATCH] decidable equality --- Data.agda | 2 + Lib/{PartDec.agda => Decidable.agda} | 65 +++++++++------------------- Prelude.agda | 2 +- Property/Eq.agda | 35 +++++---------- readme.md | 14 ++++++ 5 files changed, 48 insertions(+), 70 deletions(-) rename Lib/{PartDec.agda => Decidable.agda} (51%) diff --git a/Data.agda b/Data.agda index ab0bb2a..d212817 100644 --- a/Data.agda +++ b/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 diff --git a/Lib/PartDec.agda b/Lib/Decidable.agda similarity index 51% rename from Lib/PartDec.agda rename to Lib/Decidable.agda index 3fc3ab7..de3e8d6 100644 --- a/Lib/PartDec.agda +++ b/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 diff --git a/Prelude.agda b/Prelude.agda index 0a17b5c..546e6af 100644 --- a/Prelude.agda +++ b/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 diff --git a/Property/Eq.agda b/Property/Eq.agda index 3a6b84e..cf66168 100644 --- a/Property/Eq.agda +++ b/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,20 +80,9 @@ 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₂) = @@ -103,32 +90,30 @@ mutual 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) ∷ [] diff --git a/readme.md b/readme.md index 6ce8c39..643b6a9 100644 --- a/readme.md +++ b/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