/usr/share/agda-stdlib/Induction/Nat.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Various forms of induction for natural numbers
------------------------------------------------------------------------
module Induction.Nat where
open import Function
open import Data.Nat
open import Data.Fin
open import Data.Fin.Props
open import Data.Product
open import Data.Unit
open import Induction
open import Induction.WellFounded as WF
open import Relation.Binary.PropositionalEquality
open import Relation.Unary
------------------------------------------------------------------------
-- Ordinary induction
Rec : RecStruct ℕ
Rec P zero = ⊤
Rec P (suc n) = P n
rec-builder : RecursorBuilder Rec
rec-builder P f zero = tt
rec-builder P f (suc n) = f n (rec-builder P f n)
rec : Recursor Rec
rec = build rec-builder
------------------------------------------------------------------------
-- Complete induction
CRec : RecStruct ℕ
CRec P zero = ⊤
CRec P (suc n) = P n × CRec P n
cRec-builder : RecursorBuilder CRec
cRec-builder P f zero = tt
cRec-builder P f (suc n) = f n ih , ih
where ih = cRec-builder P f n
cRec : Recursor CRec
cRec = build cRec-builder
------------------------------------------------------------------------
-- Complete induction based on _<′_
<-Rec : RecStruct ℕ
<-Rec = WfRec _<′_
mutual
<-well-founded : Well-founded _<′_
<-well-founded n = acc (<-well-founded′ n)
<-well-founded′ : ∀ n → <-Rec (Acc _<′_) n
<-well-founded′ zero _ ()
<-well-founded′ (suc n) .n ≤′-refl = <-well-founded n
<-well-founded′ (suc n) m (≤′-step m<n) = <-well-founded′ n m m<n
open WF.All <-well-founded public
renaming ( wfRec-builder to <-rec-builder
; wfRec to <-rec
)
------------------------------------------------------------------------
-- Complete induction based on _≺_
≺-Rec : RecStruct ℕ
≺-Rec = WfRec _≺_
≺-well-founded : Well-founded _≺_
≺-well-founded = Subrelation.well-founded ≺⇒<′ <-well-founded
open WF.All ≺-well-founded public
renaming ( wfRec-builder to ≺-rec-builder
; wfRec to ≺-rec
)
------------------------------------------------------------------------
-- Examples
private
module Examples where
-- The half function.
HalfPred : ℕ → Set
HalfPred _ = ℕ
half₁ : ℕ → ℕ
half₁ = cRec HalfPred half₁'
where
half₁' : ∀ n → CRec HalfPred n → HalfPred n
half₁' zero _ = zero
half₁' (suc zero) _ = zero
half₁' (suc (suc n)) (_ , half₁n , _) = suc half₁n
half₂ : ℕ → ℕ
half₂ = <-rec HalfPred half₂'
where
half₂' : ∀ n → <-Rec HalfPred n → HalfPred n
half₂' zero _ = zero
half₂' (suc zero) _ = zero
half₂' (suc (suc n)) rec = suc (rec n (≤′-step ≤′-refl))
|