CPP 2022

deep.agda

-- Code supplement for CPP22
-- (C) 2022 Patricia Johann, Enrico Ghiorzi
-- This information is free; you can redistribute and/or modify it under the terms of CC BY-SA 4.0.

-- The code was originally for the paper "(Deep) Induction Rules for GADTs",
-- then modified by Favonia, released also under CC BY-SA 4.0

{-# OPTIONS --injective-type-constructors #-}

module _ where

open import Data.Product using (_×_ ; _,_ ; Σ-syntax ; ∃-syntax)
open import Data.List renaming ([] to nil ; _∷_ to cons)
open import Data.Unit using (⊤ ; tt)

open import Level renaming (suc to lsuc ; zero to lzero)

-- Introduction

data Rose : Set → Set where
  empty : ∀ {A : Set} → Rose A
  node  : ∀ {A : Set} → A → List (Rose A) → Rose A

-- lifting of predicates for List
List^ : ∀ {a} {l} (A : Set a) → (A → Set l) → List A → Set l
List^ A Qa nil = Lift _ ⊤
List^ A Qa (cons x xs) = Qa x × (List^ A Qa xs)

-- Pred A is the type of predicates on A valued in the l'th universe.
Pred : ∀ {l} {a} → (A : Set a) → Set _
Pred {l} A = A → Set l

-- PredMap A Q Q' is the type of morphisms from Q to Q'
PredMap : ∀ {l1 l2} {a} (A : Set a) → Pred {l1} A → Pred {l2} A → Set _
PredMap A Q Q' = ∀ (x : A) → Q x → Q' x

-- take a morphism of predicates from Q to Q' and return a morphism of predicates from (List^ A Q) to (List^ A Q')
liftListMap : ∀ {a} {l1 l2} (A : Set a) → (Q : A → Set l1) → (Q' : A → Set l2) → PredMap A Q Q' → PredMap (List A) (List^ A Q) (List^ A Q')
liftListMap A Q Q' m nil _ = lift tt
liftListMap A Q Q' m (cons a l') (y , x') = (m a y , liftListMap A Q Q' m l' x')

-- equation 1
--
-- structural induction rule for Rose

module _ (A : Set) (P : A → Set) where
  -- ListRose^ A P ts is morally List^ (Rose A) (Rose^ A P) ts
  ListRose^ : List (Rose A) → Set
  Rose^ : Rose A → Set

  ListRose^ nil = ⊤
  ListRose^ (cons x xs) = Rose^ x × ListRose^ xs

  Rose^ empty = ⊤
  Rose^ (node a ts) = P a × ListRose^ ts

module _
  (A : Set) (P : Rose A → Set) (Q : A → Set)
  (cempty : P empty)
  (cnode : ∀ (a : A) (ts : List (Rose A)) → Q a → List^ (Rose A) P ts → P (node a ts))
  where

  indRose : ∀ (x : Rose A) → Rose^ A Q x → P x
  indListRose : ∀ (ts : List (Rose A)) → ListRose^ A Q ts → List^ (Rose A) P ts

  indRose empty liftR = cempty
  indRose (node a ts) (Qa , liftts) = cnode a ts Qa (indListRose ts liftts)

  indListRose nil _ = lift tt
  indListRose (cons t ts) (liftt , liftts) = indRose t liftt , indListRose ts liftts