Adds the AVL tree's toList/Any properties

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`:

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,16 +25,19 @@ 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
 
 
 ------------------------------------------------------------------------
 -- Relation between Lists and equivalent DiffLists
 
 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⁺ _

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

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<u) = List.[] , []⁺
+listLike (node k l r bal)
+  with (ls , ls∼dls) ← listLike l
+  with (rs , rs∼drs) ← listLike r
+  = ls List.++ k List.∷ rs , (++⁺ ls∼dls (∷⁺ k rs∼drs))
+
+++≡node : (kv : K& V) →
+          (lk : Tree V l [ kv .key ] hˡ) →
+          (ku : Tree V [ kv .key ] u hʳ) →
+          (bal : hˡ ∼ hʳ ⊔ h) →
+          toList lk List.++ kv List.∷ toList ku ≡
+            toList (node kv lk ku bal)
+++≡node kv lk ku _ =
+  toList-++ (listLike lk) (kv ∷ toDiffList ku)
+
+toList⁺ : Any P t → List.Any P (toList t)
+toList⁺-node : {kv : K& V} →
+               {lk : Tree V l [ kv .key ] hˡ} →
+               {ku : Tree V [ kv .key ] u hʳ} →
+               {bal : hˡ ∼ hʳ ⊔ h} →
+               Any P (node kv lk ku bal) →
+               List.Any P (toList lk List.++ kv List.∷ toList ku)
+toList⁺ {P = P} {t = node kv lk ku bal} p =
+  subst (List.Any P) (++≡node kv lk ku bal) (toList⁺-node p)
+toList⁺-node {lk = lk} (here p) =
+  List.++⁺ʳ (toList lk) (List.here p)
+toList⁺-node (left p) =
+  List.++⁺ˡ (toList⁺ p)
+toList⁺-node {lk = lk} (right p) =
+  List.++⁺ʳ (toList lk) (List.there (toList⁺ p))
+
+toList⁻ : List.Any P (toList t) → Any P t
+toList⁻-node : {kv : K& V} →
+               {lk : Tree V l [ kv .key ] hˡ} →
+               {ku : Tree V [ kv .key ] u hʳ} →
+               {bal : hˡ ∼ hʳ ⊔ h} →
+               List.Any P (toList lk) ⊎ List.Any P (kv List.∷ toList ku) →
+               Any P (node kv lk ku bal)
+toList⁻ {P = P} {t = node kv lk ku bal} p =
+  toList⁻-node
+    (List.++⁻ (toList lk)
+      (subst (List.Any P) (sym (++≡node kv lk ku bal)) p))
+toList⁻-node (inj₁ p) = left (toList⁻ p)
+toList⁻-node (inj₂ (List.here p)) = here p
+toList⁻-node (inj₂ (List.there p)) = right (toList⁻ p)