If you look at Data.AVL.Sets , you will see that it is parameterized by the strict full order associated with the _≡_ equivalence _≡_ (defined in Relation.Binary.PropositionalEquality ):
module Data.AVL.Sets {k ℓ} {Key : Set k} {_<_ : Rel Key ℓ} (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where
Now we can see how strict general ordering is defined on a String . First, we convert String to List Char , and then compare them based on strict lexicographic ordering for lists:
strictTotalOrder = On.strictTotalOrder (StrictLex.<-strictTotalOrder Char.strictTotalOrder) toList
If we dig into the code for StrictLex.<-strictTotalOrder , we can see that the equivalence relation associated with our List of Char is built using the pointwise lift Pointwise.isEquivalence that the equivalence relation for Char is equal.
But Pointwise.isEquivalence defined in terms of this data type:
data Rel {ab ℓ} {A : Set a} {B : Set b} (_∼_ : REL AB ℓ) : List A → List B → Set (a ⊔ b ⊔ ℓ) where [] : Rel _∼_ [] [] _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Rel _∼_ xs ys) → Rel _∼_ (x ∷ xs) (y ∷ ys)
Therefore, when Agda expects a strict general order associated with _≡_ , we instead provide it with a strict overall order associated with Rel _ on toList , which has no chance of merging.
How do we move on? Well, you can define your own strict general order in lines. Alternatively, you can try turning the current into one, where _≡_ is equivalence. This is what I am going to do the rest of this post.
So, I want to reuse IsStrictTotalOrder RO with a different equivalence relation R′ . The trick is that if you can transfer values from R ab to R′ ab , then I have to be fine! Therefore, I introduce the concept of RawIso AB , which says that we can always transfer values from A to B and vice versa:
record RawIso {ℓ : Level} (AB : Set ℓ) : Set ℓ where field push : A → B pull : B → A open RawIso public
Then we can prove that RawIso retains many properties:
RawIso-IsEquivalence : {ℓ ℓ′ : Level} {A : Set ℓ} {RR′ : Rel A ℓ′} → (iso : {ab : A} → RawIso (R ab) (R′ ab)) → IsEquivalence R → IsEquivalence R′ RawIso-IsEquivalence = ... RawIso-Trichotomous : {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {RR′ : Rel A ℓ′} {O : Rel A ℓ′′} → (iso : {ab : A} → RawIso (R ab) (R′ ab)) → Trichotomous RO → Trichotomous R′ O RawIso-Trichotomous = ... RawIso-Respects₂ : {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {RR′ : Rel A ℓ′} {O : Rel A ℓ′′} → (iso : {ab : A} → RawIso (R ab) (R′ ab)) → O Respects₂ R → O Respects₂ R′ RawIso-Respects₂ = ...
All these lemmas can be combined to prove that under strict general order we can build a new one through RawIso :
RawIso-IsStrictTotalOrder : {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {RR′ : Rel A ℓ′} {O : Rel A ℓ′′} → (iso : {ab : A} → RawIso (R ab) (R′ ab)) → IsStrictTotalOrder RO → IsStrictTotalOrder R′ O RawIso-IsStrictTotalOrder = ...
Now that we know that we can transport strict total orders along these RawIso s, we just need to prove that the equivalence relation used by the strict full order defined in Data.String is in RawIso with propositional equality. This is (almost) just a matter of expanding definitions. The only problem is that symbol equality is determined first by converting them to natural numbers, and then using propositional equality. But the toNat used toNat not have a specific property (compare, for example, toList and fromList , which are said to be inverse)! I threw this hack, and I think that everything should be fine, but if someone has a better solution, I would love to know about it!
toNat-injective : {cd : 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
In any case, now that you have it, you can expand the definitions and prove:
rawIso : {ab : String} → RawIso ((Ptwise.Rel (_≡_ on toNat) on toList) ab) (a ≡ b) rawIso {a} {b} = record { push = `push ; pull = `pull } where `push : {ab : String} → (Ptwise.Rel (_≡_ on toNat) on toList) ab → 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 : {ab : String} → a ≡ b → (Ptwise.Rel (_≡_ on toNat) on toList) ab `pull refl = Ptwise.refl refl
What allow
stringSTO : IsStrictTotalOrder _ _ stringSTO = StrictTotalOrder.isStrictTotalOrder String.strictTotalOrder open Data.AVL.Sets (RawIso-IsStrictTotalOrder rawIso stringSTO)
Phew!
I downloaded raw gist so you can easily access the code, see the import, etc.