    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some examples of how to use non-trivial induction over the natural
    -- numbers.
    ------------------------------------------------------------------------

    module README.Data.Nat.Induction where

    open import Data.Nat
    open import Data.Nat.Induction
    open import Data.Product.Base using (_,_)
    open import Function.Base using (_∘_)
    open import Induction.WellFounded
    open import Relation.Binary.PropositionalEquality

    private

      n<′1+n : ∀ {n} → n <′ suc n
      n<′1+n = ≤′-refl

      n<′2+n : ∀ {n} → n <′ suc (suc n)
      n<′2+n = ≤′-step ≤′-refl

    -- Doubles its input.

    twice : ℕ → ℕ
    twice = rec _ λ
      { zero    _       → zero
      ; (suc n) twice-n → suc (suc twice-n)
      }

    -- Halves its input (rounding downwards).
    --
    -- The step function is mentioned in a proof below, so it has been
    -- given a name. (The mutual keyword is used to avoid having to give
    -- a type signature for the step function.)

    mutual

      half₁-step = λ
        { zero          _                → zero
        ; (suc zero)    _                → zero
        ; (suc (suc n)) (_ , half₁n , _) → suc half₁n
        }

      half₁ : ℕ → ℕ
      half₁ = cRec _ half₁-step

    -- An alternative implementation of half₁.

    mutual

      half₂-step = λ
        { zero          _   → zero
        ; (suc zero)    _   → zero
        ; (suc (suc n)) rec → suc (rec n<′2+n)
        }

      half₂ : ℕ → ℕ
      half₂ = <′-rec _ half₂-step

    -- The application half₁ (2 + n) is definitionally equal to
    -- 1 + half₁ n. Perhaps it is instructive to see why.

    half₁-2+ : ∀ n → half₁ (2 + n) ≡ 1 + half₁ n
    half₁-2+ n = begin

      half₁ (2 + n)                                                         ≡⟨⟩

      cRec _ half₁-step (2 + n)                                             ≡⟨⟩

      half₁-step (2 + n) (cRecBuilder _ half₁-step (2 + n))                 ≡⟨⟩

      half₁-step (2 + n)
        (let ih = cRecBuilder _ half₁-step (1 + n) in
         half₁-step (1 + n) ih , ih)                                        ≡⟨⟩

      half₁-step (2 + n)
        (let ih = cRecBuilder _ half₁-step n in
         half₁-step (1 + n) (half₁-step n ih , ih) , half₁-step n ih , ih)  ≡⟨⟩

      1 + half₁-step n (cRecBuilder _ half₁-step n)                         ≡⟨⟩

      1 + cRec _ half₁-step n                                               ≡⟨⟩

      1 + half₁ n                                                           ∎

      where open ≡-Reasoning

    -- The application half₂ (2 + n) is definitionally equal to
    -- 1 + half₂ n. Perhaps it is instructive to see why.

    half₂-2+ : ∀ n → half₂ (2 + n) ≡ 1 + half₂ n
    half₂-2+ n = begin

      half₂ (2 + n)                                               ≡⟨⟩

      <′-rec _ half₂-step (2 + n)                                 ≡⟨⟩

      half₂-step (2 + n) (<′-recBuilder _ half₂-step (2 + n))     ≡⟨⟩

      1 + <′-recBuilder _ half₂-step (2 + n) n<′2+n  ≡⟨⟩

      1 + Some.wfRecBuilder _ half₂-step (2 + n)
            (<′-wellFounded (2 + n)) n<′2+n          ≡⟨⟩

      1 + Some.wfRecBuilder _ half₂-step (2 + n)
            (acc (<′-wellFounded′ (2 + n))) n<′2+n   ≡⟨⟩

      1 + half₂-step n
            (Some.wfRecBuilder _ half₂-step n
               (<′-wellFounded′ (2 + n) n<′2+n))     ≡⟨⟩

      1 + half₂-step n
            (Some.wfRecBuilder _ half₂-step n
               (<′-wellFounded′ (1 + n) n<′1+n))               ≡⟨⟩

      1 + half₂-step n
            (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩

      1 + half₂-step n (<′-recBuilder _ half₂-step n)             ≡⟨⟩

      1 + <′-rec _ half₂-step n                                   ≡⟨⟩

      1 + half₂ n                                                 ∎

      where open ≡-Reasoning

    -- Some properties that the functions above satisfy, proved using
    -- cRec.

    half₁-+₁ : ∀ n → half₁ (twice n) ≡ n
    half₁-+₁ = cRec _ λ
      { zero          _                        → refl
      ; (suc zero)    _                        → refl
      ; (suc (suc n)) (_ , half₁twice-n≡n , _) →
          cong (suc ∘ suc) half₁twice-n≡n
      }

    half₂-+₁ : ∀ n → half₂ (twice n) ≡ n
    half₂-+₁ = cRec _ λ
      { zero          _                        → refl
      ; (suc zero)    _                        → refl
      ; (suc (suc n)) (_ , half₁twice-n≡n , _) →
          cong (suc ∘ suc) half₁twice-n≡n
      }

    -- Some properties that the functions above satisfy, proved using
    -- <′-rec.

    half₁-+₂ : ∀ n → half₁ (twice n) ≡ n
    half₁-+₂ = <′-rec _ λ
      { zero          _   → refl
      ; (suc zero)    _   → refl
      ; (suc (suc n)) rec →
          cong (suc ∘ suc) (rec n<′2+n)
      }

    half₂-+₂ : ∀ n → half₂ (twice n) ≡ n
    half₂-+₂ = <′-rec _ λ
      { zero          _   → refl
      ; (suc zero)    _   → refl
      ; (suc (suc n)) rec →
          cong (suc ∘ suc) (rec n<′2+n)
      }