{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Termination.BoveCapretta.Intricate0 where
An intricate zero function
open import Padova2025.ProgrammingBasics.Naturals.Base open import Padova2025.ProvingBasics.Equality.Base open import Padova2025.ProvingBasics.Equality.General
Let us consider the following recursive function definition.
f : ℕ → ℕ
f zero = zero
f (succ x) = f (f x)
Agda rejects this definition with the comment “Termination checking
failed”. Agda’s termination checker does not have any insight on what
the value of f x
in the recursive call f (f x)
will turn out to be. But even though this fact is not obvious to Agda,
the recursive call terminates and the function f
is
constantly zero.
Representing the function
To represent this function in Agda, we first introduce by
induction-recursion a predicate Def
and a function
f₀
. For a number n
, Def n
expresses that n
belongs to the domain, i.e. that the
recursion terminates on input n
. The function
f₀
takes two inputs, a number n
and a witness
that the recursion terminates on input n
, and computes the
result of the recursion.
data Def : ℕ → Set f₀ : (n : ℕ) → Def n → ℕ data Def where base : Def zero step : {x : ℕ} → (p : Def x) → Def (f₀ x p) → Def (succ x) f₀ zero _ = zero f₀ (succ x) (step p q) = f₀ (f₀ x p) q
As a warmup, we can prove that the numbers zero
,
one
, two
and three
indeed belong
to the domain:
defined-on-input-zero : Def zero defined-on-input-zero = {!!}
defined-on-input-one : Def one defined-on-input-one = step {!!} {!!}
defined-on-input-two : Def two defined-on-input-two = {!!}
defined-on-input-three : Def three defined-on-input-three = {!!}
Conditionally evaluating the function
Under the assumption that n
belongs to the function’s
domain, we can show that the value on input n
is zero:
all0 : (n : ℕ) → (p : Def n) → f₀ n p ≡ zero all0 = {!!}
Verifying totality
The insight expressed by all0
is enough to conclude that
the function is defined on all inputs.
total : (n : ℕ) → Def n total = {!!}
With totality in place, we can finally define f
as
follows.
f : ℕ → ℕ f n = f₀ n (total n)
Verifying the definition equation
We can also verify that the defining equation holds:
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 = {!!}
f-eq : (x : ℕ) → f (succ x) ≡ f (f x) f-eq x = f₀-extensional (f x) _ _