[ fix #718 ] Fix unsolved metas in propositional uniqueness (#719)

Author: gallais

src/Data/List/Relation/Binary/Sublist/Heterogeneous/Core.agda

@@ -5,6 +5,9 @@
 -- Data.List.Relation.Binary.Sublist.Heterogeneous.
 ------------------------------------------------------------------------
 
+-- This module should be removable if and when Agda issue
+-- https://github.com/agda/agda/issues/3210 is fixed
+
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary using (REL)

src/Data/List/Relation/Unary/AllPairs.agda

@@ -6,7 +6,10 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.List.Relation.Unary.AllPairs where
+open import Relation.Binary using (Rel)
+
+module Data.List.Relation.Unary.AllPairs
+       {a ℓ} {A : Set a} {R : Rel A ℓ} where
 
 open import Data.List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
@@ -23,65 +26,54 @@ import Relation.Nullary.Decidable as Dec
 ------------------------------------------------------------------------
 -- Definition
 
--- AllPairs R xs means that every pair of elements (x , y) in xs is a
--- member of relation R (as long as x comes before y in the list).
-
-infixr 5 _∷_
-
-data AllPairs {a ℓ} {A : Set a} (R : Rel A ℓ) : List A → Set (a ⊔ ℓ) where
-  []  : AllPairs R []
-  _∷_ : ∀ {x xs} → All (R x) xs → AllPairs R xs → AllPairs R (x ∷ xs)
+open import Data.List.Relation.Unary.AllPairs.Core public
 
 ------------------------------------------------------------------------
 -- Operations
 
-module _ {a ℓ} {A : Set a} {R : Rel A ℓ} where
+head : ∀ {x xs} → AllPairs R (x ∷ xs) → All (R x) xs
+head (px ∷ pxs) = px
 
-  head : ∀ {x xs} → AllPairs R (x ∷ xs) → All (R x) xs
-  head (px ∷ pxs) = px
+tail : ∀ {x xs} → AllPairs R (x ∷ xs) → AllPairs R xs
+tail (px ∷ pxs) = pxs
 
-  tail : ∀ {x xs} → AllPairs R (x ∷ xs) → AllPairs R xs
-  tail (px ∷ pxs) = pxs
-
-module _ {a p q} {A : Set a} {R : Rel A p} {S : Rel A q} where
+module _ {q} {S : Rel A q} where
 
   map : R ⇒ S → AllPairs R ⊆ AllPairs S
   map ~₁⇒~₂ [] = []
   map ~₁⇒~₂ (x~xs ∷ pxs) = All.map ~₁⇒~₂ x~xs ∷ (map ~₁⇒~₂ pxs)
 
-module _ {a p q r} {A : Set a} {P : Rel A p} {Q : Rel A q} {R : Rel A r} where
+module _ {s t} {S : Rel A s} {T : Rel A t} where
 
-  zipWith : P ∩ᵇ Q ⇒ R → AllPairs P ∩ᵘ AllPairs Q ⊆ AllPairs R
+  zipWith : R ∩ᵇ S ⇒ T → AllPairs R ∩ᵘ AllPairs S ⊆ AllPairs T
   zipWith f ([] , [])             = []
   zipWith f (px ∷ pxs , qx ∷ qxs) = All.zipWith f (px , qx) ∷ zipWith f (pxs , qxs)
 
-  unzipWith : R ⇒ P ∩ᵇ Q → AllPairs R ⊆ AllPairs P ∩ᵘ AllPairs Q
+  unzipWith : T ⇒ R ∩ᵇ S → AllPairs T ⊆ AllPairs R ∩ᵘ AllPairs S
   unzipWith f []         = [] , []
   unzipWith f (rx ∷ rxs) = Prod.zip _∷_ _∷_ (All.unzipWith f rx) (unzipWith f rxs)
 
-module _ {a p q} {A : Set a} {P : Rel A p} {Q : Rel A q} where
+module _ {s} {S : Rel A s} where
 
-  zip : AllPairs P ∩ᵘ AllPairs Q ⊆ AllPairs (P ∩ᵇ Q)
+  zip : AllPairs R ∩ᵘ AllPairs S ⊆ AllPairs (R ∩ᵇ S)
   zip = zipWith id
 
-  unzip : AllPairs (P ∩ᵇ Q) ⊆ AllPairs P ∩ᵘ AllPairs Q
+  unzip : AllPairs (R ∩ᵇ S) ⊆ AllPairs R ∩ᵘ AllPairs S
   unzip = unzipWith id
 
 ------------------------------------------------------------------------
 -- Properties of predicates preserved by AllPairs
 
-module _ {a ℓ} {A : Set a} {R : Rel A ℓ} where
-
-  allPairs? : B.Decidable R → U.Decidable (AllPairs R)
-  allPairs? R? []       = yes []
-  allPairs? R? (x ∷ xs) with All.all (R? x) xs
-  ... | yes px = Dec.map′ (px ∷_) tail (allPairs? R? xs)
-  ... | no ¬px = no (¬px ∘ head)
+allPairs? : B.Decidable R → U.Decidable (AllPairs R)
+allPairs? R? []       = yes []
+allPairs? R? (x ∷ xs) with All.all (R? x) xs
+... | yes px = Dec.map′ (px ∷_) tail (allPairs? R? xs)
+... | no ¬px = no (¬px ∘ head)
 
-  irrelevant : B.Irrelevant R → U.Irrelevant (AllPairs R)
-  irrelevant irr []           []           = refl
-  irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
-    cong₂ _∷_ (All.irrelevant irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)
+irrelevant : B.Irrelevant R → U.Irrelevant (AllPairs R)
+irrelevant irr []           []           = refl
+irrelevant irr (px₁ ∷ pxs₁) (px₂ ∷ pxs₂) =
+  cong₂ _∷_ (All.irrelevant irr px₁ px₂) (irrelevant irr pxs₁ pxs₂)
 
-  satisfiable : U.Satisfiable (AllPairs R)
-  satisfiable = [] , []
+satisfiable : U.Satisfiable (AllPairs R)
+satisfiable = [] , []

src/Data/List/Relation/Unary/AllPairs/Core.agda

@@ -0,0 +1,34 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Lists where every pair of elements are related (symmetrically)
+------------------------------------------------------------------------
+
+-- Core modules are not meant to be used directly outside of the
+-- standard library.
+
+-- This module should be removable if and when Agda issue
+-- https://github.com/agda/agda/issues/3210 is fixed
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Rel)
+
+module Data.List.Relation.Unary.AllPairs.Core
+       {a ℓ} {A : Set a} (R : Rel A ℓ) where
+
+open import Level
+open import Data.List.Base
+open import Data.List.Relation.Unary.All
+
+------------------------------------------------------------------------
+-- Definition
+
+-- AllPairs R xs means that every pair of elements (x , y) in xs is a
+-- member of relation R (as long as x comes before y in the list).
+
+infixr 5 _∷_
+
+data AllPairs : List A → Set (a ⊔ ℓ) where
+  []  : AllPairs []
+  _∷_ : ∀ {x xs} → All (R x) xs → AllPairs xs → AllPairs (x ∷ xs)

src/Data/List/Relation/Unary/Unique/Setoid.agda

@@ -6,22 +6,31 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary using (Rel; Setoid)
 
 module Data.List.Relation.Unary.Unique.Setoid {a ℓ} (S : Setoid a ℓ) where
 
+open Setoid S renaming (Carrier to A)
+
 open import Data.List
-open import Data.List.Relation.Unary.AllPairs as AllPairsM
+import Data.List.Relation.Unary.AllPairs as AllPairsM
 open import Level using (_⊔_)
 open import Relation.Unary using (Pred)
 open import Relation.Nullary using (¬_)
 
-open Setoid S renaming (Carrier to A)
 
 ------------------------------------------------------------------------
 -- Definition
 
-Unique : Pred (List A) (a ⊔ ℓ)
-Unique xs = AllPairs (λ x y → ¬ (x ≈ y)) xs
+private
+
+  Distinct : Rel A ℓ
+  Distinct x y = ¬ (x ≈ y)
+
+open import Data.List.Relation.Unary.AllPairs.Core Distinct
+     renaming (AllPairs to Unique)
+     public
 
-open AllPairsM public using (_∷_; []; head; tail)
+open import Data.List.Relation.Unary.AllPairs {R = Distinct}
+     using (head; tail)
+     public