From 262f453d154cec3f30faa8184b1930725796060c Mon Sep 17 00:00:00 2001 From: Michael deLorimier Date: Wed, 8 Jul 2026 12:37:22 -0700 Subject: [PATCH 1/9] Added AVL Indexed Any toList properties --- src/Data/DifferenceList/Properties.agda | 20 ++++- .../Relation/Unary/Any/Properties.agda | 1 + .../Relation/Unary/Any/Properties/ToList.agda | 74 +++++++++++++++++++ standard-library.agda-lib | 1 + 4 files changed, 92 insertions(+), 4 deletions(-) create mode 100644 src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index feb41df044..f774208b3a 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -10,12 +10,12 @@ module Data.DifferenceList.Properties where open import Data.DifferenceList.Base using (DiffList; fromList; toList; viaList; []; _∷_; [_]; _++_; _∷ʳ_; map) -open import Data.List as List using (List) +open import Data.List.Base as List using (List) open import Data.List.Properties using (++-assoc; ++-identityʳ) -open import Function using (_∘′_; id; flip) +open import Function.Base using (_∘′_; id; flip) open import Level using (Level) open import Relation.Binary.PropositionalEquality - using (_≡_; refl; cong; _≗_; module ≡-Reasoning) + using (_≡_; refl; subst; cong; _≗_; module ≡-Reasoning) open ≡-Reasoning @@ -51,6 +51,18 @@ toList⁺ {xs = xs} {ys} xs∼ys = begin ys List.[] ≡⟨⟩ toList ys ∎ +toList-refl : xs ∼ ys → toList ys ∼ ys +toList-refl {xs = xs} {ys} xs∼ys k = + subst (λ xs → fromList xs k ≡ ys k) (toList⁺ xs∼ys) (xs∼ys k) + +toList-++ : xs₁ ∼ ys₁ → (ys₂ : DiffList A) → + xs₁ List.++ toList ys₂ ≡ toList (ys₁ ++ ys₂) +toList-++ {xs₁ = xs₁} {ys₁} xs₁∼ys₁ ys₂ = begin + xs₁ List.++ toList ys₂ ≡⟨⟩ + fromList xs₁ (toList ys₂) ≡⟨ xs₁∼ys₁ (toList ys₂) ⟩ + ys₁ (toList ys₂) ≡⟨⟩ + toList (ys₁ ++ ys₂) ∎ + viaList⁺ : (f : List A → List B) → xs ∼ ys → f xs ∼ viaList f ys viaList⁺ {xs = xs} {ys = ys} f xs∼ys k = begin fromList (f xs) k ≡⟨ cong (flip fromList _ ∘′ f) (toList⁺ xs∼ys) ⟩ @@ -76,7 +88,7 @@ viaList⁺ {xs = xs} {ys = ys} f xs∼ys k = begin (ys₁ ++ ys₂) k ∎ ∷⁺ : (x : A) → xs ∼ ys → x List.∷ xs ∼ x ∷ ys -∷⁺ {xs = xs} {ys} x xs~ys k = cong (x List.∷_) (xs~ys k) +∷⁺ {xs = xs} {ys} x xs∼ys k = cong (x List.∷_) (xs∼ys k) ++-∷⁺ : (x : A) → xs₁ ∼ ys₁ → xs₂ ∼ ys₂ → xs₁ List.++ x List.∷ xs₂ ∼ ys₁ ++ x ∷ ys₂ diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda index 5ef674b2a8..6a4e8d2d3d 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda @@ -20,3 +20,4 @@ open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinLemmas sto p open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join sto public open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup sto public open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Singleton sto public +open import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.ToList sto public diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda new file mode 100644 index 0000000000..b2686e11e1 --- /dev/null +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda @@ -0,0 +1,74 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of toList related to Any +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary.Bundles using (StrictTotalOrder) + +module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.ToList + {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂) + where + +open import Data.DifferenceList.Base using (_∷_) +open import Data.DifferenceList.Properties + using (_∼_; []⁺; ++-∷⁺; toList-refl; toList-++) +import Data.List.Base as List +import Data.List.Relation.Unary.Any as List +import Data.List.Relation.Unary.Any.Properties as List +open import Data.Nat.Base using (ℕ) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Level using (Level) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; subst; sym) +open import Relation.Unary using (Pred) + +open import Data.Tree.AVL.Indexed sto +open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto + using (Any; here; left; right) + +private + variable + v : Level + V : Value v + p : Level + P : Pred (K& V) p + l u : Key⁺ + h : ℕ + t : Tree V l u h + + +toList∼toDiffList : (t : Tree V l u h) → + toList t ∼ toDiffList t +toList∼toDiffList (leaf l Date: Wed, 8 Jul 2026 12:54:12 -0700 Subject: [PATCH 2/9] updated CHANGELOG.md --- CHANGELOG.md | 6 ++++++ standard-library.agda-lib | 1 - 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 03df3230cc..815018a51e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -270,6 +270,9 @@ New modules Data.Tree.Rose.Show ``` +* `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.ToList` adds properties of + the AVL's operator `toList`: `toList⁺` and `toList⁻`. + Additions to existing modules ----------------------------- @@ -350,6 +353,9 @@ Additions to existing modules * In `Data.DifferenceList.Properties`: ```agda + toList-refl : xs ∼ ys → toList ys ∼ ys + toList-++ : xs₁ ∼ ys₁ → (ys₂ : DiffList A) → + xs₁ List.++ toList ys₂ ≡ toList (ys₁ ++ ys₂) viaList⁺ : (f : List A → List B) → xs ∼ ys → f xs ∼ viaList f ys ``` diff --git a/standard-library.agda-lib b/standard-library.agda-lib index b7b1d4ed6d..9888ce23b3 100644 --- a/standard-library.agda-lib +++ b/standard-library.agda-lib @@ -1,3 +1,2 @@ name: standard-library-3.0 include: src -flags: -WnoUnguardedEtaRecord -WnoUselessPatternDeclarationForRecord From 1e82f4c6e230500a6f5a3829e54c14bf78414507 Mon Sep 17 00:00:00 2001 From: Michael deLorimier Date: Thu, 9 Jul 2026 16:48:25 -0700 Subject: [PATCH 3/9] Added ListLike. Changed ToList to use ListLike. Changed variable names to not use substripts. --- CHANGELOG.md | 7 +- src/Data/DifferenceList/Properties.agda | 82 +++++++++---------- .../Relation/Unary/Any/Properties/ToList.agda | 21 +++-- 3 files changed, 54 insertions(+), 56 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 815018a51e..96e74a8e79 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -353,10 +353,9 @@ Additions to existing modules * In `Data.DifferenceList.Properties`: ```agda - toList-refl : xs ∼ ys → toList ys ∼ ys - toList-++ : xs₁ ∼ ys₁ → (ys₂ : DiffList A) → - xs₁ List.++ toList ys₂ ≡ toList (ys₁ ++ ys₂) - viaList⁺ : (f : List A → List B) → xs ∼ ys → f xs ∼ viaList f ys + toList-++ : ListLike dxs → (dys : DiffList A) → + toList dxs List.++ toList dys ≡ toList (dxs ++ dys) + viaList⁺ : (f : List A → List B) → xs ∼ dxs → f xs ∼ viaList f dxs ``` * In `Data.Integer.GCD`: diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index f774208b3a..ce7d4e84a9 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -12,6 +12,7 @@ open import Data.DifferenceList.Base using (DiffList; fromList; toList; viaList; []; _∷_; [_]; _++_; _∷ʳ_; map) open import Data.List.Base as List using (List) open import Data.List.Properties using (++-assoc; ++-identityʳ) +open import Data.Product using (Σ; _,_) open import Function.Base using (_∘′_; id; flip) open import Level using (Level) open import Relation.Binary.PropositionalEquality @@ -24,8 +25,8 @@ private a b : Level A : Set a B : Set b - xs xs₁ xs₂ : List A - ys ys₁ ys₂ : DiffList A + xs ys : List A + dxs dys : DiffList A ------------------------------------------------------------------------ @@ -33,7 +34,10 @@ private infix 4 _∼_ _∼_ : List A → DiffList A → Set _ -xs ∼ ys = fromList xs ≗ ys +xs ∼ dxs = fromList xs ≗ dxs + +ListLike : DiffList A → Set _ +ListLike {A = A} dxs = Σ (List A) (_∼ dxs) ------------------------------------------------------------------------ -- Properties of fromList and toList @@ -44,30 +48,27 @@ xs ∼ ys = fromList xs ≗ ys toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs toList∘fromList = ++-identityʳ -toList⁺ : xs ∼ ys → xs ≡ toList ys -toList⁺ {xs = xs} {ys} xs∼ys = begin +toList⁺ : xs ∼ dxs → xs ≡ toList dxs +toList⁺ {xs = xs} {dxs} x∼ = begin xs ≡⟨ ++-identityʳ xs ⟨ - xs List.++ List.[] ≡⟨ xs∼ys List.[] ⟩ - ys List.[] ≡⟨⟩ - toList ys ∎ - -toList-refl : xs ∼ ys → toList ys ∼ ys -toList-refl {xs = xs} {ys} xs∼ys k = - subst (λ xs → fromList xs k ≡ ys k) (toList⁺ xs∼ys) (xs∼ys k) - -toList-++ : xs₁ ∼ ys₁ → (ys₂ : DiffList A) → - xs₁ List.++ toList ys₂ ≡ toList (ys₁ ++ ys₂) -toList-++ {xs₁ = xs₁} {ys₁} xs₁∼ys₁ ys₂ = begin - xs₁ List.++ toList ys₂ ≡⟨⟩ - fromList xs₁ (toList ys₂) ≡⟨ xs₁∼ys₁ (toList ys₂) ⟩ - ys₁ (toList ys₂) ≡⟨⟩ - toList (ys₁ ++ ys₂) ∎ - -viaList⁺ : (f : List A → List B) → xs ∼ ys → f xs ∼ viaList f ys -viaList⁺ {xs = xs} {ys = ys} f xs∼ys k = begin - fromList (f xs) k ≡⟨ cong (flip fromList _ ∘′ f) (toList⁺ xs∼ys) ⟩ - fromList (f (toList ys)) k ≡⟨⟩ - viaList f ys k ∎ + xs List.++ List.[] ≡⟨ x∼ List.[] ⟩ + dxs List.[] ≡⟨⟩ + toList dxs ∎ + +toList-++ : ListLike dxs → (dys : DiffList A) → + toList dxs List.++ toList dys ≡ toList (dxs ++ dys) +toList-++ {dxs = dxs} (xs , x∼) dys = begin + toList dxs List.++ toList dys ≡⟨ cong (List._++ toList dys) (toList⁺ x∼) ⟨ + xs List.++ toList dys ≡⟨⟩ + fromList xs (toList dys) ≡⟨ x∼ (toList dys) ⟩ + dxs (toList dys) ≡⟨⟩ + toList (dxs ++ dys) ∎ + +viaList⁺ : (f : List A → List B) → xs ∼ dxs → f xs ∼ viaList f dxs +viaList⁺ {xs = xs} {dxs = dxs} f x∼ k = begin + fromList (f xs) k ≡⟨ cong (flip fromList _ ∘′ f) (toList⁺ x∼) ⟩ + fromList (f (toList dxs)) k ≡⟨⟩ + viaList f dxs k ∎ ------------------------------------------------------------------------ -- Properties of operations that preserve _∼_ @@ -78,24 +79,19 @@ viaList⁺ {xs = xs} {ys = ys} f xs∼ys k = begin [_]⁺ : (x : A) → List.[ x ] ∼ [ x ] [_]⁺ _ _ = refl -++⁺ : xs₁ ∼ ys₁ → xs₂ ∼ ys₂ → xs₁ List.++ xs₂ ∼ ys₁ ++ ys₂ -++⁺ {xs₁ = xs₁} {ys₁ = ys₁} {xs₂ = xs₂} {ys₂ = ys₂} - xs₁∼ys₁ xs₂∼ys₂ k = begin - (xs₁ List.++ xs₂) List.++ k ≡⟨ ++-assoc xs₁ xs₂ k ⟩ - xs₁ List.++ (xs₂ List.++ k) ≡⟨ cong (xs₁ List.++_) (xs₂∼ys₂ k) ⟩ - xs₁ List.++ ys₂ k ≡⟨ xs₁∼ys₁ (ys₂ k) ⟩ - ys₁ (ys₂ k) ≡⟨⟩ - (ys₁ ++ ys₂) k ∎ - -∷⁺ : (x : A) → xs ∼ ys → x List.∷ xs ∼ x ∷ ys -∷⁺ {xs = xs} {ys} x xs∼ys k = cong (x List.∷_) (xs∼ys k) +++⁺ : xs ∼ dxs → ys ∼ dys → xs List.++ ys ∼ dxs ++ dys +++⁺ {xs = xs} {dxs = dxs} {ys = ys} {dys = dys} x∼ y∼ k = begin + (xs List.++ ys) List.++ k ≡⟨ ++-assoc xs ys k ⟩ + xs List.++ (ys List.++ k) ≡⟨ cong (xs List.++_) (y∼ k) ⟩ + xs List.++ dys k ≡⟨ x∼ (dys k) ⟩ + dxs (dys k) ≡⟨⟩ + (dxs ++ dys) k ∎ -++-∷⁺ : (x : A) → xs₁ ∼ ys₁ → xs₂ ∼ ys₂ → - xs₁ List.++ x List.∷ xs₂ ∼ ys₁ ++ x ∷ ys₂ -++-∷⁺ x xs₁∼ys₁ xs₂∼ys₂ = ++⁺ xs₁∼ys₁ (∷⁺ x xs₂∼ys₂) +∷⁺ : (x : A) → xs ∼ dxs → x List.∷ xs ∼ x ∷ dxs +∷⁺ x x∼ k = cong (x List.∷_) (x∼ k) -∷ʳ⁺ : (x : A) → xs ∼ ys → xs List.∷ʳ x ∼ ys ∷ʳ x -∷ʳ⁺ {xs = xs} {ys} x xs∼ys k = ++⁺ xs∼ys [ x ]⁺ k +∷ʳ⁺ : (x : A) → xs ∼ dxs → xs List.∷ʳ x ∼ dxs ∷ʳ x +∷ʳ⁺ x x∼ k = ++⁺ x∼ [ x ]⁺ k -map⁺ : (f : A → B) → xs ∼ ys → List.map f xs ∼ map f ys +map⁺ : (f : A → B) → xs ∼ dxs → List.map f xs ∼ map f dxs map⁺ f = viaList⁺ _ diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda index b2686e11e1..bb6fabfa2d 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda @@ -12,13 +12,15 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.ToList {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂) where +open import Data.DifferenceList.Properties using () open import Data.DifferenceList.Base using (_∷_) open import Data.DifferenceList.Properties - using (_∼_; []⁺; ++-∷⁺; toList-refl; toList-++) + using (ListLike; []⁺; ∷⁺; ++⁺; toList-++) import Data.List.Base as List import Data.List.Relation.Unary.Any as List import Data.List.Relation.Unary.Any.Properties as List open import Data.Nat.Base using (ℕ) +open import Data.Product using (_,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core @@ -39,12 +41,13 @@ private h : ℕ t : Tree V l u h - -toList∼toDiffList : (t : Tree V l u h) → - toList t ∼ toDiffList t -toList∼toDiffList (leaf l Date: Fri, 10 Jul 2026 14:18:05 -0700 Subject: [PATCH 4/9] Addressed review comments. --- CHANGELOG.md | 5 +- src/Data/DifferenceList/Properties.agda | 46 ++++++------ .../Relation/Unary/Any/Properties/ToList.agda | 70 +++++++++++-------- 3 files changed, 69 insertions(+), 52 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 96e74a8e79..1f41dc4b71 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -353,8 +353,9 @@ Additions to existing modules * In `Data.DifferenceList.Properties`: ```agda - toList-++ : ListLike dxs → (dys : DiffList A) → - toList dxs List.++ toList dys ≡ toList (dxs ++ dys) + fromList-++-homo : ∀ xs ys → fromList (xs List.++ ys) ≗ fromList xs ++ fromList ys + toList-++-homo : ListLike dxs → (dys : DiffList A) → + toList dxs List.++ toList dys ≡ toList (dxs ++ dys) viaList⁺ : (f : List A → List B) → xs ∼ dxs → f xs ∼ viaList f dxs ``` diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index ce7d4e84a9..fbf127ef2d 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -49,24 +49,27 @@ toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs toList∘fromList = ++-identityʳ toList⁺ : xs ∼ dxs → xs ≡ toList dxs -toList⁺ {xs = xs} {dxs} x∼ = begin - xs ≡⟨ ++-identityʳ xs ⟨ - xs List.++ List.[] ≡⟨ x∼ List.[] ⟩ - dxs List.[] ≡⟨⟩ - toList dxs ∎ - -toList-++ : ListLike dxs → (dys : DiffList A) → - toList dxs List.++ toList dys ≡ toList (dxs ++ dys) -toList-++ {dxs = dxs} (xs , x∼) dys = begin - toList dxs List.++ toList dys ≡⟨ cong (List._++ toList dys) (toList⁺ x∼) ⟨ +toList⁺ {xs = xs} {dxs} xs∼dxs = begin + xs ≡⟨ toList∘fromList xs ⟨ + toList (fromList xs) ≡⟨ xs∼dxs List.[] ⟩ + toList dxs ∎ + +fromList-++-homo : (xs ys : List A) → + fromList (xs List.++ ys) ≗ fromList xs ++ fromList ys +fromList-++-homo = ++-assoc + +toList-++-homo : ListLike dxs → (dys : DiffList A) → + toList dxs List.++ toList dys ≡ toList (dxs ++ dys) +toList-++-homo {dxs = dxs} (xs , xs∼dxs) dys = begin + toList dxs List.++ toList dys ≡⟨ cong (List._++ toList dys) (toList⁺ xs∼dxs) ⟨ xs List.++ toList dys ≡⟨⟩ - fromList xs (toList dys) ≡⟨ x∼ (toList dys) ⟩ + fromList xs (toList dys) ≡⟨ xs∼dxs (toList dys) ⟩ dxs (toList dys) ≡⟨⟩ toList (dxs ++ dys) ∎ viaList⁺ : (f : List A → List B) → xs ∼ dxs → f xs ∼ viaList f dxs -viaList⁺ {xs = xs} {dxs = dxs} f x∼ k = begin - fromList (f xs) k ≡⟨ cong (flip fromList _ ∘′ f) (toList⁺ x∼) ⟩ +viaList⁺ {xs = xs} {dxs = dxs} f xs∼dxs k = begin + fromList (f xs) k ≡⟨ cong (flip fromList _ ∘′ f) (toList⁺ xs∼dxs) ⟩ fromList (f (toList dxs)) k ≡⟨⟩ viaList f dxs k ∎ @@ -80,18 +83,19 @@ viaList⁺ {xs = xs} {dxs = dxs} f x∼ k = begin [_]⁺ _ _ = refl ++⁺ : xs ∼ dxs → ys ∼ dys → xs List.++ ys ∼ dxs ++ dys -++⁺ {xs = xs} {dxs = dxs} {ys = ys} {dys = dys} x∼ y∼ k = begin - (xs List.++ ys) List.++ k ≡⟨ ++-assoc xs ys k ⟩ - xs List.++ (ys List.++ k) ≡⟨ cong (xs List.++_) (y∼ k) ⟩ - xs List.++ dys k ≡⟨ x∼ (dys k) ⟩ - dxs (dys k) ≡⟨⟩ - (dxs ++ dys) k ∎ +++⁺ {xs = xs} {dxs = dxs} {ys = ys} {dys = dys} xs∼dxs ys∼dys k = begin + fromList (xs List.++ ys) k ≡⟨ fromList-++-homo xs ys k ⟩ + (fromList xs ++ fromList ys) k ≡⟨⟩ + fromList xs (fromList ys k) ≡⟨ cong (fromList xs) (ys∼dys k) ⟩ + fromList xs (dys k) ≡⟨ xs∼dxs (dys k) ⟩ + dxs (dys k) ≡⟨⟩ + (dxs ++ dys) k ∎ ∷⁺ : (x : A) → xs ∼ dxs → x List.∷ xs ∼ x ∷ dxs -∷⁺ x x∼ k = cong (x List.∷_) (x∼ k) +∷⁺ x xs∼dxs k = cong (x List.∷_) (xs∼dxs k) ∷ʳ⁺ : (x : A) → xs ∼ dxs → xs List.∷ʳ x ∼ dxs ∷ʳ x -∷ʳ⁺ x x∼ k = ++⁺ x∼ [ x ]⁺ k +∷ʳ⁺ x xs∼dxs = ++⁺ xs∼dxs [ x ]⁺ map⁺ : (f : A → B) → xs ∼ dxs → List.map f xs ∼ map f dxs map⁺ f = viaList⁺ _ diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda index bb6fabfa2d..22a91d56bf 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda @@ -12,10 +12,9 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.ToList {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂) where -open import Data.DifferenceList.Properties using () open import Data.DifferenceList.Base using (_∷_) open import Data.DifferenceList.Properties - using (ListLike; []⁺; ∷⁺; ++⁺; toList-++) + using (ListLike; []⁺; ∷⁺; ++⁺; toList-++-homo) import Data.List.Base as List import Data.List.Relation.Unary.Any as List import Data.List.Relation.Unary.Any.Properties as List @@ -38,40 +37,53 @@ private p : Level P : Pred (K& V) p l u : Key⁺ - h : ℕ + hˡ hʳ h : ℕ t : Tree V l u h listLike : (t : Tree V l u h) → ListLike (toDiffList t) listLike (leaf l Date: Fri, 10 Jul 2026 14:25:17 -0700 Subject: [PATCH 5/9] refined imports --- src/Data/DifferenceList/Properties.agda | 2 +- .../AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index fbf127ef2d..ca57bdaebe 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -12,7 +12,7 @@ open import Data.DifferenceList.Base using (DiffList; fromList; toList; viaList; []; _∷_; [_]; _++_; _∷ʳ_; map) open import Data.List.Base as List using (List) open import Data.List.Properties using (++-assoc; ++-identityʳ) -open import Data.Product using (Σ; _,_) +open import Data.Product.Base using (Σ; _,_) open import Function.Base using (_∘′_; id; flip) open import Level using (Level) open import Relation.Binary.PropositionalEquality diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda index 22a91d56bf..39f4539999 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda @@ -19,7 +19,7 @@ import Data.List.Base as List import Data.List.Relation.Unary.Any as List import Data.List.Relation.Unary.Any.Properties as List open import Data.Nat.Base using (ℕ) -open import Data.Product using (_,_) +open import Data.Product.Base using (_,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core @@ -32,14 +32,14 @@ open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto private variable - v : Level + v p : Level V : Value v - p : Level P : Pred (K& V) p l u : Key⁺ hˡ hʳ h : ℕ t : Tree V l u h + listLike : (t : Tree V l u h) → ListLike (toDiffList t) listLike (leaf l Date: Fri, 10 Jul 2026 14:28:57 -0700 Subject: [PATCH 6/9] Addressed a review comment. --- src/Data/DifferenceList/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index ca57bdaebe..5e9d86c3ec 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -92,7 +92,7 @@ viaList⁺ {xs = xs} {dxs = dxs} f xs∼dxs k = begin (dxs ++ dys) k ∎ ∷⁺ : (x : A) → xs ∼ dxs → x List.∷ xs ∼ x ∷ dxs -∷⁺ x xs∼dxs k = cong (x List.∷_) (xs∼dxs k) +∷⁺ x = ++⁺ [ x ]⁺ ∷ʳ⁺ : (x : A) → xs ∼ dxs → xs List.∷ʳ x ∼ dxs ∷ʳ x ∷ʳ⁺ x xs∼dxs = ++⁺ xs∼dxs [ x ]⁺ From 37f5035799659ca7479f15c00c9cc175bf23103f Mon Sep 17 00:00:00 2001 From: Michael deLorimier Date: Tue, 14 Jul 2026 16:07:30 -0700 Subject: [PATCH 7/9] Addressed review comments --- src/Data/DifferenceList/Properties.agda | 10 +++++----- .../Relation/Unary/Any/Properties/ToList.agda | 13 ++++++------- 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index 5e9d86c3ec..8f71d9dd64 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -54,13 +54,13 @@ toList⁺ {xs = xs} {dxs} xs∼dxs = begin toList (fromList xs) ≡⟨ xs∼dxs List.[] ⟩ toList dxs ∎ -fromList-++-homo : (xs ys : List A) → +fromList-++ : (xs ys : List A) → fromList (xs List.++ ys) ≗ fromList xs ++ fromList ys -fromList-++-homo = ++-assoc +fromList-++ = ++-assoc -toList-++-homo : ListLike dxs → (dys : DiffList A) → +toList-++ : ListLike dxs → (dys : DiffList A) → toList dxs List.++ toList dys ≡ toList (dxs ++ dys) -toList-++-homo {dxs = dxs} (xs , xs∼dxs) dys = begin +toList-++ {dxs = dxs} (xs , xs∼dxs) dys = begin toList dxs List.++ toList dys ≡⟨ cong (List._++ toList dys) (toList⁺ xs∼dxs) ⟨ xs List.++ toList dys ≡⟨⟩ fromList xs (toList dys) ≡⟨ xs∼dxs (toList dys) ⟩ @@ -84,7 +84,7 @@ viaList⁺ {xs = xs} {dxs = dxs} f xs∼dxs k = begin ++⁺ : xs ∼ dxs → ys ∼ dys → xs List.++ ys ∼ dxs ++ dys ++⁺ {xs = xs} {dxs = dxs} {ys = ys} {dys = dys} xs∼dxs ys∼dys k = begin - fromList (xs List.++ ys) k ≡⟨ fromList-++-homo xs ys k ⟩ + fromList (xs List.++ ys) k ≡⟨ fromList-++ xs ys k ⟩ (fromList xs ++ fromList ys) k ≡⟨⟩ fromList xs (fromList ys k) ≡⟨ cong (fromList xs) (ys∼dys k) ⟩ fromList xs (dys k) ≡⟨ xs∼dxs (dys k) ⟩ diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda index 39f4539999..288dda859f 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda @@ -14,7 +14,7 @@ module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.ToList open import Data.DifferenceList.Base using (_∷_) open import Data.DifferenceList.Properties - using (ListLike; []⁺; ∷⁺; ++⁺; toList-++-homo) + using (ListLike; []⁺; ∷⁺; ++⁺; toList-++) import Data.List.Base as List import Data.List.Relation.Unary.Any as List import Data.List.Relation.Unary.Any.Properties as List @@ -42,11 +42,10 @@ private listLike : (t : Tree V l u h) → ListLike (toDiffList t) listLike (leaf l Date: Tue, 14 Jul 2026 16:12:03 -0700 Subject: [PATCH 8/9] Fixed CHANGELOG.md with most recent changes --- CHANGELOG.md | 6 +++--- src/Data/DifferenceList/Properties.agda | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1f41dc4b71..3faace976d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -353,9 +353,9 @@ Additions to existing modules * In `Data.DifferenceList.Properties`: ```agda - fromList-++-homo : ∀ xs ys → fromList (xs List.++ ys) ≗ fromList xs ++ fromList ys - toList-++-homo : ListLike dxs → (dys : DiffList A) → - toList dxs List.++ toList dys ≡ toList (dxs ++ dys) + fromList-++ : ∀ xs ys → fromList (xs List.++ ys) ≗ fromList xs ++ fromList ys + toList-++ : ListLike dxs → (dys : DiffList A) → + toList dxs List.++ toList dys ≡ toList (dxs ++ dys) viaList⁺ : (f : List A → List B) → xs ∼ dxs → f xs ∼ viaList f dxs ``` diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index 8f71d9dd64..058e3a5be7 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -55,11 +55,11 @@ toList⁺ {xs = xs} {dxs} xs∼dxs = begin toList dxs ∎ fromList-++ : (xs ys : List A) → - fromList (xs List.++ ys) ≗ fromList xs ++ fromList ys + fromList (xs List.++ ys) ≗ fromList xs ++ fromList ys fromList-++ = ++-assoc toList-++ : ListLike dxs → (dys : DiffList A) → - toList dxs List.++ toList dys ≡ toList (dxs ++ dys) + toList dxs List.++ toList dys ≡ toList (dxs ++ dys) toList-++ {dxs = dxs} (xs , xs∼dxs) dys = begin toList dxs List.++ toList dys ≡⟨ cong (List._++ toList dys) (toList⁺ xs∼dxs) ⟨ xs List.++ toList dys ≡⟨⟩ From 2eeaa21673eeef27135a3daf37c3a05d41339eff Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 15 Jul 2026 14:11:00 +0100 Subject: [PATCH 9/9] [ cleanup ] remove useless import --- src/Data/DifferenceList/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index 058e3a5be7..f49d8aec21 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -16,7 +16,7 @@ open import Data.Product.Base using (Σ; _,_) open import Function.Base using (_∘′_; id; flip) open import Level using (Level) open import Relation.Binary.PropositionalEquality - using (_≡_; refl; subst; cong; _≗_; module ≡-Reasoning) + using (_≡_; refl; cong; _≗_; module ≡-Reasoning) open ≡-Reasoning