Complete proofs up to Proposition 3.2 (excluding unrolling)

2 files changed, 269 insertions, 27 deletions

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index 4c53638..c4940b6 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -1,37 +1,69 @@
 {-# OPTIONS --without-K --safe #-}
 
+open import Function
 open import Relation.Binary
+import Relation.Binary.PropositionalEquality as ≡
 
 module Cfe.Expression.Base
-  {a ℓ} (setoid : Setoid a ℓ)
+  {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid setoid renaming (Carrier to A)
+open Setoid over renaming (Carrier to C)
 
-open import Cfe.Language setoid renaming (_∙_ to _∙ₗ_)
-open import Data.Fin hiding (_≤_)
-open import Data.Nat hiding (_≤_; _⊔_)
+open import Cfe.Language over as 𝕃
+open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ₗ_)
+open import Cfe.Language.Construct.Single over
+open import Cfe.Language.Construct.Union over
+open import Cfe.Language.Indexed.Construct.Iterate over
+open import Data.Fin as F hiding (_≤_)
+open import Data.Nat as ℕ hiding (_≤_; _⊔_)
 open import Data.Product
 open import Data.Vec
-open import Level renaming (suc to lsuc)
-
-data Expression : ℕ → Set a where
-  ⊥ : {n : ℕ} → Expression n
-  ε : {n : ℕ} → Expression n
-  Char : {n : ℕ} → A → Expression n
-  _∨_ : {n : ℕ} → Expression n → Expression n → Expression n
-  _∙_ : {n : ℕ} → Expression n → Expression n → Expression n
-  Var : {n : ℕ} → Fin n → Expression n
-  μ : {n : ℕ} → Expression (suc n) → Expression n
-
-〚_〛 : {n : ℕ} → Expression n → Vec Language n → Language
-〚 ⊥ 〛 _ = ∅
-〚 ε 〛 _ = ｛ε｝
-〚 Char c 〛 _ = ｛ c ｝
-〚 e₁ ∨ e₂ 〛 γ = 〚 e₁ 〛 γ ∪ 〚 e₂ 〛 γ
-〚 e₁ ∙ e₂ 〛 γ = 〚 e₁ 〛 γ ∙ₗ 〚 e₂ 〛 γ
-〚 Var n 〛 γ = lookup γ n
-〚 μ e 〛 γ = fix (λ X → 〚 e 〛 (X ∷ γ))
-
-_≋_ : {n : ℕ} → Expression n → Expression n → Set (lsuc a ⊔ lsuc ℓ)
-e₁ ≋ e₂ = ∀ γ → 〚 e₁ 〛 γ ≤ 〚 e₂ 〛 γ × 〚 e₂ 〛 γ ≤ 〚 e₁ 〛 γ
+open import Level renaming (suc to lsuc) hiding (Lift)
+open import Relation.Nullary
+
+infix 10 _[_/_]
+infix 7 _∙_
+infix 6 _∨_
+infix 4 _≋_
+
+data Expression : ℕ → Set c where
+  ⊥ : ∀ {n} → Expression n
+  ε : ∀ {n} → Expression n
+  Char : ∀ {n} → C → Expression n
+  _∨_ : ∀ {n} → Expression n → Expression n → Expression n
+  _∙_ : ∀ {n} → Expression n → Expression n → Expression n
+  Var : ∀ {n} → Fin n → Expression n
+  μ : ∀ {n} → Expression (suc n) → Expression n
+
+wkn : ∀ {n} → Expression n → Fin (suc n) → Expression (suc n)
+wkn ⊥ i = ⊥
+wkn ε i = ε
+wkn (Char x) i = Char x
+wkn (e₁ ∨ e₂) i = wkn e₁ i ∨ wkn e₂ i
+wkn (e₁ ∙ e₂) i = wkn e₁ i ∙ wkn e₂ i
+wkn (Var x) i = Var (punchIn i x)
+wkn (μ e) i = μ (wkn e (suc i))
+
+_[_/_] : ∀ {n} → Expression (suc n) → Expression n → Fin (suc n) → Expression n
+⊥ [ e′ / i ] = ⊥
+ε [ e′ / i ] = ε
+Char x [ e′ / i ] = Char x
+(e₁ ∨ e₂) [ e′ / i ] = e₁ [ e′ / i ] ∨ e₂ [ e′ / i ]
+(e₁ ∙ e₂) [ e′ / i ] = e₁ [ e′ / i ] ∙ e₂ [ e′ / i ]
+Var j [ e′ / i ] with i F.≟ j
+... | yes i≡j = e′
+... | no i≢j = Var (punchOut i≢j)
+μ e [ e′ / i ] = μ (e [ wkn e′ F.zero / suc i ])
+
+⟦_⟧ : ∀ {n : ℕ} → Expression n → Vec (Language (c ⊔ ℓ) (c ⊔ ℓ)) n → Language (c ⊔ ℓ) (c ⊔ ℓ)
+⟦ ⊥ ⟧ _ = Lift (c ⊔ ℓ) (c ⊔ ℓ) ∅
+⟦ ε ⟧ _ = Lift ℓ (c ⊔ ℓ) ｛ε｝
+⟦ Char x ⟧ _ = Lift ℓ (c ⊔ ℓ) ｛ x ｝
+⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ
+⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ₗ ⟦ e₂ ⟧ γ
+⟦ Var n ⟧ γ = lookup γ n
+⟦ μ e ⟧ γ = ⋃ (λ X → ⟦ e ⟧ (X ∷ γ))
+
+_≋_ : {n : ℕ} → Expression n → Expression n → Set (lsuc (c ⊔ ℓ))
+e₁ ≋ e₂ = ∀ γ → ⟦ e₁ ⟧ γ 𝕃.≈ ⟦ e₂ ⟧ γ
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
new file mode 100644
index 0000000..8bdc635
--- /dev/null
+++ b/src/Cfe/Expression/Properties.agda
@@ -0,0 +1,210 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Cfe.Expression.Properties
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open Setoid over using () renaming (Carrier to C)
+
+open import Algebra
+open import Cfe.Expression.Base over
+open import Cfe.Language.Base over as L
+import Cfe.Language.Construct.Concatenate over as ∙
+import Cfe.Language.Construct.Union over as ∪
+import Cfe.Language.Indexed.Construct.Iterate over as ⋃
+open import Data.Fin as F
+open import Data.Nat as ℕ hiding (_⊔_)
+open import Data.Product
+open import Data.Sum
+open import Data.Unit
+open import Data.Vec
+open import Data.Vec.Properties
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+open import Function
+open import Level renaming (suc to lsuc)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Relation.Nullary
+
+isEquivalence : ∀ n → IsEquivalence (_≋_ {n})
+isEquivalence n = record
+  { refl = λ γ → ≈-refl
+  ; sym = λ x≋y γ → ≈-sym (x≋y γ)
+  ; trans = λ x≋y y≋z γ → ≈-trans (x≋y γ) (y≋z γ)
+  }
+
+isSemiring : ∀ n → IsSemiring (_≋_ {n}) _∨_ _∙_ ⊥ ε
+isSemiring n = record
+  { isSemiringWithoutAnnihilatingZero = record
+    { +-isCommutativeMonoid = record
+      { isMonoid = record
+        { isSemigroup = record
+          { isMagma = record
+            { isEquivalence = isEquivalence n
+            ; ∙-cong = λ x≋y u≋v γ → ∪-comm.∙-cong (x≋y γ) (u≋v γ)
+            }
+          ; assoc = λ x y z γ → ∪-comm.assoc (⟦ x ⟧ γ) (⟦ y ⟧ γ) (⟦ z ⟧ γ)
+          }
+        ; identity = (λ x γ → ∪-comm.identityˡ (⟦ x ⟧ γ)) , (λ x γ → ∪-comm.identityʳ (⟦ x ⟧ γ))
+        }
+      ; comm = λ x y γ → ∪-comm.comm (⟦ x ⟧ γ) (⟦ y ⟧ γ)
+      }
+    ; *-isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = isEquivalence n
+          ; ∙-cong = λ x≋y u≋v γ → ∙-mon.∙-cong (x≋y γ) (u≋v γ)
+          }
+        ; assoc = λ x y z γ → ∙-mon.assoc (⟦ x ⟧ γ) (⟦ y ⟧ γ) (⟦ z ⟧ γ)
+        }
+      ; identity = (λ x γ → ∙-mon.identityˡ (⟦ x ⟧ γ)) , (λ x γ → ∙-mon.identityʳ (⟦ x ⟧ γ))
+      }
+    ; distrib = (λ x y z γ → record
+      { f = λ
+        { (l₁ , l₁∈⟦x⟧ , l₂ , inj₁ l₂∈⟦y⟧ , l₁++l₂≡l) → inj₁ (-, l₁∈⟦x⟧ , -, l₂∈⟦y⟧ , l₁++l₂≡l)
+        ; (l₁ , l₁∈⟦x⟧ , l₂ , inj₂ l₂∈⟦z⟧ , l₁++l₂≡l) → inj₂ (-, l₁∈⟦x⟧ , -, l₂∈⟦z⟧ , l₁++l₂≡l)
+        }
+      ; f⁻¹ = λ
+        { (inj₁ (l₁ , l₁∈⟦x⟧ , l₂ , l₂∈⟦y⟧ , l₁++l₂≡l)) → -, l₁∈⟦x⟧ , -, inj₁ l₂∈⟦y⟧ , l₁++l₂≡l
+        ; (inj₂ (l₁ , l₁∈⟦x⟧ , l₂ , l₂∈⟦z⟧ , l₁++l₂≡l)) → -, l₁∈⟦x⟧ , -, inj₂ l₂∈⟦z⟧ , l₁++l₂≡l
+        }
+      ; cong₁ = λ
+        { (l₁≈l₁′ , ∪.A≈A l₂≈l₂′) → ∪.A≈A (l₁≈l₁′ , l₂≈l₂′)
+        ; (l₁≈l₁′ , ∪.B≈B l₂≈l₂′) → ∪.B≈B (l₁≈l₁′ , l₂≈l₂′)
+        }
+      ; cong₂ = λ
+        { (∪.A≈A (l₁≈l₁′ , l₂≈l₂′)) → l₁≈l₁′ , ∪.A≈A l₂≈l₂′
+        ; (∪.B≈B (l₁≈l₁′ , l₂≈l₂′)) → l₁≈l₁′ , ∪.B≈B l₂≈l₂′
+        }
+      }) , (λ x y z γ → record
+      { f = λ
+        { (l₁ , inj₁ l₁∈⟦y⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l) → inj₁ (-, l₁∈⟦y⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l)
+        ; (l₁ , inj₂ l₁∈⟦z⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l) → inj₂ (-, l₁∈⟦z⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l)
+        }
+      ; f⁻¹ = λ
+        { (inj₁ (l₁ , l₁∈⟦y⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l)) → -, inj₁ l₁∈⟦y⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l
+        ; (inj₂ (l₁ , l₁∈⟦z⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l)) → -, inj₂ l₁∈⟦z⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l
+        }
+      ; cong₁ = λ
+        { (∪.A≈A l₁≈l₁′ , l₂≈l₂′) → ∪.A≈A (l₁≈l₁′ , l₂≈l₂′)
+        ; (∪.B≈B l₁≈l₁′ , l₂≈l₂′) → ∪.B≈B (l₁≈l₁′ , l₂≈l₂′)
+        }
+      ; cong₂ = λ
+        { (∪.A≈A (l₁≈l₁′ , l₂≈l₂′)) → ∪.A≈A l₁≈l₁′ , l₂≈l₂′
+        ; (∪.B≈B (l₁≈l₁′ , l₂≈l₂′)) → ∪.B≈B l₁≈l₁′ , l₂≈l₂′
+        }
+      })
+    }
+  ; zero = (λ x γ → record
+    { f = λ ()
+    ; f⁻¹ = λ ()
+    ; cong₁ = λ {_} {_} {l₁∈⟦⊥∙x⟧} → case l₁∈⟦⊥∙x⟧ of (λ ())
+    ; cong₂ = λ {_} {_} {l₁∈⟦⊥⟧} → case l₁∈⟦⊥⟧ of (λ ())
+    }) , (λ x γ → record
+    { f = λ ()
+    ; f⁻¹ = λ ()
+    ; cong₁ = λ {_} {_} {l₁∈⟦x∙⊥⟧} → case l₁∈⟦x∙⊥⟧ of (λ ())
+    ; cong₂ = λ {_} {_} {l₁∈⟦⊥⟧} → case l₁∈⟦⊥⟧ of (λ ())
+    })
+  }
+  where
+  module ∪-comm = IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+  module ∙-mon = IsMonoid (∙.isMonoid {ℓ} {c ⊔ ℓ})
+
+module _ where
+  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+  open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+
+  cong-env : ∀ {n} → (e : Expression n) → ∀ {γ γ′} → γ VE.≋ γ′ → ⟦ e ⟧ γ ≈ ⟦ e ⟧ γ′
+  cong-env ⊥ γ≈γ′ = ≈-refl
+  cong-env ε γ≈γ′ = ≈-refl
+  cong-env (Char x) γ≈γ′ = ≈-refl
+  cong-env (e₁ ∨ e₂) γ≈γ′ = ∪-cong (cong-env e₁ γ≈γ′) (cong-env e₂ γ≈γ′)
+    where
+    open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+  cong-env (e₁ ∙ e₂) γ≈γ′ = ∙-cong (cong-env e₁ γ≈γ′) (cong-env e₂ γ≈γ′)
+    where
+    open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+  cong-env (Var j) γ≈γ′ = PW.lookup γ≈γ′ j
+  cong-env (μ e) γ≈γ′ = ⋃.⋃-cong (λ x → cong-env e (x PW.∷ γ≈γ′))
+
+wkn-no-use : ∀ {n} → (e : Expression n) → ∀ i γ → ⟦ wkn e i ⟧ γ ≈ ⟦ e ⟧ (remove γ i)
+wkn-no-use ⊥ i γ = ≈-refl
+wkn-no-use ε i γ = ≈-refl
+wkn-no-use (Char x) i γ = ≈-refl
+wkn-no-use (e₁ ∨ e₂) i γ = ∪-cong (wkn-no-use e₁ i γ) (wkn-no-use e₂ i γ)
+  where
+  open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+wkn-no-use (e₁ ∙ e₂) i γ = ∙-cong (wkn-no-use e₁ i γ) (wkn-no-use e₂ i γ)
+  where
+  open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+wkn-no-use (Var j) i γ = reflexive (begin
+  lookup γ (punchIn i j)                                    ≡˘⟨ ≡.cong (λ x → lookup x (punchIn i j)) (insert-remove γ i) ⟩
+  lookup (insert (remove γ i) i (lookup γ i)) (punchIn i j) ≡⟨ insert-punchIn (remove γ i) i (lookup γ i) j ⟩
+  lookup (remove γ i) j                                     ∎)
+  where
+  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+  open ≡.≡-Reasoning
+wkn-no-use (μ e) i (z ∷ γ) = ⋃.⋃-cong (λ {x} {y} x≈y → begin
+  ⟦ wkn e (suc i) ⟧ (x ∷ z ∷ γ)      ≈⟨ cong-env (wkn e (suc i)) (x≈y ∷ ≋-refl) ⟩
+  ⟦ wkn e (suc i) ⟧ (y ∷ z ∷ γ)      ≈⟨ wkn-no-use e (suc i) (y ∷ z ∷ γ) ⟩
+  ⟦ e ⟧ (remove (y ∷ z ∷ γ) (suc i)) ≡⟨⟩
+  ⟦ e ⟧ (y ∷ remove (z ∷ γ) i)       ∎)
+  where
+  open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ))
+  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+
+subst-fun : ∀ {n} → (e : Expression (suc n)) → ∀ e′ i γ → ⟦ e [ e′ / i ] ⟧ γ ≈ ⟦ e ⟧ (insert γ i (⟦ e′ ⟧ γ))
+subst-fun ⊥ e′ i γ = ≈-refl
+subst-fun ε e′ i γ = ≈-refl
+subst-fun (Char x) e′ i γ = ≈-refl
+subst-fun {n} (e₁ ∨ e₂) e′ i γ = ∪-cong (subst-fun e₁ e′ i γ) (subst-fun e₂ e′ i γ)
+  where
+  open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+subst-fun (e₁ ∙ e₂) e′ i γ = ∙-cong (subst-fun e₁ e′ i γ) (subst-fun e₂ e′ i γ)
+  where
+  open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+subst-fun (Var j) e′ i γ with i F.≟ j
+... | yes _≡_.refl = sym (reflexive (insert-lookup γ i (⟦ e′ ⟧ γ)))
+  where
+  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+... | no i≢j = reflexive (begin
+                 lookup γ (punchOut i≢j) ≡˘⟨ ≡.cong (λ x → lookup x (punchOut i≢j)) (remove-insert γ i (⟦ e′ ⟧ γ)) ⟩
+                 lookup (remove (insert γ i (⟦ e′ ⟧ γ)) i) (punchOut i≢j) ≡⟨ remove-punchOut (insert γ i (⟦ e′ ⟧ γ)) i≢j ⟩
+                 lookup (insert γ i (⟦ e′ ⟧ γ)) j ∎)
+  where
+  open ≡.≡-Reasoning
+  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+subst-fun (μ e) e′ i γ = ⋃.⋃-cong λ {x} {y} x≈y → begin
+  ⟦ e [ wkn e′ F.zero / suc i ] ⟧ (x ∷ γ) ≈⟨ cong-env (e [ wkn e′ F.zero / suc i ]) (x≈y ∷ ≋-refl) ⟩
+  ⟦ e [ wkn e′ F.zero / suc i ] ⟧ (y ∷ γ) ≈⟨ subst-fun e (wkn e′ F.zero) (suc i) (y ∷ γ) ⟩
+  ⟦ e ⟧ (y ∷ insert γ i (⟦ wkn e′ F.zero ⟧ (y ∷ γ))) ≈⟨ cong-env e (≈-refl ∷ insert′ (wkn-no-use e′ F.zero (y ∷ γ)) ≋-refl i) ⟩
+  ⟦ e ⟧ (y ∷ insert γ i (⟦ e′ ⟧ γ)) ∎
+  where
+  open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ))
+  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+
+  insert′ : ∀ {n x y} {xs ys : Vec (Language (c ⊔ ℓ) (c ⊔ ℓ)) n} → x ≈ y → xs VE.≋ ys → (i : Fin (suc n)) → insert xs i x VE.≋ insert ys i y
+  insert′ x≈y xs≋ys F.zero = x≈y ∷ xs≋ys
+  insert′ x≈y (z≈w ∷ xs≋ys) (suc i) = z≈w ∷ insert′ x≈y xs≋ys i
+
+unroll : ∀ {n} → (e : Expression (suc n)) → μ e ≋ e [ μ e / F.zero ]
+unroll e γ = begin
+  ⟦ μ e ⟧ γ ≈⟨ {!!} ⟩
+  (λ X → ⟦ e ⟧ (X ∷ γ)) (⟦ μ e ⟧ γ) ≡⟨⟩
+  ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ) ≡⟨⟩
+  ⟦ e ⟧ (insert γ F.zero (⟦ μ e ⟧ γ)) ≈˘⟨ subst-fun e (μ e) F.zero γ ⟩
+  ⟦ e [ μ e / F.zero ] ⟧ γ ∎
+  where
+  open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ))
+  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+
+monotone : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
+monotone ⊥ γ≤γ′ = ≤-refl
+monotone ε γ≤γ′ = ≤-refl
+monotone (Char x) γ≤γ′ = ≤-refl
+monotone (e₁ ∨ e₂) γ≤γ′ = ∪.∪-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
+monotone (e₁ ∙ e₂) γ≤γ′ = ∙.∙-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
+monotone (Var i) γ≤γ′ = PW.lookup γ≤γ′ i
+monotone (μ e) γ≤γ′ = ⋃.⋃-monotone (λ x≤y → monotone e (x≤y PW.∷ γ≤γ′))