From 84c4ea693646fb952b3a888db8240e55e57d398f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 29 Nov 2025 22:46:49 -0800 Subject: [PATCH] Prove final postulate about cycles in graphs Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 0e8c596..8175a39 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -12,7 +12,7 @@ open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to 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) -open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith) +open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate) 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) @@ -21,6 +21,7 @@ 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.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) +open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) record Graph : Set where @@ -151,7 +152,40 @@ record Graph : Set where SplitSimpleWalkVia (step n₁,n₂∈edges done , (_ , _)) = inj₂ ((step n₁,n₂∈edges done , (empty , [])) , refl) SplitSimpleWalkVia w@(step {n₂ = nⁱ} n₁,nⁱ∈edges p@(step _ _) , (push nⁱ≢intp Unique-intp , nⁱ∈ns ∷ intp⊆ns)) = SplitSimpleWalkViaHelp nⁱ w (step n₁,nⁱ∈edges done) p (λ {()}) (λ {()}) [] refl - postulate findCycle : ∀ {n₁ n₂} (p : Path n₁ n₂) → (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w → ¬ proj₁ w ≡ done)) + open import Data.List.Membership.DecSetoid (decSetoid {A = Node} _≟_) using () renaming (_∈?_ to _∈ˡ?_) + + splitFromInterior : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) → + Σ (Path n n₂) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ ns ++ˡ interior p')) + splitFromInterior done () + splitFromInterior (step _ done) () + 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') + with (p'' , (¬IsDone-p'' , (ns , intp'≡ns++intp''))) ← splitFromInterior p' n∈intp' + rewrite intp'≡ns++intp'' = (p'' , (¬IsDone-p'' , (n' ∷ ns , refl))) + + + findCycleHelp : ∀ {n₁ nⁱ n₂} (p : Path n₁ n₂) (p₁ : Path n₁ nⁱ) (p₂ : Path nⁱ n₂) → + ¬ IsDone p₁ → Unique (interior p₁) → + p ≡ p₁ ++ p₂ → + (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w → ¬ IsDone (proj₁ w))) + findCycleHelp p p₁ done ¬IsDonep₁ Unique-intp₁ p≡p₁++done rewrite ++-done p₁ = inj₁ ((p₁ , (Unique-intp₁ , tabulate (λ {x} _ → nodes-complete x))) , sym p≡p₁++done) + findCycleHelp {nⁱ = nⁱ} p p₁ (step nⁱ,nⁱ'∈edges p₂') ¬IsDone-p₁ Unique-intp₁ p≡p₁++p₂ + with nⁱ ∈ˡ? interior p₁ + ... | no nⁱ∉intp₁ = + let p₁' = p₁ ++ step nⁱ,nⁱ'∈edges done + 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₂')) + in findCycleHelp p p₁' p₂' ¬IsDone-p₁' (subst Unique (sym intp₁'≡intp₁++[nⁱ]) (Unique-append nⁱ∉intp₁ Unique-intp₁)) p≡p₁'++p₂' + ... | yes nⁱ∈intp₁ + with (pᶜ , (¬IsDone-pᶜ , (ns , intp₁≡ns++intpᶜ))) ← splitFromInterior p₁ nⁱ∈intp₁ = + let Unique-intp₁' = subst Unique intp₁≡ns++intpᶜ Unique-intp₁ + 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 Adjacency : Set Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂) @@ -239,7 +273,7 @@ record Graph : Set where adj = throughAll (proj₁ nodes) NoCycles : Set - NoCycles = ∀ (n : Node) → All (_≡ done) (adj n n) + NoCycles = ∀ (n : Node) → All IsDone (adj n n) NoCycles⇒adj-complete : NoCycles → ∀ {n₁ n₂} {p : Path n₁ n₂} → p ∈ˡ adj n₁ n₂ NoCycles⇒adj-complete noCycles {n₁} {n₂} {p}