Quick an Dirty transformation of the STO instance for String

AVLString.agda

open import Level
import Data.AVL.Sets
open import Data.String as String
open import Relation.Binary using (module StrictTotalOrder)

open import Data.Product
open import Function
open import Relation.Binary


record RawIso {ℓ : Level} (A B : Set ℓ) : Set ℓ where
  field
    push : A → B
    pull : B → A
open RawIso public

RawIso-IsEquivalence :
  {ℓ ℓ′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) → IsEquivalence R → IsEquivalence R′
RawIso-IsEquivalence iso isEq = let open IsEquivalence isEq in
  record { refl  = push iso refl
         ; sym   = push iso ∘ sym ∘ pull iso
         ; trans = λ p q → push iso $ trans (pull iso p) (pull iso q) }

RawIso-Trichotomous :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  Trichotomous R O → Trichotomous R′ O
RawIso-Trichotomous iso tri x y with tri x y
... | tri< a ¬b ¬c = tri< a (¬b ∘ pull iso) ¬c
... | tri≈ ¬a b ¬c = tri≈ ¬a (push iso b) ¬c
... | tri> ¬a ¬b c = tri> ¬a (¬b ∘ pull iso) c

RawIso-Respects₂ :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  O Respects₂ R → O Respects₂ R′
RawIso-Respects₂ iso (b , f) = b ∘ pull iso
                             , f ∘ pull iso

RawIso-IsStrictTotalOrder :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  IsStrictTotalOrder R O → IsStrictTotalOrder R′ O
RawIso-IsStrictTotalOrder {A = A} iso isSTO = let open IsStrictTotalOrder isSTO in
  record { isEquivalence = RawIso-IsEquivalence iso isEquivalence
         ; trans         = trans
         ; compare       = RawIso-Trichotomous iso compare
         ; <-resp-≈      = RawIso-Respects₂ iso <-resp-≈ }

import Data.Nat.Properties as NatProp
open import Data.List
open import Data.Char
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
import Relation.Binary.List.Pointwise as Ptwise

toNat-injective : {c d : Char} → toNat c ≡ toNat d → c ≡ d
toNat-injective {c} pr with toNat c
toNat-injective refl | ._ = trustMe -- probably unsafe
  where open import Relation.Binary.PropositionalEquality.TrustMe


rawIso : {a b : String} → RawIso ((Ptwise.Rel (_≡_ on toNat) on toList) a b) (a ≡ b)
rawIso {a} {b} = record { push = `push ; pull = `pull } where

  `push : {a b : String} → (Ptwise.Rel (_≡_ on toNat) on toList) a b → a ≡ b
  `push {a} {b} pr =
    begin
      a                   ≡⟨ sym (fromList∘toList a) ⟩
      fromList (toList a) ≡⟨ cong fromList (aux pr) ⟩
      fromList (toList b) ≡⟨ fromList∘toList b ⟩
      b
    ∎ where

     aux : {xs ys : List Char} → Ptwise.Rel (_≡_ on toNat) xs ys → xs ≡ ys
     aux = Ptwise.rec (λ {xs} {ys} _ → xs ≡ ys) (cong₂ _∷_ ∘ toNat-injective) refl

  `pull : {a b : String} → a ≡ b → (Ptwise.Rel (_≡_ on toNat) on toList) a b
  `pull refl = Ptwise.refl refl

stringSTO : IsStrictTotalOrder (StrictTotalOrder._≈_ String.strictTotalOrder) (StrictTotalOrder._<_ String.strictTotalOrder)
stringSTO = StrictTotalOrder.isStrictTotalOrder String.strictTotalOrder

open Data.AVL.Sets (RawIso-IsStrictTotalOrder rawIso stringSTO)