WellFounded proofs for transitive closure

CHANGELOG.md

@@ -2929,6 +2929,21 @@ Other minor changes
                     f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂
   ```
 
+* Added new proofs to `Relation.Binary.Construct.Closure.Transitive`:
+  ```
+  accessible⁻ : ∀ {x} → Acc _∼⁺_ x → Acc _∼_ x
+  wellFounded⁻ : WellFounded _∼⁺_ → WellFounded _∼_
+  ```
+  as instances of the corresponding proofs in `Induction.WellFounded.Subrelation`,
+  together with a refactoring of the former proof
+  ```
+  wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
+  ```
+  in terms of a new proof:
+  ```
+  accessible : ∀ {x} → Acc _∼_ x → Acc _∼⁺_ x
+  ```
+
 * Added new operations in `Relation.Binary.PropositionalEquality.Properties`:
   ```
   J       : (B : (y : A) → x ≡ y → Set b) (p : x ≡ y) → B x refl → B y p

src/Relation/Binary/Construct/Closure/Transitive.agda

@@ -58,6 +58,7 @@ module _ {_∼_ : Rel A ℓ} where
 module _ (_∼_ : Rel A ℓ) where
   private
     _∼⁺_ = TransClosure _∼_
+    module ∼⊆∼⁺ = Subrelation {_<₂_ = _∼⁺_} [_]
 
   reflexive : Reflexive _∼_ → Reflexive _∼⁺_
   reflexive refl = [ refl ]
@@ -69,17 +70,21 @@ module _ (_∼_ : Rel A ℓ) where
   transitive : Transitive _∼⁺_
   transitive = _++_
 
-  wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
-  wellFounded wf = λ x → acc (accessible′ (wf x))
-    where
-    downwardsClosed : ∀ {x y} → Acc _∼⁺_ y → x ∼ y → Acc _∼⁺_ x
-    downwardsClosed (acc rec) x∼y = acc (λ z z∼x → rec z (z∼x ∷ʳ x∼y))
+  accessible⁻ : ∀ {x} → Acc _∼⁺_ x → Acc _∼_ x
+  accessible⁻ = accessible where open ∼⊆∼⁺
 
-    accessible′ : ∀ {x} → Acc _∼_ x → WfRec _∼⁺_ (Acc _∼⁺_) x
-    accessible′ (acc rec) y [ y∼x ]      = acc (accessible′ (rec y y∼x))
-    accessible′ acc[x]    y (y∼z ∷ z∼⁺x) =
-      downwardsClosed (accessible′ acc[x] _ z∼⁺x) y∼z
+  wellFounded⁻ : WellFounded _∼⁺_ → WellFounded _∼_
+  wellFounded⁻ = wellFounded where open ∼⊆∼⁺
 
+  accessible : ∀ {x} → Acc _∼_ x → Acc _∼⁺_ x
+  accessible acc[x] = acc (wf-acc acc[x])
+    where
+    wf-acc : ∀ {x} → Acc _∼_ x → WfRec _∼⁺_ (Acc _∼⁺_) x
+    wf-acc (acc rec) _ [ y∼x ]   = acc (wf-acc (rec _ y∼x))
+    wf-acc acc[x] _ (y∼z ∷ z∼⁺x) = acc-inverse (wf-acc acc[x] _ z∼⁺x) _ [ y∼z ]
+
+  wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
+  wellFounded wf x = accessible (wf x)
 
 
 ------------------------------------------------------------------------