DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add some utility proofs about uniqueness etc.

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-12-07 19:28:27 -08:00
parent 84c4ea6936
commit ef3c351bb0
1 changed files with 30 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
Utils.agda
View File

@ -6,17 +6,22 @@ open import Data.Nat using (ℕ; suc)
open import Data.Fin as Fin using (Fin; suc; zero)
open import Data.Fin.Properties using (suc-injective)
open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional using (_∈_; lose)
open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
open import Data.List.Relation.Unary.All.Properties using (++⁻ˡ)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there) -- TODO: re-export these with nicer names from map
open import Data.List.Relation.Unary.All using (All; []; _∷_; map; all?; lookup)
open import Data.List.Relation.Unary.All.Properties using (++⁻ˡ; ++⁻ʳ)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there; any?) -- TODO: re-export these with nicer names from map
open import Data.Sum using (_⊎_)
open import Function.Definitions using (Injective)
open import Relation.Binary using (Antisymmetric) renaming (Decidable to Decidable²)
open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary using (¬_; yes; no; Dec)
open import Relation.Unary using (Decidable)
All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
data Unique {c} {C : Set c} : List C → Set c where
empty : Unique []
push : ∀ {x : C} {xs : List C}
@ -45,6 +50,16 @@ Unique-++⁻ʳ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs
Unique-++⁻ʳ [] Unique-ys = Unique-ys
Unique-++⁻ʳ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = Unique-++⁻ʳ xs Unique-xs++ys
Unique-∈-++ˡ : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} → Unique (xs ++ ys) → x ∈ xs → ¬ x ∈ ys
Unique-∈-++ˡ [] _ ()
Unique-∈-++ˡ {x = x} (x' ∷ xs) (push x≢xs++ys _) (here refl) = All¬-¬Any (++⁻ʳ xs x≢xs++ys)
Unique-∈-++ˡ {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-∈-++ˡ xs Unique-xs++ys x̷∈xs
Unique-narrow : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} → Unique (xs ++ ys) → x ∈ xs → Unique (x ∷ ys)
Unique-narrow [] _ ()
Unique-narrow {x = x} (x' ∷ xs) (push x≢xs++ys Unique-xs++ys) (here refl) = push (++⁻ʳ xs x≢xs++ys) (Unique-++⁻ʳ xs Unique-xs++ys)
Unique-narrow {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-narrow xs Unique-xs++ys x̷∈xs
All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
@ -57,10 +72,6 @@ Unique-map : ∀ {c d} {C : Set c} {D : Set d} {l : List C} (f : C → D) →
Unique-map {l = []} _ _ _ = empty
Unique-map {l = x ∷ xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)
All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
¬Any-map : ∀ {p₁ p₂ c} {C : Set c} {P₁ : C → Set p₁} {P₂ : C → Set p₂} {l : List C} → (∀ {x} → P₁ x → P₂ x) → ¬ Any P₂ l → ¬ Any P₁ l
¬Any-map f ¬Any-P₂ Any-P₁ = ¬Any-P₂ (Any.map f Any-P₁)
@ -141,3 +152,13 @@ fins (suc n') =
fins-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ (proj₁ (fins n))
fins-complete (suc n') zero = here refl
fins-complete (suc n') (suc f') = there (x∈xs⇒fx∈fxs suc (fins-complete n' f'))
findUniversal : ∀ {p c} {C : Set c} {R : C → C → Set p} (l : List C) → Decidable² R →
Dec (Any (λ x → All (R x) l) l)
findUniversal l Rdec = any? (λ x → all? (Rdec x) l) l
findUniversal-unique : ∀ {p c} {C : Set c} (R : C → C → Set p) (l : List C) →
Antisymmetric _≡_ R →
∀ x₁ x₂ → x₁ ∈ l → x₂ ∈ l → All (R x₁) l → All (R x₂) l →
x₁ ≡ x₂
findUniversal-unique R l Rantisym x₁ x₂ x₁∈l x₂∈l Allx₁ Allx₂ = Rantisym (lookup Allx₁ x₂∈l) (lookup Allx₂ x₁∈l)