Add properties that characterize Data.Tree.AVL.Indexed.delete. (#2961)

* Add properties that characterize `Data.Tree.AVL.Indexed.delete`.

These are properties for the core delete on AVL trees and similar to the prexisting properties of `insert`.

Lemmas added for `delete` are `delete⁺`, `delete-tree⁻`, `delete-key-∈⁻` and `delete-key⁻`.
Together these can be used to prove `(k′ ∈ delete k t) ⇔ (k′ ≉ k × k′ ∈ t)`, which fully characterizes `delete`.

`delete⁺`, `delete-tree⁻`, and `delete-key⁻` correspond to Coq.FSets.FSetInterface's `remove_2`, `remove_3`, and `remove_1`, respectively.

Just like other lemmas in this file, `delete⁺`, `delete-tree⁻`, `delete-key⁻` generalize `k′ ∈ t` to `Any P t`.
`delete-key-∈⁻` is essentally a helper for `delete-key⁻`, which would be difficult to prove directly.

Many more lemmas were added for AVL functions that `delete` depends on.
These additional lemmas characterize the functions `castʳ`, `joinˡ⁺`, `joinʳ⁺`, `joinˡ⁻`, `joinʳ⁻`, `headTail`, and `join`.
Adding all this code to Properties.agda caused `make test` to overflow past the 4096 MB default heap size.
This was solved by breaking Properties.agda into multiple files, with roughly one file for each AVL function.

Added proofs are a similar style the preexisting proofs in Properties.agda.

* telescoped arguments in Singleton.agda

* removed unused vars, merged cases using Any.toSum for JoinConstFuns.agda

* addressed review comments on Join.agda

* addressed comments in Insert.agda

* addressed review comments for HeadTail.agda

* addressed review comments for Delete.agda

* Moved Data.Tree.AVL.Indexed.Relation.Unary.Any.* into Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.*

* Simplified proofs by removing subterms that recapitulate the subject  function.

* Changed whitespace to align matches.

* More alignment.

* addressed review comments to use var in let and moved implicits to variable block

* Recorded changes in CHANGELOG.md. Addressed review comments for AnyLookup.

* Apply suggestion from @jamesmckinna

Cosmetic tweak to text

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Author: mikedelorimier

CHANGELOG.md

@@ -67,6 +67,11 @@ Minor improvements
   `refl`, `sym`, and `trans` have been weakened to allow relations of different
   levels to be used.
 
+* Due to becoming large, `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties`
+  has been split into small modules
+  `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.*`
+  that are reexported by the original `Properties`.
+
 Deprecated modules
 ------------------
 
@@ -171,6 +176,19 @@ New modules
   Data.List.NonEmpty.Membership.Setoid
   ```
 
+* Refactoring of `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties` as smaller modules:
+  ```
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Lookup
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Delete
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.HeadTail
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Insert
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Join
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.LookupFun
+  Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Singleton
+  ```
+
 * `Relation.Binary.Morphism.Construct.On`: given a relation `_∼_` on `B`,
   and a function `f : A → B`, construct the canonical `IsRelMonomorphism`
   between `_∼_ on f` and `_∼_`, witnessed by `f` itself.
@@ -397,6 +415,87 @@ Additions to existing modules
   showAtPrecision : ℕ → ℚᵘ → String
   ```
 
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Cast`:
+  ```agda
+  castʳ⁺ : Any P lm → Any P (castʳ lm m<u)
+  castʳ⁻ : Any P (castʳ lm m<u) → Any P lm
+  ```
+
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.Delete`:
+  ```agda
+  delete⁺ : (t : Tree V l u h) (seg : l < k < u) →
+            (p : Any P t) → lookupKey p ≉ k →
+            Any P (proj₂ (delete k t seg))
+  delete-tree⁻ : (t : Tree V l u h) (seg : l < k < u) →
+                 Any P (proj₂ (delete k t seg)) →
+                 Any P t
+  delete-key-∈⁻ : (t : Tree V l u h) (seg : l < k < u) →
+                  {kp : Key} →
+                  Any ((kp ≈_) ∘′ key) (proj₂ (delete k t seg)) →
+                  kp ≉ k
+  delete-key⁻ : (t : Tree V l u h) (seg : l < k < u) →
+                (p : Any P (proj₂ (delete k t seg))) →
+                Any.lookupKey p ≉ k
+  ```
+
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.HeadTail`:
+  ```
+  headTail⁺ : (t : Tree V l u (1 + h)) →
+              let kv , _ , _ , t⁻ = headTail t in
+              Any P t → P kv ⊎ Any P t⁻
+  headTail-head⁻ : (t : Tree V l u (suc h)) →
+                   P (proj₁ (headTail t)) → Any P t
+  headTail-tail⁻ : (t : Tree V l u (1 + h)) →
+                   let _ , _ , _ , t⁻ = headTail t in
+                   Any P t⁻ → Any P t
+  ```
+
+* In `Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.JoinConstFuns`:
+  ```
+  joinˡ⁻-here⁺ : (kv : K& V) →
+                 (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
+                 (r : Tree V [ kv .key ] u hʳ) →
+                 (bal : hˡ ∼ hʳ ⊔ h) →
+                 P kv → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+  joinˡ⁻-left⁺ : (kv : K& V) →
+                 (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
+                 (r : Tree V [ kv .key ] u hʳ) →
+                 (bal : hˡ ∼ hʳ ⊔ h) →
+                 Any P (proj₂ l) → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+  joinˡ⁻-right⁺ : (kv : K& V) →
+                  (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
+                  (r : Tree V [ kv .key ] u hʳ) →
+                  (bal : hˡ ∼ hʳ ⊔ h) →
+                  Any P r → Any P (proj₂ (joinˡ⁻ hˡ kv l r bal))
+  joinˡ⁻⁻ : (kv : K& V) →
+            (l : ∃ λ i → Tree V l [ kv .key ] pred[ i ⊕ hˡ ]) →
+            (r : Tree V [ kv .key ] u hʳ) →
+            (bal : hˡ ∼ hʳ ⊔ h) →
+            Any P (proj₂ (joinˡ⁻ hˡ kv l r bal)) →
+            P kv ⊎ Any P (proj₂ l) ⊎ Any P r
+  joinʳ⁻-here⁺ : (kv : K& V) →
+                 (l : Tree V l [ kv .key ] hˡ) →
+                 (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+                 (bal : hˡ ∼ hʳ ⊔ h) →
+                 P kv → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+  joinʳ⁻-left⁺ : (kv : K& V) →
+                 (l : Tree V l [ kv .key ] hˡ) →
+                 (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+                 (bal : hˡ ∼ hʳ ⊔ h) →
+                 Any P l → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+  joinʳ⁻-right⁺ : (kv : K& V) →
+                  (l : Tree V l [ kv .key ] hˡ) →
+                  (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+                  (bal : hˡ ∼ hʳ ⊔ h) →
+                  Any P (proj₂ r) → Any P (proj₂ (joinʳ⁻ hʳ kv l r bal))
+  joinʳ⁻⁻ : (kv : K& V) →
+            (l : Tree V l [ kv .key ] hˡ) →
+            (r : ∃ λ i → Tree V [ kv .key ] u pred[ i ⊕ hʳ ]) →
+            (bal : hˡ ∼ hʳ ⊔ h) →
+            Any P (proj₂ (joinʳ⁻ hʳ kv l r bal)) →
+            P kv ⊎ Any P l ⊎ Any P (proj₂ r)
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   map-removeAt : ∀ (f : A → B) (xs : Vec A (suc n)) (i : Fin (suc n)) →