Advent of proof submissions.HEADmaster

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

1 files changed, 80 insertions, 0 deletions

diff --git a/src/Problem21.agda b/src/Problem21.agda
new file mode 100644
index 0000000..e5d27e2
--- /dev/null
+++ b/src/Problem21.agda
@@ -0,0 +1,80 @@
+{-# OPTIONS --safe #-}
+
+module Problem21 (Atom : Set) where
+
+open import Data.List
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Data.Empty
+open import Data.Nat
+open import Data.Fin
+open import Data.Fin.Patterns
+open import Data.Product
+
+data L : Set where
+    ⟨_⟩ : Atom → L
+    ⟨_⟩ᶜ : Atom → L
+    _⊗_ : L → L → L
+    _⅋_ : L → L → L
+    ⊥' : L
+    𝟙  : L
+
+variable A B C : L
+variable Δ Γ : List L
+variable α β η : Atom
+
+_ᶜ : L → L
+⟨ A ⟩   ᶜ = ⟨ A ⟩ᶜ
+⟨ A ⟩ᶜ  ᶜ = ⟨ A ⟩
+(A ⊗ B) ᶜ = (A ᶜ) ⅋ (B ᶜ)
+(A ⅋ B) ᶜ = (A ᶜ) ⊗ (B ᶜ)
+𝟙       ᶜ = ⊥'
+⊥'      ᶜ = 𝟙
+
+_⊸_ : L → L → L
+A ⊸ B = (A ᶜ) ⅋ B
+
+infixl 2 ⊢_
+data ⊢_ : List L → Set where
+    one      : ⊢ [ 𝟙 ]
+    identity : ⊢ ⟨ α ⟩ ∷ ⟨ α ⟩ᶜ ∷ []
+    exch     :  (n : Fin (length Δ))
+             → ⊢ lookup Δ n ∷ (Δ ─ n)
+             → ⊢ Δ
+    times    : (n : ℕ)
+             → ⊢ A ∷ take n Δ
+             → ⊢ B ∷ drop n Δ
+             → ⊢ A ⊗ B ∷ Δ
+    par      : ⊢ A ∷ B ∷ Δ
+             → ⊢ A ⅋ B ∷ Δ
+    bottom   : ⊢ Δ
+             → ⊢ ⊥' ∷ Δ
+
+    cut      : ⊢ A ∷ Δ
+             → ⊢ A ᶜ ∷ Γ
+             → ⊢ Δ ++ Γ
+
+id : {A : L} → ⊢ A ∷ A ᶜ ∷ []
+id {⟨ x ⟩} = identity
+id {⟨ x ⟩ᶜ} = exch 1F identity
+id {A ⊗ B} = exch 1F (par (exch 2F (times 1 (id {A}) (id {B}))))
+id {A ⅋ B} = par (exch 2F (times 1 (exch 1F (id {A})) (exch 1F (id {B}))))
+id {⊥'} = bottom one
+id {𝟙} = exch 1F (bottom one)
+
+id′ : {A : L} → ⊢ A ᶜ ∷ A ∷ []
+id′ = exch 1F id
+
+_≈_ : L → L → Set
+A ≈ B = (⊢ [ A ] → ⊢ [ B ]) × (⊢ [ B ] → ⊢ [ A ])
+
+lem₁ : ((A ⊗ B) ⊸ C) ≈ (A ⊸ (B ⊸ C))
+lem₁ .proj₁ prf = cut prf (exch 1F (par (exch 1F (par (exch 2F (exch 3F (times 2 (times 1 id′ id′) id′)))))))
+lem₁ .proj₂ prf = cut prf (exch 1F (par (par (exch 3F (times 1 id′ (times 1 id′ id′))))))
+
+lem₂ : (A ⊸ (B ⅋ C)) ≈ ((A ⊸ B) ⅋ C)
+lem₂ .proj₁ prf = cut prf (exch 1F (par (par (exch 3F (times 1 id′ (times 1 id′ id′))))))
+lem₂ .proj₂ prf = cut prf (exch 1F (par (exch 1F (par (exch 2F (exch 3F (times 2 (times 1 id′ id′) id′)))))))
+
+lem₃ : (A ⊸ B) ≈ ((B ᶜ) ⊸ (A ᶜ))
+lem₃ .proj₁ prf = cut prf (exch 1F (par (exch 1F (exch 2F (times 1 id′ id)))))
+lem₃ .proj₂ prf = cut prf (exch 1F (par (exch 1F (exch 2F (times 1 (exch 1F (cut id′ id)) id′)))))