blob: b2ab10dd98a7f3113ebb335479a0f2e45e1ecd82 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
{-# 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)
|
