Deprecated Induction.WellFounded.Lexicographic (#1094)

Author: MatthewDaggitt

CHANGELOG.md

@@ -235,6 +235,9 @@ discourage their use.
 
 * `Algebra.Solver.Monoid` and `Data.List.Solver`
 
+* The module `Data.Induction.WellFounded.Lexicographic` is deprecated.
+  Please use the proofs in `Data.Product.Relation.Binary.Lex.Strict` instead.
+  
 Deprecated names
 ----------------
 
@@ -742,6 +745,16 @@ Other minor additions
   ⊓-pres-m< : m < n → m < o → m < n ⊓ o
   ```
 
+* Improved the universe polymorphism of 
+  `Data.Product.Relation.Binary.Lex.Strict/NonStrict`
+  so that the equality and order relations need not live at the
+  same universe level.
+
+* Added new proofs to `Data.Product.Relation.Binary.Lex.Strict`:
+  ```
+  ×-wellFounded : WellFounded _<₁_ → WellFounded _<₂_ → WellFounded _<ₗₑₓ_
+  ```
+  
 * Added new proofs to `Data.String.Unsafe`:
   ```agda
   toList-++        : toList (s ++ t) ≡ toList s ++ toList t
@@ -791,6 +804,7 @@ Other minor additions
 
 * Added new proofs to `Induction.WellFounded`:
   ```agda
+  Acc-resp-≈            : Symmetric _≈_ → _<_ Respectsʳ _≈_ → (Acc _<_) Respects _≈_
   some-wfRec-irrelevant : Some.wfRec P f x q ≡ Some.wfRec P f x q'
   wfRecBuilder-wfRec    : All.wfRecBuilder P f x y y<x ≡ All.wfRec P f y
   unfold-wfRec          : All.wfRec P f x ≡ f x λ y _ → All.wfRec P f y

src/Data/Product/Relation/Binary/Lex/NonStrict.agda

@@ -13,51 +13,86 @@ module Data.Product.Relation.Binary.Lex.NonStrict where
 
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base using (inj₁; inj₂)
+open import Level using (Level)
 open import Relation.Binary
 open import Relation.Binary.Consequences
 import Relation.Binary.Construct.NonStrictToStrict as Conv
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
   using (Pointwise)
 import Data.Product.Relation.Binary.Lex.Strict as Strict
 
-module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where
+private
+  variable
+    a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
+    A : Set a
+    B : Set b
 
 ------------------------------------------------------------------------
--- A lexicographic ordering over products
+-- Definition
 
-  ×-Lex : (_≈₁_ _≤₁_ : Rel A₁ ℓ₁) (_≤₂_ : Rel A₂ ℓ₂) → Rel (A₁ × A₂) _
-  ×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_
+×-Lex : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂) (_≤₂_ : Rel B ℓ₃) →
+        Rel (A × B) _
+×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_
 
 ------------------------------------------------------------------------
--- Some properties which are preserved by ×-Lex (under certain
--- assumptions).
-
-  ×-reflexive : ∀ _≈₁_ _≤₁_ {_≈₂_} _≤₂_ →
-                _≈₂_ ⇒ _≤₂_ →
-                (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
-  ×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
-    Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂
-
-  ×-transitive : ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
-                 ∀ {_≤₂_} → Transitive _≤₂_ →
-                 Transitive (×-Lex _≈₁_ _≤₁_ _≤₂_)
-  ×-transitive {_≈₁_} {_≤₁_} po₁ {_≤₂_} trans₂ =
-    Strict.×-transitive
-      {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
+-- Properties
+
+×-reflexive : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂)
+              {_≈₂_ : Rel B ℓ₃} (_≤₂_ : Rel B ℓ₄) →
+              _≈₂_ ⇒ _≤₂_ →
+              (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
+×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
+  Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂
+
+module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂} {_≤₂_ : Rel B ℓ₃} where
+
+  private
+    _≤ₗₑₓ_ = ×-Lex _≈₁_ _≤₁_ _≤₂_
+
+  ×-transitive : IsPartialOrder _≈₁_ _≤₁_ → Transitive _≤₂_ →
+                 Transitive _≤ₗₑₓ_
+  ×-transitive po₁ trans₂ =
+    Strict.×-transitive {_≈₁_ = _≈₁_} {_<₂_ = _≤₂_}
       isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
       (Conv.<-trans _ _ po₁)
-      {_≤₂_} trans₂
+      trans₂
     where open IsPartialOrder po₁
 
-  ×-antisymmetric :
-    ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
-    ∀ {_≈₂_ _≤₂_} → Antisymmetric _≈₂_ _≤₂_ →
-    Antisymmetric (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
-  ×-antisymmetric {_≈₁_} {_≤₁_}
-                  po₁ {_≤₂_ = _≤₂_} antisym₂ =
-    Strict.×-antisymmetric {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
-                           ≈-sym₁ irrefl₁ asym₁
-                           {_≤₂_ = _≤₂_} antisym₂
+  ×-total : Symmetric _≈₁_ → Decidable _≈₁_ → Antisymmetric _≈₁_ _≤₁_ →
+            Total _≤₁_ → Total _≤₂_ → Total _≤ₗₑₓ_
+  ×-total sym₁ dec₁ antisym₁ total₁ total₂ =
+    total
+    where
+    tri₁ : Trichotomous _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
+    tri₁ = Conv.<-trichotomous _ _ sym₁ dec₁ antisym₁ total₁
+
+    total : Total _≤ₗₑₓ_
+    total x y with tri₁ (proj₁ x) (proj₁ y)
+    ... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
+    ... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
+    ... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
+    ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
+    ...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))
+
+  ×-decidable : Decidable _≈₁_ → Decidable _≤₁_ → Decidable _≤₂_ →
+                Decidable _≤ₗₑₓ_
+  ×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
+    Strict.×-decidable dec-≈₁ (Conv.<-decidable _ _ dec-≈₁ dec-≤₁)
+                       dec-≤₂
+
+module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
+         {_≈₂_ : Rel B ℓ₃} {_≤₂_ : Rel B ℓ₄}
+         where
+
+  private
+    _≤ₗₑₓ_ = ×-Lex _≈₁_ _≤₁_ _≤₂_
+    _≋_    = Pointwise _≈₁_ _≈₂_
+
+  ×-antisymmetric : IsPartialOrder _≈₁_ _≤₁_ → Antisymmetric _≈₂_ _≤₂_ →
+                   Antisymmetric _≋_ _≤ₗₑₓ_
+  ×-antisymmetric po₁ antisym₂ =
+    Strict.×-antisymmetric {_≈₁_ = _≈₁_} {_<₂_ = _≤₂_}
+       ≈-sym₁ irrefl₁ asym₁ antisym₂
     where
     open IsPartialOrder po₁
     open Eq renaming (refl to ≈-refl₁; sym to ≈-sym₁)
@@ -69,77 +104,48 @@ module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where
     asym₁ = trans∧irr⟶asym {_≈_ = _≈₁_}
                            ≈-refl₁ (Conv.<-trans _ _ po₁) irrefl₁
 
-  ×-respects₂ :
-    ∀ {_≈₁_ _≤₁_} → IsEquivalence _≈₁_ → _≤₁_ Respects₂ _≈₁_ →
-    ∀ {_≈₂_ _≤₂_ : Rel A₂ ℓ₂} → _≤₂_ Respects₂ _≈₂_ →
-    (×-Lex _≈₁_ _≤₁_ _≤₂_) Respects₂ (Pointwise _≈₁_ _≈₂_)
+  ×-respects₂ : IsEquivalence _≈₁_ →
+                _≤₁_ Respects₂ _≈₁_ → _≤₂_ Respects₂ _≈₂_ →
+                _≤ₗₑₓ_ Respects₂ _≋_
   ×-respects₂ eq₁ resp₁ resp₂ =
     Strict.×-respects₂ eq₁ (Conv.<-resp-≈ _ _ eq₁ resp₁) resp₂
 
-  ×-decidable : ∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → Decidable _≤₁_ →
-                ∀ {_≤₂_} → Decidable _≤₂_ →
-                Decidable (×-Lex _≈₁_ _≤₁_ _≤₂_)
-  ×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
-    Strict.×-decidable dec-≈₁ (Conv.<-decidable _ _ dec-≈₁ dec-≤₁)
-                       dec-≤₂
-
-  ×-total : ∀ {_≈₁_ _≤₁_} → Symmetric _≈₁_ → Decidable _≈₁_ →
-                            Antisymmetric _≈₁_ _≤₁_ → Total _≤₁_ →
-            ∀ {_≤₂_} → Total _≤₂_ →
-            Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
-  ×-total {_≈₁_} {_≤₁_} sym₁ dec₁ antisym₁ total₁ {_≤₂_} total₂ =
-    total
-    where
-    tri₁ : Trichotomous _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
-    tri₁ = Conv.<-trichotomous _ _ sym₁ dec₁ antisym₁ total₁
-
-    total : Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
-    total x y with tri₁ (proj₁ x) (proj₁ y)
-    ... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
-    ... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
-    ... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
-    ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
-    ...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))
 
-  -- Some collections of properties which are preserved by ×-Lex
-  -- (under certain assumptions).
+------------------------------------------------------------------------
+-- Structures
 
-  ×-isPartialOrder :
-    ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
-    ∀ {_≈₂_ _≤₂_} → IsPartialOrder _≈₂_ _≤₂_ →
-    IsPartialOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
-  ×-isPartialOrder {_≈₁_} {_≤₁_} po₁
-                     {_≤₂_ = _≤₂_} po₂ = record
+  ×-isPartialOrder : IsPartialOrder _≈₁_ _≤₁_ →
+                     IsPartialOrder _≈₂_ _≤₂_ →
+                     IsPartialOrder _≋_ _≤ₗₑₓ_
+  ×-isPartialOrder po₁ po₂ = record
     { isPreorder = record
         { isEquivalence = Pointwise.×-isEquivalence
                             (isEquivalence po₁)
                             (isEquivalence po₂)
         ; reflexive     = ×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
-        ; trans         = ×-transitive po₁ {_≤₂_ = _≤₂_} (trans po₂)
+        ; trans         = ×-transitive {_≤₂_ = _≤₂_} po₁ (trans po₂)
         }
-    ; antisym = ×-antisymmetric {_≤₁_ = _≤₁_} po₁
-                                {_≤₂_ = _≤₂_} (antisym po₂)
+    ; antisym = ×-antisymmetric po₁ (antisym po₂)
     }
     where open IsPartialOrder
 
-  ×-isTotalOrder :
-    ∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → IsTotalOrder _≈₁_ _≤₁_ →
-    ∀ {_≈₂_ _≤₂_} → IsTotalOrder _≈₂_ _≤₂_ →
-    IsTotalOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
-  ×-isTotalOrder {_≤₁_ = _≤₁_} ≈₁-dec to₁ {_≤₂_ = _≤₂_} to₂ = record
+  ×-isTotalOrder : Decidable _≈₁_ →
+                   IsTotalOrder _≈₁_ _≤₁_ →
+                   IsTotalOrder _≈₂_ _≤₂_ →
+                   IsTotalOrder _≋_ _≤ₗₑₓ_
+  ×-isTotalOrder ≈₁-dec to₁ to₂ = record
     { isPartialOrder = ×-isPartialOrder
                          (isPartialOrder to₁) (isPartialOrder to₂)
-    ; total          = ×-total {_≤₁_ = _≤₁_} (Eq.sym to₁) ≈₁-dec
+    ; total          = ×-total (Eq.sym to₁) ≈₁-dec
                                              (antisym to₁) (total to₁)
-                               {_≤₂_ = _≤₂_} (total to₂)
+                               (total to₂)
     }
     where open IsTotalOrder
 
-  ×-isDecTotalOrder :
-    ∀ {_≈₁_ _≤₁_} → IsDecTotalOrder _≈₁_ _≤₁_ →
-    ∀ {_≈₂_ _≤₂_} → IsDecTotalOrder _≈₂_ _≤₂_ →
-    IsDecTotalOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
-  ×-isDecTotalOrder {_≤₁_ = _≤₁_} to₁ {_≤₂_ = _≤₂_} to₂ = record
+  ×-isDecTotalOrder : IsDecTotalOrder _≈₁_ _≤₁_ →
+                      IsDecTotalOrder _≈₂_ _≤₂_ →
+                      IsDecTotalOrder _≋_ _≤ₗₑₓ_
+  ×-isDecTotalOrder to₁ to₂ = record
     { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
@@ -149,31 +155,26 @@ module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where
     where open IsDecTotalOrder
 
 ------------------------------------------------------------------------
--- "Bundles" can also be combined.
-
-module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} where
-
-  ×-poset : Poset ℓ₁ ℓ₂ _ → Poset ℓ₃ ℓ₄ _ → Poset _ _ _
-  ×-poset p₁ p₂ = record
-    { isPartialOrder = ×-isPartialOrder
-                         (isPartialOrder p₁) (isPartialOrder p₂)
-    } where open Poset
-
-  ×-totalOrder : DecTotalOrder ℓ₁ ℓ₂ _ → TotalOrder ℓ₃ ℓ₄ _ →
-                 TotalOrder _ _ _
-  ×-totalOrder t₁ t₂ = record
-    { isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
-    }
-    where
-    module T₁ = DecTotalOrder t₁
-    module T₂ =    TotalOrder t₂
-
-  ×-decTotalOrder : DecTotalOrder ℓ₁ ℓ₂ _ → DecTotalOrder ℓ₃ ℓ₄ _ →
-                    DecTotalOrder _ _ _
-  ×-decTotalOrder t₁ t₂ = record
-    { isDecTotalOrder = ×-isDecTotalOrder
-        (isDecTotalOrder t₁) (isDecTotalOrder t₂)
-    } where open DecTotalOrder
+-- Bundles
+
+×-poset : Poset a ℓ₁ ℓ₂ → Poset b ℓ₃ ℓ₄ → Poset _ _ _
+×-poset p₁ p₂ = record
+  { isPartialOrder = ×-isPartialOrder O₁.isPartialOrder O₂.isPartialOrder
+  } where module O₁ = Poset p₁; module O₂ = Poset p₂
+
+×-totalOrder : DecTotalOrder a ℓ₁ ℓ₂ →
+               TotalOrder b ℓ₃ ℓ₄ →
+               TotalOrder _ _ _
+×-totalOrder t₁ t₂ = record
+  { isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
+  } where module T₁ = DecTotalOrder t₁; module T₂ = TotalOrder t₂
+
+×-decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ →
+                  DecTotalOrder b ℓ₃ ℓ₄ →
+                  DecTotalOrder _ _ _
+×-decTotalOrder t₁ t₂ = record
+  { isDecTotalOrder = ×-isDecTotalOrder O₁.isDecTotalOrder O₂.isDecTotalOrder
+  } where module O₁ = DecTotalOrder t₁; module O₂ = DecTotalOrder t₂
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES