Advent of proof submissions.HEADmaster

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

1 files changed, 159 insertions, 0 deletions

diff --git a/src/Problem19.agda b/src/Problem19.agda
new file mode 100644
index 0000000..130d46e
--- /dev/null
+++ b/src/Problem19.agda
@@ -0,0 +1,159 @@
+{-# OPTIONS --safe #-}
+
+module Problem19 where
+
+open import Data.List hiding ([_])
+open import Data.Product
+open import Data.Empty
+open import Data.List.Properties
+open import Data.Sum
+open import Data.Unit hiding (_≟_)
+open import Data.Char
+open import Data.Maybe
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality hiding ([_])
+
+data Regex : Set where
+    ∅ : Regex
+    ε : Regex
+    [_] : Char → Regex
+    _∘_ : Regex → Regex → Regex
+    _∪_ : Regex → Regex → Regex
+    _⋆  : Regex → Regex
+
+variable c : Char
+variable R S : Regex
+variable s t : List Char
+
+data Matches : Regex → List Char → Set where
+   empty : Matches ε []
+   char  : Matches [ c ] (c ∷ [])
+   comp  : Matches R s → Matches S t → Matches (R ∘ S) (s ++ t)
+   un₁   : Matches R s → Matches (R ∪ S) s
+   un₂   : Matches S s → Matches (R ∪ S) s
+   starₑ : Matches (R ⋆) []
+   starₛ : Matches R s → Matches (R ⋆) t → Matches (R ⋆) (s ++ t)
+
+comp⁻¹ : Matches (R ∘ S) s → ∃₂ λ t₁ t₂ → t₁ ++ t₂ ≡ s × Matches R t₁ × Matches S t₂
+comp⁻¹ (comp prf prf₁) = _ , _ , refl , prf , prf₁
+
+star⁻¹′ : Matches (R ⋆) s → s ≡ [] ⊎ ∃[ c ] ∃[ t₁ ] ∃[ t₂ ] c ∷ t₁ ++ t₂ ≡ s × Matches R (c ∷ t₁) × Matches (R ⋆) t₂
+star⁻¹′ starₑ = inj₁ refl
+star⁻¹′ (starₛ {s = []} prf prf₁) = star⁻¹′ prf₁
+star⁻¹′ (starₛ {s = x ∷ s} prf prf₁) = inj₂ (x , s , _ , refl , prf , prf₁)
+
+Nullable : Regex → Set
+Nullable ∅ = ⊥
+Nullable ε = ⊤
+Nullable [ x ] = ⊥
+Nullable (r ∘ r₁) = Nullable r × Nullable r₁
+Nullable (r ∪ r₁) = Nullable r ⊎ Nullable r₁
+Nullable (r ⋆) = ⊤
+
+nullable? : (r : Regex) → Dec (Nullable r)
+nullable? ∅ = no (λ x → x)
+nullable? ε = yes tt
+nullable? [ x ] = no (λ x → x)
+nullable? (r ∘ r₁) with nullable? r | nullable? r₁
+... | no p  | _     = no λ (a , b) → p a
+... | _     | no p  = no λ (a , b) → p b
+... | yes p | yes q = yes (p , q)
+nullable? (r ∪ r₁)  with nullable? r | nullable? r₁
+... | yes p | _     = yes (inj₁ p)
+... | _     | yes p = yes (inj₂ p)
+... | no p  | no q  = no λ { (inj₁ a) → p a ; (inj₂ b) → q b }
+nullable? (r ⋆) = yes tt
+
+nullable-correct₁ : ∀ R → Nullable R → Matches R []
+nullable-correct₁ ε        _               = empty
+nullable-correct₁ (r ∘ r₁) (null₁ , null₂) = comp (nullable-correct₁ r null₁) (nullable-correct₁ r₁ null₂)
+nullable-correct₁ (r ∪ r₁) (inj₁ null)     = un₁ (nullable-correct₁ r null)
+nullable-correct₁ (r ∪ r₁) (inj₂ null)     = un₂ (nullable-correct₁ r₁ null)
+nullable-correct₁ (r ⋆)    _               = starₑ
+
+st≡[]⇒s≡[] : s ++ t ≡ [] → s ≡ []
+st≡[]⇒s≡[] {[]} {t} prf = refl
+
+st≡[]⇒t≡[] : s ++ t ≡ [] → t ≡ []
+st≡[]⇒t≡[] {[]} {t} prf = prf
+
+nullable-correct₂′ : ∀ {R} → Matches R s → s ≡ [] → Nullable R
+nullable-correct₂′ empty            s≡[]  = _
+nullable-correct₂′ (comp s∈r t∈r₁)  st≡[] = nullable-correct₂′ s∈r (st≡[]⇒s≡[] st≡[]) , nullable-correct₂′ t∈r₁ (st≡[]⇒t≡[] st≡[])
+nullable-correct₂′ (un₁ s∈r)        s≡[]  = inj₁ (nullable-correct₂′ s∈r s≡[])
+nullable-correct₂′ (un₂ s∈r)        s≡[]  = inj₂ (nullable-correct₂′ s∈r s≡[])
+nullable-correct₂′ starₑ            s≡[]  = _
+nullable-correct₂′ (starₛ s∈r s∈r₁) s≡[]  = _
+
+nullable-correct₂ : ∀ R → Matches R [] → Nullable R
+nullable-correct₂ r []∈r = nullable-correct₂′ []∈r refl
+
+step : Regex → Char → Regex
+step ∅ c = ∅
+step ε c = ∅
+step [ x ] c with c ≟ x
+... |  yes p = ε
+... |  no  p = ∅
+step (r ∘ r₁) c with nullable? r
+... | yes p = (step r c ∘ r₁) ∪ step r₁ c
+... | no  p = step r c ∘ r₁
+step (r ∪ r₁) c = step r c ∪ step r₁ c
+step (r ⋆) c = step r c ∘ (r ⋆)
+
+steps : Regex → List Char → Regex
+steps R (x ∷ xs) = steps (step R x) xs
+steps R [] = R
+
+step-correct₁ : ∀ R c s → Matches (step R c) s → Matches R (c ∷ s)
+step-correct₁ [ x ]    c s   prf   with c ≟ x
+step-correct₁ [ x ]    c s empty | yes refl = char
+step-correct₁ [ x ]    c s ()    | no p
+
+step-correct₁ (R ∘ R₁) c s prf                   with nullable? R
+step-correct₁ (R ∘ R₁) c s (un₁ (comp prf prf₁)) | yes p = comp (step-correct₁ R c _ prf) prf₁
+step-correct₁ (R ∘ R₁) c s (un₂ prf)             | yes p = comp (nullable-correct₁ R p) (step-correct₁ R₁ c _ prf)
+step-correct₁ (R ∘ R₁) c s (comp prf prf₁)       | no p  = comp (step-correct₁ R c _ prf) prf₁
+
+step-correct₁ (R ∪ R₁) c s (un₁ prf) = un₁ (step-correct₁ R c s prf)
+step-correct₁ (R ∪ R₁) c s (un₂ prf) = un₂ (step-correct₁ R₁ c s prf)
+
+step-correct₁ (R ⋆)    c s (comp prf prf₁) = starₛ (step-correct₁ R c _ prf) prf₁
+
+step-correct₂ : ∀ R c s → Matches R (c ∷ s) → Matches (step R c) s
+step-correct₂ [ x ]    c s char with x ≟ x
+... | yes p = empty
+... | no  p = ⊥-elim (p refl)
+step-correct₂ (R ∘ R₁) c s prf with nullable? R | comp⁻¹ prf
+... | yes p | []     , t₂ , refl , prf , prf₁ = un₂ (step-correct₂ R₁ c s prf₁)
+... | yes p | x ∷ t₁ , t₂ , eq   , prf , prf₁ =
+  un₁ (subst₂ Matches (cong (λ - → step R - ∘ R₁) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
+    (comp (step-correct₂ R x t₁ prf) prf₁))
+... | no p  | []     , t₂ , eq   , prf , prf₁ = ⊥-elim (p (nullable-correct₂ R prf))
+... | no p  | x ∷ t₁ , t₂ , eq   , prf , prf₁ =
+  subst₂ Matches (cong (λ - → step R - ∘ R₁) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
+    (comp (step-correct₂ R x t₁ prf) prf₁)
+step-correct₂ (R ∪ R₁) c s (un₁ prf) = un₁ (step-correct₂ R c s prf)
+step-correct₂ (R ∪ R₁) c s (un₂ prf) = un₂ (step-correct₂ R₁ c s prf)
+step-correct₂ (R ⋆)    c s prf with star⁻¹′ prf
+... | inj₂ (x , t₁ , t₂ , eq , prf , prf₁) =
+  subst₂ Matches (cong (λ - → step R - ∘ (R ⋆)) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
+    (comp (step-correct₂ R x t₁ prf) prf₁)
+
+steps-correct₁ : ∀ R s → Matches (steps R s) [] → Matches R s
+steps-correct₁ R []      prf = prf
+steps-correct₁ R (x ∷ s) prf = step-correct₁ R x s (steps-correct₁ (step R x) s prf)
+
+steps-correct₂ : ∀ R s → Matches R s → Matches (steps R s) []
+steps-correct₂ R []      prf = prf
+steps-correct₂ R (x ∷ s) prf = steps-correct₂ (step R x) s (step-correct₂ R x s prf)
+
+check-lemma₁ : ∀ R s → Nullable (steps R s) → Matches R s
+check-lemma₁ R s null = steps-correct₁ R s (nullable-correct₁ (steps R s) null)
+
+check-lemma₂ : ∀ R s → Matches R s → Nullable (steps R s)
+check-lemma₂ R s prf = nullable-correct₂ (steps R s) (steps-correct₂ R s prf)
+
+check : (R : Regex) (s : List Char) → Dec (Matches R s)
+check R s with nullable? (steps R s)
+... | yes p = yes (check-lemma₁ R s p)
+... | no p = no λ m → p (check-lemma₂ R s m)