{-|
This module defines intrinsically well-staged lists, its membership relation, and operations on them.
The module is parameterized by a ℕ-indexed type Item that represents the types of items in the staged list.
-}

{-# OPTIONS --safe #-}
open import Data.Nat using (ℕ)
module Data.StagedList (Item : ℕ → Set) where

open import Data.Nat using (ℕ; zero; suc; _≥‴_; _≤‴_; ≤‴-refl; ≤‴-step)
open import Data.Nat.Properties as ℕ
open import Function using (id; _∘_)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂)

-- For ℕ to ∋-witness conversion
open import Data.Nat using (_+_; _∸_; _<_; s≤s; z≤n)
open import Data.Product as P using (∃-syntax; _×_; -,_; proj₁; proj₂)
open import Relation.Nullary.Decidable using (yes; no; toWitness; True)

variable
  m n m′ n′ : ℕ
  m≥n : m ≥‴ n
  m′≥n : m′ ≥‴ n


-- | Transitivity of the ≤‴ relation.
≤‴-trans : n′ ≤‴ n → n ≤‴ m → n′ ≤‴ m
≤‴-trans ≤‴-refl n≤m  = n≤m
≤‴-trans (≤‴-step sn′≤m) n≤m = ≤‴-step (≤‴-trans sn′≤m n≤m)

{-|
A staged list data structure that maintains elements with stage levels greater than or equal to a minimum stage n.

The StagedList type represents a list where each element has an associated stage level,
and all elements must have stages greater than or equal to the list's minimum stage parameter.

Concatenation is defined as a constructor so that most operations distribute over it definitionally.

Parameters:
  n : ℕ - The minimum stage level for all elements in the list

Constructors:
  ∅ : Empty staged list
  _,[_^_] : Cons operation that adds an Item with stage m to a StagedList n,
            requiring proof that m ≥‴ n
  _++_ : Concatenation of two staged lists with the same minimum stage level

Both the cons operation _,[_^_] and concatenation _++_ are left associative.
-}
infixl  _,[_^_] _++_
data StagedList (n : ℕ) : Set where
  ∅ : StagedList n
  _,[_^_] : StagedList n → Item m → (m≥n : m ≥‴ n) → StagedList n
  _++_ : StagedList n → StagedList n → StagedList n

-- StagedList operations

-- | Remove items at stage n from a StagedList n, producing a StagedList (suc n).
infixl  _↾
_↾ : StagedList n → StagedList (suc n)
∅ ↾ = ∅
xs ,[ x ^ ≤‴-refl ] ↾ = xs ↾
xs ,[ x ^ ≤‴-step m≥n ] ↾ = xs ↾ ,[ x ^ m≥n ] 
xs ++ ys ↾ = (xs ↾) ++ (ys ↾)

-- | Remove items below level m from a StagedList n, producing a StagedList m.
-- The second argument is a proof that m ≥ n.
infixl  _↾≥_
_↾≥_ : StagedList n → m ≥‴ n → StagedList m
xs ↾≥ ≤‴-refl = xs
xs ↾≥ ≤‴-step m≥sn = xs ↾ ↾≥ m≥sn

-- | Convert a StagedList (suc n) into a StagedList n by weakening the witnesses.
-- The items remain the same.
inject₁ : StagedList (suc n) → StagedList n
inject₁ ∅ = ∅
inject₁ (xs ,[ x ^ m≥sn ]) = inject₁ xs ,[ x ^ ≤‴-step m≥sn ]
inject₁ (xs ++ ys) = inject₁ xs ++ inject₁ ys

-- | Convert a StagedList m into a StagedList n, where m ≥‴ n.
-- The items remain the same.
inject≥ : m ≥‴ n → StagedList m → StagedList n
inject≥ ≤‴-refl xs = xs
inject≥ (≤‴-step m≥sn) xs = inject₁ (inject≥ m≥sn xs)

-- | Concatenate two StagedLists n, flattening the _++_ constructors in the second list.
infixl  _++♭_
_++♭_ : StagedList n → StagedList n → StagedList n
xs ++♭ ∅ = xs
xs ++♭ (ys ,[ y ^ m≥n ]) = xs ++♭ ys ,[ y ^ m≥n ]
xs ++♭ (ys ++ zs) = (xs ++♭ ys) ++♭ zs

private variable
  xs ys zs : StagedList n
  xs₁ xs₂ xs₃ : StagedList n
  ys₁ ys₂ ys₃ : StagedList n
  x x′ y z : Item n

-- Properties of StagedList operations

-- | _↾≥_ distributes over ≤‴-trans.
↾≥-↾≥ : (m≥n : m ≥‴ n) (m′≥m : m′ ≥‴ m) → xs ↾≥ m≥n ↾≥ m′≥m ≡ xs ↾≥ (≤‴-trans m≥n m′≥m)
↾≥-↾≥ ≤‴-refl m′≥m = refl
↾≥-↾≥ (≤‴-step m≥n) m′≥m = ↾≥-↾≥ m≥n m′≥m

--∅-++ : ∅ ++ xs ≡ xs
--∅-++ {xs = ∅} = refl
--∅-++ {xs = xs ,[ x ^ m≥n ]} = cong (_,[ x ^ m≥n ]) ∅-++

--++-assoc : ∀ zs → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
--++-assoc ∅ = refl
--++-assoc (zs ,[ z ^ m≥n ]) = cong (_,[ z ^ m≥n ]) (++-assoc zs)

-- | _↾_ distributes over _++_.
++-↾ : ∀ ys → (xs ++ ys) ↾ ≡ xs ↾ ++ (ys ↾)
++-↾ ys = refl

-- | _↾≥_ distributes over _++_.
++-↾≥ : ∀ ys (m≥n : m ≥‴ n) → (xs ++ ys) ↾≥ m≥n ≡ xs ↾≥ m≥n ++ (ys ↾≥ m≥n)
++-↾≥ ys ≤‴-refl = refl
++-↾≥ ys (≤‴-step m≥sn) = ++-↾≥ (ys ↾) m≥sn

-- | Computation rule for _ ,[ _ ^ m≥n ] ↾≥ m≥n.
,-↾≥ : ∀ (m≥n : m ≥‴ n) → xs ,[ x ^ m≥n ] ↾≥ m≥n ≡ xs ↾≥ m≥n ,[ x ^ ≤‴-refl ]
,-↾≥ ≤‴-refl = refl
,-↾≥ (≤‴-step m≥n) = ,-↾≥ m≥n

-- | _↾ is left-inverse of inject₁.
inject₁-↾ : ∀ (xs : StagedList (suc n)) → (inject₁ xs) ↾ ≡ xs
inject₁-↾ ∅ = refl
inject₁-↾ (xs ,[ x ^ m≥n ]) = cong (_,[ x ^ m≥n ]) (inject₁-↾ xs)
inject₁-↾ (xs ++ ys) = cong₂ _++_ (inject₁-↾ xs) (inject₁-↾ ys)

-- | A frequent pattern for inject₁-↾.
++-inject₁-↾ : ∀ (ys : StagedList (suc n)) → xs ↾ ++ (inject₁ ys ↾) ≡ xs ↾ ++ ys
++-inject₁-↾ ys = cong (_ ++_) (inject₁-↾ ys) 

-- | inject₁ distributes over _++_.
inject₁-++ : ∀ (ys : StagedList (suc n)) → inject₁ (xs ++ ys) ≡ inject₁ xs ++ inject₁ ys
inject₁-++ ys = refl

-- | inject≥ maps ∅ to ∅.
inject≥-∅ : (m≥n : m ≥‴ n) → inject≥ m≥n ∅ ≡ ∅
inject≥-∅ ≤‴-refl = refl
inject≥-∅ (≤‴-step m≥n) = cong inject₁ (inject≥-∅ m≥n) 

{-|
Membership relation for staged lists.

xs ∋[ x ^ m≥n ] defines witnesses for membership of an item x with stage m in a StagedList n.
This data type represents the debruijn indices when the list is viewed as a context.

Parameters:
  xs    : StagedList n  - The staged list to check membership in
  x     : Item m        - The item to check for membership
  m≥n   : m ≥‴ n        - Proof that the item's stage m is at least the list's stage n

Constructors:
  Z : Base case - the item is the last item in the list
  S : Skip case - the item is in the init of the list
  L : Left case - the item is in the left sublist of a concatenation
  R : Right case - the item is in the right sublist of a concatenation
-}
infix  _∋[_^_]
data _∋[_^_] : StagedList n → Item m → m ≥‴ n → Set where
  Z : xs ,[ x ^ m≥n ] ∋[ x ^ m≥n ]
  S : xs ∋[ x ^ m≥n ] → xs ,[ y ^ m′≥n ] ∋[ x ^ m≥n ]
  L : xs ∋[ x ^ m≥n ] → xs ++ ys ∋[ x ^ m≥n ]
  R : ys ∋[ y ^ m≥n ] → xs ++ ys ∋[ y ^ m≥n ]

-- Membership properties
--∋-++⁻ : ∀ ys → xs ++ ys ∋[ x ^ m≥n ] → xs ∋[ x ^ m≥n ] ⊎ ys ∋[ x ^ m≥n ]
--∋-++⁻ ∅ xs∋x = inj₁ xs∋x
--∋-++⁻ (ys ,[ x ^ m≥n ]) Z = inj₂ Z
--∋-++⁻ (ys ,[ x ^ m≥n ]) (S xs++ys∋x) = Sum.map id S (∋-++⁻ ys xs++ys∋x)

--∋-++⁺ˡ : ∀ ys → xs ∋[ x ^ m≥n ] → xs ++ ys ∋[ x ^ m≥n ]
--∋-++⁺ˡ ∅ = id
--∋-++⁺ˡ (ys ,[ y ^ m≥n ]) = S ∘ ∋-++⁺ˡ ys

--∋-++⁺ʳ : ∀ xs → ys ∋[ y ^ m≥n ] → xs ++ ys ∋[ y ^ m≥n ]
--∋-++⁺ʳ xs Z = Z
--∋-++⁺ʳ xs (S ys∋y) = S (∋-++⁺ʳ xs ys∋y)

-- Membership properties

-- | Eliminate _↾ from a membership relation.
∋-↾⁻ : ∀ {m≥sn} → xs ↾ ∋[ x ^ m≥sn ] → xs ∋[ x ^ ≤‴-step m≥sn ]
∋-↾⁻ {xs = xs ,[ x ^ ≤‴-refl ]} xs↾∋x = S (∋-↾⁻ xs↾∋x)
∋-↾⁻ {xs = xs ,[ x ^ ≤‴-step m≥n ]} Z = Z
∋-↾⁻ {xs = xs ,[ x ^ ≤‴-step m≥n ]} (S xs↾∋x) = S (∋-↾⁻ xs↾∋x)
∋-↾⁻ {xs = xs ++ ys} (L xs↾∋x) = L (∋-↾⁻ xs↾∋x)
∋-↾⁻ {xs = xs ++ ys} (R ys↾∋y) = R (∋-↾⁻ ys↾∋y)

-- | Introduce _↾ into a membership relation.
∋-↾⁺ : ∀ {m≥sn} → xs ∋[ x ^ ≤‴-step m≥sn ] → xs ↾ ∋[ x ^ m≥sn ]
∋-↾⁺ Z = Z
∋-↾⁺ (S {m′≥n = ≤‴-refl} xs∋x) = ∋-↾⁺ xs∋x
∋-↾⁺ (S {m′≥n = ≤‴-step m′≥n} xs∋x) = S (∋-↾⁺ xs∋x)
∋-↾⁺ (L xs∋x) = L (∋-↾⁺ xs∋x)
∋-↾⁺ (R ys∋y) = R (∋-↾⁺ ys∋y)

-- | Eliminate _↾≥ from a membership relation.
∋-↾≥⁻ : ∀ n≥n′ → xs ↾≥ n≥n′ ∋[ x ^ m≥n ] → xs ∋[ x ^ ≤‴-trans n≥n′ m≥n ] 
∋-↾≥⁻ ≤‴-refl = id
∋-↾≥⁻ (≤‴-step n≥n′) = ∋-↾⁻ ∘ ∋-↾≥⁻ n≥n′

-- | Introduce _↾≥ into a membership relation.
∋-↾≥⁺ : ∀ m≥n → xs ∋[ x ^ m≥n ] → xs ↾≥ m≥n ∋[ x ^ ≤‴-refl ]
∋-↾≥⁺ ≤‴-refl = id
∋-↾≥⁺ (≤‴-step m≥n) = ∋-↾≥⁺ m≥n ∘ ∋-↾⁺

-- | Introduce inject₁ into a membership relation.
∋-inject₁⁺ : xs ∋[ x ^ m≥n ] → inject₁ xs ∋[ x ^ ≤‴-step m≥n ]
∋-inject₁⁺ Z = Z
∋-inject₁⁺ (S xs∋x) = S (∋-inject₁⁺ xs∋x)
∋-inject₁⁺ (L xs∋x) = L (∋-inject₁⁺ xs∋x)
∋-inject₁⁺ (R ys∋y) = R (∋-inject₁⁺ ys∋y)

-- | Eliminate inject₁ from a membership relation.
∋-inject₁⁻ : inject₁ xs ∋[ x ^ ≤‴-step m≥n ] → xs ∋[ x ^ m≥n ]
∋-inject₁⁻ {xs = xs ,[ _ ^ _ ]} Z = Z
∋-inject₁⁻ {xs = xs ,[ _ ^ _ ]} (S xs∋x) = S (∋-inject₁⁻ xs∋x)
∋-inject₁⁻ {xs = xs ++ ys} (L xs∋x) = L (∋-inject₁⁻ xs∋x)
∋-inject₁⁻ {xs = xs ++ ys} (R ys∋y) = R (∋-inject₁⁻ ys∋y)

-- | Introduce inject≥ into a membership relation.
∋-inject≥⁺ : (n≥n′ : n ≥‴ n′) → xs ∋[ x ^ m≥n ] → inject≥ n≥n′ xs ∋[ x ^ ≤‴-trans n≥n′ m≥n ]
∋-inject≥⁺ ≤‴-refl = id
∋-inject≥⁺ (≤‴-step n≥sn′) = ∋-inject₁⁺ ∘ ∋-inject≥⁺ n≥sn′

-- | xs ++ ys ,[ y ^ m≥n ] ⊆ xs ++ (ys ,[ y ^ m≥n ]).
∋-++-, : xs ++ ys ,[ y ^ m≥n ] ∋[ z ^ m′≥n ] → xs ++ (ys ,[ y ^ m≥n ]) ∋[ z ^ m′≥n ]
∋-++-, Z = R Z
∋-++-, (S (L xs∋z)) = L xs∋z
∋-++-, (S (R ys∋z)) = R (S ys∋z)

-- | xs ++ (ys ,[ y ^ m≥n ]) ⊆ xs ++ ys ,[ y ^ m≥n ].
∋-++-,⁻¹ : xs ++ (ys ,[ y ^ m≥n ]) ∋[ z ^ m′≥n ] → xs ++ ys ,[ y ^ m≥n ] ∋[ z ^ m′≥n ]
∋-++-,⁻¹ (L xs∋z) = S (L xs∋z)
∋-++-,⁻¹ (R (S ys∋z)) = S (R ys∋z)
∋-++-,⁻¹ (R Z) = Z

-- | xs ++ ys ++ zs ⊆ xs ++ (ys ++ zs).
∋-++-++ : xs ++ ys ++ zs ∋[ z ^ m≥n ] → xs ++ (ys ++ zs) ∋[ z ^ m≥n ]
∋-++-++ (L (L xs∋z)) = L xs∋z
∋-++-++ (L (R ys∋z)) = R (L ys∋z)
∋-++-++ (R zs∋z) = R (R zs∋z)

-- | xs ++ (ys ++ zs) ⊆ xs ++ ys ++ zs.
∋-++-++⁻¹ : xs ++ (ys ++ zs) ∋[ z ^ m≥n ] → xs ++ ys ++ zs ∋[ z ^ m≥n ]
∋-++-++⁻¹ (L xs∋z) = L (L xs∋z)
∋-++-++⁻¹ (R (L ys∋z)) = L (R ys∋z)
∋-++-++⁻¹ (R (R zs∋z)) = R zs∋z

-- | The result of inject₁ does not contain the item at stage n.
inject₁-∌-refl : ¬ (inject₁ xs ∋[ x ^ ≤‴-refl ])
inject₁-∌-refl {xs = xs ,[ _ ^ _ ]} (S xs∋x) = inject₁-∌-refl xs∋x
inject₁-∌-refl {xs = xs ++ ys} (L xs∋x) = inject₁-∌-refl xs∋x
inject₁-∌-refl {xs = xs ++ ys} (R ys∋y) = inject₁-∌-refl ys∋y

-- | Cast a membership relation from one staged list to another.
∋-castˡ : xs ≡ ys → xs ∋[ x ^ m≥n ] → ys ∋[ x ^ m≥n ]
∋-castˡ refl x = x

-- | Computation rule for ∋-castˡ and Z.
∋-castˡ-Z : ∀ (eq : xs ≡ ys) → ∋-castˡ (cong (_,[ x ^ m≥n ]) eq) Z ≡ Z
∋-castˡ-Z refl = refl

-- | Computation rule for ∋-castˡ and S.
∋-castˡ-S : ∀ (eq : xs ≡ ys) (xs∋x : xs ∋[ x ^ m≥n ]) → ∋-castˡ (cong (_,[ x′ ^ m′≥n ]) eq) (S xs∋x) ≡ S (∋-castˡ eq xs∋x)
∋-castˡ-S refl xs∋x = refl

-- | Computation rule for ∋-castˡ and L.
∋-castˡ-L : ∀ (eq₁ : xs₁ ≡ ys₁) (eq₂ : xs₂ ≡ ys₂) (xs∋x : xs₁ ∋[ x ^ m≥n ]) → ∋-castˡ (cong₂ (_++_) eq₁ eq₂) (L xs∋x) ≡ L (∋-castˡ eq₁ xs∋x)
∋-castˡ-L refl refl xs∋x = refl

-- | Computation rule for ∋-castˡ and R.
∋-castˡ-R : ∀ (eq₁ : xs₁ ≡ ys₁) (eq₂ : xs₂ ≡ ys₂) (xs∋x : xs₂ ∋[ x ^ m≥n ]) → ∋-castˡ (cong₂ (_++_) eq₁ eq₂) (R xs∋x) ≡ R (∋-castˡ eq₂ xs∋x)
∋-castˡ-R refl refl xs∋x = refl

-- | The ⊆ relation for staged lists.
-- We call it Rename since it renames the debrijn indices when the staged lists are used as contexts.
Rename : StagedList n → StagedList n → Set
Rename xs ys = ∀ {m} {x} {m≥n : m ≥‴ _} → xs ∋[ x ^ m≥n ] → ys ∋[ x ^ m≥n ]

-- | Extend a Rename by adding one identity mapping on the right.
ext : Rename xs ys → Rename (xs ,[ z ^ m≥n ]) (ys ,[ z ^ m≥n ])
ext ρ Z = Z
ext ρ (S xs∋x) = S (ρ xs∋x)

-- | Extend a Rename by adding identity mappings on the right.
ext++ : ∀ zs → Rename xs ys → Rename (xs ++ zs) (ys ++ zs)
ext++ zs ρ (L xs∋x) = L (ρ xs∋x)
ext++ zs ρ (R zs∋z) = R (zs∋z)

-- | Extend a Rename by adding identity mappings on the left.
ext++ˡ : ∀ zs → Rename xs ys → Rename (zs ++ xs) (zs ++ ys)
ext++ˡ zs ρ (L zs∋z) = L (zs∋z)
ext++ˡ zs ρ (R xs∋x) = R (ρ xs∋x)

-- | Restrict a Rename by removing mappings for items at stage n.
ext↾ : Rename xs ys → Rename (xs ↾) (ys ↾)
ext↾ ρ = ∋-↾⁺ ∘ ρ ∘ ∋-↾⁻ 

-- | Restrict a Rename by removing mappings for items below stage m.
ext↾≥ : ∀ (m≥n : m ≥‴ n) → Rename xs ys → Rename (xs ↾≥ m≥n) (ys ↾≥ m≥n)
ext↾≥ ≤‴-refl ρ = ρ
ext↾≥ (≤‴-step m≥sn) ρ = ext↾≥ m≥sn (ext↾ ρ)

-- | ext↾≥ followed by ext++.
ext↾≥++ : ∀ (m≥n : m ≥‴ n) zs → Rename xs ys → Rename (xs ↾≥ m≥n ++ zs) (ys ↾≥ m≥n ++ zs)
ext↾≥++ m≥n zs = ext++ zs ∘ ext↾≥ m≥n

-- | inject₁ on both sides of a Rename can be cancelled.
Rename-inject₁⁻ : ∀ {xs ys : StagedList (suc n)} → Rename (inject₁ xs) (inject₁ ys) → Rename xs ys
Rename-inject₁⁻ ρ = ∋-inject₁⁻ ∘ ρ ∘  ∋-inject₁⁺

-- | ↾ followed by inject₁ returns a sublist of the original staged list.
↾-inject₁ : (xs : StagedList n) → Rename (inject₁ (xs ↾)) xs
↾-inject₁ (xs ,[ x ^ ≤‴-refl ]) = S ∘ ↾-inject₁ xs
↾-inject₁ (xs ,[ x ^ ≤‴-step m≥n ]) Z = Z
↾-inject₁ (xs ,[ x ^ ≤‴-step m≥n ]) (S xs∋x) = S (↾-inject₁ xs xs∋x)
↾-inject₁ (xs ++ ys) (L xs∋x) = L (↾-inject₁ xs xs∋x)
↾-inject₁ (xs ++ ys) (R ys∋y) = R (↾-inject₁ ys ys∋y)

-- | xs ++ ys ⊆ xs ++♭ ys.
∋-++♭⁺ : ∀ ys → xs ++ ys ∋[ z ^ m≥n ] → xs ++♭ ys ∋[ z ^ m≥n ]
∋-++♭⁺ ∅ (L x) = x
∋-++♭⁺ (ys ,[ x ^ m≥n ]) = ext (∋-++♭⁺ ys) ∘ ∋-++-,⁻¹
∋-++♭⁺ (ys ++ ys′) = ∋-++♭⁺ ys′ ∘ ext++ ys′ (∋-++♭⁺ ys) ∘ ∋-++-++⁻¹

-- | xs ++♭ ys ⊆ xs ++ ys.
∋-++♭⁻ : ∀ ys → xs ++♭ ys ∋[ z ^ m≥n ] → xs ++ ys ∋[ z ^ m≥n ]
∋-++♭⁻ ∅ = L
∋-++♭⁻ (ys ,[ y ^ m≥n ]) = ∋-++-, ∘ ext (∋-++♭⁻ ys)
∋-++♭⁻ (ys ++ ys′) = ∋-++-++ ∘ ext++ ys′ (∋-++♭⁻ ys) ∘ ∋-++♭⁻ ys′

-- | Equivalence relation for functions that take membership witnesses as input.
module _ {B : ∀ (m : ℕ) (x : Item m) (m≥n : m ≥‴ n) → Set} where
  private variable
    f g h : ∀ {m} {x} {m≥n : m ≥‴ _} → xs ∋[ x ^ m≥n ] → B m x m≥n

  infix  _≗_
  _≗_ : (f g : ∀ {m} {x} {m≥n : m ≥‴ _} → xs ∋[ x ^ m≥n ] → B m x m≥n) → Set
  _≗_ {xs = xs} ρ ρ′ = ∀ {m} {x} {m≥n : m ≥‴ _} (xs∋x : xs ∋[ x ^ m≥n ]) → ρ xs∋x ≡ ρ′ xs∋x

  ≗-refl : f ≗ f
  ≗-refl _ = refl

  ≗-sym : f ≗ g → g ≗ f
  ≗-sym f≗g xs∋x = sym (f≗g xs∋x)

  ≗-trans : f ≗ g → g ≗ h → f ≗ h
  ≗-trans f≗g g≗h xs∋x = trans (f≗g xs∋x) (g≗h xs∋x)

-- Renaming properties

-- | ∋-↾⁻ is left-inverse of ∋-↾⁺.
∋-↾⁻-∋-↾⁺ : (xs∋x : xs ∋[ x ^ ≤‴-step m≥n ]) → ∋-↾⁻ (∋-↾⁺ xs∋x) ≡ xs∋x
∋-↾⁻-∋-↾⁺ Z = refl
∋-↾⁻-∋-↾⁺ (S {m′≥n = ≤‴-refl} xs∋x) = cong S (∋-↾⁻-∋-↾⁺ xs∋x)
∋-↾⁻-∋-↾⁺ (S {m′≥n = ≤‴-step _} xs∋x) = cong S (∋-↾⁻-∋-↾⁺ xs∋x)
∋-↾⁻-∋-↾⁺ (L xs∋x) = cong L (∋-↾⁻-∋-↾⁺ xs∋x)
∋-↾⁻-∋-↾⁺ (R xs∋x) = cong R (∋-↾⁻-∋-↾⁺ xs∋x)

-- | ∋-↾⁺ is left-inverse of ∋-↾⁻.
∋-↾⁺-∋-↾⁻ : (xs∋x : xs ↾ ∋[ x ^ m≥n ]) → ∋-↾⁺ (∋-↾⁻ {xs = xs} xs∋x) ≡ xs∋x
∋-↾⁺-∋-↾⁻ {xs = xs ,[ _ ^ ≤‴-refl ]} xs∋x = ∋-↾⁺-∋-↾⁻ {xs = xs} xs∋x
∋-↾⁺-∋-↾⁻ {xs = xs ,[ x ^ ≤‴-step m≥n ]} Z = refl
∋-↾⁺-∋-↾⁻ {xs = xs ,[ _ ^ ≤‴-step _ ]} (S xs∋x) = cong S (∋-↾⁺-∋-↾⁻ {xs = xs} xs∋x)
∋-↾⁺-∋-↾⁻ {xs = xs ++ _} (L x) = cong L (∋-↾⁺-∋-↾⁻ {xs = xs} x)
∋-↾⁺-∋-↾⁻ {xs = _ ++ xs} (R x) = cong R (∋-↾⁺-∋-↾⁻ {xs = xs} x)

-- | ∋-inject₁⁻ is left-inverse of ∋-inject₁⁺.
∋-inject₁⁻-∋-inject₁⁺ : (xs∋x : xs ∋[ x ^ m≥n ]) → ∋-inject₁⁻ (∋-inject₁⁺ xs∋x) ≡ xs∋x
∋-inject₁⁻-∋-inject₁⁺ Z = refl
∋-inject₁⁻-∋-inject₁⁺ (S xs∋x) = cong S (∋-inject₁⁻-∋-inject₁⁺ xs∋x)
∋-inject₁⁻-∋-inject₁⁺ (L xs∋x) = cong L (∋-inject₁⁻-∋-inject₁⁺ xs∋x)
∋-inject₁⁻-∋-inject₁⁺ (R xs∋x) = cong R (∋-inject₁⁻-∋-inject₁⁺ xs∋x)

-- | ∋-inject₁⁺ is left-inverse of ∋-inject₁⁻.
∋-inject₁⁺-∋-inject₁⁻ : ∀ {xs : StagedList (suc n)} (xs∋x : inject₁ xs ∋[ x ^ ≤‴-step m≥n ]) → ∋-inject₁⁺ (∋-inject₁⁻ xs∋x) ≡ xs∋x
∋-inject₁⁺-∋-inject₁⁻ {xs = xs ,[ x ^ m≥n ]} Z = refl
∋-inject₁⁺-∋-inject₁⁻ {xs = xs ,[ x ^ m≥n ]} (S xs∋x) = cong S (∋-inject₁⁺-∋-inject₁⁻ xs∋x)
∋-inject₁⁺-∋-inject₁⁻ {xs = xs ++ xs₁} (L xs∋x) = cong L (∋-inject₁⁺-∋-inject₁⁻ xs∋x)
∋-inject₁⁺-∋-inject₁⁻ {xs = xs ++ xs₁} (R xs∋x) = cong R (∋-inject₁⁺-∋-inject₁⁻ xs∋x)

-- | ∋-inject₁⁻ ∋-↾⁻ ∋-↾⁺ ∋-inject₁⁺ is identity.
∋-inject₁⁻-∋-↾⁻-∋-↾⁺-∋-inject₁⁺ : ∀ (xs∋x : xs ∋[ x ^ m≥n ]) → ∋-inject₁⁻ (∋-↾⁻ (∋-↾⁺ (∋-inject₁⁺ xs∋x))) ≡ xs∋x
∋-inject₁⁻-∋-↾⁻-∋-↾⁺-∋-inject₁⁺ xs∋x = trans (cong ∋-inject₁⁻ (∋-↾⁻-∋-↾⁺ (∋-inject₁⁺ xs∋x))) (∋-inject₁⁻-∋-inject₁⁺ xs∋x)

-- | ∋-↾⁺ ∋-inject₁⁺ ∋-inject₁⁻ ∋-↾⁻ is identity.
∋-↾⁺-∋-inject₁⁺-∋-inject₁⁻-∋-↾⁻ : ∀ {xs : StagedList (suc n)} (xs∋x : inject₁ xs ↾ ∋[ x ^ m≥n ]) → ∋-↾⁺ (∋-inject₁⁺ {xs = xs} (∋-inject₁⁻ (∋-↾⁻ xs∋x))) ≡ xs∋x
∋-↾⁺-∋-inject₁⁺-∋-inject₁⁻-∋-↾⁻ {xs = xs} xs∋x = trans (cong ∋-↾⁺ (∋-inject₁⁺-∋-inject₁⁻ {xs = xs} (∋-↾⁻ xs∋x))) (∋-↾⁺-∋-↾⁻ {xs = inject₁ xs} xs∋x)

-- | ext respects the _≗_ relation.
ext-resp-≗ : {ρ ρ′ : Rename xs ys} → ρ ≗ ρ′ → ext {z = z} {m≥n = m≥n} ρ ≗ ext ρ′
ext-resp-≗ ρ≗ρ′ Z = refl
ext-resp-≗ ρ≗ρ′ (S _) = cong S (ρ≗ρ′ _)

-- | ext++ respects the _≗_ relation.
ext++-resp-≗ : ∀ zs → {ρ ρ′ : Rename xs ys} → ρ ≗ ρ′ → ext++ zs ρ ≗ ext++ zs ρ′
ext++-resp-≗ zs ρ≗ρ′ (L _) = cong L (ρ≗ρ′ _)
ext++-resp-≗ zs ρ≗ρ′ (R _) = refl

-- | ext↾ respects the _≗_ relation.
ext↾-resp-≗ : {ρ ρ′ : Rename xs ys} → ρ ≗ ρ′ → ext↾ ρ ≗ ext↾ ρ′
ext↾-resp-≗ ρ≗ρ′ = cong ∋-↾⁺ ∘ ρ≗ρ′ ∘ ∋-↾⁻

-- | ext↾≥ respects the _≗_ relation.
ext↾≥-resp-≗ : ∀ (m≥n : m ≥‴ n) → {ρ ρ′ : Rename xs ys} → ρ ≗ ρ′ → ext↾≥ m≥n ρ ≗ ext↾≥ m≥n ρ′
ext↾≥-resp-≗ ≤‴-refl ρ≗ρ′ = ρ≗ρ′
ext↾≥-resp-≗ (≤‴-step m≥n) ρ≗ρ′ = ext↾≥-resp-≗ m≥n (ext↾-resp-≗ ρ≗ρ′)

-- | ext id ≗ id
ext-id : ext {xs = xs} {z = z} {m≥n = m≥n} id ≗ id
ext-id Z = refl
ext-id (S _) = refl

-- | ext distributes over composition of renamings.
ext-∘ : (ρ′ : Rename xs₂ xs₃) → (ρ : Rename xs₁ xs₂) → ext {z = z} {m≥n = m≥n} (ρ′ ∘ ρ) ≗ ext ρ′ ∘ ext ρ
ext-∘ ρ′ ρ Z = refl
ext-∘ ρ′ ρ (S _) = refl

-- | ext++ zs id ≗ id
ext++-id : ∀ (zs : StagedList n) → ext++ {xs = xs} zs id ≗ id
ext++-id zs (L _) = refl
ext++-id zs (R _) = refl 

-- | ext++ zs distributes over composition of renamings.
ext++-∘ : (zs : StagedList n) → (ρ′ : Rename xs₂ xs₃) → (ρ : Rename xs₁ xs₂) → ext++ zs (ρ′ ∘ ρ) ≗ ext++ zs ρ′ ∘ ext++ zs ρ
ext++-∘ zs ρ′ ρ (L _) = refl
ext++-∘ zs ρ′ ρ (R _) = refl

-- | ext↾ id ≗ id
ext↾-id : ext↾ {xs = xs} id ≗ id
ext↾-id {xs = xs ,[ x ^ ≤‴-refl ]} xs∋x = ext↾-id {xs = xs} xs∋x
ext↾-id {xs = xs ,[ x ^ ≤‴-step m≥n ]} Z = refl
ext↾-id {xs = xs ,[ x ^ ≤‴-step m≥n ]} (S xs∋x) = cong S (ext↾-id {xs = xs} xs∋x)
ext↾-id {xs = xs ++ ys} (L xs∋x) = cong L (ext↾-id {xs = xs} xs∋x)
ext↾-id {xs = xs ++ ys} (R ys∋x) = cong R (ext↾-id {xs = ys} ys∋x)

-- | ext↾ distributes over composition of renamings.
ext↾-∘ : (ρ′ : Rename xs₂ xs₃) → (ρ : Rename xs₁ xs₂) → ext↾ (ρ′ ∘ ρ) ≗ ext↾ ρ′ ∘ ext↾ ρ
ext↾-∘ {xs₁ = xs₁ ,[ x ^ m≥n ]} ρ′ ρ xs∋x = cong (∋-↾⁺ ∘ ρ′) (sym (∋-↾⁻-∋-↾⁺ _))
ext↾-∘ {xs₁ = xs ++ ys} ρ′ ρ (L xs∋x) = cong (∋-↾⁺ ∘ ρ′) ((sym (∋-↾⁻-∋-↾⁺ _)))
ext↾-∘ {xs₁ = xs ++ ys} ρ′ ρ (R ys∋x) = cong (∋-↾⁺ ∘ ρ′) ((sym (∋-↾⁻-∋-↾⁺ _)))

-- | Commutation of ext↾ and ∋-↾⁺.
ext↾-∋-↾⁺ : (ρ : Rename xs ys) (xs∋x : xs ∋[ x ^ ≤‴-step m≥n ]) → ext↾ ρ (∋-↾⁺ xs∋x) ≡ ∋-↾⁺ (ρ xs∋x)
ext↾-∋-↾⁺ ρ Z = refl
ext↾-∋-↾⁺ ρ (S {m′≥n = ≤‴-refl} xs∋x) = cong (∋-↾⁺ ∘ ρ ∘ S) (∋-↾⁻-∋-↾⁺ xs∋x)
ext↾-∋-↾⁺ ρ (S {m′≥n = ≤‴-step _} xs∋x) = cong (∋-↾⁺ ∘ ρ ∘ S) (∋-↾⁻-∋-↾⁺ xs∋x)
ext↾-∋-↾⁺ ρ (L xs∋x) = ext↾-∋-↾⁺ (ρ ∘ L) xs∋x
ext↾-∋-↾⁺ ρ (R xs∋x) = ext↾-∋-↾⁺ (ρ ∘ R) xs∋x

-- | ext↾≥ m≥n id ≗ id
ext↾≥-id : ∀ (m≥n : m ≥‴ n) → ext↾≥ {xs = xs} m≥n id ≗ id
ext↾≥-id ≤‴-refl = ≗-refl {f = id}
ext↾≥-id {xs = xs} (≤‴-step m≥n) = ≗-trans (ext↾≥-resp-≗ m≥n (ext↾-id {xs = xs})) (ext↾≥-id m≥n)

-- | ext↾≥ m≥n distributes over composition of renamings.
ext↾≥-∘ :  ∀ (m≥n : m ≥‴ n) → (ρ′ : Rename xs₂ xs₃) → (ρ : Rename xs₁ xs₂) → ext↾≥ m≥n (ρ′ ∘ ρ) ≗ ext↾≥ m≥n ρ′ ∘ ext↾≥ m≥n ρ
ext↾≥-∘ ≤‴-refl ρ′ ρ = ≗-refl {f = (ρ′ ∘ ρ)}
ext↾≥-∘ (≤‴-step m≥n) ρ′ ρ = ≗-trans ((ext↾≥-resp-≗ m≥n (ext↾-∘ ρ′ ρ))) (ext↾≥-∘ m≥n (ext↾ ρ′) (ext↾ ρ))

-- | Rename-inject₁⁻ id ≗ id
Rename-inject₁⁻-id : ∀ {xs : StagedList (suc n)} → Rename-inject₁⁻ {xs = xs} id ≗ id
Rename-inject₁⁻-id Z = refl
Rename-inject₁⁻-id (S x) = cong S (Rename-inject₁⁻-id x)
Rename-inject₁⁻-id (L x) = cong L (Rename-inject₁⁻-id x)
Rename-inject₁⁻-id (R x) = cong R (Rename-inject₁⁻-id x)

-- | Rename-inject₁⁻ R ≗ R
Rename-inject₁⁻-R : ∀ {xs ys : StagedList (suc n)} → Rename-inject₁⁻ {xs = ys} (R {xs = inject₁ xs}) ≗ R
Rename-inject₁⁻-R Z = refl
Rename-inject₁⁻-R (S x) = cong (R ∘ S) (Rename-inject₁⁻-id x)
Rename-inject₁⁻-R (L x) = cong (R ∘ L) (Rename-inject₁⁻-id x)
Rename-inject₁⁻-R (R x) = cong (R ∘ R) (Rename-inject₁⁻-id x)

-- | Rename-inject₁⁻ L ≗ L
Rename-inject₁⁻-L : ∀ {xs ys : StagedList (suc n)} → Rename-inject₁⁻ {xs = xs} (L {ys = inject₁ ys}) ≗ L
Rename-inject₁⁻-L Z = refl
Rename-inject₁⁻-L (S x) = cong (L ∘ S) (Rename-inject₁⁻-id x)
Rename-inject₁⁻-L (L x) = cong (L ∘ L) (Rename-inject₁⁻-id x)
Rename-inject₁⁻-L (R x) = cong (L ∘ R) (Rename-inject₁⁻-id x)

-- The following code defines the # operator, which converts a natural number to a membership witness in a staged list.

-- | The length of a staged list.
length : StagedList n → ℕ
length ∅ = zero
length (xs ,[ _ ^ _ ]) = suc (length xs)
length (xs ++ ys) = length ys + length xs

-- | Lookup the k-th item in a staged list, given a proof that k is less than the length of the list.
lookupℕ : {xs : StagedList n} → {k : ℕ} → (p : k < length xs) → ∃[ m ] (Item m × m ≥‴ n)
lookupℕ {xs = xs ,[ x ^ m≥n ]} {k = zero} (s≤s z≤n) = -, x P., m≥n
lookupℕ {xs = xs ,[ _ ^ _ ]} {k = suc k} (s≤s p) = lookupℕ {xs = xs} p
lookupℕ {xs = xs ++ ys} {k = k} p with k ℕ.<? (length ys)
... | yes p′ = lookupℕ {xs = ys} p′
... | no k≮ny = lookupℕ {xs = xs} {k = k ∸ length ys} (ℕ.+-cancelʳ-< (length ys) _ _ (
  begin
      suc (k ∸ length ys + length ys)
    ≡⟨ cong suc (m∸n+n≡m (≮⇒≥ k≮ny)) ⟩
      suc k
    ≤⟨ p ⟩
      length ys + length xs
    ≡⟨ ℕ.+-comm (length ys) (length xs) ⟩
      length xs + length ys
  ∎))
  where open ℕ.≤-Reasoning

-- | Membership witness for the result of lookupℕ.
countℕ : {xs : StagedList n} → {k : ℕ} → (p : k < length xs) → xs ∋[ lookupℕ {xs = xs} p .proj₂ .proj₁ ^ lookupℕ {xs = xs} p .proj₂ .proj₂ ]
countℕ {xs = xs ,[ x ^ m≥n ]} {k = zero} (s≤s z≤n) = Z
countℕ {xs = xs ,[ x ^ m≥n ]} {k = suc k} (s≤s p) = S (countℕ p)
countℕ {xs = xs ++ ys} {k = k} p with k ℕ.<? (length ys)
... | yes p′ = R (countℕ {xs = ys} _)
... | no _ = L (countℕ {xs = xs} _)

-- | Convert a natural number to a membership witness in a staged list.
# : ∀ {xs : StagedList n}
  → (k : ℕ)
  → {k∈Γ : True (k <? length xs)}
    --------------------------------
  → xs ∋[ lookupℕ {xs = xs} (toWitness k∈Γ) .proj₂ .proj₁ ^ lookupℕ {xs = xs} (toWitness k∈Γ) .proj₂ .proj₂ ]
# n {k∈Γ} = countℕ (toWitness k∈Γ)