Advent of proof submissions.HEADmaster

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

1 files changed, 116 insertions, 0 deletions

diff --git a/src/Problem17.agda b/src/Problem17.agda
new file mode 100644
index 0000000..d02502e
--- /dev/null
+++ b/src/Problem17.agda
@@ -0,0 +1,116 @@
+{-# OPTIONS --safe #-}
+
+module Problem17 (Act : Set) where
+
+open import Data.Empty
+open import Data.List
+open import Data.List.Membership.Propositional
+open import Data.List.Membership.Propositional.Properties
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.Product hiding (map)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Unit
+open import Function.Base using (id)
+open import Relation.Binary.PropositionalEquality hiding ([_])
+
+data Process : Set where
+  ⟨_⟩   : Act → Process
+  skip  : Process
+  abort : Process
+  -- not the normal semicolon, use \; and choose the correct option..
+  _;_   : Process → Process → Process
+  _+_   : Process → Process → Process
+  _∥_   : Process → Process → Process
+
+infixr 60 _;_
+infixr 70 _+_
+infixr 80 _∥_
+variable P P′ Q Q′ : Process
+variable a b c x : Act
+variable xs : List Act
+
+NoPar : Process → Set
+NoPar (P ; Q) = NoPar P × NoPar Q
+NoPar (P + Q) = NoPar P × NoPar Q
+NoPar (P ∥ Q) = ⊥
+NoPar ⟨ _ ⟩   = ⊤
+NoPar skip    = ⊤
+NoPar abort   = ⊤
+
+interleave : List Act → List Act → List (List Act)
+interleave [] ys = [ ys ]
+interleave xs [] = [ xs ]
+interleave (x ∷ xs) (y ∷ ys) = map (x ∷_) (interleave xs (y ∷ ys)) ++ map (y ∷_) (interleave (x ∷ xs) ys)
+
+⟦_⟧ : Process → List (List Act)
+⟦ ⟨ a ⟩ ⟧ = [ [ a ] ]
+⟦ skip  ⟧ = [ [] ]
+⟦ abort ⟧ = []
+⟦ P + Q ⟧ = ⟦ P ⟧ ++ ⟦ Q ⟧
+⟦ P ; Q ⟧ = concatMap (λ p → map (p ++_) ⟦ Q ⟧) ⟦ P ⟧
+⟦ P ∥ Q ⟧ = concatMap (λ p → concatMap (interleave p) ⟦ Q ⟧) ⟦ P ⟧
+
+_≈_ : Process → Process → Set
+P ≈ Q = ∀ xs → (xs ∈ ⟦ P ⟧ → xs ∈ ⟦ Q ⟧) × (xs ∈ ⟦ Q ⟧ → xs ∈ ⟦ P ⟧)
+
+-- Helpers for dealing with sequential traces
+
+;-trace : ∀ (P Q : Process) {xs ys} → xs ∈ ⟦ P ⟧ → ys ∈ ⟦ Q ⟧ → xs ++ ys ∈ ⟦ P ; Q ⟧
+;-trace P Q {xs} xs∈⟦P⟧ ys∈⟦Q⟧ =
+  ∈-concat⁺′ (∈-map⁺ (xs ++_) ys∈⟦Q⟧) (∈-map⁺ (λ p → map (p ++_) ⟦ Q ⟧) xs∈⟦P⟧)
+
+;-trace⁻¹ :
+  ∀ (P Q : Process) {xs} →
+  xs ∈ ⟦ P ; Q ⟧ → ∃₂ λ ys zs → xs ≡ ys ++ zs × ys ∈ ⟦ P ⟧ × zs ∈ ⟦ Q ⟧
+;-trace⁻¹ P Q {xs} xs∈⟦P;Q⟧ with ∈-concat⁻′ (map (λ p → map (p ++_) ⟦ Q ⟧) ⟦ P ⟧) xs∈⟦P;Q⟧
+... | xss , xs∈xss , xss∈⟦P⟧++⟦Q⟧ with ∈-map⁻ (λ p → map (p ++_) ⟦ Q ⟧) xss∈⟦P⟧++⟦Q⟧
+... | ys , ys∈⟦P⟧ , refl with ∈-map⁻ (ys ++_) xs∈xss
+... | zs , zs∈⟦Q⟧ , refl = ys , zs , refl , ys∈⟦P⟧ , zs∈⟦Q⟧
+
+-- Idea
+-- Each trace has a canonical process---the list of actions. We can map a list
+-- of possible traces to a canonical process by taking the sum of all individual
+-- traces.
+--
+-- We show the canonical process for list of traces is correct (contains all
+-- traces) and unique (contains only the desired traces).
+
+canonical₁ : List Act → Process
+canonical₁ []       = skip
+canonical₁ (a ∷ as) = ⟨ a ⟩ ; canonical₁ as
+
+canonical : List (List Act) → Process
+canonical []         = abort
+canonical (as ∷ ass) = canonical₁ as + canonical ass
+
+canonical₁-correct : ∀ as → as ∈ ⟦ canonical₁ as ⟧
+canonical₁-correct []       = here refl
+canonical₁-correct (a ∷ as) = ;-trace ⟨ a ⟩ (canonical₁ as) (here refl) (canonical₁-correct as)
+
+canonical₁-unique : ∀ as {xs} → xs ∈ ⟦ canonical₁ as ⟧ → xs ≡ as
+canonical₁-unique []       (here prf) = prf
+canonical₁-unique (a ∷ as) prf with ;-trace⁻¹ ⟨ a ⟩ (canonical₁ as) prf
+... | .([ a ]) , xs , refl , here refl , prf = cong (a ∷_) (canonical₁-unique as prf)
+
+canonical₁-NoPar : ∀ as → NoPar (canonical₁ as)
+canonical₁-NoPar []       = _
+canonical₁-NoPar (a ∷ as) = _ , canonical₁-NoPar as
+
+canonical-correct : ∀ ass {as} → as ∈ ass → as ∈ ⟦ canonical ass ⟧
+canonical-correct (as ∷ ass) (here refl) = ∈-++⁺ˡ (canonical₁-correct as)
+canonical-correct (as ∷ ass) (there prf) = ∈-++⁺ʳ ⟦ canonical₁ as ⟧ (canonical-correct ass prf)
+
+canonical-unique : ∀ ass {as} → as ∈ ⟦ canonical ass ⟧ → as ∈ ass
+canonical-unique (as ∷ ass) prf with ∈-++⁻ ⟦ canonical₁ as ⟧ prf
+... | inj₁ prf with refl ← canonical₁-unique as prf = here refl
+... | inj₂ prf = there (canonical-unique ass prf)
+
+canonical-NoPar : ∀ ass → NoPar (canonical ass)
+canonical-NoPar []         = _
+canonical-NoPar (as ∷ ass) = canonical₁-NoPar as , canonical-NoPar ass
+
+goal : ∀ (P : Process) → ∃[ P′ ] (P′ ≈ P) × NoPar P′
+goal P =
+    canonical ⟦ P ⟧
+  , (λ as → canonical-unique ⟦ P ⟧ , canonical-correct ⟦ P ⟧)
+  , canonical-NoPar ⟦ P ⟧