πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}
open import Padova2025.ProvingBasics.Termination.WellFounded.Base
open import Padova2025.ProvingBasics.Equality.Base

The purpose of this module is to provide, given a recursion rule called step in the context of a well-founded relation, the resulting recursive function rec together with a verification that it validates the recursion rule.

module Padova2025.ProvingBasics.Termination.WellFounded.Scheme
  {X : Set}
  (_<_ : X β†’ X β†’ Set)
  {A : X β†’ Set}
  (step : (x : X) β†’ ((y : X) β†’ y < x β†’ A y) β†’ A x)
  (step-extensional : (x : X) (u v : (y : X) β†’ y < x β†’ A y) β†’ ((y : X) (p : y < x) β†’ u y p ≑ v y p) β†’ step x u ≑ step x v)
  (wf : (x : X) β†’ Acc _<_ x)
  where

A general recursion scheme

go : (x : X) β†’ Acc _<_ x β†’ A x
go = {!!}

rec : (x : X) β†’ A x
rec x = go x (wf x)

go-extensional : (x : X) (p q : Acc _<_ x) β†’ go x p ≑ go x q
go-extensional = {!!}

Assuming function extensionality, we can verify (without supposing step-extensional) that any two values of type Acc _<_ x are equal and hence trivially conclude go-extensional just with cong (go x). Function extensionality is not available in standard Agda, but (unless we introduce custom postulates) it is also not refuted. Hence in practice, it should always be possible to supply step-extensional, even if it is a nuisance.

rec-eq : (x : X) β†’ rec x ≑ step x (Ξ» y y<x β†’ rec y)
rec-eq = {!!}