WellFounded proofs for transitive closure (#2082)

CHANGELOG.md

@@ -2951,6 +2951,13 @@ Other minor changes
  f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂
  ```
 
+* Added new proofs to `Relation.Binary.Construct.Closure.Transitive`:
+ ```
+ accessible⁻ : ∀ {x} → Acc _∼⁺_ x → Acc _∼_ x
+ wellFounded⁻ : WellFounded _∼⁺_ → WellFounded _∼_
+ 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
 
- 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
 
+ 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)
 
 
 ------------------------------------------------------------------------