------------------------------------------------------------------------ -- The Agda standard library -- -- Well-founded induction ------------------------------------------------------------------------ open import Relation.Binary module Induction.WellFounded where open import Data.Product open import Function open import Induction open import Level open import Relation.Unary -- When using well-founded recursion you can recurse arbitrarily, as -- long as the arguments become smaller, and "smaller" is -- well-founded. WfRec : ∀ {a r} {A : Set a} → Rel A r → ∀ {ℓ} → RecStruct A ℓ _ WfRec _<_ P x = ∀ y → y < x → P y -- The accessibility predicate: x is accessible if everything which is -- smaller than x is also accessible (inductively). data Acc {a ℓ} {A : Set a} (_<_ : Rel A ℓ) (x : A) : Set (a ⊔ ℓ) where acc : (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x -- The accessibility predicate encodes what it means to be -- well-founded; if all elements are accessible, then _<_ is -- well-founded. Well-founded : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _ Well-founded _<_ = ∀ x → Acc _<_ x -- Well-founded induction for the subset of accessible elements: module Some {a lt} {A : Set a} {_<_ : Rel A lt} {ℓ} where wfRec-builder : SubsetRecursorBuilder (Acc _<_) (WfRec _<_ {ℓ = ℓ}) wfRec-builder P f x (acc rs) = λ y y