Lexicographic ordering of pairs/lists in Agda using the standard library

Question

The Agda standard library contains some modules Relation.Binary.*.(Non)StrictLex (currently only for Product and List). We can use these modules to easily construct an instance of, for example, IsStrictTotalOrder for pairs of natural numbers (i.e. ℕ × ℕ).

open import Data.Nat as ℕ using (ℕ; _<_)
open import Data.Nat.Properties as ℕ
open import Relation.Binary using (module StrictTotalOrder; IsStrictTotalOrder)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Binary.Product.StrictLex using (×-Lex; _×-isStrictTotalOrder_)
open import Relation.Binary.Product.Pointwise using (_×-Rel_)

ℕ-isSTO : IsStrictTotalOrder _≡_ _<_
ℕ-isSTO = StrictTotalOrder.isStrictTotalOrder ℕ.strictTotalOrder

ℕ×ℕ-isSTO : IsStrictTotalOrder (_≡_ ×-Rel _≡_) (×-Lex _≡_ _<_ _<_)
ℕ×ℕ-isSTO = ℕ-isSTO ×-isStrictTotalOrder ℕ-isSTO

This creates an instance using the pointwise equality _≡_ ×-Rel _≡_. In the case of propositional equality, this should be equivalent to using just propositional equality.

Is there an easy way of converting the instance above to an instance of type IsStrictTotalOrder _≡_ (×-Lex _≡_ _<_ _<_), using normal propositional equality?

Answer 1

The definition given by @Cactus seems a bit too elaborate: only the core of the argument, the function/lemma compare seems relevant... Accordingly, for the current master branch of agda/agda-stdlib:

open import Data.Nat as ℕ using (ℕ; _<_)
open import Data.Nat.Properties as ℕ
open import Data.Product.Base using (_,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
  using (≡×≡⇒≡; ≡⇒≡×≡)
open import Data.Product.Relation.Binary.Lex.Strict
  using (×-Lex; ×-isStrictTotalOrder)
open import Function.Base using (_∘_)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _⇔_)
open import Relation.Binary.Definitions using (Trichotomous; tri<; tri≈; tri>)
open import Relation.Binary.Structures using (IsStrictTotalOrder)
open import Relation.Binary.PropositionalEquality using (_≡_; isEquivalence)

private
  variable
    a ℓ₁ ℓ₂ : Level
    A : Set a

------------------------------------------------------------------------
-- The `compare` lemma: stability of `Trichotomous` under equivalence
-- between the underlying equality relations

Trichotomous⇔ : ∀ {_≈₁_ : Rel A ℓ₁} {_≈₂_ : Rel A ℓ₂} (eq : _≈₁_ ⇔ _≈₂_) →
                {_<_ : Rel A a} → Trichotomous  _≈₁_ _<_ → Trichotomous  _≈₂_ _<_
Trichotomous⇔ (≈₁⇒≈₂ , ≈₂⇒≈₁) tri x y with tri x y
... | tri< a ¬b ¬c = tri< a (¬b ∘ ≈₂⇒≈₁) ¬c
... | tri≈ ¬a b ¬c = tri≈ ¬a (≈₁⇒≈₂ b) ¬c
... | tri> ¬a ¬b c = tri> ¬a (¬b ∘ ≈₂⇒≈₁) c
  

------------------------------------------------------------------------
-- Answering Wen's question

ℕ×ℕ-isSTO : IsStrictTotalOrder _≡_ (×-Lex _≡_ _<_ _<_)
ℕ×ℕ-isSTO = record
  { isEquivalence = isEquivalence
  ; trans = trans
  ; compare = λ x y → Trichotomous⇔ (≡×≡⇒≡ , ≡⇒≡×≡) compare x y
  }
  where
  ℕ-isSTO : IsStrictTotalOrder _≡_ _<_
  ℕ-isSTO = ℕ.<-isStrictTotalOrder
  open IsStrictTotalOrder (×-isStrictTotalOrder ℕ-isSTO ℕ-isSTO) using (trans; compare)

Answer 2

The kit required isn't too hard to assemble:

open import Data.Product
open import Function using (_∘_; case_of_)
open import Relation.Binary

_⇔₂_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ₂ → Set _
_≈_ ⇔₂ _≈′_ = (∀ {x y} → x ≈ y → x ≈′ y) × (∀ {x y} → x ≈′ y → x ≈ y)

-- I was unable to write this nicely using Data.Product.map... 
-- hence it is moved here to a toplevel where it can pattern-match
-- on the product of proofs
transform-resp : ∀ {a ℓ₁ ℓ₂ ℓ} {A : Set a} {≈ : Rel A ℓ₁} {≈′ : Rel A ℓ₂} {< : Rel A ℓ} →
                 ≈ ⇔₂ ≈′ →
                 < Respects₂ ≈ → < Respects₂ ≈′
transform-resp (to ,  from) = λ { (resp₁ , resp₂) → (resp₁ ∘ from , resp₂ ∘ from) }

transform-isSTO : ∀ {a ℓ₁ ℓ₂ ℓ} {A : Set a} {≈ : Rel A ℓ₁} {≈′ : Rel A ℓ₂} {< : Rel A ℓ} →
                  ≈ ⇔₂ ≈′ →
                  IsStrictTotalOrder ≈ < → IsStrictTotalOrder ≈′ <
transform-isSTO {≈′ = ≈′} {< = <} (to , from) isSTO = record
  { isEquivalence = let open IsEquivalence (IsStrictTotalOrder.isEquivalence isSTO)
                    in record { refl = to refl
                              ; sym = to ∘ sym ∘ from
                              ; trans = λ x y → to (trans (from x) (from y))
                              }
  ; trans = IsStrictTotalOrder.trans isSTO
  ; compare = compare
  ; <-resp-≈ = transform-resp (to , from) (IsStrictTotalOrder.<-resp-≈ isSTO)
  }
  where
    compare : Trichotomous ≈′ <
    compare x y with IsStrictTotalOrder.compare isSTO x y
    compare x y | tri< a ¬b ¬c = tri< a (¬b ∘ from) ¬c
    compare x y | tri≈ ¬a b ¬c = tri≈ ¬a (to b) ¬c
    compare x y | tri> ¬a ¬b c = tri> ¬a (¬b ∘ from) c

Then we can use this to solve your original problem:

ℕ×ℕ-isSTO′ : IsStrictTotalOrder _≡_ (×-Lex _≡_ _<_ _<_)
ℕ×ℕ-isSTO′ = transform-isSTO (to , from) ℕ×ℕ-isSTO
  where
    open import Function using (_⟨_⟩_)
    open import Relation.Binary.PropositionalEquality

    to : ∀ {a b} {A : Set a} {B : Set b}
         {x x′ : A} {y y′ : B} → (x , y) ⟨ _≡_ ×-Rel _≡_ ⟩ (x′ , y′) → (x , y) ≡ (x′ , y′)
    to (refl , refl) = refl

    from : ∀ {a b} {A : Set a} {B : Set b}
           {x x′ : A} {y y′ : B} → (x , y) ≡ (x′ , y′) → (x , y) ⟨ _≡_ ×-Rel _≡_ ⟩ (x′ , y′)
    from refl = refl , refl