Language/Graphs.agda

@@ -124,6 +124,28 @@ buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
 buildCfg (if _ then s₁ else s₂) = buildCfg s₁ ∙ buildCfg s₂
 buildCfg (while _ repeat s) = loop (buildCfg s)
 
+private
+    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
+    z≢sf f ()
+
+    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
+    z≢mapsfs [] = []
+    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+    finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+    finValues 0 = ([] , Utils.empty)
+    finValues (suc n') =
+        let
+            (inds' , unids') = finValues n'
+        in
+            ( zero ∷ List.map suc inds'
+            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+            )
+
+    finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
+    finValues-complete (suc n') zero = RelAny.here refl
+    finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
+
 module _ (g : Graph) where
     open import Data.Product.Properties as ProdProp using ()
     private _≟_ = ProdProp.≡-dec (FinProp._≟_ {Graph.size g})
@@ -132,13 +154,13 @@ module _ (g : Graph) where
     open import Data.List.Membership.DecPropositional (_≟_) using (_∈?_)
 
     indices : List (Graph.Index g)
-    indices = proj₁ (fins (Graph.size g))
+    indices = proj₁ (finValues (Graph.size g))
 
     indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
-    indices-complete = fins-complete (Graph.size g)
+    indices-complete = finValues-complete (Graph.size g)
 
     indices-Unique : Unique indices
-    indices-Unique = proj₂ (fins (Graph.size g))
+    indices-Unique = proj₂ (finValues (Graph.size g))
 
     predecessors : (Graph.Index g) → List (Graph.Index g)
     predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices

Utils.agda

@@ -1,16 +1,13 @@
 module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
-open import Data.Product as Prod using (Σ; _×_; _,_; proj₁; proj₂)
+open import Data.Product as Prod using (_×_)
 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.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 using (Any; here; there) -- TODO: re-export these with nicer names from map
-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.Sum using (_⊎_)
 open import Function.Definitions using (Injective)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
@@ -37,14 +34,6 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
         help {[]} _ = x'≢x ∷ []
         help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
 
-Unique-++⁻ˡ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique xs
-Unique-++⁻ˡ [] Unique-ys = empty
-Unique-++⁻ˡ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = push (++⁻ˡ xs {ys = ys} x≢xs++ys) (Unique-++⁻ˡ xs Unique-xs++ys)
-
-Unique-++⁻ʳ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique ys
-Unique-++⁻ʳ [] Unique-ys = Unique-ys
-Unique-++⁻ʳ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = Unique-++⁻ʳ xs Unique-xs++ys
-
 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)
@@ -61,9 +50,6 @@ All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x
 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₁)
-
 All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
 All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
 All-single {c = c} {l = x ∷ xs} (p ∷ ps) (there c∈xs) = All-single ps c∈xs
@@ -120,24 +106,3 @@ _∧_ P Q a = P a × Q a
 
 it : ∀ {a} {A : Set a} {{_ : A}} → A
 it {{x}} = x
-
-z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (Fin.zero ≡ Fin.suc f)
-z≢sf f ()
-
-z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
-z≢mapsfs [] = []
-z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
-
-fins : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-fins 0 = ([] , empty)
-fins (suc n') =
-    let
-        (inds' , unids') = fins n'
-    in
-        ( zero ∷ mapˡ suc inds'
-        , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-        )
-
-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'))