diff --git a/CHANGELOG.md b/CHANGELOG.md index 03df3230cc..3faace976d 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,7 +353,10 @@ Additions to existing modules * In `Data.DifferenceList.Properties`: ```agda - viaList⁺ : (f : List A → List B) → xs ∼ ys → f xs ∼ viaList f ys + 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 ``` * In `Data.Integer.GCD`: diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda index feb41df044..f49d8aec21 100644 --- a/src/Data/DifferenceList/Properties.agda +++ b/src/Data/DifferenceList/Properties.agda @@ -10,9 +10,10 @@ 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 Data.Product.Base using (Σ; _,_) +open import Function.Base using (_∘′_; id; flip) open import Level using (Level) open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; _≗_; module ≡-Reasoning) @@ -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,18 +48,30 @@ 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 - xs ≡⟨ ++-identityʳ xs ⟨ - xs List.++ List.[] ≡⟨ xs∼ys List.[] ⟩ - ys List.[] ≡⟨⟩ - toList 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 ∎ +toList⁺ : xs ∼ dxs → xs ≡ toList dxs +toList⁺ {xs = xs} {dxs} xs∼dxs = begin + xs ≡⟨ toList∘fromList xs ⟨ + toList (fromList xs) ≡⟨ xs∼dxs List.[] ⟩ + toList dxs ∎ + +fromList-++ : (xs ys : List A) → + 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 = 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) ⟩ + 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 xs∼dxs k = begin + fromList (f xs) k ≡⟨ cong (flip fromList _ ∘′ f) (toList⁺ xs∼dxs) ⟩ + fromList (f (toList dxs)) k ≡⟨⟩ + viaList f dxs k ∎ ------------------------------------------------------------------------ -- Properties of operations that preserve _∼_ @@ -66,24 +82,20 @@ 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} xs∼dxs ys∼dys k = begin + 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) ⟩ + 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 ]⁺ -∷ʳ⁺ : (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 xs∼dxs = ++⁺ xs∼dxs [ x ]⁺ -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.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..288dda859f --- /dev/null +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties/ToList.agda @@ -0,0 +1,88 @@ +------------------------------------------------------------------------ +-- 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 (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.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 p : Level + V : Value v + 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