Add more properties to Data.Tree.Binary.Properties (#1273)

Author: Taneb

CHANGELOG.md

@@ -520,6 +520,12 @@ Other minor additions
   index-∈-lookup : (i : Fin n) (xs : Vec A n) → Any.index (∈-lookup i xs) ≡ i
   ```
 
+* Added new proofs to `Data.Tree.Binary.Properties`:
+  ```agda
+  map-compose : map (f₁ ∘ f₂) (g₁ ∘ g₂) ≗ map f₁ g₁ ∘ map f₂ g₂
+  map-cong : f₁ ≗ f₂ → g₁ ≗ g₂ → map f₁ g₁ ≗ map f₂ g₂
+  ```
+
 Refactorings
 ------------
 

src/Data/Tree/Binary/Properties.agda

@@ -8,6 +8,8 @@
 
 module Data.Tree.Binary.Properties where
 
+open import Function using (_∘_)
+open import Function.Nary.NonDependent using (congₙ)
 open import Level using (Level)
 open import Data.Nat.Base using (suc; _+_)
 open import Data.Tree.Binary
@@ -16,12 +18,14 @@ open import Relation.Binary.PropositionalEquality
 
 private
   variable
-    a n n₁ l l₁ : Level
+    a n n₁ n₂ l l₁ l₂ : Level
     A : Set a
     N : Set n
     N₁ : Set n₁
+    N₂ : Set n₂
     L : Set l
     L₁ : Set l₁
+    L₂ : Set l₂
 
 #nodes-map : ∀ (f : N → N₁) (g : L → L₁) t → #nodes (map f g t) ≡ #nodes t
 #nodes-map f g (leaf x)     = refl
@@ -48,3 +52,12 @@ private
 map-id : ∀ (t : Tree N L) → map id id t ≡ t
 map-id (leaf x)     = refl
 map-id (node l v r) = cong₂ (flip node v) (map-id l) (map-id r)
+
+map-compose : ∀ {f₁ : N₁ → N₂} {f₂ : N → N₁} {g₁ : L₁ → L₂} {g₂ : L → L₁} →
+              map (f₁ ∘ f₂) (g₁ ∘ g₂) ≗ map f₁ g₁ ∘ map f₂ g₂
+map-compose (leaf x) = refl
+map-compose (node l v r) = cong₂ (λ l r → node l _ r) (map-compose l) (map-compose r)
+
+map-cong : ∀ {f₁ f₂ : N → N₁} {g₁ g₂ : L → L₁} → f₁ ≗ f₂ → g₁ ≗ g₂ → map f₁ g₁ ≗ map f₂ g₂
+map-cong p q (leaf x) = cong leaf (q x)
+map-cong p q (node l v r) = congₙ 3 node (map-cong p q l) (p v) (map-cong p q r)