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

* basic result

* added missing lemma; is there a better name for this?

* renamed lemma

* final tidying up; `CHANGELOG`

* final tidying up

* missing `CHANGELOG` entry

* `InfiniteDescent` definition and proof

* revised `InfiniteDescent` definition and proof

* major revision: renames things, plus additional corollaries

* spacing

* added `NoSmallestCounterExample` principles for `Stable` predicates

* refactoring; move `Stable` to `Relation.Unary`

* refactoring; remove explicit definition of `CounterExample`

* refactoring; rename qualified `import`

* [fixes #2130] Moving `Properties.HeytingAlgebra` from `Relation.Binary` to `Relation.Binary.Lattice` (#2131)

* [fixes #2127] Fixes #1930 `import` bug (#2128)

* [fixes #1214] Add negated ordering relation symbols systematically to `Relation.Binary.*` (#2095)

* Refactoring (inversion) properties of `_<_` on `Nat`, plus consequences (#2000)

* Bump CI tests to Agda-2.6.4 (#2134)

* Remove `Algebra.Ordered` (#2133)

* [ fix ] missing name in LICENCE file (#2139)

* Add new blocking primitives to `Reflection.TCM` (#1972)

* Change definition of `IsStrictTotalOrder` (#2137)

* Add _<$>_ operator for Function bundle (#2144)

* [ fix #2086 ] new web deployment strategy (#2147)

* [ admin ] fix sorting logic (#2151)

With the previous script we were sorting entries of the form
html/vX.Y.Z/index.html but the order is such that vX.Y/ < vX.Y.Z/
and so we were ending up with v1.7 coming after v1.7.3.

This fixes that by using sed to get rid of the html/ prefix
and the /index.html suffix before the sorting phase.

* Add coincidence law to modules (#1898)

* Make reasoning modular by adding new `Reasoning.Syntax` module (#2152)

* Fixes typos identified in #2154 (#2158)

* tackles #2124 as regards `case_return_of_` (#2157)

* Rename preorder ~ relation reasoning combinators (#2156)

* Move ≡-Reasoning from Core to Properties and implement using syntax (#2159)

* Add consistent deprecation warnings to old function hierarchy (#2163)

* Rename symmetric reasoning combinators. Minimal set of changes (#2160)

* Restore 'return' as an alias for 'pure' (#2164)

* [ fix #2153 ] Properly re-export specialised combinators (#2161)

* Connect `LeftInverse` with (`Split`)`Surjection` (#2054)

* Added remaining flipped and negated relations to binary relation bundles (#2162)

* Tidy up CHANGELOG in preparation for release candidate (#2165)

* Spellcheck CHANGELOG (#2167)

* spellcheck; `fix-whitespace`; unfixed: a few alignment issues; typo `predications` to `predicates` in `Relation.Unary.Relation.Binary.Equality`

* Fixed Agda version typo in README (#2176)

* Fixed in deprecation warning for `<-transˡ` (#2173)

* Bump Haskell CI (original!) to latest minor GHC versions (#2187)

* [fixes #2175] Documentation misc. typos etc. for RC1  (#2183)

* missing comma!

* corrected reference to `README.Design.Decidability`

* typo: capitalisation

* updated `installation-guide`

* added word to `NonZero` section heading

* Run workflows on any PR

* Add merge-group trigger to workflows

---------

Co-authored-by: MatthewDaggitt <[email protected]>

* [fixes #2178] regularise and specify/systematise, the conventions for symbol usage (#2185)

* regularise and specify/systematise, the conventions for symbol usage

* typos/revisions

* Move `T?` to `Relation.Nullary.Decidable.Core` (#2189)

* Move `T?` to `Relation.Nullary.Decidable.Core`

* Var name fix

* Some refactoring

* Fix failing tests and address remaining comments

* Fix style-guide

* Make decidable versions of sublist functions the default (#2186)

* Make decdable versions of sublist functions the default

* Remove imports Bool.Properties

* Address comments

* new `CHANGELOG`

* resolved merge conflict

* resolved merge conflict, this time

* revised in line with review comments

* tweaked `export`s; does that fix things now?

* Fix merge mistake

* Refactored to remove a indirection and nested modules

* Touch up names

* Reintroduce anonymous module for descent

* cosmetics asper final comment

---------

Co-authored-by: MatthewDaggitt <[email protected]>
Co-authored-by: G. Allais <[email protected]>
Co-authored-by: Amélia <[email protected]>
Co-authored-by: Nathan van Doorn <[email protected]>
Co-authored-by: James Wood <[email protected]>
Co-authored-by: Andreas Abel <[email protected]>

Author: 7 people

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
@@ -254,6 +259,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)