📥 Download raw
{-# 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.