ReductionProblem.agda

{-# OPTIONS --without-K #-}

module ReductionProblem where

open import Agda.Builtin.Nat using (Nat; suc; zero)
open import Agda.Primitive using (_⊔_)
open import Agda.Builtin.Equality using (_≡_; refl)

-- The Acc type, defined as a record:
record Acc {a r} {A : Set a} (R : A → A → Set r) (x : A) : Set (a ⊔ r) where
  inductive
  constructor acc
  field step : ∀ y → R y x → Acc R y
open Acc public

WellFounded : ∀ {a r} {A : Set a} → (R : A → A → Set r) → Set (a ⊔ r)
WellFounded R = ∀ x → Acc R x

-- The usual ordering definition on Nats for well-founded recursion:
infix 4 _≤_
data _≤_ (n : Nat) : Nat → Set where
  ≤-refl : n ≤ n
  ≤-step : ∀ {m} → n ≤ m → n ≤ suc m

infix 4 _<_
_<_ : Nat → Nat → Set
n < m = suc n ≤ m

-- We can prove that it's well founded with copatterns:
≤-wellFounded : WellFounded _<_
step (≤-wellFounded (suc n)) .n ≤-refl      = ≤-wellFounded n
step (≤-wellFounded (suc n)) m (≤-step m<n) = ≤-wellFounded n .step m m<n

-- An identity function on Nats:
id₁ : Nat → Nat
id₁ zero    = zero
id₁ (suc n) = suc (id₁ n)

-- A contrived way to define an identity which fails the termination checker:
pred : Nat → Nat
pred zero    = zero
pred (suc n) = n

-- Fails the termination checker, as it should:
{-# TERMINATING #-}
id₂ : Nat → Nat
id₂ zero    = zero
id₂ (suc n) = suc (id₂ (pred (suc n)))

-- A version of id₂ which uses well-founded recursion:
id₃-helper : (n : Nat) → Acc _<_ n → Nat
id₃-helper zero    (acc wf) = zero
id₃-helper (suc n) (acc wf) = id₃-helper (pred (suc n)) (wf (pred (suc n)) ≤-refl)

id₃ : Nat → Nat
id₃ n = id₃-helper n (≤-wellFounded n)

-- id₁ and id₂ compute just fine; id₃ does not reduce at all.
_ : id₁ 10 ≡ 10
_ = refl

_ : id₂ 10 ≡ 10
_ = refl

_ : id₃ 10 ≡ 10
_ = refl

-- The error message is:
--   id₃-helper 10 (≤-wellFounded 10) != 10 of type Nat
--   when checking that the expression refl has type id₃ 10 ≡ 10