------------------------------------------------------------------------
-- The Agda standard library
--
-- Various forms of induction for natural numbers
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Nat.Induction where

open import Function
open import Data.Nat.Base
open import Data.Nat.Properties using (≤⇒≤′; n<1+n)
open import Data.Product
open import Data.Unit.Polymorphic
open import Induction
open import Induction.WellFounded as WF
open import Level using (Level)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary

private
  variable
     : Level

------------------------------------------------------------------------
-- Re-export accessability

open WF public using (Acc; acc)

------------------------------------------------------------------------
-- Ordinary induction

Rec :    RecStruct   
Rec  P zero    = 
Rec  P (suc n) = P n

recBuilder :  {}  RecursorBuilder (Rec )
recBuilder P f zero    = _
recBuilder P f (suc n) = f n (recBuilder P f n)

rec :  {}  Recursor (Rec )
rec = build recBuilder

------------------------------------------------------------------------
-- Complete induction

CRec :    RecStruct   
CRec  P zero    = 
CRec  P (suc n) = P n × CRec  P n

cRecBuilder :  {}  RecursorBuilder (CRec )
cRecBuilder P f zero    = _
cRecBuilder P f (suc n) = f n ih , ih
  where ih = cRecBuilder P f n

cRec :  {}  Recursor (CRec )
cRec = build cRecBuilder

------------------------------------------------------------------------
-- Complete induction based on _<′_

<′-Rec :  {}  RecStruct   
<′-Rec = WfRec _<′_

mutual

  <′-wellFounded : WellFounded _<′_
  <′-wellFounded n = acc (<′-wellFounded′ n)

  <′-wellFounded′ :  n  <′-Rec (Acc _<′_) n
  <′-wellFounded′ (suc n) .n ≤′-refl       = <′-wellFounded n
  <′-wellFounded′ (suc n)  m (≤′-step m<n) = <′-wellFounded′ n m m<n

module _ {} where
  open WF.All <′-wellFounded  public
    renaming ( wfRecBuilder to <′-recBuilder
             ; wfRec        to <′-rec
             )
    hiding (wfRec-builder)

------------------------------------------------------------------------
-- Complete induction based on _<_

<-Rec :  {}  RecStruct   
<-Rec = WfRec _<_

<-wellFounded : WellFounded _<_
<-wellFounded = Subrelation.wellFounded ≤⇒≤′ <′-wellFounded

-- A version of `<-wellFounded` that cheats by skipping building
-- the first billion proofs. Use this when you require the function
-- using the proof of well-foundedness to evaluate fast.
--
-- IMPORTANT: You have to be a little bit careful when using this to always
-- make the function be strict in some other argument than the accessibility
-- proof, otherwise you will have neutral terms unfolding a billion times
-- before getting stuck.
<-wellFounded-fast : WellFounded _<_
<-wellFounded-fast = <-wellFounded-skip 1000000000
  where
  <-wellFounded-skip :  (k : )  WellFounded _<_
  <-wellFounded-skip zero    n       = <-wellFounded n
  <-wellFounded-skip (suc k) zero    = <-wellFounded 0
  <-wellFounded-skip (suc k) (suc n) = acc  m _  <-wellFounded-skip k m)

module _ {} where
  open WF.All <-wellFounded  public
    renaming ( wfRecBuilder to <-recBuilder
             ; wfRec        to <-rec
             )
    hiding (wfRec-builder)