/usr/share/agda-stdlib/Data/Fin/Dec.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Decision procedures for finite sets and subsets of finite sets
------------------------------------------------------------------------
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 PropositionalEquality to PropVecEq)
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 Relation.Binary as B
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary as U using (Pred)
infix 4 _∈?_
_∈?_ : ∀ {n} x (p : Subset n) → Dec (x ∈ p)
zero ∈? inside ∷ p = yes here
zero ∈? outside ∷ p = no λ()
suc n ∈? s ∷ p with n ∈? p
... | yes n∈p = yes (there n∈p)
... | no n∉p = no (n∉p ∘ drop-there)
private
restrictP : ∀ {p n} → (Fin (suc n) → Set p) → (Fin n → Set p)
restrictP P f = P (suc f)
restrict : ∀ {p n} {P : Fin (suc n) → Set p} →
U.Decidable P → U.Decidable (restrictP P)
restrict dec f = dec (suc f)
any? : ∀ {n} {P : Fin n → Set} →
U.Decidable P → Dec (∃ P)
any? {zero} {P} dec = no (((λ()) ∶ ¬ Fin 0) ∘ proj₁)
any? {suc n} {P} dec with dec zero | any? (restrict dec)
... | yes p | _ = yes (_ , p)
... | _ | yes (_ , p') = yes (_ , p')
... | no ¬p | no ¬p' = no helper
where
helper : ∄ P
helper (zero , p) = ¬p p
helper (suc f , p') = ¬p' (_ , p')
nonempty? : ∀ {n} (p : Subset n) → Dec (Nonempty p)
nonempty? p = any? (λ x → x ∈? p)
private
restrict∈ : ∀ {p q n}
(P : Fin (suc n) → Set p) {Q : Fin (suc n) → Set q} →
(∀ {f} → Q f → Dec (P f)) →
(∀ {f} → restrictP Q f → Dec (restrictP P f))
restrict∈ _ dec {f} Qf = dec {suc f} Qf
decFinSubset : ∀ {p q n} {P : Fin n → Set p} {Q : Fin n → Set q} →
U.Decidable Q →
(∀ {f} → Q f → Dec (P f)) →
Dec (∀ {f} → Q f → P f)
decFinSubset {n = zero} _ _ = yes λ{}
decFinSubset {n = suc n} {P} {Q} decQ decP = helper
where
helper : Dec (∀ {f} → Q f → P f)
helper with decFinSubset (restrict decQ) (restrict∈ P decP)
helper | no ¬q⟶p = no (λ q⟶p → ¬q⟶p (λ {f} q → q⟶p {suc f} q))
helper | yes q⟶p with decQ zero
helper | yes q⟶p | yes q₀ with decP q₀
helper | yes q⟶p | yes q₀ | no ¬p₀ = no (λ q⟶p → ¬p₀ (q⟶p {zero} q₀))
helper | yes q⟶p | yes q₀ | yes p₀ = yes (λ {_} → hlpr _)
where
hlpr : ∀ f → Q f → P f
hlpr zero _ = p₀
hlpr (suc f) qf = q⟶p qf
helper | yes q⟶p | no ¬q₀ = yes (λ {_} → hlpr _)
where
hlpr : ∀ f → Q f → P f
hlpr zero q₀ = ⊥-elim (¬q₀ q₀)
hlpr (suc f) qf = q⟶p qf
all∈? : ∀ {n p} {P : Fin n → Set p} {q} →
(∀ {f} → f ∈ q → Dec (P f)) →
Dec (∀ {f} → f ∈ q → P f)
all∈? {q = q} dec = decFinSubset (λ f → f ∈? q) dec
all? : ∀ {n p} {P : Fin n → Set p} →
U.Decidable P → Dec (∀ f → P 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} →
U.Decidable P → U.Decidable (Lift P)
decLift dec p = all∈? (λ {x} _ → dec x)
private
restrictSP : ∀ {n} → Side → (Subset (suc n) → Set) → (Subset n → Set)
restrictSP s P p = P (s ∷ p)
restrictS : ∀ {n} {P : Subset (suc n) → Set} →
(s : Side) → U.Decidable P → U.Decidable (restrictSP s P)
restrictS s dec p = dec (s ∷ p)
anySubset? : ∀ {n} {P : Subset n → Set} →
U.Decidable P → Dec (∃ P)
anySubset? {zero} {P} dec with dec []
... | yes P[] = yes (_ , P[])
... | no ¬P[] = no helper
where
helper : ∄ P
helper ([] , P[]) = ¬P[] P[]
anySubset? {suc n} {P} dec with anySubset? (restrictS inside dec)
| anySubset? (restrictS outside dec)
... | yes (_ , Pp) | _ = yes (_ , Pp)
... | _ | yes (_ , Pp) = yes (_ , Pp)
... | no ¬Pp | no ¬Pp' = no helper
where
helper : ∄ P
helper (inside ∷ p , Pp) = ¬Pp (_ , Pp)
helper (outside ∷ p , Pp') = ¬Pp' (_ , Pp')
-- If a decidable predicate P over a finite set is sometimes false,
-- then we can find the smallest value for which this is the case.
¬∀⟶∃¬-smallest :
∀ n {p} (P : Fin n → Set p) → U.Decidable P →
¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
¬∀⟶∃¬-smallest zero P dec ¬∀iPi = ⊥-elim (¬∀iPi (λ()))
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi with dec zero
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | no ¬P0 = (zero , ¬P0 , λ ())
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | yes P0 =
Prod.map suc (Prod.map id extend′) $
¬∀⟶∃¬-smallest n (λ n → P (suc n)) (dec ∘ suc) (¬∀iPi ∘ extend)
where
extend : (∀ i → P (suc i)) → (∀ i → P i)
extend ∀iP[1+i] zero = P0
extend ∀iP[1+i] (suc i) = ∀iP[1+i] i
extend′ : ∀ {i : Fin n} →
((j : Fin′ i) → P (suc (inject j))) →
((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} → B.Decidable (_⊆_ {n = n})
p₁ ⊆? p₂ =
Dec.map (Eq.sym NaturalPoset.orders-equivalent) $
Dec.map′ PropVecEq.to-≡ PropVecEq.from-≡ $
VecEq.DecidableEquality._≟_ Bool.decSetoid p₁ (p₁ ∩ p₂)
|