agda-stdlib/src/Induction/NoInfiniteDescent.agda at d31034917c2b4565e509e0d4cd3a7d7f3421a182 · jamesmckinna/agda-stdlib · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
------------------------------------------------------------------------
-- 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.Nat.Base using (ℕ; zero; suc)
open import Data.Product.Base using (_,_; Σ-syntax; ∃-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.PropositionalEquality.Core
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Unary using (Pred; _∩_; _⇒_; IUniversal)

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

    AccDescent : Set _
    AccDescent = ∀[ Acc _<_ ⇒ DescentAt ]

    Descent : Set _
    Descent = ∀[ DescentAt ]

    InfiniteDescentAt : Pred A _
    InfiniteDescentAt x = P x →
      Σ[ f ∈ (ℕ → A) ] f zero ≡ x × ∀ n → f (suc n) < f n × P (f n)

    AccInfiniteDescent : Set _
    AccInfiniteDescent = ∀[ Acc _<_ ⇒ InfiniteDescentAt ]

    InfiniteDescent : Set _
    InfiniteDescent = ∀[ InfiniteDescentAt ]

------------------------------------------------------------------------
-- Basic result: assumes unrestricted descent

    module Lemmas (descent : Descent) where

      accInfiniteDescent : AccInfiniteDescent
      accInfiniteDescent {x} = Some.wfRec InfiniteDescentAt rec x
        where
        rec : _
        rec y rec[y] py
          with z , z<y , pz ← descent py
          with g , g0≡z , g<P ← rec[y] z<y pz
            = f , f0≡y , f<P
          where
          f : ℕ → A
          f zero = y
          f (suc n) = g n
          f0≡y : f zero ≡ y
          f0≡y = refl
          f<P : ∀ n → f (suc n) < f n × P (f n)
          f<P zero rewrite g0≡z = z<y , py
          f<P (suc n)           = g<P n

      wfInfiniteDescent : WellFounded _<_ → InfiniteDescent
      wfInfiniteDescent wf = accInfiniteDescent (wf _)

      accNoInfiniteDescent : ∀[ Acc _<_ ⇒ ¬_ ∘ P ]
      accNoInfiniteDescent {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

      wfNoInfiniteDescent : WellFounded _<_ → ∀[ ¬_ ∘ P ]
      wfNoInfiniteDescent wf = accNoInfiniteDescent (wf _)

------------------------------------------------------------------------
-- Extended result: assumes descent only for accessible elements

module _ {_<_ : Rel A r} (P : Pred A ℓ) where

    open InfiniteDescent _<_ P public

    module Corollaries (descent : AccDescent) where

      private

        P∩Acc : Pred A _
        P∩Acc = P ∩ (Acc _<_)

        module ID∩ = InfiniteDescent _<_ P∩Acc

        descent∩ : ID∩.Descent
        descent∩ (px , ax) = let y , y<x , py = descent ax px in
          y , y<x , py , acc-inverse ax y<x

        module Lemmas∩ = ID∩.Lemmas descent∩

      accInfiniteDescent : AccInfiniteDescent
      accInfiniteDescent {x} ax px =
        let f , f0≡x , f<P∩ = Lemmas∩.accInfiniteDescent ax (px , ax)
        in f , f0≡x , λ n → let f∘suc<f , Pf , _ = f<P∩ n in f∘suc<f , Pf

      wfInfiniteDescent : WellFounded _<_ → InfiniteDescent
      wfInfiniteDescent wf = accInfiniteDescent (wf _)

      accNoInfiniteDescent : ∀[ Acc _<_ ⇒ ¬_ ∘ P ]
      accNoInfiniteDescent ax px = Lemmas∩.accNoInfiniteDescent ax (px , ax)

      wfNoInfiniteDescent : WellFounded _<_ → ∀[ ¬_ ∘ P ]
      wfNoInfiniteDescent wf = accNoInfiniteDescent (wf _)

------------------------------------------------------------------------
-- Exports

open Corollaries public