Lexikographische Anordnung von Paaren/Listen in Agda mit der Standardbibliothek

Question

Die Agda-Standardbibliothek enthält einige Module Relation.Binary.*.(Non)StrictLex (derzeit nur für Product und List). Wir können diese Module verwenden, um leicht eine Instanz von beispielsweise IsStrictTotalOrder für Paare von natürlichen Zahlen zu konstruieren (d. H. ℕ × ℕ).

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 

Dies erzeugt eine Instanz mit der punktuellen Gleichheit _≡_ ×-Rel _≡_. Im Fall der propositionalen Gleichheit sollte dies gleichbedeutend mit der Verwendung von aussagengleichheit sein.

Gibt es eine einfache Möglichkeit, die obige Instanz in eine Instanz des Typs IsStrictTotalOrder _≡_ (×-Lex _≡_ _<_ _<_) zu konvertieren, wobei die normale propositionale Gleichheit verwendet wird?

Answer 1

Das Kit erforderlich ist, nicht zu schwer zu montieren:

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 

Dann können wir diese benutzen, um Ihr ursprüngliches Problem zu lösen:

ℕ×ℕ-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