Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

1 files changed, 44 insertions, 0 deletions

diff --git a/src/Problem5.agda b/src/Problem5.agda
new file mode 100644
index 0000000..b2ab10d
--- /dev/null
+++ b/src/Problem5.agda
@@ -0,0 +1,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)