Imported Upstream version 0.5

1 files changed, 22 insertions, 2 deletions

diff --git a/src/Data/Fin/Dec.agda b/src/Data/Fin/Dec.agda
index 7b50302..d54ca0c 100644
--- a/src/Data/Fin/Dec.agda
+++ b/src/Data/Fin/Dec.agda
@@ -7,15 +7,23 @@
 module Data.Fin.Dec where
 
 open import Function
+import Data.Bool as Bool
 open import Data.Nat hiding (_<_)
 open import Data.Vec hiding (_∈_)
+open import Data.Vec.Equality as VecEq
+  using () renaming (module HeterogeneousEquality to HetVecEq)
 open import Data.Fin
 open import Data.Fin.Subset
 open import Data.Fin.Subset.Props
 open import Data.Product as Prod
 open import Data.Empty
+open import Function
+import Function.Equivalence as Eq
 open import Level hiding (Lift)
+open import Relation.Binary
+import Relation.Binary.HeterogeneousEquality as H
 open import Relation.Nullary
+import Relation.Nullary.Decidable as Dec
 open import Relation.Unary using (Pred)
 
 infix 4 _∈?_
@@ -92,8 +100,8 @@ all∈? {q = q} dec = decFinSubset (λ f → f ∈? q) dec
 all? : ∀ {n} {P : Fin n → Set} →
        (∀ f → Dec (P f)) →
        Dec (∀ f → P f)
-all? dec with all∈? {q = all inside} (λ {f} _ → dec f)
-...      | yes ∀p = yes (λ f → ∀p (allInside f))
+all? dec with all∈? {q = ⊤} (λ {f} _ → dec f)
+...      | yes ∀p = yes (λ f → ∀p ∈⊤)
 ...      | no ¬∀p = no  (λ ∀p → ¬∀p (λ {f} _ → ∀p f))
 
 decLift : ∀ {n} {P : Fin n → Set} →
@@ -153,3 +161,15 @@ anySubset? {suc n} {P} dec with anySubset? (restrictS inside  dec)
             ((j : Fin′ (suc i)) → P (inject j))
   extend′ g zero    = P0
   extend′ g (suc j) = g j
+
+-- Decision procedure for _⊆_ (obtained via the natural lattice
+-- order).
+
+infix 4 _⊆?_
+
+_⊆?_ : ∀ {n} → Decidable (_⊆_ {n = n})
+p₁ ⊆? p₂ =
+  Dec.map (Eq.sym NaturalPoset.orders-equivalent) $
+  Dec.map′ H.≅-to-≡ H.≡-to-≅ $
+  Dec.map′ HetVecEq.to-≅ HetVecEq.from-≅ $
+  VecEq.DecidableEquality._≟_ Bool.decSetoid p₁ (p₁ ∩ p₂)