#2075: Remove symmetry assumption from lexicographic well-foundedness (#2077)

Author: jamesmckinna

CHANGELOG.md

@@ -781,6 +781,12 @@ Non-backwards compatible changes
   properties about the orderings themselves the second index must be provided
   explicitly.
 
+* Issue #2075 (Johannes Waldmann): wellfoundedness of the lexicographic ordering
+  on products, defined in `Data.Product.Relation.Binary.Lex.Strict`, no longer
+  requires the assumption of symmetry for the first equality relation `_≈₁_`,
+  leading to a new lemma `Induction.WellFounded.Acc-resp-flip-≈`, and refactoring
+  of the previous proof `Induction.WellFounded.Acc-resp-≈`.
+
 * The operation `SymClosure` on relations in
   `Relation.Binary.Construct.Closure.Symmetric` has been reimplemented
   as a data type `SymClosure _⟶_ a b` that is parameterized by the
@@ -2515,13 +2521,13 @@ Other minor changes
   ×-≡,≡←≡ : p₁ ≡ p₂ → (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂)
   ```
 
-* Added new proof to `Data.Product.Relation.Binary.Lex.Strict`
+* Added new proofs to `Data.Product.Relation.Binary.Lex.Strict`
   ```agda
   ×-respectsʳ : Transitive _≈₁_ →
                 _<₁_ Respectsʳ _≈₁_ → _<₂_ Respectsʳ _≈₂_ → _<ₗₑₓ_ Respectsʳ _≋_
   ×-respectsˡ : Symmetric _≈₁_ → Transitive _≈₁_ →
                  _<₁_ Respectsˡ _≈₁_ → _<₂_ Respectsˡ _≈₂_ → _<ₗₑₓ_ Respectsˡ _≋_
-  ×-wellFounded' : Symmetric  _≈₁_ → Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ →
+  ×-wellFounded' : Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ →
                    WellFounded _<₁_ → WellFounded _<₂_ → WellFounded _<ₗₑₓ_
   ```
 
@@ -2686,7 +2692,7 @@ Other minor changes
                 ∀ {m n} → _Respectsˡ_ (_<_ {m} {n}) _≋_
   <-respectsʳ : IsPartialEquivalence _≈_ → _≺_ Respectsʳ _≈_ →
                 ∀ {m n} → _Respectsʳ_ (_<_ {m} {n}) _≋_
-  <-wellFounded : Symmetric _≈_ →  Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ →
+  <-wellFounded : Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ →
                   ∀ {n} → WellFounded (_<_ {n})
 ```
 
@@ -3356,6 +3362,11 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ⊆-mergeʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys
   ```
 
+* Added new proof to `Induction.WellFounded`
+  ```agda
+  Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
+  ```
+
 * Added new file `Relation.Binary.Reasoning.Base.Apartness`
 
   This is how to use it:

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

@@ -28,7 +28,7 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Transitive; Symmetric; Irreflexive; Asymmetric; Total; Decidable; Antisymmetric; Trichotomous; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri>; tri≈)
 open import Relation.Binary.Consequences
-open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 private
   variable
@@ -192,23 +192,24 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ
   private
     _<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_
 
-  ×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ →
+  ×-wellFounded' : Transitive _≈₁_ →
                    _<₁_ Respectsʳ _≈₁_ →
                    WellFounded _<₁_ →
                    WellFounded _<₂_ →
                    WellFounded _<ₗₑₓ_
-  ×-wellFounded' sym trans resp wf₁ wf₂ (x , y) = acc (×-acc (wf₁ x) (wf₂ y))
+  ×-wellFounded' trans resp wf₁ wf₂ (x , y) = acc (×-acc (wf₁ x) (wf₂ y))
     where
     ×-acc : ∀ {x y} →
             Acc _<₁_ x → Acc _<₂_ y →
             WfRec _<ₗₑₓ_ (Acc _<ₗₑₓ_) (x , y)
     ×-acc (acc rec₁) acc₂ (u , v) (inj₁ u<x)
       = acc (×-acc (rec₁ u u<x) (wf₂ v))
-    ×-acc {x₁} acc₁ (acc rec₂) (u , v) (inj₂ (u≈x , v<y))
-      = Acc-resp-≈ (Pointwise.×-symmetric {_∼₁_ = _≈₁_} {_∼₂_ = _≡_ } sym ≡.sym)
-                   (×-respectsʳ {_<₁_ = _<₁_} {_<₂_ = _<₂_} trans resp (≡.respʳ _<₂_))
-                   (sym u≈x , _≡_.refl)
-                   (acc (×-acc acc₁ (rec₂ v v<y)))
+    ×-acc acc₁ (acc rec₂) (u , v) (inj₂ (u≈x , v<y))
+      = Acc-resp-flip-≈
+        (×-respectsʳ {_<₁_ = _<₁_} {_<₂_ = _<₂_} trans resp (≡.respʳ _<₂_))
+        (u≈x , ≡.refl)
+        (acc (×-acc acc₁ (rec₂ v v<y)))
+
 
 module _ {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel B ℓ₂} where
 
@@ -218,7 +219,7 @@ module _ {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel B ℓ₂} where
   ×-wellFounded : WellFounded _<₁_ →
                   WellFounded _<₂_ →
                   WellFounded _<ₗₑₓ_
-  ×-wellFounded = ×-wellFounded' ≡.sym ≡.trans (≡.respʳ _<₁_)
+  ×-wellFounded = ×-wellFounded' ≡.trans (≡.respʳ _<₁_)
 
 ------------------------------------------------------------------------
 -- Collections of properties which are preserved by ×-Lex.

src/Data/Vec/Relation/Binary/Lex/Strict.agda

@@ -130,7 +130,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
                  ∀ {m n} → Irrelevant (_<_ {m} {n})
   <-irrelevant = Core.irrelevant (λ ())
 
-  module _ (≈-sym : Symmetric _≈_) (≈-trans : Transitive _≈_) (≺-respʳ : _≺_ Respectsʳ _≈_ ) (≺-wf : WellFounded _≺_)
+  module _ (≈-trans : Transitive _≈_) (≺-respʳ : _≺_ Respectsʳ _≈_ ) (≺-wf : WellFounded _≺_)
     where
 
     <-wellFounded : ∀ {n} → WellFounded (_<_ {n})
@@ -142,7 +142,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
         <⇒uncons-Lex {x ∷ xs} {y ∷ ys} (next x≈y xs<ys) = inj₂ (x≈y , xs<ys)
 
         uncons-Lex-wellFounded : WellFounded (×-Lex _≈_ _≺_ _<_ on uncons)
-        uncons-Lex-wellFounded = On.wellFounded uncons (×-wellFounded' ≈-sym ≈-trans ≺-respʳ ≺-wf <-wellFounded)
+        uncons-Lex-wellFounded = On.wellFounded uncons (×-wellFounded' ≈-trans ≺-respʳ ≺-wf <-wellFounded)
 
 ------------------------------------------------------------------------
 -- Structures

src/Induction/WellFounded.agda

@@ -9,7 +9,7 @@
 module Induction.WellFounded where
 
 open import Data.Product.Base using (Σ; _,_; proj₁)
-open import Function.Base using (_on_)
+open import Function.Base using (_∘_; flip; _on_)
 open import Induction
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel)
@@ -54,10 +54,13 @@ acc-inverse : ∀ {_<_ : Rel A ℓ} {x : A} (q : Acc _<_ x) →
               (y : A) → y < x → Acc _<_ y
 acc-inverse (acc rs) y y<x = rs y y<x
 
-Acc-resp-≈ : {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} → Symmetric _≈_ →
-             _<_ Respectsʳ _≈_ → (Acc _<_) Respects _≈_
-Acc-resp-≈ sym respʳ x≈y (acc rec) =
-  acc (λ z z<y → rec z (respʳ (sym x≈y) z<y))
+module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
+
+  Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
+  Acc-resp-flip-≈ respʳ x≈y (acc rec) = acc λ z z<y → rec z (respʳ x≈y z<y)
+
+  Acc-resp-≈ : Symmetric _≈_ → _<_ Respectsʳ _≈_ → (Acc _<_) Respects _≈_
+  Acc-resp-≈ sym respʳ x≈y wf = Acc-resp-flip-≈ (respʳ ∘ sym) x≈y wf
 
 ------------------------------------------------------------------------
 -- Well-founded induction for the subset of accessible elements:
@@ -120,7 +123,7 @@ module Subrelation {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂}
                    (<₁⇒<₂ : ∀ {x y} → x <₁ y → x <₂ y) where
 
   accessible : Acc _<₂_ ⊆ Acc _<₁_
-  accessible (acc rs) = acc (λ y y<x → accessible (rs y (<₁⇒<₂ y<x)))
+  accessible (acc rs) = acc λ y y<x → accessible (rs y (<₁⇒<₂ y<x))
 
   wellFounded : WellFounded _<₂_ → WellFounded _<₁_
   wellFounded wf = λ x → accessible (wf x)
@@ -131,7 +134,7 @@ module Subrelation {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂}
 module InverseImage {_<_ : Rel B ℓ} (f : A → B) where
 
   accessible : ∀ {x} → Acc _<_ (f x) → Acc (_<_ on f) x
-  accessible (acc rs) = acc (λ y fy<fx → accessible (rs (f y) fy<fx))
+  accessible (acc rs) = acc λ y fy<fx → accessible (rs (f y) fy<fx)
 
   wellFounded : WellFounded _<_ → WellFounded (_<_ on f)
   wellFounded wf = λ x → accessible (wf (f x))
@@ -158,7 +161,7 @@ module TransitiveClosure {A : Set a} (_<_ : Rel A ℓ) where
     trans : ∀ {x y z} (x<y : x <⁺ y) (y<z : y <⁺ z) → x <⁺ z
 
   downwardsClosed : ∀ {x y} → Acc _<⁺_ y → x <⁺ y → Acc _<⁺_ x
-  downwardsClosed (acc rs) x<y = acc (λ z z<x → rs z (trans z<x x<y))
+  downwardsClosed (acc rs) x<y = acc λ z z<x → rs z (trans z<x x<y)
 
   mutual