📥 Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Termination.BoveCapretta.Digits where

Digits, revisited

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Termination.Ordering
open import Padova2025.ProvingBasics.Termination.WellFounded.Base

Representing the function

data Def :   Set
f₀ : (n : )  Def n  

data Def where
  base : Def zero
  step : {x : }  Def (half (succ x))  Def (succ x)

f₀ zero       base     = zero
f₀ x@(succ _) (step p) = succ (f₀ (half x) p)

Verifying totality by well-founded induction

total : (x : )  Def x
total x = go x (ℕ-wf x)
  where
  go : (x : ) (gas : Acc _<'_ x)  Def x
  go zero       gas     = {!!}
  go x@(succ _) (acc f) = {!!}
digits₅ :   
digits₅ x = f₀ x (total x)

Verifying the defining equation

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
Def-prop : {x : } (p q : Def x)  p  q
Def-prop = {!!}
f₀-extensional : (x : ) (p q : Def x)  f₀ x p  f₀ x q
f₀-extensional = {!!}
digits₅-eq : (x : )  digits₅ (succ x)  succ (digits₅ (half (succ x)))
digits₅-eq = {!!}