Induction principle for RoseTrees

RoseTree.agda

module RoseTree where

open import Level
open import Data.List as List
open import Data.Unit
open import Data.Product

data RoseTree {ℓ : Level} (A : Set ℓ) : Set ℓ where
  node : (a : A) (ts : List (RoseTree A)) → RoseTree A

All : {ℓ ℓ′ : Level} {A : Set ℓ} (P : A → Set ℓ′) → List A → Set ℓ′
All P []       = Lift ⊤
All P (t ∷ ts) = P t × All P ts

module Induction
       {ℓ ℓ′ : Level}
       {A : Set ℓ}
       (P : RoseTree A → Set ℓ′)
       (ih : (a : A) {ts : List (RoseTree A)} → All P ts → P (node a ts))
       where

  mutual

    induction : (t : RoseTree A) → P t
    induction (node a ts) = ih a (inductions ts)

    inductions : (ts : List (RoseTree A)) → All P ts
    inductions []       = lift tt
    inductions (t ∷ ts) = induction t , inductions ts

module Induction′
       {ℓ ℓ′ ℓ′′ : Level}
       {A   : Set ℓ}
       (P   : RoseTree A → Set ℓ′)
       (Q   : List (RoseTree A) → Set ℓ′′)
       (Q[] : Q [])
       (Q∷  : {t : RoseTree A} {ts : List (RoseTree A)} → P t → Q ts → Q (t ∷ ts))
       (ih  : (a : A) {ts : List (RoseTree A)} → Q ts → P (node a ts))
       where

  mutual

    induction : (t : RoseTree A) → P t
    induction (node a ts) = ih a (inductions ts)

    inductions : (ts : List (RoseTree A)) → Q ts
    inductions []       = Q[]
    inductions (t ∷ ts) = Q∷ (induction t) (inductions ts)