-- Code supplement for Sections 1 through 5
-- (C) 2020 Patricia Johann, Andrew Polonsky
-- This information is free; you can redistribute and/or modify it under the terms of CC BY-SA 4.0.

module Examples where

open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Data.Product
open import Data.Nat
open import Data.Nat.Primality using (Prime)
open import Data.Maybe renaming (map to Maybe-map)


-- Code for Section 1


data List (a : Set) : Set where
  Nil : List a
  Cons : a → List a → List a

-- Structural induction for lists
Lind : ∀ (a : Set) (P : List a → Set)
       → P Nil
       → (∀ (x : a) (xs : List a) → P xs → P (Cons x xs))
       → ∀ (xs : List a) → P xs
Lind a P PNil PCons Nil = PNil
Lind a P PNil PCons (Cons x l) = PCons x l (Lind a P PNil PCons l)

List^ : ∀ {a : Set} → (a → Set) → (List a → Set)
List^ Q Nil = ⊤
List^ Q (Cons x xs) = Q x × List^ Q xs

-- Deep induction for lists
DLind : ∀ (a : Set) (P : List a → Set) (Q : a → Set) →
        P Nil → (∀(x : a) (xs : List a) → Q x → P xs → P (Cons x xs)) →
        ∀ (xs : List a) → List^ Q xs → P xs
DLind a P Q PNil PCons Nil tt = PNil
DLind a P Q PNil PCons (Cons x xs) (p , ps) =
        PCons x xs p (DLind a P Q PNil PCons xs ps)



-- Predicates need not be representable as data types
Lind-prime : ∀ (P : List ℕ → Set)
            → P Nil → (∀ (y : ℕ) (ys : List ℕ) → Prime y → P ys → P (Cons y ys))
            → ∀ (xs : List ℕ) → List^ Prime xs → P xs
Lind-prime P = DLind ℕ P Prime




data Forest (a : Set) : Set where
  FEmpty : Forest a
  FNode : a → List (Forest a) → Forest a

-- Structural induction for forests
FInd : ∀ (a : Set) (P : Forest a → Set) → P FEmpty → 
      (∀ (x : a) (ts : List (Forest a)) → List^ P ts → P (FNode x ts)) →
       ∀ (x : Forest a) → P x
FInd-aux : ∀ (a : Set) (P : Forest a → Set) → P FEmpty →
      (∀ (x : a) (ts : List (Forest a)) → List^ P ts → P (FNode x ts)) →
       ∀ (ts : List (Forest a)) → List^ P ts

FInd  a P PFEmpty PFNode FEmpty       = PFEmpty
FInd  a P PFEmpty PFNode (FNode x ts) = PFNode x ts (FInd-aux a P PFEmpty PFNode ts)

FInd-aux a P PFEmpty PFNode Nil         = tt
FInd-aux a P PFEmpty PFNode (Cons x ts) = (FInd a P PFEmpty PFNode x) , (FInd-aux a P PFEmpty PFNode ts)

{-# TERMINATING #-}
Forest^ : ∀ {a : Set} → (a → Set) → (Forest a → Set)
Forest^ Q FEmpty = ⊤
Forest^ Q (FNode x ts) = Q x × List^ (Forest^ Q) ts

-- Deep induction for forests
DFInd : ∀ (a : Set) (P : Forest a → Set) (Q : a → Set) → P FEmpty → 
      (∀ (x : a) (ts : List (Forest a)) → Q x → List^ P ts → P (FNode x ts)) →
       ∀ (x : Forest a) → Forest^ Q x → P x

DFInd-aux : ∀ (a : Set) (P : Forest a → Set) (Q : a → Set) → P FEmpty →
      (∀ (x : a) (ts : List (Forest a)) → Q x → List^ P ts → P (FNode x ts)) →
       ∀ (ts : List (Forest a)) → List^ (Forest^ Q) ts → List^ P ts

DFInd     a P Q PFEmpty PFNode FEmpty              q = PFEmpty
DFInd     a P Q PFEmpty PFNode (FNode x ts) (q , qs) = PFNode x ts q (DFInd-aux a P Q PFEmpty PFNode ts qs)

DFInd-aux a P Q PFEmpty PFNode Nil q = tt
DFInd-aux a P Q PFEmpty PFNode (Cons x ts) (q , qs) = (DFInd a P Q PFEmpty PFNode x q) , (DFInd-aux a P Q PFEmpty PFNode ts qs)



data Expr : Set
data BExpr : Set

data Expr where
  Lit : ℕ → Expr
  Add : Expr → Expr → Expr
  If  : BExpr → Expr →  Expr → Expr

data BExpr where
  BLit : Bool → BExpr
  And  : BExpr → BExpr → BExpr
  Not  : BExpr → BExpr
  Equal : Expr → Expr → BExpr

ExprInd : ∀ (P : Expr → Set) (Q : BExpr → Set) →
           (∀ (n : ℕ) → P (Lit n)) →
           (∀ (e1 : Expr) (e2 : Expr) → P e1 → P e2 → P (Add e1 e2)) →
           (∀ (b : BExpr) (e1 : Expr) (e2 : Expr) → Q b → P e1 → P e2 → P (If b e1 e2)) →
           (∀ (b : Bool) → Q (BLit b)) →
           (∀ (b1 : BExpr) (b2 : BExpr) → Q b1 → Q b2 → Q (And b1 b2)) →
           (∀ (b : BExpr) → Q b → Q (Not b)) →
           (∀ (e1 : Expr) (e2 : Expr) → P e1 → P e2 → Q (Equal e1 e2)) →
           ∀ (e : Expr) → P e
BExprInd : ∀ (P : Expr → Set) (Q : BExpr → Set) →
           (∀ (n : ℕ) → P (Lit n)) →
           (∀ (e1 : Expr) (e2 : Expr) → P e1 → P e2 → P (Add e1 e2)) →
           (∀ (b : BExpr) (e1 : Expr) (e2 : Expr) → Q b → P e1 → P e2 → P (If b e1 e2)) →
           (∀ (b : Bool) → Q (BLit b)) →
           (∀ (b1 : BExpr) (b2 : BExpr) → Q b1 → Q b2 → Q (And b1 b2)) →
           (∀ (b : BExpr) → Q b → Q (Not b)) →
           (∀ (e1 : Expr) (e2 : Expr) → P e1 → P e2 → Q (Equal e1 e2)) →
           ∀ (b : BExpr) → Q b

-- Deep induction for expressions
ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual (Lit n) = PLit n
ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual (Add m n) = PAdd m n pm pn
  where pm = ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual m
        pn = ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual n
ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual (If b e1 e2) = PIf b e1 e2 qb p1 p2
  where qb = BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual b
        p1 = ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual e1
        p2 = ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual e2

BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual (BLit b) = QBLit b
BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual (And b1 b2) = QAnd b1 b2 q1 q2
  where q1 = BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual b1
        q2 = BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual b2
BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual (Not b) = QNot b q
  where q = BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual b
BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual (Equal m n) = QEqual m n pm pn
  where pm = ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual m
        pn = ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual n

EBInd : ∀ (P : Expr → Set) (Q : BExpr → Set) →
         (∀ (n : ℕ) → P (Lit n)) →
         (∀ (e1 : Expr) (e2 : Expr) → P e1 → P e2 → P (Add e1 e2)) →
         (∀ (b : BExpr) (e1 : Expr) (e2 : Expr) → Q b → P e1 → P e2 → P (If b e1 e2)) →
         (∀ (b : Bool) → Q (BLit b)) →
         (∀ (b1 : BExpr) (b2 : BExpr) → Q b1 → Q b2 → Q (And b1 b2)) →
         (∀ (b : BExpr) → Q b → Q (Not b)) →
         (∀ (e1 : Expr) (e2 : Expr) → P e1 → P e2 → Q (Equal e1 e2)) →
         (∀ (e : Expr) → P e) ×  (∀ (b : BExpr) → Q b)
EBInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual =
    (λ e → ExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual e)
  , (λ b → BExprInd P Q PLit PAdd PIf QBLit QAnd QNot QEqual b)



-- Code for Section 3


data PTree (a : Set) : Set where
  PLeaf : a → PTree a
  PNode : PTree (a × a) → PTree a

Pair^ : ∀ {a : Set} → (a → Set) → (a × a → Set)
Pair^ Q (x , y) = Q x × Q y

PTree^ : ∀ {a : Set} → (a → Set) → (PTree a → Set)
PTree^ Q (PLeaf x) = Q x
PTree^ Q (PNode t) = PTree^ (Pair^ Q) t

-- Structural induction for perfect trees
PInd : ∀ (P : ∀ (a : Set) → PTree a → Set) →
         (∀ (a : Set) (x : a) → P a (PLeaf x)) →
         (∀ (a : Set) (x : PTree (a × a)) → P (a × a) x → P a (PNode x)) →
         ∀ (a : Set) (x : PTree a) → P a x
PInd P PPLeaf PPNode a (PLeaf x) = PPLeaf a x
PInd P PPLeaf PPNode a (PNode t) = PPNode a t (PInd P PPLeaf PPNode (a × a) t)

-- Deep induction for perfect trees
PDInd : ∀ (P : ∀ (a : Set) → (a → Set) → PTree a → Set) →
         (∀ (a : Set) (Q : a → Set) (x : a) → Q x → P a Q (PLeaf x)) →
         (∀ (a : Set) (Q : a → Set) (x : PTree (a × a)) → P (a × a) (Pair^ Q) x → P a Q (PNode x)) →
         ∀ (a : Set) (Q : a → Set) (x : PTree a) → PTree^ Q x → P a Q x
PDInd P PPLeaf PPNode a Q (PLeaf x) q = PPLeaf a Q x q
PDInd P PPLeaf PPNode a Q (PNode t) q = PPNode a Q t (PDInd P PPLeaf PPNode (a × a) (Pair^ Q) t q)



-- Example 4

data Lam (a : Set) : Set where
  Var : a → Lam a
  App : Lam a → Lam a → Lam a
  Abs : Lam (Maybe a) → Lam a

-- Structural induction for lambda terms
LamInd : ∀ (P : ∀ (a : Set) → Lam a → Set) →
         (∀ (a : Set) (x : a) → P a (Var x)) →
         (∀ (a : Set) (x : Lam a) (y : Lam a) → P a x → P a y → P a (App x y)) →
         (∀ (a : Set) (x : Lam (Maybe a)) → P (Maybe a) x → P a (Abs x)) →
         ∀ (a : Set) (x : Lam a) → P a x
LamInd P PVar PApp PAbs a (Var x) = PVar a x
LamInd P PVar PApp PAbs a (App t₁ t₂) = PApp a t₁ t₂ (LamInd P PVar PApp PAbs a t₁)
                                                     (LamInd P PVar PApp PAbs a t₂)
LamInd P PVar PApp PAbs a (Abs t) = PAbs a t (LamInd P PVar PApp PAbs (Maybe a) t)


Lind-nested : ∀ (P : ∀ (a : Set) → List a → Set) →
                (∀ (a : Set) → P a Nil) →
                (∀ (a : Set) (y : a) (x : List a) → P a x → P a (Cons y x)) →
                ∀ (a : Set) (x : List a) → P a x
Lind-nested P PNil PCons a Nil = PNil a
Lind-nested P PNil PCons a (Cons x xs) = PCons a x xs (Lind-nested P PNil PCons a xs)


Maybe^ : ∀ {a : Set} → (a → Set) → Maybe a → Set
Maybe^ P (just x) = P x
Maybe^ P nothing = ⊤


Lam^ : ∀ {a : Set} → (a → Set) → Lam a → Set
Lam^ P (Var x) = P x
Lam^ P (App s t) = Lam^ P s × Lam^ P t
Lam^ P (Abs t) = Lam^ (Maybe^ P) t

-- Deep induction for lambda terms
LamDeepInd : ∀ (P : ∀ (a : Set) → (a → Set) → Lam a → Set) →
               (∀ (a : Set) (Q : a → Set) (x : a) → Q x → P a Q (Var x)) →
               (∀ (a : Set) (Q : a → Set) (x : Lam a) (y : Lam a) → P a Q x → P a Q y → P a Q (App x y)) →
               (∀ (a : Set) (Q : a → Set) (x : Lam (Maybe a)) → P (Maybe a) (Maybe^ Q) x → P a Q (Abs x)) →
               ∀ (a : Set) (Q : a → Set) (x : Lam a) → Lam^ Q x → P a Q x
LamDeepInd P PVar PApp PAbs a Q (Var x) q = PVar a Q x q
LamDeepInd P PVar PApp PAbs a Q (App s t) (qs , qt) = PApp a Q s t ps pt
  where ps = LamDeepInd P PVar PApp PAbs a Q s qs
        pt = LamDeepInd P PVar PApp PAbs a Q t qt
LamDeepInd P PVar PApp PAbs a Q (Abs t) q = PAbs a Q t p
  where p = LamDeepInd P PVar PApp PAbs (Maybe a) (Maybe^ Q) t q




-- Example 5

data Bush (a : Set) : Set where
  BNil : Bush a
  BCons : a → Bush (Bush a) → Bush a

-- Structural induction for bushes
BInd : ∀ (P : ∀ (a : Set) → Bush a → Set) →
            (∀ (a : Set) → P a BNil) →
            (∀ (a : Set) (x : a) (y : Bush (Bush a)) → P (Bush a) y → P a (BCons x y)) →
            ∀ (a : Set) (x : Bush a) → P a x
BInd P PBNil PBCons a BNil = PBNil a
BInd P PBNil PBCons a (BCons x b) = PBCons a x b (BInd P PBNil PBCons (Bush a) b)


-- The following functions must be declared terminating, because Agda does not
-- recognize recursion over truly nested types as well-founded.

{-# TERMINATING #-}
Bush^ : ∀ {a : Set} → (a → Set) → Bush a → Set
Bush^ P BNil = ⊤
Bush^ P (BCons x b) = P x × Bush^ (Bush^ P) b


{-# TERMINATING #-}
Bush^-map : ∀ {a : Set} (P Q : a → Set) (PQ : ∀ (x : a) → P x → Q x)
                → ∀ (b : Bush a) → Bush^ P b → Bush^ Q b
Bush^-map P Q PQ BNil p = tt
Bush^-map P Q PQ (BCons x b) (p , ps) = (PQ x p , Bush^-map (Bush^ P) (Bush^ Q) (Bush^-map P Q PQ) b ps )


-- Deep induction for bushes
{-# TERMINATING #-}
BDInd : ∀ (P : ∀ (a : Set) → (a → Set) → Bush a → Set) →
                (∀ (a : Set) (Q : a → Set) → P a Q BNil) →
                (∀ (a : Set) (Q : a → Set) (x : a) (y : Bush (Bush a)) →
                    Q x → P (Bush a) (P a Q) y → P a Q (BCons x y)) →
                ∀ (a : Set) (Q : a → Set) → ∀ (x : Bush a) → Bush^ Q x → P a Q x
BDInd P PBNil PBCons a Q BNil q = PBNil a Q
BDInd P PBNil PBCons a Q (BCons x b) (q , qs) =
  PBCons a Q x b q (BDInd P PBNil PBCons (Bush a) (P a Q) b
      (Bush^-map (Bush^ Q) (P a Q) (BDInd P PBNil PBCons a Q) b qs))


-- Mutual deep induction for bushes.  Pcons takes P (Bush X) (Q X Y) as IH.
{-# TERMINATING #-}
MBDind : ∀ (P : ∀ (X : Set) → (X → Set) → Bush X → Set)
           (Q : ∀ (X : Set) → (X → Set) → Bush X → Set)
           (Pnil : ∀ X Y → P X Y BNil )
           (Qnil : ∀ X Y → Q X Y BNil )
           (Pcons : ∀ X Y x bbx → Y x → P (Bush X) (Q X Y) bbx → P X Y (BCons x bbx) )
           (Qcons : ∀ X Y x bbx → Y x → Q (Bush X) (P X Y) bbx → Q X Y (BCons x bbx) )
           → ∀ X Y b → Bush^ Y b → P X Y b × Q X Y b
MBDind P Q PBNil QBNil PBCons QBCons X Y BNil bigtt = PBNil X Y , QBNil X Y
MBDind P Q PBNil QBNil PBCons QBCons X Y (BCons x b) (y , bby) =
  let rec = MBDind P Q PBNil QBNil PBCons QBCons
   in (PBCons X Y x b y (proj₁ (rec (Bush X) (Q X Y) b
        (Bush^-map _ _ (λ bx by → proj₂ (rec X Y bx by)) b bby)))) ,
      (QBCons X Y x b y (proj₂ (rec (Bush X) (P X Y) b
        (Bush^-map _ _ (λ bx by → proj₁ (rec X Y bx by)) b bby))))

Pred-map : ∀ {X : Set} → (X → Set) → (X → Set) → Set
Pred-map P Q = ∀ x → P x → Q x

BDInd⇒MBDInd :
  ∀ (P : ∀ (X : Set) → (X → Set) → Bush X → Set)
    (Q : ∀ (X : Set) → (X → Set) → Bush X → Set)
    (Pmap : ∀ {X} {Y1 Y2 : X → Set} → Pred-map Y1 Y2 → Pred-map (P X Y1) (P X Y2) )
    (Qmap : ∀ {X} {Y1 Y2 : X → Set} → Pred-map Y1 Y2 → Pred-map (Q X Y1) (Q X Y2) )
    (PBNil : ∀ X Y → P X Y BNil )
    (QBNil : ∀ X Y → Q X Y BNil )
    (PBCons : ∀ X Y x bbx → Y x → P (Bush X) (Q X Y) bbx → P X Y (BCons x bbx) )
    (QBCons : ∀ X Y x bbx → Y x → Q (Bush X) (P X Y) bbx → Q X Y (BCons x bbx) )
     → ∀ X Y b → Bush^ Y b → P X Y b × Q X Y b
BDInd⇒MBDInd P Q Pmap Qmap PBNil QBNil PBCons QBCons =
  BDInd (λ X Y b → P X Y b × Q X Y b)
        (λ X Y → PBNil X Y , QBNil X Y)
        (λ X Y x bbx y → λ {(ppqy , qpqy) →
              PBCons X Y x bbx y (Pmap (λ _ → proj₂) bbx ppqy)
            , QBCons X Y x bbx y (Qmap (λ _ → proj₁) bbx qpqy) })