a reversed ascending list descends, by general abstract nonsense

Reverse2.agda

{-# OPTIONS --postfix-projections #-}
open import Data.List using (List; []; _∷_; _++_)
open import Function using (flip)
open import Level
open import Relation.Binary using (Rel; _=[_]⇒_)
open import Relation.Binary.PropositionalEquality

module Reverse2 where

-- Some general abstract nonsense.
record Preord {A : Set} (R : Rel A zero) : Set where
  field ident : ∀{a} → R a a
  field compo : ∀{a b c} → R a b → R b c → R a c

open Preord public
open Preord {{...}} public renaming (ident to id; compo to _∙_)

instance
  -- Used in rev∷. Often useful elsewhere in my experience.
  equals : ∀{A} → Preord {A} _≡_
  Preord.ident equals = refl
  Preord.compo equals refl refl = refl

-- I'd like to make this an instance but it makes Agda instance search overflow
-- its stack, since flip can be applied indefinitely.
opp : ∀{A R} → Preord {A} (flip R) → Preord R
opp C .ident = ident C
opp C .compo  = flip (compo C)


-- Adjoining -∞ and ∞ in a generic way.
data Bound (A : Set) : Set where
  -∞ ∞ : Bound A
  # : A → Bound A

data Bound≤ {A} (R : A → A → Set) : Bound A → Bound A → Set where
  -∞ : ∀{a} → Bound≤ R -∞ a
  ∞ : ∀{a} → Bound≤ R a ∞
  # : ∀{a b} → R a b → Bound≤ R (# a) (# b)

instance
  bounds : ∀{A R} {{_ : Preord {A} R}} → Preord (Bound≤ R)
  bounds .ident { -∞} = -∞; bounds .ident {∞} = ∞; bounds .ident {# x} = # id
  bounds .compo -∞ _ = -∞; bounds .compo _ ∞ = ∞; bounds .compo (# p) (# q) = # (p ∙ q)

-- Order inversion on bounded types.
invert : ∀{A} → Bound A → Bound A
invert -∞ = ∞; invert ∞ = -∞; invert (# x) = # x

invert-mono : ∀{A R} → flip (Bound≤ {A} R) =[ invert ]⇒ Bound≤ (flip R)
invert-mono -∞ = ∞; invert-mono ∞ = -∞; invert-mono (# x) = # x


-- When is a list sorted between two bounds?
module _ {A : Set} (_≺_ : Rel A zero) where
  private _⊏_ = Bound≤ _≺_
  data Sorted (lo hi : Bound A) : List A → Set where
    nil : lo ⊏ hi → Sorted lo hi []
    _∷_ : ∀{x L} → lo ⊏ # x → Sorted (# x) hi L → Sorted lo hi (x ∷ L)

  module _ {{P : Preord _≺_}} where
    sorted≤ : ∀{lo mid hi L} → lo ⊏ mid → Sorted mid hi L → Sorted lo hi L
    sorted≤ p (nil q) = nil (p ∙ q)
    sorted≤ p (q ∷ S) = p ∙ q ∷ S

    sorted++ : ∀{lo mid hi L₁ L₂} → Sorted lo mid L₁ → Sorted mid hi L₂ → Sorted lo hi (L₁ ++ L₂)
    sorted++ (nil p) S₂ = sorted≤ p S₂
    sorted++ (p ∷ S₁) S₂ = p ∷ sorted++ S₁ S₂


-- Parameterise over a preordered type of list elements and a reverse function.
postulate
  A : Set
  _≺_ : Rel A zero
  instance preord≺ : Preord _≺_
  reverse : List A → List A
  rev++ : ∀ x y → reverse (x ++ y) ≡ reverse y ++ reverse x
  rev1 : ∀ x → reverse (x ∷ []) ≡ x ∷ []
  -- it should be possible to prove rev[] from rev++, but it's annoying
  rev[] : reverse [] ≡ []

instance opp≺ = opp preord≺

rev∷ : ∀ x L → reverse (x ∷ L) ≡ reverse L ++ (x ∷ [])
rev∷ x L = rev++ (x ∷ []) L ∙ cong (reverse L ++_) (rev1 x)

rev : ∀{L lo hi} → Sorted _≺_ lo hi L → Sorted (flip _≺_) (invert hi) (invert lo) (reverse L)
rev (nil p) = subst (Sorted _ _ _) (sym rev[]) (nil (invert-mono p))
rev {x ∷ L} (p ∷ S) rewrite rev∷ x L = sorted++ _ (rev S) (id ∷ nil (invert-mono p))

-- Every step is obvious but there are too many of them.

Hmm. The fact you can't reuse the machinery in Data.AVL.Key because
it's all relying on the fact that you have a StrictTotalOrder is quite annoying.

I've opened an issue: agda/agda-stdlib#437