------------------------------------------------------------------------ -- The Agda standard library -- -- An abstraction of various forms of recursion/induction ------------------------------------------------------------------------ -- The idea underlying Induction.* comes from Epigram 1, see Section 4 -- of "The view from the left" by McBride and McKinna. -- Note: The types in this module can perhaps be easier to understand -- if they are normalised. Note also that Agda can do the -- normalisation for you. {-# OPTIONS --cubical-compatible --safe #-} module Induction where open import Level open import Relation.Unary open import Relation.Unary.PredicateTransformer using (PT) private variable a ℓ ℓ₁ ℓ₂ : Level A : Set a Q : Pred A ℓ Rec : PT A A ℓ₁ ℓ₂ ------------------------------------------------------------------------ -- A RecStruct describes the allowed structure of recursion. The -- examples in Data.Nat.Induction should explain what this is all -- about. RecStruct : Set a → (ℓ₁ ℓ₂ : Level) → Set _ RecStruct A = PT A A -- A recursor builder constructs an instance of a recursion structure -- for a given input. RecursorBuilder : RecStruct A ℓ₁ ℓ₂ → Set _ RecursorBuilder Rec = ∀ P → Rec P ⊆′ P → Universal (Rec P) -- A recursor can be used to actually compute/prove something useful. Recursor : RecStruct A ℓ₁ ℓ₂ → Set _ Recursor Rec = ∀ P → Rec P ⊆′ P → Universal P -- And recursors can be constructed from recursor builders. build : RecursorBuilder Rec → Recursor Rec build builder P f x = f x (builder P f x) -- We can repeat the exercise above for subsets of the type we are -- recursing over. SubsetRecursorBuilder : Pred A ℓ → RecStruct A ℓ₁ ℓ₂ → Set _ SubsetRecursorBuilder Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ Rec P SubsetRecursor : Pred A ℓ → RecStruct A ℓ₁ ℓ₂ → Set _ SubsetRecursor Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ P subsetBuild : SubsetRecursorBuilder Q Rec → SubsetRecursor Q Rec subsetBuild builder P f x q = f x (builder P f x q)