{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Termination.WellFounded.Base where
Well-founded relations
module _ {X : Set} (_<_ : X → X → Set) where data Acc : X → Set where acc : {x : X} → ({y : X} → y < x → Acc y) → Acc x acc-inverse : {x : X} → Acc x → {y : X} → y < x → Acc y acc-inverse (acc f) = f
open import Padova2025.ProgrammingBasics.Naturals.Base open import Padova2025.ProgrammingBasics.Naturals.Arithmetic open import Padova2025.ProvingBasics.Termination.Ordering hiding (_<_) renaming (_<'_ to _<_; base' to base; step' to step)
The natural numbers are well-founded
lemma-zero-is-accessible : Acc _<_ zero lemma-zero-is-accessible = acc λ ()
lemma-one-is-accessible : Acc _<_ one lemma-one-is-accessible = acc λ { base → lemma-zero-is-accessible }
lemma-two-is-accessible : Acc _<_ two lemma-two-is-accessible = acc λ { base → lemma-one-is-accessible ; (step base) → lemma-zero-is-accessible }
lemma-three-is-accessible : Acc _<_ three lemma-three-is-accessible = acc λ { base → lemma-two-is-accessible ; (step base) → lemma-one-is-accessible ; (step (step base)) → lemma-zero-is-accessible }
ℕ-wf : (n : ℕ) → Acc _<_ n ℕ-wf = {!!}
Exercise: Well-founded relations are irreflexive
open import Padova2025.ProvingBasics.Negation
wf⇒irr : {X : Set} → (R : X → X → Set) → (a : X) → Acc R a → ¬ (R a a) wf⇒irr = {!!}
Exercise: No infinite descending sequences
no-descending-sequences : {X : Set} {_<_ : X → X → Set} → (α : ℕ → X) → ((n : ℕ) → α (succ n) < α n) → Acc _<_ (α zero) → ⊥ no-descending-sequences = {!!}
Add remark about converse.
Exercise: Binary digits
digits₄ : ℕ → ℕ digits₄ x = go x (ℕ-wf x) where go : (x : ℕ) → (gas : Acc _<_ x) → ℕ go zero p = {!!} go x@(succ _) (acc f) = {!!}
Unlike with using natural numbers as gas as in digits₃
,
no bailout case is needed. This recursion will always reach its base
case—and no extra proof of this fact is needed.
The verification of the fundamental identity
digits₄ x ≡ succ (digits₄ (half x))
for positive
x
is best done in the greater generality offered by the next
module.