📥 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.