Lattice/Builder.agda

@@ -2,29 +2,26 @@ module Lattice.Builder where
 
 open import Lattice
 open import Equivalence
-open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal; Decidable-¬)
+open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; All¬-¬Any; ¬Any-map; fins; fins-complete)
 open import Data.Nat as Nat using (ℕ)
 open import Data.Fin as Fin using (Fin; suc; zero; _≟_)
 open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
 open import Data.Maybe.Properties using (just-injective)
 open import Data.Unit using (⊤; tt)
 open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
-open import Data.List.Membership.Propositional as MemProp using (lose) renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ)
+open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ)
 open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ; ∈-++⁺ˡ to ∈ˡ-++⁺ˡ; ∈-cartesianProductWith⁺ to ∈ˡ-cartesianProductWith⁺)
-open import Data.List.Relation.Unary.Any using (Any; here; there; any?; satisfied)
+open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.List.Relation.Unary.Any.Properties using (¬Any[])
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate)
-open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate; all?)
 open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺; ++⁻ʳ to ++ˡ⁻ʳ)
 open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_)
 open import Data.List.Properties using () renaming (++-conicalʳ to ++ˡ-conicalʳ; ++-identityʳ to ++ˡ-identityʳ; ++-assoc to ++ˡ-assoc)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂; uncurry)
 open import Data.Empty using (⊥; ⊥-elim)
-open import Relation.Nullary using (¬_; Dec; yes; no; ¬?)
+open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
-open import Relation.Binary using () renaming (Decidable to Decidable²)
-open import Relation.Unary using (Decidable)
 open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
 
 record Graph : Set where
@@ -52,10 +49,6 @@ record Graph : Set where
     data IsDone : ∀ {n₁ n₂} → Path n₁ n₂ → Set where
         isDone : ∀ {n : Node} → IsDone (done {n})
 
-    IsDone? : ∀ {n₁ n₂} → Decidable (IsDone {n₁} {n₂})
-    IsDone? done = yes isDone
-    IsDone? (step _ _) = no (λ {()})
-
     _++_ : ∀ {n₁ n₂ n₃} → Path n₁ n₂ → Path n₂ n₃ → Path n₁ n₃
     done ++ p = p
     (step e p₁) ++ p₂ = step e (p₁ ++ p₂)
@@ -161,26 +154,15 @@ record Graph : Set where
 
     open import Data.List.Membership.DecSetoid (decSetoid {A = Node} _≟_) using () renaming (_∈?_ to _∈ˡ?_)
 
-    splitFromInteriorʳ : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
+    splitFromInterior : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
-                        Σ (Path n n₂) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ ns ++ˡ n ∷ interior p'))
+                        Σ (Path n n₂) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ ns ++ˡ interior p'))
-    splitFromInteriorʳ done ()
+    splitFromInterior done ()
-    splitFromInteriorʳ (step _ done) ()
+    splitFromInterior (step _ done) ()
-    splitFromInteriorʳ (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (p' , ((λ {()}) , ([] , refl)))
+    splitFromInterior (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (p' , ((λ {()}) , (n' ∷ [] , refl)))
-    splitFromInteriorʳ (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
+    splitFromInterior (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
-        with (p'' , (¬IsDone-p'' , (ns , intp'≡ns++intp''))) ← splitFromInteriorʳ p' n∈intp'
+        with (p'' , (¬IsDone-p'' , (ns , intp'≡ns++intp''))) ← splitFromInterior p' n∈intp'
-        rewrite intp'≡ns++intp'' = (p'' , (¬IsDone-p'' , (n' ∷ ns , refl)))
+             rewrite intp'≡ns++intp'' = (p'' , (¬IsDone-p'' , (n' ∷ ns , refl)))
 
-    splitFromInteriorˡ : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
-                        Σ (Path n₁ n) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ interior p' ++ˡ ns))
-    splitFromInteriorˡ done ()
-    splitFromInteriorˡ (step _ done) ()
-    splitFromInteriorˡ p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (step n₁,n'∈edges done , ((λ {()}) , (interior p , refl)))
-    splitFromInteriorˡ p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
-        with splitFromInteriorˡ p' n∈intp'
-    ...   | (p''@(step _ _) , (¬IsDone-p'' , (ns , intp'≡intp''++ns)))
-            rewrite intp'≡intp''++ns
-            = (step n₁,n'∈edges p'' , ((λ { () }) , (ns , refl)))
-    ...   | (done , (¬IsDone-Done , _)) = ⊥-elim (¬IsDone-Done isDone)
 
     findCycleHelp : ∀ {n₁ nⁱ n₂} (p : Path n₁ n₂) (p₁ : Path n₁ nⁱ) (p₂ : Path nⁱ n₂) →
                       ¬ IsDone p₁ → Unique (interior p₁) →
@@ -194,55 +176,17 @@ record Graph : Set where
                 intp₁'≡intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ'∈edges done) ¬IsDone-p₁ (λ {()}))
                 ¬IsDone-p₁' = IsDone-++ˡ p₁ (step nⁱ,nⁱ'∈edges done) ¬IsDone-p₁
                 p≡p₁'++p₂' = trans p≡p₁++p₂ (sym (++-assoc p₁ (step nⁱ,nⁱ'∈edges done) p₂'))
-                Unique-intp₁' = subst Unique (sym intp₁'≡intp₁++[nⁱ]) (Unique-append nⁱ∉intp₁ Unique-intp₁)
+            in findCycleHelp p p₁' p₂' ¬IsDone-p₁' (subst Unique (sym intp₁'≡intp₁++[nⁱ]) (Unique-append nⁱ∉intp₁ Unique-intp₁)) p≡p₁'++p₂'
-            in findCycleHelp p p₁' p₂' ¬IsDone-p₁' Unique-intp₁' p≡p₁'++p₂'
     ...   | yes nⁱ∈intp₁
-            with (pᶜ , (¬IsDone-pᶜ , (ns , intp₁≡ns++intpᶜ))) ← splitFromInteriorʳ p₁ nⁱ∈intp₁
+            with (pᶜ , (¬IsDone-pᶜ , (ns , intp₁≡ns++intpᶜ))) ← splitFromInterior p₁ nⁱ∈intp₁ =
-            rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior pᶜ)) =
             let Unique-intp₁' = subst Unique intp₁≡ns++intpᶜ Unique-intp₁
-            in inj₂ (nⁱ , ((pᶜ , (Unique-++⁻ʳ (ns ++ˡ nⁱ ∷ [])  Unique-intp₁' , tabulate (λ {x} _ → nodes-complete x))) , ¬IsDone-pᶜ))
+            in inj₂ (nⁱ , ((pᶜ , (Unique-++⁻ʳ ns  Unique-intp₁' , tabulate (λ {x} _ → nodes-complete x))) , ¬IsDone-pᶜ))
 
     findCycle : ∀ {n₁ n₂} (p : Path n₁ n₂) →  (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w →  ¬ IsDone (proj₁ w)))
     findCycle done = inj₁ ((done , (empty , [])) , refl)
     findCycle (step n₁,n₂∈edges done) = inj₁ ((step n₁,n₂∈edges done , (empty , [])) , refl)
     findCycle p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) = findCycleHelp p (step n₁,n'∈edges done) p' (λ {()}) empty refl
 
-    toSimpleWalk : ∀ {n₁ n₂} (p : Path n₁ n₂) → SimpleWalkVia (proj₁ nodes) n₁ n₂
-    toSimpleWalk done = (done , (empty , []))
-    toSimpleWalk (step {n₂ = nⁱ} n₁,nⁱ∈edges p')
-        with toSimpleWalk p'
-    ...   | (done , _) = (step n₁,nⁱ∈edges done , (empty , []))
-    ...   | (p''@(step _ _) , (Unique-intp'' , intp''⊆nodes))
-            with nⁱ ∈ˡ? interior p''
-    ...       | no nⁱ∉intp'' = (step n₁,nⁱ∈edges p'' , (push (tabulate (λ { n∈intp'' refl →  nⁱ∉intp'' n∈intp'' })) Unique-intp'' , (nodes-complete nⁱ) ∷ intp''⊆nodes))
-    ...       | yes nⁱ∈intp''
-                with splitFromInteriorʳ p'' nⁱ∈intp''
-    ...           | (done , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = ⊥-elim (¬IsDone=p''ʳ isDone)
-    ...           | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) =
-                    -- no rewrites because then I can't reason about the return value of toSimpleWalk
-                    -- rewrite intp''≡ns++intp''ʳ
-                    -- rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ)) =
-                    let reassoc-intp''≡ns++intp''ʳ = subst (interior p'' ≡_) (sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ))) intp''≡ns++intp''ʳ
-                        intp''ʳ⊆nodes = ++ˡ⁻ʳ (ns ++ˡ nⁱ ∷ []) (subst (All (_∈ˡ (proj₁ nodes))) reassoc-intp''≡ns++intp''ʳ intp''⊆nodes)
-                        Unique-ns++intp''ʳ = subst Unique reassoc-intp''≡ns++intp''ʳ Unique-intp''
-                        nⁱ∈p''ˡ = ∈ˡ-++⁺ʳ ns {ys = nⁱ ∷ []} (here refl)
-                    in (step n₁,nⁱ∈edges p''ʳ , (Unique-narrow (ns ++ˡ nⁱ ∷ []) Unique-ns++intp''ʳ nⁱ∈p''ˡ , nodes-complete nⁱ ∷ intp''ʳ⊆nodes ))
-
-    toSimpleWalk-IsDone⁻ : ∀ {n₁ n₂} (p : Path n₁ n₂) →
-                          ¬ IsDone p → ¬ IsDone (proj₁ (toSimpleWalk p))
-    toSimpleWalk-IsDone⁻ done ¬IsDone-p _ = ¬IsDone-p isDone
-    toSimpleWalk-IsDone⁻ (step {n₂ = nⁱ} n₁,nⁱ∈edges p') _ isDone-w
-        with toSimpleWalk p'
-    ...   | (done , _) with () ← isDone-w
-    ...   | (p''@(step _ _) , (Unique-intp'' , intp''⊆nodes))
-            with nⁱ ∈ˡ? interior p''
-    ...       | no nⁱ∉intp'' with () ← isDone-w
-    ...       | yes nⁱ∈intp''
-                with splitFromInteriorʳ p'' nⁱ∈intp''
-    ...           | (done , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = ¬IsDone=p''ʳ isDone
-    ...           | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ)))
-                    with () ← isDone-w
-
     Adjacency : Set
     Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)
 
@@ -328,54 +272,11 @@ record Graph : Set where
     adj : Adjacency
     adj = throughAll (proj₁ nodes)
 
-    PathExists : Node → Node → Set
-    PathExists n₁ n₂ = Path n₁ n₂
-
-    PathExists? : Decidable² PathExists
-    PathExists? n₁ n₂
-        with allSimplePathsNoted ← paths-throughAll {n₁ = n₁} {n₂ = n₂} (proj₁ nodes)
-        with adj n₁ n₂
-    ...   | [] = no (λ p →  let w = toSimpleWalk p in ¬Any[] (allSimplePathsNoted w))
-    ...   | (p ∷ ps) = yes p
-
     NoCycles : Set
-    NoCycles = ∀ {n} (p : Path n n) →  IsDone p
+    NoCycles = ∀ (n : Node) →  All IsDone (adj n n)
-
-    NoCycles? : Dec NoCycles
-    NoCycles? with any? (λ n → any? (Decidable-¬ IsDone?) (adj n n)) (proj₁ nodes)
-    ... | yes existsCycle =
-          no (λ ∀p,IsDonep →  let (n , n,n-cycle) = satisfied existsCycle in
-                              let (p , ¬IsDone-p) = satisfied n,n-cycle in
-                              ¬IsDone-p (∀p,IsDonep p))
-    ... | no noCycles =
-          yes (λ { done →  isDone
-                 ; p@(step {n₁ = n} _ _) →
-                    let w = toSimpleWalk p in
-                    let ¬IsDone-w = toSimpleWalk-IsDone⁻ p (λ {()}) in
-                    let w∈adj = paths-throughAll (proj₁ nodes) w in
-                    ⊥-elim (noCycles (lose (nodes-complete n) (lose w∈adj ¬IsDone-w)))
-                 })
 
     NoCycles⇒adj-complete : NoCycles → ∀ {n₁ n₂} {p : Path n₁ n₂} →  p ∈ˡ adj n₁ n₂
     NoCycles⇒adj-complete noCycles {n₁} {n₂} {p}
         with findCycle p
     ...   | inj₁ (w , w≡p) rewrite sym w≡p = paths-throughAll (proj₁ nodes) w
-    ...   | inj₂ (nᶜ , (wᶜ , wᶜ≢done)) = ⊥-elim (wᶜ≢done (noCycles (proj₁ wᶜ)))
+    ...   | inj₂ (nᶜ , (wᶜ , wᶜ≢done)) = ⊥-elim (wᶜ≢done (lookup (noCycles nᶜ) (paths-throughAll (proj₁ nodes) wᶜ)))
-
-    Is-⊤ : Node → Set
-    Is-⊤ n = All (PathExists n) (proj₁ nodes)
-
-    Is-⊥ : Node → Set
-    Is-⊥ n = All (λ n' → PathExists n' n) (proj₁ nodes)
-
-    Has-⊤ : Set
-    Has-⊤ = Any Is-⊤ (proj₁ nodes)
-
-    Has-T? : Dec Has-⊤
-    Has-T? = findUniversal (proj₁ nodes) PathExists?
-
-    Has-⊥ : Set
-    Has-⊥ = Any Is-⊥ (proj₁ nodes)
-
-    Has-⊥? : Dec Has-⊥
-    Has-⊥? = findUniversal (proj₁ nodes) (λ n₁ n₂ → PathExists? n₂ n₁)

Utils.agda

@@ -6,26 +6,17 @@ 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 (_∈_; lose)
+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; all?; lookup)
+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.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.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 using (Antisymmetric) renaming (Decidable to Decidable²)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
-open import Relation.Nullary using (¬_; yes; no; Dec)
+open import Relation.Nullary using (¬_; yes; no)
-open import Relation.Nullary.Decidable using (¬?)
 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
-
-Decidable-¬ : ∀ {p c} {C : Set c} {P : C → Set p} → Decidable P → Decidable (λ x → ¬ P x)
-Decidable-¬ Decidable-P x = ¬? (Decidable-P x)
-
 data Unique {c} {C : Set c} : List C → Set c where
     empty : Unique []
     push : ∀ {x : C} {xs : List C}
@@ -54,16 +45,6 @@ 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)
@@ -76,6 +57,10 @@ 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₁)
 
@@ -156,13 +141,3 @@ 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)