|
| 1 | +------------------------------------------------------------------------ |
| 2 | +-- The Agda standard library |
| 3 | +-- |
| 4 | +-- A standard consequence of accessibility/well-foundedness: |
| 5 | +-- the impossibility of 'infinite descent' from any (accessible) |
| 6 | +-- element x satisfying P to 'smaller' y also satisfying P |
| 7 | +------------------------------------------------------------------------ |
| 8 | + |
| 9 | +{-# OPTIONS --cubical-compatible --safe #-} |
| 10 | + |
| 11 | +module Induction.InfiniteDescent where |
| 12 | + |
| 13 | +open import Data.Nat.Base as ℕ using (ℕ; zero; suc) |
| 14 | +open import Data.Nat.Properties as ℕ |
| 15 | +open import Data.Product.Base using (_,_; proj₁; ∃-syntax; _×_) |
| 16 | +open import Function.Base using (_∘_) |
| 17 | +open import Induction.WellFounded |
| 18 | + using (WellFounded; Acc; acc; acc-inverse; module Some) |
| 19 | +open import Level using (Level) |
| 20 | +open import Relation.Binary.Core using (Rel) |
| 21 | +open import Relation.Binary.Construct.Closure.Transitive |
| 22 | +open import Relation.Binary.PropositionalEquality.Core |
| 23 | +open import Relation.Nullary.Negation.Core as Negation using (¬_) |
| 24 | +open import Relation.Unary |
| 25 | + using (Pred; ∁; _∩_; _⊆_; _⇒_; Universal; IUniversal; Stable; Empty) |
| 26 | + |
| 27 | +private |
| 28 | + variable |
| 29 | + a r ℓ : Level |
| 30 | + A : Set a |
| 31 | + f : ℕ → A |
| 32 | + _<_ : Rel A r |
| 33 | + P : Pred A ℓ |
| 34 | + |
| 35 | +------------------------------------------------------------------------ |
| 36 | +-- Definitions |
| 37 | + |
| 38 | +InfiniteDescendingSequence : Rel A r → (ℕ → A) → Set _ |
| 39 | +InfiniteDescendingSequence _<_ f = ∀ n → f (suc n) < f n |
| 40 | + |
| 41 | +InfiniteDescendingSequenceFrom : Rel A r → (ℕ → A) → Pred A _ |
| 42 | +InfiniteDescendingSequenceFrom _<_ f x = f zero ≡ x × InfiniteDescendingSequence _<_ f |
| 43 | + |
| 44 | +InfiniteDescendingSequence⁺ : Rel A r → (ℕ → A) → Set _ |
| 45 | +InfiniteDescendingSequence⁺ _<_ f = ∀ {m n} → m ℕ.< n → TransClosure _<_ (f n) (f m) |
| 46 | + |
| 47 | +InfiniteDescendingSequenceFrom⁺ : Rel A r → (ℕ → A) → Pred A _ |
| 48 | +InfiniteDescendingSequenceFrom⁺ _<_ f x = f zero ≡ x × InfiniteDescendingSequence⁺ _<_ f |
| 49 | + |
| 50 | +DescentFrom : Rel A r → Pred A ℓ → Pred A _ |
| 51 | +DescentFrom _<_ P x = P x → ∃[ y ] y < x × P y |
| 52 | + |
| 53 | +Descent : Rel A r → Pred A ℓ → Set _ |
| 54 | +Descent _<_ P = ∀ {x} → DescentFrom _<_ P x |
| 55 | + |
| 56 | +InfiniteDescentFrom : Rel A r → Pred A ℓ → Pred A _ |
| 57 | +InfiniteDescentFrom _<_ P x = P x → ∃[ f ] InfiniteDescendingSequenceFrom _<_ f x × ∀ n → P (f n) |
| 58 | + |
| 59 | +InfiniteDescent : Rel A r → Pred A ℓ → Set _ |
| 60 | +InfiniteDescent _<_ P = ∀ {x} → InfiniteDescentFrom _<_ P x |
| 61 | + |
| 62 | +InfiniteDescentFrom⁺ : Rel A r → Pred A ℓ → Pred A _ |
| 63 | +InfiniteDescentFrom⁺ _<_ P x = P x → ∃[ f ] InfiniteDescendingSequenceFrom⁺ _<_ f x × ∀ n → P (f n) |
| 64 | + |
| 65 | +InfiniteDescent⁺ : Rel A r → Pred A ℓ → Set _ |
| 66 | +InfiniteDescent⁺ _<_ P = ∀ {x} → InfiniteDescentFrom⁺ _<_ P x |
| 67 | + |
| 68 | +NoSmallestCounterExample : Rel A r → Pred A ℓ → Set _ |
| 69 | +NoSmallestCounterExample _<_ P = ∀ {x} → Acc _<_ x → DescentFrom (TransClosure _<_) (∁ P) x |
| 70 | + |
| 71 | +------------------------------------------------------------------------ |
| 72 | +-- We can swap between transitively closed and non-transitively closed |
| 73 | +-- definitions |
| 74 | + |
| 75 | +sequence⁺ : InfiniteDescendingSequence (TransClosure _<_) f → |
| 76 | + InfiniteDescendingSequence⁺ _<_ f |
| 77 | +sequence⁺ {_<_ = _<_} {f = f} seq[f] = seq⁺[f]′ ∘ ℕ.<⇒<′ |
| 78 | + where |
| 79 | + seq⁺[f]′ : ∀ {m n} → m ℕ.<′ n → TransClosure _<_ (f n) (f m) |
| 80 | + seq⁺[f]′ ℕ.<′-base = seq[f] _ |
| 81 | + seq⁺[f]′ (ℕ.<′-step m<′n) = seq[f] _ ++ seq⁺[f]′ m<′n |
| 82 | + |
| 83 | +sequence⁻ : InfiniteDescendingSequence⁺ _<_ f → |
| 84 | + InfiniteDescendingSequence (TransClosure _<_) f |
| 85 | +sequence⁻ seq[f] = seq[f] ∘ n<1+n |
| 86 | + |
| 87 | +------------------------------------------------------------------------ |
| 88 | +-- Results about unrestricted descent |
| 89 | + |
| 90 | +module _ (descent : Descent _<_ P) where |
| 91 | + |
| 92 | + descent∧acc⇒infiniteDescentFrom : (Acc _<_) ⊆ (InfiniteDescentFrom _<_ P) |
| 93 | + descent∧acc⇒infiniteDescentFrom {x} = |
| 94 | + Some.wfRec (InfiniteDescentFrom _<_ P) rec x |
| 95 | + where |
| 96 | + rec : _ |
| 97 | + rec y rec[y] py |
| 98 | + with z , z<y , pz ← descent py |
| 99 | + with g , (g0≡z , g<P) , Π[P∘g] ← rec[y] z<y pz |
| 100 | + = h , (h0≡y , h<P) , Π[P∘h] |
| 101 | + where |
| 102 | + h : ℕ → _ |
| 103 | + h zero = y |
| 104 | + h (suc n) = g n |
| 105 | + |
| 106 | + h0≡y : h zero ≡ y |
| 107 | + h0≡y = refl |
| 108 | + |
| 109 | + h<P : ∀ n → h (suc n) < h n |
| 110 | + h<P zero rewrite g0≡z = z<y |
| 111 | + |
| 112 | + |
| 113 | + Π[P∘h] : ∀ n → P (h n) |
| 114 | + Π[P∘h] zero rewrite g0≡z = py |
| 115 | + Π[P∘h] (suc n) = Π[P∘g] n |
| 116 | + |
| 117 | + descent∧wf⇒infiniteDescent : WellFounded _<_ → InfiniteDescent _<_ P |
| 118 | + descent∧wf⇒infiniteDescent wf = descent∧acc⇒infiniteDescentFrom (wf _) |
| 119 | + |
| 120 | + descent∧acc⇒unsatisfiable : Acc _<_ ⊆ ∁ P |
| 121 | + descent∧acc⇒unsatisfiable {x} = Some.wfRec (∁ P) rec x |
| 122 | + where |
| 123 | + rec : _ |
| 124 | + rec y rec[y] py = let z , z<y , pz = descent py in rec[y] z<y pz |
| 125 | + |
| 126 | + descent∧wf⇒empty : WellFounded _<_ → Empty P |
| 127 | + descent∧wf⇒empty wf x = descent∧acc⇒unsatisfiable (wf x) |
| 128 | + |
| 129 | +------------------------------------------------------------------------ |
| 130 | +-- Results about descent only from accessible elements |
| 131 | + |
| 132 | +module _ (accDescent : Acc _<_ ⊆ DescentFrom _<_ P) where |
| 133 | + |
| 134 | + private |
| 135 | + descent∩ : Descent _<_ (P ∩ Acc _<_) |
| 136 | + descent∩ (px , acc[x]) = |
| 137 | + let y , y<x , py = accDescent acc[x] px |
| 138 | + in y , y<x , py , acc-inverse acc[x] y<x |
| 139 | + |
| 140 | + accDescent∧acc⇒infiniteDescentFrom : Acc _<_ ⊆ InfiniteDescentFrom _<_ P |
| 141 | + accDescent∧acc⇒infiniteDescentFrom acc[x] px = |
| 142 | + let f , sequence[f] , Π[[P∩Acc]∘f] = descent∧acc⇒infiniteDescentFrom descent∩ acc[x] (px , acc[x]) |
| 143 | + in f , sequence[f] , proj₁ ∘ Π[[P∩Acc]∘f] |
| 144 | + |
| 145 | + accDescent∧wf⇒infiniteDescent : WellFounded _<_ → InfiniteDescent _<_ P |
| 146 | + accDescent∧wf⇒infiniteDescent wf = accDescent∧acc⇒infiniteDescentFrom (wf _) |
| 147 | + |
| 148 | + accDescent∧acc⇒unsatisfiable : Acc _<_ ⊆ ∁ P |
| 149 | + accDescent∧acc⇒unsatisfiable acc[x] px = descent∧acc⇒unsatisfiable descent∩ acc[x] (px , acc[x]) |
| 150 | + |
| 151 | + wf⇒empty : WellFounded _<_ → Empty P |
| 152 | + wf⇒empty wf x = accDescent∧acc⇒unsatisfiable (wf x) |
| 153 | + |
| 154 | +------------------------------------------------------------------------ |
| 155 | +-- Results about transitively-closed descent only from accessible elements |
| 156 | + |
| 157 | +module _ (accDescent⁺ : Acc _<_ ⊆ DescentFrom (TransClosure _<_) P) where |
| 158 | + |
| 159 | + private |
| 160 | + descent : Acc (TransClosure _<_) ⊆ DescentFrom (TransClosure _<_) P |
| 161 | + descent = accDescent⁺ ∘ accessible⁻ _ |
| 162 | + |
| 163 | + accDescent⁺∧acc⇒infiniteDescentFrom⁺ : Acc _<_ ⊆ InfiniteDescentFrom⁺ _<_ P |
| 164 | + accDescent⁺∧acc⇒infiniteDescentFrom⁺ acc[x] px |
| 165 | + with f , (f0≡x , sequence[f]) , Π[P∘f] |
| 166 | + ← accDescent∧acc⇒infiniteDescentFrom descent (accessible _ acc[x]) px |
| 167 | + = f , (f0≡x , sequence⁺ sequence[f]) , Π[P∘f] |
| 168 | + |
| 169 | + accDescent⁺∧wf⇒infiniteDescent⁺ : WellFounded _<_ → InfiniteDescent⁺ _<_ P |
| 170 | + accDescent⁺∧wf⇒infiniteDescent⁺ wf = accDescent⁺∧acc⇒infiniteDescentFrom⁺ (wf _) |
| 171 | + |
| 172 | + accDescent⁺∧acc⇒unsatisfiable : Acc _<_ ⊆ ∁ P |
| 173 | + accDescent⁺∧acc⇒unsatisfiable = accDescent∧acc⇒unsatisfiable descent ∘ accessible _ |
| 174 | + |
| 175 | + accDescent⁺∧wf⇒empty : WellFounded _<_ → Empty P |
| 176 | + accDescent⁺∧wf⇒empty = wf⇒empty descent ∘ (wellFounded _) |
| 177 | + |
| 178 | +------------------------------------------------------------------------ |
| 179 | +-- Finally: the (classical) no smallest counterexample principle itself |
| 180 | + |
| 181 | +module _ (stable : Stable P) (noSmallest : NoSmallestCounterExample _<_ P) where |
| 182 | + |
| 183 | + noSmallestCounterExample∧acc⇒satisfiable : Acc _<_ ⊆ P |
| 184 | + noSmallestCounterExample∧acc⇒satisfiable = |
| 185 | + stable _ ∘ accDescent⁺∧acc⇒unsatisfiable noSmallest |
| 186 | + |
| 187 | + noSmallestCounterExample∧wf⇒universal : WellFounded _<_ → Universal P |
| 188 | + noSmallestCounterExample∧wf⇒universal wf = |
| 189 | + stable _ ∘ accDescent⁺∧wf⇒empty noSmallest wf |
0 commit comments