From fdc2c02045d7cf6f2f24a875cabcf2bf03c97906 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 30 Jul 2025 11:28:00 +0100 Subject: [PATCH 1/2] [ refactoring ] decidable `Data.Fin.Properties` --- src/Data/Fin/Properties.agda | 62 +++++++++++++++++++++--------------- 1 file changed, 37 insertions(+), 25 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 0f87eef534..377272c3d7 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -28,7 +28,7 @@ open import Data.Product.Properties using (,-injective) open import Data.Product.Algebra using (×-cong) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) open import Data.Sum.Properties using ([,]-map; [,]-∘) -open import Function.Base using (_∘_; id; _$_; flip) +open import Function.Base using (_∘_; id; _$_; flip; const; λ-; _$-) open import Function.Bundles using (Injection; _↣_; _⇔_; _↔_; mk⇔; mk↔ₛ′) open import Function.Definitions using (Injective; Surjective) open import Function.Consequences.Propositional using (contraInjective) @@ -54,10 +54,13 @@ open import Relation.Unary.Properties using (U?) private variable - a : Level + a p q : Level A : Set a m n o : ℕ i j : Fin n + P : Pred (Fin n) p + Q : Pred (Fin n) q + ------------------------------------------------------------------------ -- Fin @@ -954,7 +957,7 @@ pinch-injective {i = suc i} {suc j} {suc k} 1+i≢j 1+i≢k eq = -- Quantification ------------------------------------------------------------------------ -module _ {p} {P : Pred (Fin (suc n)) p} where +module _ {P : Pred (Fin (suc n)) p} where ∀-cons : P zero → Π[ P ∘ suc ] → Π[ P ] ∀-cons z s zero = z @@ -976,33 +979,19 @@ module _ {p} {P : Pred (Fin (suc n)) p} where ⊎⇔∃ : (P zero ⊎ ∃⟨ P ∘ suc ⟩) ⇔ ∃⟨ P ⟩ ⊎⇔∃ = mk⇔ [ ∃-here , ∃-there ] ∃-toSum -decFinSubset : ∀ {p q} {P : Pred (Fin n) p} {Q : Pred (Fin n) q} → - Decidable Q → (∀ {i} → Q i → Dec (P i)) → Dec (Q ⊆ P) -decFinSubset {zero} {_} {_} Q? P? = yes λ {} -decFinSubset {suc n} {P = P} {Q} Q? P? - with Q? zero | ∀-cons {P = λ x → Q x → P x} -... | false because [¬Q0] | cons = - map′ (λ f {x} → cons (⊥-elim ∘ invert [¬Q0]) (λ x → f {x}) x) - (λ f {x} → f {suc x}) - (decFinSubset (Q? ∘ suc) P?) -... | true because [Q0] | cons = - map′ (uncurry λ P0 rec {x} → cons (λ _ → P0) (λ x → rec {x}) x) - < _$ invert [Q0] , (λ f {x} → f {suc x}) > - (P? (invert [Q0]) ×-dec decFinSubset (Q? ∘ suc) P?) - -any? : ∀ {p} {P : Pred (Fin n) p} → Decidable P → Dec (∃ P) -any? {zero} {P = _} P? = no λ { (() , _) } -any? {suc n} {P = P} P? = Dec.map ⊎⇔∃ (P? zero ⊎-dec any? (P? ∘ suc)) - -all? : ∀ {p} {P : Pred (Fin n) p} → Decidable P → Dec (∀ f → P f) -all? P? = map′ (λ ∀p f → ∀p tt) (λ ∀p {x} _ → ∀p x) - (decFinSubset U? (λ {f} _ → P? f)) +any? : Decidable P → Dec (∃ P) +any? {zero} P? = no λ{ (() , _) } +any? {suc _} P? = Dec.map ⊎⇔∃ (P? zero ⊎-dec any? (P? ∘ suc)) + +all? : Decidable P → Dec (∀ i → P i) +all? {zero} P? = yes λ() +all? {suc _} P? = Dec.map ∀-cons-⇔ (P? zero ×-dec all? (P? ∘ suc)) private -- A nice computational property of `all?`: -- The boolean component of the result is exactly the -- obvious fold of boolean tests (`foldr _∧_ true`). - note : ∀ {p} {P : Pred (Fin 3) p} (P? : Decidable P) → + note : ∀ {P : Pred (Fin 3) p} (P? : Decidable P) → ∃ λ z → Dec.does (all? P?) ≡ z note P? = Dec.does (P? 0F) ∧ Dec.does (P? 1F) ∧ Dec.does (P? 2F) ∧ true , refl @@ -1025,6 +1014,29 @@ private ¬ (∀ i → P i) → (∃ λ i → ¬ P i) ¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P) +-- Kleisli lifting of Dec over Unary subset relation + +decFinSubset : Decidable Q → Q ⊆ Dec ∘ P → Dec (Q ⊆ P) +decFinSubset {zero} {_} {_} Q? P? = yes λ{} +decFinSubset {suc _} {Q = Q} {P = P} Q? P? = dec[Q⊆P] + module DecFinSubset where + Q⊆₀P = Q 0F → P 0F + Q⊆ₛP = Q ∘ suc ⊆ P ∘ suc + + cons : Q⊆₀P → Q⊆ₛP → Q ⊆ P + cons q₀⊆p₀ qₛ⊆pₛ = ∀-cons {P = Q U.⇒ P} q₀⊆p₀ (λ- qₛ⊆pₛ) $- + + ih : Dec Q⊆ₛP + ih = decFinSubset (Q? ∘ suc) P? + + Q⊆P⇒Q⊆ₛP : Q ⊆ P → Q⊆ₛP + Q⊆P⇒Q⊆ₛP q⊆p {x} = q⊆p {suc x} + + dec[Q⊆P] : Dec (Q ⊆ P) + dec[Q⊆P] with Q? zero + ... | no ¬q₀ = map′ (cons (flip contradiction ¬q₀)) Q⊆P⇒Q⊆ₛP ih + ... | yes q₀ = map′ (uncurry (cons ∘ const)) < _$ q₀ , Q⊆P⇒Q⊆ₛP > (P? q₀ ×-dec ih) + ------------------------------------------------------------------------ -- Properties of functions to and from Fin ------------------------------------------------------------------------ From 2af5d2155c0892ebb0bae11e5fb3370d1f0a4aa2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 2 Aug 2025 09:48:21 +0100 Subject: [PATCH 2/2] refactor: make `variable`s `P`, `Q` local again --- src/Data/Fin/Properties.agda | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 377272c3d7..38cc0ff2ca 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -58,8 +58,6 @@ private A : Set a m n o : ℕ i j : Fin n - P : Pred (Fin n) p - Q : Pred (Fin n) q ------------------------------------------------------------------------ @@ -979,11 +977,11 @@ module _ {P : Pred (Fin (suc n)) p} where ⊎⇔∃ : (P zero ⊎ ∃⟨ P ∘ suc ⟩) ⇔ ∃⟨ P ⟩ ⊎⇔∃ = mk⇔ [ ∃-here , ∃-there ] ∃-toSum -any? : Decidable P → Dec (∃ P) +any? : ∀ {P : Pred (Fin n) p} → Decidable P → Dec (∃ P) any? {zero} P? = no λ{ (() , _) } any? {suc _} P? = Dec.map ⊎⇔∃ (P? zero ⊎-dec any? (P? ∘ suc)) -all? : Decidable P → Dec (∀ i → P i) +all? : ∀ {P : Pred (Fin n) p} → Decidable P → Dec (∀ i → P i) all? {zero} P? = yes λ() all? {suc _} P? = Dec.map ∀-cons-⇔ (P? zero ×-dec all? (P? ∘ suc)) @@ -1016,9 +1014,10 @@ private -- Kleisli lifting of Dec over Unary subset relation -decFinSubset : Decidable Q → Q ⊆ Dec ∘ P → Dec (Q ⊆ P) +decFinSubset : ∀ {P : Pred (Fin n) p} {Q : Pred (Fin n) q} → + Decidable Q → Q ⊆ Dec ∘ P → Dec (Q ⊆ P) decFinSubset {zero} {_} {_} Q? P? = yes λ{} -decFinSubset {suc _} {Q = Q} {P = P} Q? P? = dec[Q⊆P] +decFinSubset {suc _} {P = P} {Q = Q} Q? P? = dec[Q⊆P] module DecFinSubset where Q⊆₀P = Q 0F → P 0F Q⊆ₛP = Q ∘ suc ⊆ P ∘ suc