{-# 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 does indeed terminate and the function f is constantly zero. The goal of this section is to represent this function in Agda in a way that Agda accepts and then verify totality.

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) _ _