[ new ] Basic unary predicates for Data.Tree.AVL (#1385)

Author: gallais

.travis.yml

@@ -48,7 +48,7 @@ matrix:
              cd ../ &&
              git clone https://github.com/agda/agda &&
              cd agda &&
-             git checkout tags/v2.6.1.1 &&
+             git checkout tags/v2.6.1.3 &&
              cabal install --only-dependencies --dry -v > $HOME/installplan.txt ;
           fi
 

CHANGELOG.md

@@ -1,7 +1,7 @@
 Version 1.6-dev
 ===============
 
-The library has been tested using Agda 2.6.1 and 2.6.1.1.
+The library has been tested using Agda 2.6.1 and 2.6.1.3.
 
 Highlights
 ----------
@@ -15,23 +15,23 @@ Highlights
 Bug-fixes
 ---------
 
-* Despite being designed for use with non-reflexive relations, the combinators 
+* Despite being designed for use with non-reflexive relations, the combinators
   in `Relation.Binary.Reasoning.Base.Partial` required users to provide a proof
   of reflexivity of the relation over the last element in the chain:
   ```agda
-  begin 
+  begin
     x  ⟨ x∼y ⟩
     y  ∎⟨ y∼y ⟩
   ```
   These have now been redefined so that this proof is no longer needed:
   ```agda
-  begin 
+  begin
     x  ⟨ x∼y ⟩
     y  ∎
   ```
-  For direct users of `Relation.Binary.Reasoning.PartialSetoid` API this is a 
+  For direct users of `Relation.Binary.Reasoning.PartialSetoid` API this is a
   backwards compatible change as the `_∎⟨_⟩` combinator has simply been deprecated. For
-  users who were building their own reasoning combinators on top of 
+  users who were building their own reasoning combinators on top of
   `Relation.Binary.Reasoning.Base.Partial`, they will need to adjust their additional
   combinators to use the new `singleStep`/`multiStep` constructors of `_IsRelatedTo_`.
 
@@ -48,6 +48,9 @@ Bug-fixes
   Their definitions have now been moved out of the anonymous modules so that they no
   longer require these unnecessary arguments.
 
+* In `Relation.Binary.Reasoning.StrictPartialOrder` filled a missing argument to the
+  re-exported `Relation.Binary.Reasoning.Base.Triple`.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -67,6 +70,12 @@ Non-backwards compatible changes
   only a breaking change if you were supplying the module arguments upon import, in which
   case you will have to change to supplying them upon application of the proofs.
 
+* In `Data.Tree.AVL.Indexed` the type alias `K&_` defined in terms of `Σ` has been changed
+  into a standalone record to help with parameter inference. The record constructor remains
+  the same so you will only observe the change if you are using functions explicitly expecting
+  a pair (e.g. `(un)curry`). In this case you can use `Data.Tree.AVL.Value`'s `(to/from)Pair`
+  to convert back and forth.
+
 Deprecated modules
 ------------------
 
@@ -221,6 +230,18 @@ New modules
   Data.Tree.Binary.Show
   ```
 
+* Added new modules in `Data.Tree.AVL`:
+  ```
+  Data.Tree.AVL.Indexed.Relation.Unary.All
+
+  Data.Tree.AVL.Relation.Unary.Any
+
+  Data.Tree.AVL.Indexed.Relation.Unary.Any
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties
+
+  Data.Tree.AVL.Map.Relation.Unary.Any
+  ```
+
 * Bundles for binary relation morphisms
   ```
   Relation.Binary.Morphism.Bundles
@@ -979,6 +1000,17 @@ Other minor additions
   Main : Set
   ```
 
+* Added new functions and pattern synonyms to `Data.Tree.AVL.Indexed`:
+  ```agda
+  foldr : (∀ {k} → Val k → A → A) → A → Tree V l u h → A
+  size  : Tree V → ℕ
+
+  pattern node⁺ k₁ t₁ k₂ t₂ t₃ bal = node k₁ t₁ (node k₂ t₂ t₃ bal) ∼+
+  pattern node⁻ k₁ k₂ t₁ t₂ bal t₃ = node k₁ (node k₂ t₁ t₂ bal) t₃ ∼-
+
+  ordered : Tree V l u n → l <⁺ u
+  ```
+
 * Added new functions to `Codata.Stream`:
   ```agda
   nats : Stream ℕ ∞
@@ -998,6 +1030,18 @@ Other minor additions
   record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂)
   ```
 
+* Re-exported and defined new functions in `Data.Tree.AVL.Key`:
+  ```agda
+  _≈⁺_    : Rel Key _
+  [_]ᴱ    : x ≈ y → [ x ] ≈⁺ [ y ]
+  refl⁺   : Reflexive _≈⁺_
+  sym⁺    : l ≈⁺ u → u ≈⁺ l
+  irrefl⁺ : ∀ k → ¬ (k <⁺ k)
+
+  strictPartialOrder : StrictPartialOrder _ _ _
+  strictTotalOrder   : StrictTotalOrder _ _ _
+  ```
+
 * Added new proofs to `Relation.Binary.Properties.Poset`:
   ```agda
   mono⇒cong     : f Preserves _≤_ ⟶ _≤_ → f Preserves _≈_ ⟶ _≈_
@@ -1028,7 +1072,7 @@ Other minor additions
   setoidHomomorphism : SetoidHomomorphism S T → SetoidHomomorphism T U → SetoidHomomorphism S U
   setoidMonomorphism : SetoidMonomorphism S T → SetoidMonomorphism T U → SetoidMonomorphism S U
   setoidIsomorphism  : SetoidIsomorphism S T → SetoidIsomorphism T U → SetoidIsomorphism S U
-  
+
   preorderHomomorphism : PreorderHomomorphism P Q → PreorderHomomorphism Q R → PreorderHomomorphism P R
   posetHomomorphism    : PosetHomomorphism P Q → PosetHomomorphism Q R → PosetHomomorphism P R
   ```
@@ -1038,7 +1082,7 @@ Other minor additions
   setoidHomomorphism : (S : Setoid a ℓ₁) → SetoidHomomorphism S S
   setoidMonomorphism : (S : Setoid a ℓ₁) → SetoidMonomorphism S S
   setoidIsomorphism  : (S : Setoid a ℓ₁) → SetoidIsomorphism S S
-  
+
   preorderHomomorphism : (P : Preorder a ℓ₁ ℓ₂) → PreorderHomomorphism P P
   posetHomomorphism    : (P : Poset a ℓ₁ ℓ₂) → PosetHomomorphism P P
   ```

README/Data/Tree/AVL.agda

@@ -20,6 +20,7 @@ import Data.Tree.AVL
 -- natural numbers as keys and vectors of strings as values.
 
 open import Data.Nat.Properties using (<-strictTotalOrder)
+open import Data.Product as Prod using (_,_; _,′_)
 open import Data.String using (String)
 open import Data.Vec using (Vec; _∷_; [])
 open import Relation.Binary.PropositionalEquality
@@ -60,7 +61,6 @@ t₃ = delete 2 t₂
 -- Conversion of a list of key-value mappings to a tree.
 
 open import Data.List using (_∷_; [])
-open import Data.Product as Prod using (_,_; _,′_)
 
 t₄ : Tree
 t₄ = fromList ((2 , v₂) ∷ (1 , v₁) ∷ [])
@@ -111,14 +111,14 @@ open import Function.Base using (id)
 v₆ : headTail t₀ ≡ nothing
 v₆ = refl
 
-v₇ : Maybe.map (Prod.map id toList) (headTail t₂) ≡
+v₇ : Maybe.map (Prod.map₂ toList) (headTail t₂) ≡
      just ((1 , v₁) , ((2 , v₂) ∷ []))
 v₇ = refl
 
 v₈ : initLast t₀ ≡ nothing
 v₈ = refl
 
-v₉ : Maybe.map (Prod.map toList id) (initLast t₄) ≡
+v₉ : Maybe.map (Prod.map₁ toList) (initLast t₄) ≡
      just (((1 , v₁) ∷ []) ,′ (2 , v₂))
 v₉ = refl
 

src/Data/Integer/Properties.agda

@@ -2437,8 +2437,6 @@ Please use *-cancelˡ-<-nonNeg instead."
 Please use *-cancelʳ-<-nonNeg instead."
 #-}
 
-
-
 -- Version 1.6
 
 m≤n⇒m⊓n≡m = i≤j⇒i⊓j≡i

src/Data/Tree/AVL.agda

@@ -36,12 +36,12 @@ private
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
 import Data.Tree.AVL.Indexed strictTotalOrder as Indexed
-open Indexed using (K&_ ; ⊥⁺ ; ⊤⁺; ⊥⁺<⊤⁺; ⊥⁺<[_]<⊤⁺; ⊥⁺<[_]; [_]<⊤⁺)
+open Indexed using (⊥⁺; ⊤⁺; ⊥⁺<⊤⁺; ⊥⁺<[_]<⊤⁺; ⊥⁺<[_]; [_]<⊤⁺)
 
 ------------------------------------------------------------------------
 -- Re-export some core definitions publically
 
-open Indexed using (Value; MkValue; const) public
+open Indexed using (K&_;_,_; toPair; fromPair; Value; MkValue; const) public
 
 ------------------------------------------------------------------------
 -- Types and functions with hidden indices
@@ -92,12 +92,12 @@ module _ {v} {V : Value v} where
   _∈?_ : Key → Tree V → Bool
   k ∈? t = is-just (lookup k t)
 
-  headTail : Tree V → Maybe ((K& V) × Tree V)
+  headTail : Tree V → Maybe (K& V × Tree V)
   headTail (tree (Indexed.leaf _)) = nothing
   headTail (tree {h = suc _} t)    with Indexed.headTail t
   ... | (k , _ , _ , t′) = just (k , tree (Indexed.castˡ ⊥⁺<[ _ ] t′))
 
-  initLast : Tree V → Maybe (Tree V × (K& V))
+  initLast : Tree V → Maybe (Tree V × K& V)
   initLast (tree (Indexed.leaf _)) = nothing
   initLast (tree {h = suc _} t)    with Indexed.initLast t
   ... | (k , _ , _ , t′) = just (tree (Indexed.castʳ t′ [ _ ]<⊤⁺) , k)
@@ -108,7 +108,7 @@ module _ {v} {V : Value v} where
   -- The input does not need to be ordered.
 
   fromList : List (K& V) → Tree V
-  fromList = List.foldr (uncurry insert) empty
+  fromList = List.foldr (uncurry insert ∘′ toPair) empty
 
   -- Returns an ordered list.
 

src/Data/Tree/AVL/Indexed.agda

@@ -17,14 +17,14 @@ open import Data.Product using (Σ; ∃; _×_; _,_; proj₁)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.List.Base as List using (List)
 open import Data.DifferenceList using (DiffList; []; _∷_; _++_)
-open import Function as F hiding (const)
+open import Function.Base as F hiding (const)
 open import Relation.Unary
 open import Relation.Binary using (_Respects_; Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 private
   variable
-    l : Level
+    l v : Level
     A : Set l
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
@@ -39,9 +39,6 @@ open import Data.Tree.AVL.Height public
 ------------------------------------------------------------------------
 -- Definitions of the tree
 
-K&_ : ∀ {v} (V : Value v) → Set (a ⊔ v)
-K& V = Σ Key (Value.family V)
-
 -- The trees have three parameters/indices: a lower bound on the
 -- keys, an upper bound, and a height.
 --
@@ -50,14 +47,18 @@ K& V = Σ Key (Value.family V)
 data Tree {v} (V : Value v) (l u : Key⁺) : ℕ → Set (a ⊔ v ⊔ ℓ₂) where
   leaf : (l<u : l <⁺ u) → Tree V l u 0
   node : ∀ {hˡ hʳ h}
-         (k : K& V)
-         (lk : Tree V l [ proj₁ k ] hˡ)
-         (ku : Tree V [ proj₁ k ] u hʳ)
+         (kv : K& V)
+         (lk : Tree V l [ kv .key ] hˡ)
+         (ku : Tree V [ kv .key ] u hʳ)
          (bal : hˡ ∼ hʳ ⊔ h) →
          Tree V l u (suc h)
 
 module _ {v} {V : Value v} where
 
+  ordered : ∀ {l u n} → Tree V l u n → l <⁺ u
+  ordered (leaf l<u)          = l<u
+  ordered (node kv lk ku bal) = trans⁺ _ (ordered lk) (ordered ku)
+
   private
     Val = Value.family V
     V≈  = Value.respects V
@@ -67,8 +68,8 @@ module _ {v} {V : Value v} where
 
   node-injective-key :
     ∀ {hˡ₁ hˡ₂ hʳ₁ hʳ₂ h l u k₁ k₂}
-      {lk₁ : Tree V l [ proj₁ k₁ ] hˡ₁} {lk₂ : Tree V l [ proj₁ k₂ ] hˡ₂}
-      {ku₁ : Tree V [ proj₁ k₁ ] u hʳ₁} {ku₂ : Tree V [ proj₁ k₂ ] u hʳ₂}
+      {lk₁ : Tree V l [ k₁ .key ] hˡ₁} {lk₂ : Tree V l [ k₂ .key ] hˡ₂}
+      {ku₁ : Tree V [ k₁ .key ] u hʳ₁} {ku₂ : Tree V [ k₂ .key ] u hʳ₂}
       {bal₁ : hˡ₁ ∼ hʳ₁ ⊔ h} {bal₂ : hˡ₂ ∼ hʳ₂ ⊔ h} →
     node k₁ lk₁ ku₁ bal₁ ≡ node k₂ lk₂ ku₂ bal₂ → k₁ ≡ k₂
   node-injective-key refl = refl
@@ -97,46 +98,46 @@ module _ {v} {V : Value v} where
   -- Various constant-time functions which construct trees out of
   -- smaller pieces, sometimes using rotation.
 
+  pattern node⁺ k₁ t₁ k₂ t₂ t₃ bal = node k₁ t₁ (node k₂ t₂ t₃ bal) ∼+
+
   joinˡ⁺ : ∀ {l u hˡ hʳ h} →
            (k : K& V) →
-           (∃ λ i → Tree V l [ proj₁ k ] (i ⊕ hˡ)) →
-           Tree V [ proj₁ k ] u hʳ →
+           (∃ λ i → Tree V l [ k .key ] (i ⊕ hˡ)) →
+           Tree V [ k .key ] u hʳ →
            (bal : hˡ ∼ hʳ ⊔ h) →
            ∃ λ i → Tree V l u (i ⊕ (1 + h))
-  joinˡ⁺ k₆ (1# , node k₂ t₁
-                    (node k₄ t₃ t₅ bal)
-                                ∼+) t₇ ∼-  = (0# , node k₄
-                                                        (node k₂ t₁ t₃ (max∼ bal))
-                                                        (node k₆ t₅ t₇ (∼max bal))
-                                                        ∼0)
-  joinˡ⁺ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼-  = (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
-  joinˡ⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼-  = (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
-  joinˡ⁺ k₂ (1# , t₁)               t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼-)
-  joinˡ⁺ k₂ (1# , t₁)               t₃ ∼+  = (0# , node k₂ t₁ t₃ ∼0)
-  joinˡ⁺ k₂ (0# , t₁)               t₃ bal = (0# , node k₂ t₁ t₃ bal)
+  joinˡ⁺ k₂ (0# , t₁)                t₃ bal = (0# , node k₂ t₁ t₃ bal)
+  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼0  = (1# , node k₂ t₁ t₃ ∼-)
+  joinˡ⁺ k₂ (1# , t₁)                t₃ ∼+  = (0# , node k₂ t₁ t₃ ∼0)
+  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼-) t₅ ∼-  = (0# , node k₂ t₁ (node k₄ t₃ t₅ ∼0) ∼0)
+  joinˡ⁺ k₄ (1# , node  k₂ t₁ t₃ ∼0) t₅ ∼-  = (1# , node k₂ t₁ (node k₄ t₃ t₅ ∼-) ∼+)
+  joinˡ⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼-
+    = (0# , node k₄ (node k₂ t₁ t₃ (max∼ bal))
+                    (node k₆ t₅ t₇ (∼max bal))
+                    ∼0)
+
+  pattern node⁻ k₁ k₂ t₁ t₂ bal t₃ = node k₁ (node k₂ t₁ t₂ bal) t₃ ∼-
 
   joinʳ⁺ : ∀ {l u hˡ hʳ h} →
            (k : K& V) →
-           Tree V l [ proj₁ k ] hˡ →
-           (∃ λ i → Tree V [ proj₁ k ] u (i ⊕ hʳ)) →
+           Tree V l [ k .key ] hˡ →
+           (∃ λ i → Tree V [ k .key ] u (i ⊕ hʳ)) →
            (bal : hˡ ∼ hʳ ⊔ h) →
            ∃ λ i → Tree V l u (i ⊕ (1 + h))
-  joinʳ⁺ k₂ t₁ (1# , node k₆
-                       (node k₄ t₃ t₅ bal)
-                                t₇ ∼-) ∼+  = (0# , node k₄
-                                                        (node k₂ t₁ t₃ (max∼ bal))
-                                                        (node k₆ t₅ t₇ (∼max bal))
-                                                        ∼0)
-  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+  = (0# , node k₄ (node k₂ t₁ t₃ ∼0) t₅ ∼0)
-  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+  = (1# , node k₄ (node k₂ t₁ t₃ ∼+) t₅ ∼-)
+  joinʳ⁺ k₂ t₁ (0# , t₃)               bal = (0# , node k₂ t₁ t₃ bal)
   joinʳ⁺ k₂ t₁ (1# , t₃)               ∼0  = (1# , node k₂ t₁ t₃ ∼+)
   joinʳ⁺ k₂ t₁ (1# , t₃)               ∼-  = (0# , node k₂ t₁ t₃ ∼0)
-  joinʳ⁺ k₂ t₁ (0# , t₃)               bal = (0# , node k₂ t₁ t₃ bal)
+  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+  = (0# , node k₄ (node k₂ t₁ t₃ ∼0) t₅ ∼0)
+  joinʳ⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼0) ∼+  = (1# , node k₄ (node k₂ t₁ t₃ ∼+) t₅ ∼-)
+  joinʳ⁺ k₂ t₁ (1# , node⁻ k₆ k₄ t₃ t₅ bal t₇) ∼+
+    = (0# , node k₄ (node k₂ t₁ t₃ (max∼ bal))
+                    (node k₆ t₅ t₇ (∼max bal))
+                    ∼0)
 
   joinˡ⁻ : ∀ {l u} hˡ {hʳ h} →
            (k : K& V) →
-           (∃ λ i → Tree V l [ proj₁ k ] pred[ i ⊕ hˡ ]) →
-           Tree V [ proj₁ k ] u hʳ →
+           (∃ λ i → Tree V l [ k .key ] pred[ i ⊕ hˡ ]) →
+           Tree V [ k .key ] u hʳ →
            (bal : hˡ ∼ hʳ ⊔ h) →
            ∃ λ i → Tree V l u (i ⊕ h)
   joinˡ⁻ zero    k₂ (0# , t₁) t₃ bal = (1# , node k₂ t₁ t₃ bal)
@@ -148,8 +149,8 @@ module _ {v} {V : Value v} where
 
   joinʳ⁻ : ∀ {l u hˡ} hʳ {h} →
            (k : K& V) →
-           Tree V l [ proj₁ k ] hˡ →
-           (∃ λ i → Tree V [ proj₁ k ] u pred[ i ⊕ hʳ ]) →
+           Tree V l [ k .key ] hˡ →
+           (∃ λ i → Tree V [ k .key ] u pred[ i ⊕ hʳ ]) →
            (bal : hˡ ∼ hʳ ⊔ h) →
            ∃ λ i → Tree V l u (i ⊕ h)
   joinʳ⁻ zero    k₂ t₁ (0# , t₃) bal = (1# , node k₂ t₁ t₃ bal)
@@ -163,8 +164,8 @@ module _ {v} {V : Value v} where
   -- Logarithmic in the size of the tree.
 
   headTail : ∀ {l u h} → Tree V l u (1 + h) →
-             ∃ λ (k : K& V) → l <⁺ [ proj₁ k ] ×
-                            ∃ λ i → Tree V [ proj₁ k ] u (i ⊕ h)
+             ∃ λ (k : K& V) → l <⁺ [ k .key ] ×
+                            ∃ λ i → Tree V [ k .key ] u (i ⊕ h)
   headTail (node k₁ (leaf l<k₁) t₂ ∼+) = (k₁ , l<k₁ , 0# , t₂)
   headTail (node k₁ (leaf l<k₁) t₂ ∼0) = (k₁ , l<k₁ , 0# , t₂)
   headTail (node {hˡ = suc _} k₃ t₁₂ t₄ bal) with headTail t₁₂
@@ -174,8 +175,8 @@ module _ {v} {V : Value v} where
   -- Logarithmic in the size of the tree.
 
   initLast : ∀ {l u h} → Tree V l u (1 + h) →
-             ∃ λ (k : K& V) → [ proj₁ k ] <⁺ u ×
-                            ∃ λ i → Tree V l [ proj₁ k ] (i ⊕ h)
+             ∃ λ (k : K& V) → [ k .key ] <⁺ u ×
+                            ∃ λ i → Tree V l [ k .key ] (i ⊕ h)
   initLast (node k₂ t₁ (leaf k₂<u) ∼-) = (k₂ , k₂<u , (0# , t₁))
   initLast (node k₂ t₁ (leaf k₂<u) ∼0) = (k₂ , k₂<u , (0# , t₁))
   initLast (node {hʳ = suc _} k₂ t₁ t₃₄ bal) with initLast t₃₄