    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Tree Zipper-related properties
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Tree.Binary.Zipper.Properties where

    open import Data.List.Base as List using (List ; [] ; _∷_)
    open import Data.Maybe.Base using (Maybe; just; nothing)
    open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
    open import Data.Nat.Base using (ℕ; suc; _+_)
    open import Data.Nat.Properties using (+-identityʳ; +-comm; +-assoc)
    open import Data.Nat.ListAction using (sum)
    open import Data.Tree.Binary as BT using (Tree; node; leaf)
    open import Data.Tree.Binary.Zipper using (Zipper; toTree; up; mkZipper;
      leftBranch; rightBranch; left; right; #nodes; Crumb; getTree; #leaves;
      map; foldr; _⟪_⟫ˡ_; _⟪_⟫ʳ_)
    open import Function.Base using (_on_; _∘_; _$_)
    open import Level using (Level)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; refl; cong)
    open import Relation.Binary.PropositionalEquality.Properties
      using (module ≡-Reasoning)
    open ≡-Reasoning

    private
      variable
        a n l n₁ l₁ : Level
        A : Set a
        N : Set n
        L : Set l
        N₁ : Set n₁
        L₁ : Set l₁

    -- Invariant: Zipper represents a given tree

    -- Stability under moving

    toTree-up-identity : (zp : Zipper N L) → All ((_≡_ on toTree) zp) (up zp)
    toTree-up-identity (mkZipper [] foc) = nothing
    toTree-up-identity (mkZipper (leftBranch m l ∷ ctx) foc) = just refl
    toTree-up-identity (mkZipper (rightBranch m r ∷ ctx) foc) = just refl

    toTree-left-identity : (zp : Zipper N L) → All ((_≡_ on toTree) zp) (left zp)
    toTree-left-identity (mkZipper ctx (leaf x)) = nothing
    toTree-left-identity (mkZipper ctx (node l m r)) = just refl

    toTree-right-identity : (zp : Zipper N L) → All ((_≡_ on toTree) zp) (right zp)
    toTree-right-identity (mkZipper ctx (leaf x)) = nothing
    toTree-right-identity (mkZipper ctx (node l m r)) = just refl

    ------------------------------------------------------------------------
    -- Tree-like operations indeed correspond to their counterparts

    toTree-#nodes : ∀ (zp : Zipper N L) → #nodes zp ≡ BT.#nodes (toTree zp)
    toTree-#nodes (mkZipper c v) = helper c v
      where
        helper : (cs : List (Crumb N L)) →
                 (t : Tree N L) →
                 #nodes (mkZipper cs t) ≡ BT.#nodes (toTree (mkZipper cs t))
        helper [] foc = +-identityʳ (BT.#nodes foc)
        helper cs@(leftBranch m l ∷ ctx) foc = let
          #ctx = sum (List.map (suc ∘ BT.#nodes ∘ getTree) ctx)
          #foc = BT.#nodes foc
          #l = BT.#nodes l in begin
          #foc + (1 + (#l + #ctx))             ≡⟨ +-assoc #foc 1 (#l + #ctx) ⟨
          #foc + 1 + (#l + #ctx)               ≡⟨ cong (_+ (#l + #ctx)) (+-comm #foc 1) ⟩
          1 + #foc + (#l + #ctx)               ≡⟨ +-assoc (1 + #foc) #l #ctx ⟨
          1 + #foc + #l + #ctx                 ≡⟨ cong (_+ #ctx) (+-comm (1 + #foc) #l) ⟩
          #nodes (mkZipper ctx (node l m foc)) ≡⟨ helper ctx (node l m foc) ⟩
          BT.#nodes (toTree (mkZipper cs foc)) ∎
        helper cs@(rightBranch m r ∷ ctx) foc = let
          #ctx = sum (List.map (suc ∘ BT.#nodes ∘ getTree) ctx)
          #foc = BT.#nodes foc
          #r = BT.#nodes r in begin
          #foc + (1 + (#r + #ctx))             ≡⟨ cong (#foc +_) (+-assoc 1 #r #ctx) ⟨
          #foc + (1 + #r + #ctx)               ≡⟨ +-assoc #foc (suc #r) #ctx ⟨
          #nodes (mkZipper ctx (node foc m r)) ≡⟨ helper ctx (node foc m r) ⟩
          BT.#nodes (toTree (mkZipper cs foc)) ∎

    toTree-#leaves : ∀ (zp : Zipper N L) → #leaves zp ≡ BT.#leaves (toTree zp)
    toTree-#leaves (mkZipper c v) = helper c v
      where
        helper : (cs : List (Crumb N L)) →
                 (t : Tree N L) →
                 #leaves (mkZipper cs t) ≡ BT.#leaves (toTree (mkZipper cs t))
        helper [] foc = +-identityʳ (BT.#leaves foc)
        helper cs@(leftBranch m l ∷ ctx) foc = let
          #ctx = sum (List.map (BT.#leaves ∘ getTree) ctx)
          #foc = BT.#leaves foc
          #l = BT.#leaves l in begin
          #foc + (#l + #ctx)                    ≡⟨ +-assoc #foc #l #ctx ⟨
          #foc + #l + #ctx                      ≡⟨ cong (_+ #ctx) (+-comm #foc #l) ⟩
          #leaves (mkZipper ctx (node l m foc)) ≡⟨ helper ctx (node l m foc) ⟩
          BT.#leaves (toTree (mkZipper cs foc)) ∎
        helper cs@(rightBranch m r ∷ ctx) foc = let
          #ctx = sum (List.map (BT.#leaves ∘ getTree) ctx)
          #foc = BT.#leaves foc
          #r = BT.#leaves r in begin
          #foc + (#r + #ctx)                    ≡⟨ +-assoc #foc #r #ctx ⟨
          #leaves (mkZipper ctx (node foc m r)) ≡⟨ helper ctx (node foc m r) ⟩
          BT.#leaves (toTree (mkZipper cs foc)) ∎

    toTree-map : ∀ (f : N → N₁) (g : L → L₁) zp → toTree (map f g zp) ≡ BT.map f g (toTree zp)
    toTree-map {N = N} {L = L} f g (mkZipper c v) = helper c v
      where
        helper : (cs : List (Crumb N L)) →
                 (t : Tree N L) →
                 toTree (map f g (mkZipper cs t)) ≡ BT.map f g (toTree (mkZipper cs t))
        helper [] foc = refl
        helper (leftBranch m l ∷ ctx) foc = helper ctx (node l m foc)
        helper (rightBranch m r ∷ ctx) foc = helper ctx (node foc m r)

    toTree-foldr : ∀ (f : A → N → A → A) (g : L → A) zp → foldr f g zp ≡ BT.foldr f g (toTree zp)
    toTree-foldr {N = N} {L = L} f g (mkZipper c v) = helper c v
      where
        helper : (cs : List (Crumb N L)) →
                 (t : Tree N L) →
                 foldr f g (mkZipper cs t) ≡ BT.foldr f g (toTree (mkZipper cs t))
        helper [] foc = refl
        helper (leftBranch m l ∷ ctx) foc = helper ctx (node l m foc)
        helper (rightBranch m r ∷ ctx) foc = helper ctx (node foc m r)

    ------------------------------------------------------------------------
    -- Properties of the building functions

    -- _⟪_⟫ˡ_ properties

    toTree-⟪⟫ˡ : ∀ l m (zp : Zipper N L) → toTree (l ⟪ m ⟫ˡ zp) ≡ node l m (toTree zp)
    toTree-⟪⟫ˡ {N = N} {L = L} l m (mkZipper c v) = helper c v
      where
        helper : (cs : List (Crumb N L)) →
                 (t : Tree N L) →
                 toTree (l ⟪ m ⟫ˡ mkZipper cs t) ≡ node l m (toTree $ mkZipper cs t)
        helper [] foc = refl
        helper (leftBranch m l ∷ ctx) foc = helper ctx (node l m foc)
        helper (rightBranch m r ∷ ctx) foc = helper ctx (node foc m r)

    -- _⟪_⟫ʳ_ properties

    toTree-⟪⟫ʳ : ∀ (zp : Zipper N L) m r → toTree (zp ⟪ m ⟫ʳ r) ≡ node (toTree zp) m r
    toTree-⟪⟫ʳ {N = N} {L = L} (mkZipper c v) m r = helper c v
      where
        helper : (cs : List (Crumb N L)) →
                 (t : Tree N L) →
                 toTree (mkZipper cs t ⟪ m ⟫ʳ r) ≡ node (toTree $ mkZipper cs t) m r
        helper [] foc = refl
        helper (leftBranch m l ∷ ctx) foc = helper ctx (node l m foc)
        helper (rightBranch m r ∷ ctx) foc = helper ctx (node foc m r)

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.0

    toTree-#nodes-commute = toTree-#nodes
    {-# WARNING_ON_USAGE toTree-#nodes-commute
    "Warning: toTree-#nodes-commute was deprecated in v2.0.
    Please use toTree-#nodes instead."
    #-}

    toTree-#leaves-commute = toTree-#leaves
    {-# WARNING_ON_USAGE toTree-#leaves-commute
    "Warning: toTree-#leaves-commute was deprecated in v2.0.
    Please use toTree-#leaves instead."
    #-}

    toTree-map-commute = toTree-map
    {-# WARNING_ON_USAGE toTree-map-commute
    "Warning: toTree-map-commute was deprecated in v2.0.
    Please use toTree-map instead."
    #-}

    toTree-foldr-commute = toTree-foldr
    {-# WARNING_ON_USAGE toTree-foldr-commute
    "Warning: toTree-foldr-commute was deprecated in v2.0.
    Please use toTree-foldr instead."
    #-}

    toTree-⟪⟫ˡ-commute = toTree-⟪⟫ˡ
    {-# WARNING_ON_USAGE toTree-⟪⟫ˡ-commute
    "Warning: toTree-⟪⟫ˡ-commute was deprecated in v2.0.
    Please use toTree-⟪⟫ˡ instead."
    #-}

    toTree-⟪⟫ʳ-commute = toTree-⟪⟫ʳ
    {-# WARNING_ON_USAGE toTree-⟪⟫ʳ-commute
    "Warning: toTree-⟪⟫ʳ-commute was deprecated in v2.0.
    Please use toTree-⟪⟫ʳ instead."
    #-}