finish confluence

src/AOP/LTL.agda

@@ -0,0 +1,82 @@
+module LTL where
+
+open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Data.Nat.Properties using (+-identityʳ)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym)
+open Eq.≡-Reasoning using (begin_; step-≡-∣; _∎)
+
+infixr 5 F_ , G_
+infix 2 _≅_ _⊨_
+
+data Empty : Set where
+
+¬ : Set → Set
+¬ A = A → Empty
+
+record ∃ {A : Set} (P : A → Set) : Set where
+  constructor ⟨_,_⟩
+  field
+    wit : A
+    proof : P wit
+
+syntax ∃ (λ x → B) = ∃[ x ] B
+
+data _×_ (A B : Set) : Set where
+  ⟨_,_⟩ : A → B → A × B
+
+Atom : Set
+Atom = ℕ
+
+data Formula : Set where
+  ⊤ ⊥ : Formula
+  ‵_ : Atom → Formula
+  F_ G_ : Formula → Formula
+
+data Bool : Set where
+  true, false : Bool
+
+data List (A : Set) : Set where
+  [] : List A
+  _::_ : A → List A → List A
+
+-- Drop the first n elements
+drop : ∀ {A : Set} → List A → (m : ℕ) → List A
+drop xs zero = xs
+drop [] (suc m) = []
+drop (x :: xs) (suc m) = drop xs m
+
+Path : Set
+Path = List (Atom → Bool)
+
+_at_ : Path → (m : ℕ) → Path
+_at_ = drop
+
+data _⊨_ : Path → Formula → Set where
+  ⊨⊤ : ∀ {π : Path} → π ⊨ ⊤
+  ⊨G  : ∀ {π : Path} {ϕ : Formula} → (∀ i → π at i ⊨ ϕ) → π ⊨ G ϕ
+  ⊨F  : ∀ {π : Path} {ϕ : Formula} → (∃[ i ] (π at i ⊨ ϕ)) → π ⊨ F ϕ
+
+_iff_ : (A B : Set) → Set
+A iff B = (A → B) × (B → A)
+
+data _≅_ : Formula → Formula → Set where
+  sem : ∀ {ϕ ψ : Formula}
+      → (∀ {π : Path} → (π ⊨ ϕ) iff (π ⊨ ψ))
+      → ϕ ≅ ψ
+
+-- A helper lemma
+subst : ∀ {π₁ π₂ : Path} {ϕ : Formula} → π₁ ⊨ ϕ → π₁ ≡ π₂ → π₂ ⊨ ϕ
+subst x refl = x
+
+-- G is idempotent
+idem-G : ∀ {ϕ : Formula} → G G ϕ ≅ G ϕ
+idem-G {ϕ} = sem ⟨ forward , {!   !} ⟩ where
+  forward : ∀ {π} → π ⊨ G G ϕ → π ⊨ G ϕ
+  forward {π} (⊨G x) = ⊨G (λ i → helper i (x i)) where
+    helper : (i : ℕ) → (π at i) ⊨ G ϕ → (π at i) ⊨ ϕ
+    helper i (⊨G x) = x {! i  !}
+
+-- F is idempotent
+idem-F : ∀ {ϕ : Formula} → F F ϕ ≅ F ϕ
+idem-F = {!   !}

src/AOP/VecEnc.agda

@@ -0,0 +1,62 @@
+module VecEnc where
+
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst)
+
+{-
+  This problem is about encoding Vectors as iterated products,
+  i.e. Vec A n = (A × ⋯ × A) for n times,
+  using eliminators instead of dependent pattern matching.
+-}
+
+{- Setup -}
+data _×_ (A B : Set) : Set where
+  _,_ : A → B → A × B
+
+π1 : ∀{A B} → A × B → A
+π1 (x , y) = x
+
+π2 : ∀{A B} → A × B → B
+π2 (x , y) = y
+
+data One : Set where
+  one : One
+
+{- Eliminator for ℕ -}
+
+iter : 
+  ∀{i}{P : ℕ → Set i} → 
+  P 0 → ((n : ℕ) → P n → P (suc n)) → 
+  (n : ℕ) → P n
+iter z s zero = z
+iter z s (suc n) = s n (iter z s n)
+
+{- Q1: Give the Vector type as iterated products. -}
+Vec : Set → ℕ → Set
+Vec A n = iter One (λ _ A* → A* × A) n
+
+{- Q2 : Give the constructors nil and cons. -}
+nil : ∀{A} → Vec A 0
+nil = one
+
+cons : ∀{A n} → A → Vec A n → Vec A (suc n)
+cons x ls = ls , x
+
+{- Q3 : Give the eliminator. -}
+one-elim : ∀ {i} {P : One → Set i} (p : P one) → (o : One) → P o
+one-elim p one = p
+
+elim-vec :
+  ∀{i A}{P : (n : ℕ) → Vec A n → Set i} → 
+  (P 0 (nil {A})) → 
+  (∀{n} → (x : A) → (xs : Vec A n) → P n xs → P (suc n) (cons {A} {n} x xs)) → 
+  ∀{n}(xs : Vec A n) → P n xs
+elim-vec {i} {A} {P} nn cc {n} xs = f xs where
+  f = iter {P = λ n → (a : Vec A n) → P n a}
+    (λ a → one-elim {P = λ x → P 0 x} nn a)
+    (λ m x a → let z = cc {n = m} {!   !} {!   !} {!   !} in {!   !}) n
+
+{- Q4: Implement append using the eliminator. -}
+append : ∀{A m n} → Vec A m → Vec A n → Vec A (m + n)
+append {A} {m} {n} xs ys = elim-vec {P = λ x v → {! Vec   !}} {!   !} {!   !} {!   !}
+

src/AOP/confluence.agda

@@ -0,0 +1,98 @@
+open import Data.Product 
+
+Relation : Set → Set₁
+Relation X = X → X → Set
+
+variable X : Set
+
+data _⁼ (R : Relation X) : Relation X where
+    ⁼-refl : ∀ {x} → (R ⁼) x x
+    ⁼-rel : ∀{x y} → R x y → (R ⁼) x y
+    
+data _⋆ (R : Relation X) : Relation X where
+    ⋆-refl : ∀ {x} → (R ⋆) x x
+    ⋆-step : ∀ {x y z} → R x y → (R ⋆) y z → (R ⋆) x z
+
+LocalConfluent : Relation X → Set
+LocalConfluent R = ∀{x a b} → R x a → R x b → ∃[ y ] (R ⋆) a y × (R ⋆) b y
+
+GlobalConfluent : Relation X → Set
+GlobalConfluent R = ∀{x a b} → (R ⋆) x a → (R ⋆) x b → ∃[ y ] (R ⋆) a y × (R ⋆) b y
+
+SemiConfluent : Relation X → Set
+SemiConfluent R = ∀{x a b} → R x a → (R ⋆) x b → ∃[ y ] (R ⋆) a y × (R ⋆) b y
+
+StrongConfluent : Relation X → Set
+StrongConfluent R = ∀{x a b} → R x a → R x b → ∃[ y ] (R ⋆) a y × (R ⁼) b y
+
+global2local : ∀ (R : Relation X) → GlobalConfluent R → LocalConfluent (R ⋆)
+global2local R gcr x~a x~b =
+  let gc = gcr x~a x~b in
+  gc .proj₁ , ⋆-step (gc .proj₂ .proj₁) ⋆-refl , ⋆-step (gc .proj₂ .proj₂) ⋆-refl
+
+lemma1 : ∀ {R : Relation X} {a b c} → (R ⋆) a b → (R ⋆) b c → (R ⋆) a c
+lemma1 ⋆-refl rb = rb
+lemma1 (⋆-step x ra) rb = ⋆-step x (lemma1 ra rb)
+
+lemma2 : ∀ {R : Relation X} {a} {b} → ((R ⋆) ⋆) a b → (R ⋆) a b
+lemma2 {a} {b} ⋆-refl = ⋆-refl
+lemma2 {a} {b} (⋆-step ⋆-refl s) = lemma2 s
+lemma2 {a} {b} (⋆-step (⋆-step r s) t) = ⋆-step r (lemma1 s (lemma2 t))
+
+local2global : ∀ (R : Relation X) → LocalConfluent (R ⋆) → GlobalConfluent R
+local2global R lcr x~a x~b =
+  let lc = lcr x~a x~b in
+  lc .proj₁ , lemma2 (lc .proj₂ .proj₁) , lemma2 (lc .proj₂ .proj₂)
+
+global2semi : ∀ (R : Relation X) → GlobalConfluent R → SemiConfluent R
+global2semi R gcr x~a x~b = gcr (⋆-step x~a ⋆-refl) x~b
+
+semi2global : ∀ (R : Relation X) → SemiConfluent R → GlobalConfluent R
+semi2global R scr {b = b} ⋆-refl x~b = b , x~b , ⋆-refl
+semi2global R scr (⋆-step x~y y~a) x~b =
+  let sc = scr x~y x~b in
+  let IH = semi2global R scr y~a (sc .proj₂ .proj₁) in
+  IH .proj₁ , IH .proj₂ .proj₁ , lemma1 (sc .proj₂ .proj₂) (IH .proj₂ .proj₂)
+
+lemma3 : ∀ (R : Relation X) → StrongConfluent R → SemiConfluent R
+lemma3 R scr {a = a} x~a ⋆-refl = a , ⋆-refl , ⋆-step x~a ⋆-refl
+lemma3 R scr x~a (⋆-step x~y y~b) with scr x~a x~y
+lemma3 R scr {b = b} x~a (⋆-step x~y z~b) | z , a~z , ⁼-refl = b , (lemma1 a~z z~b) , ⋆-refl
+lemma3 R scr x~a (⋆-step x~y y~b) | z , a~z , ⁼-rel y~z =
+  let IH = lemma3 R scr y~z y~b in
+  IH .proj₁ , lemma1 a~z (IH .proj₂ .proj₁) , IH .proj₂ .proj₂
+
+strong2global : ∀ (R : Relation X) → StrongConfluent R → GlobalConfluent R
+strong2global R scr = semi2global R (lemma3 R scr)
+
+-- Old direct proof before reading the hint:
+-- strong2global R scr {a = a} x~a ⋆-refl = a , ⋆-refl , x~a
+-- strong2global R scr {b = b} ⋆-refl x~b = b , x~b , ⋆-refl
+-- strong2global R scr {a = a} {b = b} (⋆-step {y = p} x~p p~a) (⋆-step {y = q} x~q q~b) =
+--   sc₄ , {!  a~sc₄ !} , {!  b~sc₄ !} where
+--     helper : ∀ {sc₁} (q~b : (R ⋆) q b) (q~sc₁ : (R ⁼) q sc₁) → ∃[ sc₃ ] ((R ⋆) sc₁ sc₃) × ((R ⋆) b sc₃)
+--     helper q~b ⁼-refl = b , q~b , ⋆-refl
+--     helper q~b (⁼-rel q~sc₁) = strong2global R scr (⋆-step q~sc₁ ⋆-refl) q~b
+
+--     IH₁ = scr x~p x~q
+--     sc₁ = IH₁ .proj₁
+--     p~sc₁ = IH₁ .proj₂ .proj₁
+--     q~sc₁ = IH₁ .proj₂ .proj₂
+
+--     IH₂ = strong2global R scr p~a p~sc₁
+--     sc₂ = IH₂ .proj₁
+--     a~sc₂ = IH₂ .proj₂ .proj₁
+--     sc₁~sc₂ = IH₂ .proj₂ .proj₂
+
+--     IH₃ = helper q~b q~sc₁
+--     sc₃ = IH₃ .proj₁
+--     sc₁~sc₃ = IH₃ .proj₂ .proj₁
+--     b~sc₃ = IH₃ .proj₂ .proj₂
+
+--     IH₄ = strong2global R scr sc₁~sc₂ sc₁~sc₃
+--     sc₄ = IH₄ .proj₁
+--     sc₂~sc₄ = IH₄ .proj₂ .proj₁
+--     sc₃~sc₄ = IH₄ .proj₂ .proj₂
+
+--     a~sc₄ = lemma1 a~sc₂ sc₂~sc₄
+--     b~sc₄ = lemma1 b~sc₃ sc₃~sc₄