'No infinite descent' for (Accessible elements of) WellFounded relations

CHANGELOG.md

@@ -599,7 +599,7 @@ Non-backwards compatible changes
   with the consequence that all arguments involving about accesibility and
   wellfoundedness proofs were polluted by almost-always-inferrable explicit
   arguments for the `y` position. The definition has now been changed to
-  make that argument *implicit*, as 
+  make that argument *implicit*, as
   ```agda
   WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
   WfRec _<_ P x = ∀ {y} → y < x → P y
@@ -621,7 +621,7 @@ Non-backwards compatible changes
   raw bundles to `Data.X.Base`, this definition can now be made directly. Knock-on
   consequences include the need to retain the old constructor name, now introduced
   as a pattern synonym, and introduction of (a function equivalent to) the former
-  field name/projection function `proof` as `≤″-proof` in `Data.Nat.Properties`. 
+  field name/projection function `proof` as `≤″-proof` in `Data.Nat.Properties`.
 
 * Accordingly, the definition has been changed to:
   ```agda
@@ -879,12 +879,12 @@ Non-backwards compatible changes
   ```
   _─_ ↦ removeAt
   ```
-  
+
 * In `Data.Vec.Base`:
   ```agda
   insert ↦ insertAt
   remove ↦ removeAt
-  
+
   updateAt : Fin n → (A → A) → Vec A n → Vec A n
     ↦
   updateAt : Vec A n → Fin n → (A → A) → Vec A n
@@ -895,12 +895,12 @@ Non-backwards compatible changes
   remove : Fin (suc n) → Vector A (suc n) → Vector A n
     ↦
   removeAt : Vector A (suc n) → Fin (suc n) → Vector A n
- 
+
   updateAt : Fin n → (A → A) → Vector A n → Vector A n
     ↦
   updateAt : Vector A n → Fin n → (A → A) → Vector A n
   ```
-  
+
 * The old names (and the names of all proofs about these functions) have been deprecated appropriately.
 
 ### Changes to triple reasoning interface
@@ -925,7 +925,7 @@ Non-backwards compatible changes
   Data.Vec.Relation.Binary.Lex.NonStrict
   Relation.Binary.Reasoning.StrictPartialOrder
   Relation.Binary.Reasoning.PartialOrder
-  ```	
+  ```
 
 ### Other
 
@@ -1103,7 +1103,7 @@ Non-backwards compatible changes
 * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
   `¬¬-excluded-middle`.
 
-* `iterate` and `replicate` in `Data.Vec.Base` and `Data.Vec.Functional` 
+* `iterate` and `replicate` in `Data.Vec.Base` and `Data.Vec.Functional`
   now take the length of vector, `n`, as an explicit rather than an implicit argument.
   ```agda
   iterate : (A → A) → A → ∀ n → Vec A n
@@ -1658,7 +1658,7 @@ Deprecated names
   take-drop-id  ↦  take++drop≡id
 
   map-insert       ↦  map-insertAt
-  
+
   insert-lookup    ↦  insertAt-lookup
   insert-punchIn   ↦  insertAt-punchIn
   remove-PunchOut  ↦  removeAt-punchOut
@@ -1684,7 +1684,7 @@ Deprecated names
   updateAt-cong-relative    ↦  updateAt-cong-local
 
   map-updateAt              ↦  map-updateAt-local
-  
+
   insert-lookup             ↦  insertAt-lookup
   insert-punchIn            ↦  insertAt-punchIn
   remove-punchOut           ↦  removeAt-punchOut
@@ -1904,6 +1904,11 @@ New modules
   Function.Properties.Surjection
   ```
 
+* The 'no infinite descent' principle for (accessible elements of) well-founded relations:
+  ```
+  Induction.NoInfiniteDescent
+  ```
+
 * In order to improve modularity, the contents of `Relation.Binary.Lattice` has been
   split out into the standard:
   ```
@@ -3162,6 +3167,11 @@ Additions to existing modules
   _⋆     : _⟶₁_ ⇒ SymClosure _⟶₂_ → SymClosure _⟶₁_ ⇒ SymClosure _⟶₂_
   ```
 
+* Added new proof in `Relation.Binary.Construct.Closure.Transitive`:
+  ```
+  transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
+  ```
+
 * Added new proofs to `Relation.Binary.Lattice.Properties.{Join,Meet}Semilattice`:
   ```agda
   isPosemigroup : IsPosemigroup _≈_ _≤_ _∨_

src/Induction/NoInfiniteDescent.agda

@@ -0,0 +1,81 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A standard consequence of accessibility/well-foundedness:
+-- the impossibility of 'infinite descent' from any (accessible)
+-- element x satisfying P to 'smaller' y also satisfying P
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Induction.NoInfiniteDescent where
+
+open import Data.Product.Base using (_,_; ∃-syntax; _×_)
+open import Function.Base using (_∘_)
+open import Induction.WellFounded using (WellFounded; Acc; acc-inverse; module Some)
+open import Level using (Level)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Unary using (Pred; _∩_)
+
+private
+  variable
+    a r ℓ : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- Definitions
+
+module InfiniteDescent (_<_ : Rel A r) (P : Pred A ℓ)  where
+
+    DescentAt : Pred A _
+    DescentAt x = P x → ∃[ y ] y < x × P y
+
+    InfiniteDescent : Set _
+    InfiniteDescent = ∀ {x} → DescentAt x
+
+    AccInfiniteDescent : Set _
+    AccInfiniteDescent = ∀ {x} → Acc _<_ x → DescentAt x
+
+------------------------------------------------------------------------
+-- Basic result: assumes unrestricted descent
+
+    module Lemma (descent : InfiniteDescent) where
+
+      accNoInfiniteDescent : ∀ {x} → Acc _<_ x → ¬ (P x)
+      accNoInfiniteDescent = Some.wfRec (¬_ ∘ P)
+        (λ _ hy py → let z , z<y , pz = descent py in hy z<y pz) _
+
+      wfNoInfiniteDescent : WellFounded _<_ → ∀ {x} → ¬ (P x)
+      wfNoInfiniteDescent wf = accNoInfiniteDescent (wf _)
+
+------------------------------------------------------------------------
+-- Extended result: assumes descent only for accessible elements
+
+module _ {_<_ : Rel A r} (P : Pred A ℓ) where
+
+    open InfiniteDescent _<_ P hiding (module Lemma)
+
+    module Corollary (descent : AccInfiniteDescent) where
+
+      accNoInfiniteDescent : ∀ {x} → Acc _<_ x → ¬ (P x)
+      accNoInfiniteDescent ax px = ID∩.Lemma.accNoInfiniteDescent descent∩ ax (px , ax)
+
+        where
+        P∩Acc : Pred A _
+        P∩Acc = P ∩ (Acc _<_)
+
+        module ID∩ = InfiniteDescent _<_ P∩Acc
+
+        descent∩ : ID∩.InfiniteDescent
+        descent∩ (px , ax) = let y , y<x , py = descent ax px in
+          y , y<x , py , acc-inverse ax y<x
+
+      wfNoInfiniteDescent : WellFounded _<_ → ∀ {x} → ¬ (P x)
+      wfNoInfiniteDescent wf = accNoInfiniteDescent (wf _)
+
+------------------------------------------------------------------------
+-- Exports
+
+open InfiniteDescent public using (InfiniteDescent; AccInfiniteDescent; module Lemma)
+open Corollary public

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

@@ -70,6 +70,13 @@ module _ (_∼_ : Rel A ℓ) where
   transitive : Transitive _∼⁺_
   transitive = _++_
 
+  transitive⁻ : Transitive _∼_ → _∼⁺_ ⇒ _∼_
+  transitive⁻ trans = ∼⁺⊆∼
+    where
+    ∼⁺⊆∼ : _∼⁺_ ⇒ _∼_
+    ∼⁺⊆∼ [ x∼y ]      = x∼y
+    ∼⁺⊆∼ (x∼y ∷ x∼⁺y) = trans x∼y (∼⁺⊆∼ x∼⁺y)
+
   accessible⁻ : ∀ {x} → Acc _∼⁺_ x → Acc _∼_ x
   accessible⁻ = ∼⊆∼⁺.accessible