Reversing an ascending list in Agda

AscList.agda

-- Reversing an ascending list in Agda.
-- Challenge by @arntzenius: https://twitter.com/arntzenius/status/1034919539467677696
module AscList where

-- We'll go without libraries to make things clearer.

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A → B → C) → B → A → C
flip f x y = f y x

-- Step one is to define ordered lists. We'll roughly follow Conor McBride's approach
-- from How to keep your neighbours in order [1].

-- Lists will be indexed by upper and lower bounds. An unrestricted list is bounded by
-- -∞ and ∞.
data Bound (A : Set) : Set where
  -∞ : Bound A
  #  : A → Bound A
  ∞  : Bound A

-- Any relation on A can be lifted to Bound A. As expected -∞ is smaller than anything
-- and ∞ is bigger than anything.
data liftB {A : Set} (_≤_ : A → A → Set) : (lo hi : Bound A) → Set where
  -∞≤ : ∀ {b} → liftB _≤_ -∞ b
  ≤∞  : ∀ {b} → liftB _≤_ b ∞
  #   : ∀ {x y} → x ≤ y → liftB _≤_ (# x) (# y)

-- Now, given an A and a relation _≤_ over A we can define ascending lists of A's.
module _ {A : Set} (_≤_ : A → A → Set) where

  private _≤ᵇ_ = liftB _≤_

  data AscendingList (lo hi : Bound A) : Set where

    -- The empty list can have any bounds you like, as long as the lower bound is
    -- below the upper bound.
    nil  : lo ≤ᵇ hi → AscendingList lo hi

    -- When consing an element x onto a list xs, x needs to be above the expected
    -- lower bound and x should be a lower bound for xs. The upper bound is enforced
    -- by the fact that xs is bounded by # x and hi.
    cons : (x : A) → lo ≤ᵇ # x → AscendingList (# x) hi → AscendingList lo hi

-- A descending list is an ascending list with the ordering flipped, but we also need to flip
-- -∞ and ∞.

flipB : ∀ {A} → Bound A → Bound A
flipB -∞    = ∞
flipB (# x) = # x
flipB ∞     = -∞

DescendingList : {A : Set} (_≤_ : A → A → Set) (lo hi : Bound A) → Set
DescendingList _≤_ hi lo = AscendingList (flip _≤_) (flipB hi) (flipB lo)

-- So, DescendingList _≤_ ∞ -∞ = AscendingList (flip _≤_) -∞ ∞.

-- Those are all the definitions we'll need. Time to get reversing.

module _ {A : Set} {_≤_ : A → A → Set} where

  -- Let's have some nicer names for ordering proofs. The proofs in the ascending list
  -- will be _≤ᵇ_s, and the proofs in the descending list should be _≥ᵇ_s.
  private
    _≤ᵇ_ = liftB _≤_
    _≥ᵇ_ = λ hi lo → liftB (flip _≤_) (flipB hi) (flipB lo)

  -- Turning one into the other is straightforward.
  flip≤ᵇ : ∀ {lo hi} → lo ≤ᵇ hi → hi ≥ᵇ lo
  flip≤ᵇ -∞≤    = ≤∞
  flip≤ᵇ ≤∞     = -∞≤
  flip≤ᵇ (# lt) = # lt

  -- Usually the helper function for reverse takes two lists, one to be reversed and one
  -- accumulator for the result. In this case however we need to be a bit more precise about
  -- the bounds, so we take the element that should go next on the accumulator as a separate
  -- argument. This also makes shuffling of the proofs easier: note how the x≤y proof moves
  -- from the cons cell of y to the cons cell of x when reversing.
  rev : ∀ {lo hi} (x : A) → AscendingList _≤_ (# x) hi → DescendingList _≤_ (# x) lo →
                            DescendingList _≤_ hi lo
  rev x (nil x≤hi)      ys = cons x (flip≤ᵇ x≤hi) ys
  rev x (cons y x≤y xs) ys = rev y xs (cons x (flip≤ᵇ x≤y) ys)

  -- Since rev requires an element we need to match on the list in reverse as well. Fortunately
  -- the nil case is trivial.
  reverse : ∀ {lo hi} → AscendingList _≤_ lo hi → DescendingList _≤_ hi lo
  reverse (nil lt)       = nil (flip≤ᵇ lt)
  reverse (cons x lt xs) = rev x xs (nil (flip≤ᵇ lt))

-- [1] https://scholar.google.se/scholar?q=How+to+Keep+Your+Neighbours+in+Order