← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring-proposed

« back to all changes in this revision

Viewing changes to src/Induction.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Tags: upstream-0.3
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Induction.agda
 
1
------------------------------------------------------------------------
 
2
-- An abstraction of various forms of recursion/induction
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
-- Note: The types in this module can perhaps be easier to understand
 
8
-- if they are normalised. Note also that Agda can do the
 
9
-- normalisation for you.
 
10
 
 
11
module Induction where
 
12
 
 
13
open import Level
 
14
open import Relation.Unary
 
15
 
 
16
-- A RecStruct describes the allowed structure of recursion. The
 
17
-- examples in Induction.Nat should explain what this is all about.
 
18
 
 
19
RecStruct : ∀ {a} → Set a → Set (suc a)
 
20
RecStruct {a} A = Pred A a → Pred A a
 
21
 
 
22
-- A recursor builder constructs an instance of a recursion structure
 
23
-- for a given input.
 
24
 
 
25
RecursorBuilder : ∀ {a} {A : Set a} → RecStruct A → Set _
 
26
RecursorBuilder Rec = ∀ P → Rec P ⊆′ P → Universal (Rec P)
 
27
 
 
28
-- A recursor can be used to actually compute/prove something useful.
 
29
 
 
30
Recursor : ∀ {a} {A : Set a} → RecStruct A → Set _
 
31
Recursor Rec = ∀ P → Rec P ⊆′ P → Universal P
 
32
 
 
33
-- And recursors can be constructed from recursor builders.
 
34
 
 
35
build : ∀ {a} {A : Set a} {Rec : RecStruct A} →
 
36
        RecursorBuilder Rec →
 
37
        Recursor Rec
 
38
build builder P f x = f x (builder P f x)
 
39
 
 
40
-- We can repeat the exercise above for subsets of the type we are
 
41
-- recursing over.
 
42
 
 
43
SubsetRecursorBuilder : ∀ {a ℓ} {A : Set a} →
 
44
                        Pred A ℓ → RecStruct A → Set _
 
45
SubsetRecursorBuilder Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ Rec P
 
46
 
 
47
SubsetRecursor : ∀ {a ℓ} {A : Set a} →
 
48
                 Pred A ℓ → RecStruct A → Set _
 
49
SubsetRecursor Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ P
 
50
 
 
51
subsetBuild : ∀ {a ℓ} {A : Set a} {Q : Pred A ℓ} {Rec : RecStruct A} →
 
52
              SubsetRecursorBuilder Q Rec →
 
53
              SubsetRecursor Q Rec
 
54
subsetBuild builder P f x q = f x (builder P f x q)