{-# 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 ℓ
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
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
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)
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)
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 _)
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