{-# OPTIONS --safe #-}

module Problem5 where

open import Data.List
open import Data.List.Properties using (++-assoc; ++-identityʳ)
open import Data.Product
open import Relation.Binary.PropositionalEquality hiding ([_])

data Symbol : Set where
   ⟨ : Symbol
   ⟩ : Symbol

data M : List Symbol → Set where
    M-empty : M []
    M-juxt  : ∀{a b} → M a → M b → M (a ++ b)
    M-nest  : ∀{a} → M a → M (⟨ ∷ a ++ [ ⟩ ])

data ListOf (P : List Symbol → Set) : List Symbol → Set where
    ListOf-empty : ListOf P []
    ListOf-cons  : ∀{a b} → P a → ListOf P b → ListOf P (a ++ b)

data N : List Symbol → Set where
    N-nest : ∀{a} → ListOf N a → N (⟨ ∷ a ++ [ ⟩ ])

L = ListOf N

ListOf-++ : {P : List Symbol → Set} {xs ys : List Symbol} → ListOf P xs → ListOf P ys → ListOf P (xs ++ ys)
ListOf-++ ListOf-empty pys = pys
ListOf-++ {ys = ys} (ListOf-cons {xs₁} {xs₂} px pxs) pys =
  subst (ListOf _) (sym (++-assoc xs₁ xs₂ ys)) (ListOf-cons px (ListOf-++ pxs pys))


goal : ∀{s} → M s → L s
goal M-empty        = ListOf-empty
goal (M-juxt m₁ m₂) = ListOf-++ (goal m₁) (goal m₂)
goal (M-nest m)     = subst L (++-assoc (⟨ ∷ _) [ ⟩ ] []) (ListOf-cons (N-nest (goal m)) ListOf-empty)

-- The other direction is straightforward in Agda but extremely difficult in Lean!
-- goal₁ : ∀{s} → L s → M s
-- goal₂ : ∀{s} → N s → M s
-- goal₁ ListOf-empty = M-empty
-- goal₁ (ListOf-cons x l) = M-juxt (goal₂ x) (goal₁ l)
-- goal₂ (N-nest x) = M-nest (goal₁ x)