← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Induction/Nat.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Induction/Nat.agda
4
4
 
5
5
module Induction.Nat where
6
6
 
7
 
open import Data.Function
 
7
open import Function
8
8
open import Data.Nat
9
9
open import Data.Fin
10
10
open import Data.Fin.Props
11
11
open import Data.Product
12
12
open import Data.Unit
13
13
open import Induction
14
 
import Induction.WellFounded as WF
 
14
open import Induction.WellFounded as WF
15
15
open import Relation.Binary.PropositionalEquality
 
16
open import Relation.Unary
16
17
 
17
18
------------------------------------------------------------------------
18
19
-- Ordinary induction
46
47
------------------------------------------------------------------------
47
48
-- Complete induction based on _<′_
48
49
 
49
 
open WF _<′_ using (acc) renaming (Acc to <-Acc)
50
 
 
51
 
<-allAcc : ∀ n → <-Acc n
52
 
<-allAcc n = acc (helper n)
53
 
  where
54
 
  helper : ∀ n m → m <′ n → <-Acc m
55
 
  helper zero     _ ()
56
 
  helper (suc n) .n ≤′-refl       = acc (helper n)
57
 
  helper (suc n)  m (≤′-step m<n) = helper n m m<n
58
 
 
59
 
open WF _<′_ public using () renaming (WfRec to <-Rec)
60
 
open WF.All _<′_ <-allAcc public
 
50
<-Rec : RecStruct ℕ
 
51
<-Rec = WfRec _<′_
 
52
 
 
53
mutual
 
54
 
 
55
  <-well-founded : Well-founded _<′_
 
56
  <-well-founded n = acc (<-well-founded′ n)
 
57
 
 
58
  <-well-founded′ : ∀ n → <-Rec (Acc _<′_) n
 
59
  <-well-founded′ zero     _ ()
 
60
  <-well-founded′ (suc n) .n ≤′-refl       = <-well-founded n
 
61
  <-well-founded′ (suc n)  m (≤′-step m<n) = <-well-founded′ n m m<n
 
62
 
 
63
open WF.All <-well-founded public
61
64
  renaming ( wfRec-builder to <-rec-builder
62
65
           ; wfRec to <-rec
63
66
           )
65
68
------------------------------------------------------------------------
66
69
-- Complete induction based on _≺_
67
70
 
68
 
open WF _≺_ renaming (Acc to ≺-Acc)
69
 
 
70
 
<-Acc⇒≺-Acc : ∀ {n} → <-Acc n → ≺-Acc n
71
 
<-Acc⇒≺-Acc (acc rs) =
72
 
  acc (λ m m≺n → <-Acc⇒≺-Acc (rs m (≺⇒<′ m≺n)))
73
 
 
74
 
≺-allAcc : ∀ n → ≺-Acc n
75
 
≺-allAcc n = <-Acc⇒≺-Acc (<-allAcc n)
76
 
 
77
 
open WF _≺_ public using () renaming (WfRec to ≺-Rec)
78
 
open WF.All _≺_ ≺-allAcc public
 
71
≺-Rec : RecStruct ℕ
 
72
≺-Rec = WfRec _≺_
 
73
 
 
74
≺-well-founded : Well-founded _≺_
 
75
≺-well-founded = Subrelation.well-founded ≺⇒<′ <-well-founded
 
76
 
 
77
open WF.All ≺-well-founded public
79
78
  renaming ( wfRec-builder to ≺-rec-builder
80
79
           ; wfRec to ≺-rec
81
80
           )