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

CHANGELOG.md

@@ -50,6 +50,11 @@ New modules
 -----------
 * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
 
+* Consequences of 'infinite descent' for (accessible elements of) well-founded relations:
+  ```agda
+  Induction.InfiniteDescent
+  ```
+
 * The unique morphism from the initial, resp. terminal, algebra:
   ```agda
   Algebra.Morphism.Construct.Initial
@@ -242,6 +247,15 @@ Additions to existing modules
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
+
+* Added new definition in `Relation.Binary.Construct.Closure.Transitive`
+  ```
+  transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_
+  ```
+
+* Added new definition in `Relation.Unary`
+  ```
+  Stable : Pred A ℓ → Set _
   ```
 
 * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can

src/Induction/InfiniteDescent.agda

@@ -0,0 +1,189 @@
+------------------------------------------------------------------------
+-- 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.InfiniteDescent where
+
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Nat.Properties as ℕ
+open import Data.Product.Base using (_,_; proj₁; ∃-syntax; _×_)
+open import Function.Base using (_∘_)
+open import Induction.WellFounded
+  using (WellFounded; Acc; acc; acc-inverse; module Some)
+open import Level using (Level)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Construct.Closure.Transitive
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Nullary.Negation.Core as Negation using (¬_)
+open import Relation.Unary
+  using (Pred; ∁; _∩_; _⊆_;  _⇒_; Universal; IUniversal; Stable; Empty)
+
+private
+  variable
+    a r ℓ : Level
+    A : Set a
+    f : ℕ → A
+    _<_ : Rel A r
+    P : Pred A ℓ
+
+------------------------------------------------------------------------
+-- Definitions
+
+InfiniteDescendingSequence : Rel A r → (ℕ → A) → Set _
+InfiniteDescendingSequence _<_ f = ∀ n → f (suc n) < f n
+
+InfiniteDescendingSequenceFrom : Rel A r → (ℕ → A) → Pred A _
+InfiniteDescendingSequenceFrom _<_ f x = f zero ≡ x × InfiniteDescendingSequence _<_ f
+
+InfiniteDescendingSequence⁺ : Rel A r → (ℕ → A) → Set _
+InfiniteDescendingSequence⁺ _<_ f = ∀ {m n} → m ℕ.< n → TransClosure _<_ (f n) (f m)
+
+InfiniteDescendingSequenceFrom⁺ : Rel A r → (ℕ → A) → Pred A _
+InfiniteDescendingSequenceFrom⁺ _<_ f x = f zero ≡ x × InfiniteDescendingSequence⁺ _<_ f
+
+DescentFrom : Rel A r → Pred A ℓ → Pred A _
+DescentFrom _<_ P x = P x → ∃[ y ] y < x × P y
+
+Descent : Rel A r → Pred A ℓ → Set _
+Descent _<_ P = ∀ {x} → DescentFrom _<_ P x
+
+InfiniteDescentFrom : Rel A r → Pred A ℓ → Pred A _
+InfiniteDescentFrom _<_ P x = P x → ∃[ f ] InfiniteDescendingSequenceFrom _<_ f x × ∀ n → P (f n)
+
+InfiniteDescent : Rel A r → Pred A ℓ →  Set _
+InfiniteDescent _<_ P = ∀ {x} → InfiniteDescentFrom _<_ P x
+
+InfiniteDescentFrom⁺ : Rel A r → Pred A ℓ → Pred A _
+InfiniteDescentFrom⁺ _<_ P x = P x → ∃[ f ] InfiniteDescendingSequenceFrom⁺ _<_ f x × ∀ n → P (f n)
+
+InfiniteDescent⁺ : Rel A r → Pred A ℓ → Set _
+InfiniteDescent⁺ _<_ P = ∀ {x} → InfiniteDescentFrom⁺ _<_ P x
+
+NoSmallestCounterExample : Rel A r → Pred A ℓ →  Set _
+NoSmallestCounterExample _<_ P = ∀ {x} → Acc _<_ x → DescentFrom (TransClosure _<_) (∁ P) x
+
+------------------------------------------------------------------------
+-- We can swap between transitively closed and non-transitively closed
+-- definitions
+
+sequence⁺ : InfiniteDescendingSequence (TransClosure _<_) f →
+            InfiniteDescendingSequence⁺ _<_ f
+sequence⁺ {_<_ = _<_} {f = f} seq[f] = seq⁺[f]′ ∘ ℕ.<⇒<′
+  where
+  seq⁺[f]′ : ∀ {m n} → m ℕ.<′ n → TransClosure _<_ (f n) (f m)
+  seq⁺[f]′ ℕ.<′-base        = seq[f] _
+  seq⁺[f]′ (ℕ.<′-step m<′n) = seq[f] _ ++ seq⁺[f]′ m<′n
+
+sequence⁻ : InfiniteDescendingSequence⁺ _<_ f →
+            InfiniteDescendingSequence (TransClosure _<_) f
+sequence⁻ seq[f] = seq[f] ∘ n<1+n
+
+------------------------------------------------------------------------
+-- Results about unrestricted descent
+
+module _ (descent : Descent _<_ P) where
+
+  descent∧acc⇒infiniteDescentFrom : (Acc _<_) ⊆ (InfiniteDescentFrom _<_ P)
+  descent∧acc⇒infiniteDescentFrom {x} =
+    Some.wfRec (InfiniteDescentFrom _<_ P) rec x
+    where
+    rec : _
+    rec y rec[y] py
+      with z , z<y , pz ← descent py
+      with g , (g0≡z , g<P) , Π[P∘g] ← rec[y] z<y pz
+         = h , (h0≡y , h<P) , Π[P∘h]
+      where
+      h : ℕ → _
+      h zero = y
+      h (suc n) = g n
+
+      h0≡y : h zero ≡ y
+      h0≡y = refl
+
+      h<P : ∀ n → h (suc n) < h n
+      h<P zero rewrite g0≡z = z<y
+      h<P (suc n)           = g<P n
+
+      Π[P∘h] : ∀ n →  P (h n)
+      Π[P∘h] zero rewrite g0≡z = py
+      Π[P∘h] (suc n)           = Π[P∘g] n
+
+  descent∧wf⇒infiniteDescent : WellFounded _<_ → InfiniteDescent _<_ P
+  descent∧wf⇒infiniteDescent wf = descent∧acc⇒infiniteDescentFrom (wf _)
+
+  descent∧acc⇒unsatisfiable : Acc _<_ ⊆ ∁ P
+  descent∧acc⇒unsatisfiable {x} = Some.wfRec (∁ P) rec x
+    where
+    rec : _
+    rec y rec[y] py = let z , z<y , pz = descent py in rec[y] z<y pz
+
+  descent∧wf⇒empty : WellFounded _<_ → Empty P
+  descent∧wf⇒empty wf x = descent∧acc⇒unsatisfiable (wf x)
+
+------------------------------------------------------------------------
+-- Results about descent only from accessible elements
+
+module _ (accDescent : Acc _<_ ⊆ DescentFrom _<_ P) where
+
+  private
+    descent∩ : Descent _<_ (P ∩ Acc _<_)
+    descent∩ (px , acc[x]) =
+      let y , y<x , py = accDescent acc[x] px
+      in  y , y<x , py , acc-inverse acc[x] y<x
+
+  accDescent∧acc⇒infiniteDescentFrom : Acc _<_ ⊆ InfiniteDescentFrom _<_ P
+  accDescent∧acc⇒infiniteDescentFrom acc[x] px =
+    let f , sequence[f] , Π[[P∩Acc]∘f] = descent∧acc⇒infiniteDescentFrom descent∩ acc[x] (px , acc[x])
+    in f , sequence[f] , proj₁ ∘ Π[[P∩Acc]∘f]
+
+  accDescent∧wf⇒infiniteDescent : WellFounded _<_ → InfiniteDescent _<_ P
+  accDescent∧wf⇒infiniteDescent wf = accDescent∧acc⇒infiniteDescentFrom (wf _)
+
+  accDescent∧acc⇒unsatisfiable : Acc _<_ ⊆ ∁ P
+  accDescent∧acc⇒unsatisfiable acc[x] px = descent∧acc⇒unsatisfiable descent∩ acc[x] (px , acc[x])
+
+  wf⇒empty : WellFounded _<_ → Empty P
+  wf⇒empty wf x = accDescent∧acc⇒unsatisfiable (wf x)
+
+------------------------------------------------------------------------
+-- Results about transitively-closed descent only from accessible elements
+
+module _ (accDescent⁺ : Acc _<_ ⊆ DescentFrom (TransClosure _<_) P) where
+
+  private
+    descent : Acc (TransClosure _<_) ⊆ DescentFrom (TransClosure _<_) P
+    descent = accDescent⁺  ∘ accessible⁻ _
+
+  accDescent⁺∧acc⇒infiniteDescentFrom⁺ : Acc _<_ ⊆ InfiniteDescentFrom⁺ _<_ P
+  accDescent⁺∧acc⇒infiniteDescentFrom⁺ acc[x] px
+    with f , (f0≡x , sequence[f]) , Π[P∘f]
+       ← accDescent∧acc⇒infiniteDescentFrom descent (accessible _ acc[x]) px
+       = f , (f0≡x , sequence⁺ sequence[f]) , Π[P∘f]
+
+  accDescent⁺∧wf⇒infiniteDescent⁺ : WellFounded _<_ → InfiniteDescent⁺ _<_ P
+  accDescent⁺∧wf⇒infiniteDescent⁺ wf = accDescent⁺∧acc⇒infiniteDescentFrom⁺ (wf _)
+
+  accDescent⁺∧acc⇒unsatisfiable : Acc _<_ ⊆ ∁ P
+  accDescent⁺∧acc⇒unsatisfiable = accDescent∧acc⇒unsatisfiable descent ∘ accessible _
+
+  accDescent⁺∧wf⇒empty : WellFounded _<_ → Empty P
+  accDescent⁺∧wf⇒empty = wf⇒empty descent ∘ (wellFounded _)
+
+------------------------------------------------------------------------
+-- Finally: the (classical) no smallest counterexample principle itself
+
+module _ (stable : Stable P) (noSmallest : NoSmallestCounterExample _<_ P) where
+
+  noSmallestCounterExample∧acc⇒satisfiable : Acc _<_ ⊆ P
+  noSmallestCounterExample∧acc⇒satisfiable =
+    stable _ ∘ accDescent⁺∧acc⇒unsatisfiable noSmallest
+
+  noSmallestCounterExample∧wf⇒universal : WellFounded _<_ → Universal P
+  noSmallestCounterExample∧wf⇒universal wf =
+    stable _ ∘ accDescent⁺∧wf⇒empty noSmallest wf

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

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

src/Relation/Unary.agda

@@ -14,7 +14,8 @@ open import Data.Product.Base using (_×_; _,_; Σ-syntax; ∃; uncurry; swap)
 open import Data.Sum.Base using (_⊎_; [_,_])
 open import Function.Base using (_∘_; _|>_)
 open import Level using (Level; _⊔_; 0ℓ; suc; Lift)
-open import Relation.Nullary as Nullary using (¬_; Dec; True)
+open import Relation.Nullary.Decidable.Core using (Dec; True)
+open import Relation.Nullary as Nullary using (¬_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 private
@@ -173,7 +174,7 @@ Irrelevant P = ∀ {x} → Nullary.Irrelevant (P x)
 Recomputable : Pred A ℓ → Set _
 Recomputable P = ∀ {x} → Nullary.Recomputable (P x)
 
--- Weak Decidability
+-- Stability - instances of P are stable wrt double negation
 
 Stable : Pred A ℓ → Set _
 Stable P = ∀ x → Nullary.Stable (P x)