πŸ“₯ Download raw
module Padova2025.ProvingBasics.Termination.WellFounded.Examples where

Examples

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Termination.WellFounded.Base
import Padova2025.ProvingBasics.Termination.WellFounded.Scheme as Scheme

Digits, revisited

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

Reimplement the digitsβ‚„ function using the general recursion scheme by following the sketched outline.

digits-step : (x : β„•) β†’ ((y : β„•) β†’ y <' x β†’ β„•) β†’ β„•
digits-step zero       f = {!!}
digits-step x@(succ _) f = {!!}

digits-step-extensional
  : (x : β„•) (u v : (y : β„•) β†’ y <' x β†’ β„•)
  β†’ ((y : β„•) (p : y <' x) β†’ u y p ≑ v y p)
  β†’ digits-step x u ≑ digits-step x v
digits-step-extensional = {!!}

module D = Scheme {β„•} _<'_ {Ξ» _ β†’ β„•} digits-step digits-step-extensional β„•-wf

digitsβ‚„' : β„• β†’ β„•
digitsβ‚„' = D.rec

digitsβ‚„'-eq : (x : β„•) β†’ digitsβ‚„' (succ x) ≑ succ (digitsβ‚„' (half (succ x)))
digitsβ‚„'-eq x = D.rec-eq (succ x)

Modulo, revisited

open import Padova2025.ProvingBasics.EvenOdd
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Termination.Ordering

Reimplement the _%_ function using the general recursion scheme by following the sketched outline.

%-step : (b : β„•) β†’ IsPositive b β†’ (x : β„•) β†’ ((y : β„•) β†’ y <' x β†’ β„•) β†’ β„•
%-step = {!!}

%-step-extensional
  : (b : β„•) β†’ (b>0 : IsPositive b)
  β†’ (x : β„•) (u v : (y : β„•) β†’ y <' x β†’ β„•)
  β†’ ((y : β„•) (p : y <' x) β†’ u y p ≑ v y p)
  β†’ %-step b b>0 x u ≑ %-step b b>0 x v
%-step-extensional b b>0 x u v p with ≀-<-connex b x
... | left  b≀x = p (x ∸ b) (<β‡’<' (monus-< x b b>0 b≀x))
... | right x<b = refl

module M (b : β„•) (b>0 : IsPositive b) = Scheme {β„•} _<'_ {Ξ» _ β†’ β„•} (%-step b b>0) (%-step-extensional b b>0) β„•-wf

_%'_ : β„• β†’ β„• β†’ β„•
a %' zero   = a
a %' succ b = M.rec (succ b) (case-succ b) a

%'-<β‚€ : (a b : β„•) β†’ (b>0 : IsPositive b) β†’ a β‰₯ b β†’ %-step b b>0 a (Ξ» y y<a β†’ M.rec b b>0 y) < b
%'-<β‚€ a (succ b) b>0 aβ‰₯b with ≀-<-connex (succ b) a
... | left  b<a = {!%'-<β‚€ (a ∸ succ b) (succ b) b>0!}
... | right a≀b = a≀b