From adad5280af0d81a2f171df619e9c7169dcb43a02 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 27 Mar 2021 20:32:03 +0000
Subject: Introduce non-terminating proof of derivation existence.

---
 src/Cfe/Parse/Base.agda       | 12 +++++++-----
 src/Cfe/Parse/Properties.agda | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 5 deletions(-)

(limited to 'src/Cfe/Parse')

diff --git a/src/Cfe/Parse/Base.agda b/src/Cfe/Parse/Base.agda
index 50e085a..0f8ad21 100644
--- a/src/Cfe/Parse/Base.agda
+++ b/src/Cfe/Parse/Base.agda
@@ -6,18 +6,20 @@ module Cfe.Parse.Base
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid over renaming (Carrier to C)
+open Setoid over renaming (Carrier to C; _≈_ to _∼_)
 
-open import Cfe.Expression over
+open import Cfe.Expression over hiding (_≋_)
 open import Data.Fin
 open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid over
+open import Level using (_⊔_)
 
 infix 4 _⤇_
 
-data _⤇_ : Expression 0 → List C → Set c where
+data _⤇_ : Expression 0 → List C → Set (c ⊔ ℓ) where
   Eps : ε ⤇ []
-  Char : ∀ {c} → Char c ⤇ [ c ]
-  Cat : ∀ {e₁ e₂ l₁ l₂} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → e₁ ∙ e₂ ⤇ l₁ ++ l₂
+  Char : ∀ {c y} → c ∼ y → Char c ⤇ [ y ]
+  Cat : ∀ {e₁ e₂ l₁ l₂ l} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → l₁ ++ l₂ ≋ l → e₁ ∙ e₂ ⤇ l
   Veeˡ : ∀ {e₁ e₂ l} → e₁ ⤇ l → e₁ ∨ e₂ ⤇ l
   Veeʳ : ∀ {e₁ e₂ l} → e₂ ⤇ l → e₁ ∨ e₂ ⤇ l
   Fix : ∀ {e l} → e [ μ e / zero ] ⤇ l → μ e ⤇ l
diff --git a/src/Cfe/Parse/Properties.agda b/src/Cfe/Parse/Properties.agda
index 7803f82..830b0f2 100644
--- a/src/Cfe/Parse/Properties.agda
+++ b/src/Cfe/Parse/Properties.agda
@@ -5,3 +5,44 @@ open import Relation.Binary using (Setoid)
 module Cfe.Parse.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
+
+open Setoid over renaming (Carrier to C)
+
+open import Cfe.Context over
+open import Cfe.Expression over
+open import Cfe.Language over
+open import Cfe.Language.Indexed.Construct.Iterate over
+open import Cfe.Judgement over
+open import Cfe.Parse.Base over
+open import Cfe.Type over using (_⊛_; _⊨_)
+open import Data.Bool using (T; not; true; false)
+open import Data.Empty using (⊥-elim)
+open import Data.Fin as F
+open import Data.List hiding (null)
+open import Data.List.Relation.Binary.Equality.Setoid over
+open import Data.Nat as ℕ hiding (_⊔_; _^_)
+open import Data.Product
+open import Data.Sum
+open import Data.Vec
+open import Data.Vec.Relation.Binary.Pointwise.Inductive
+open import Data.Vec.Relation.Binary.Pointwise.Extensional
+open import Function
+open import Level
+open import Relation.Binary.PropositionalEquality hiding (subst₂; setoid)
+
+l∈⟦e⟧⇒e⤇l : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → l ∈ ⟦ e ⟧ [] → e ⤇ l
+l∈⟦e⟧⇒e⤇l Eps (lift refl) = Eps
+l∈⟦e⟧⇒e⤇l (Char c) (lift (c∼y ∷ [])) = Char c∼y
+l∈⟦e⟧⇒e⤇l {μ e} (Fix ∙,τ⊢e∶τ) (suc n , l∈⟦e⟧ⁿ⁺¹) = Fix (l∈⟦e⟧⇒e⤇l (subst₂ z≤n ∙,τ⊢e∶τ (Fix ∙,τ⊢e∶τ)) l∈⟦e[μe]⟧)
+  where
+  open import Relation.Binary.Reasoning.PartialOrder (poset (c ⊔ ℓ))
+  ⟦e⟧ⁿ⁺¹≤⟦e[μe]⟧ = begin
+    ⟦ e ⟧ (((λ X → ⟦ e ⟧ (X ∷ [])) ^ n) (⟦ ⊥ ⟧ []) ∷ []) ≤⟨ mono e ((fⁿ≤⋃f (λ X → ⟦ e ⟧ (X ∷ [])) n) ∷ []) ⟩
+    ⟦ e ⟧ (⋃ (λ X → ⟦ e ⟧ (X ∷ [])) ∷ [])                ≡⟨⟩
+    ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ [])                              ≈˘⟨ subst-fun e (μ e) F.zero [] ⟩
+    ⟦ e [ μ e / F.zero ] ⟧ []                            ∎
+  l∈⟦e[μe]⟧ = _≤_.f ⟦e⟧ⁿ⁺¹≤⟦e[μe]⟧ l∈⟦e⟧ⁿ⁺¹
+l∈⟦e⟧⇒e⤇l (Cat ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁⊛τ₂) record { l₁∈A = l₁∈⟦e₁⟧ ; l₂∈B = l₂∈⟦e₂⟧ ; eq = eq } =
+  Cat (l∈⟦e⟧⇒e⤇l ∙,∙⊢e₁∶τ₁ l₁∈⟦e₁⟧) (l∈⟦e⟧⇒e⤇l ∙,∙⊢e₂∶τ₂ l₂∈⟦e₂⟧) eq
+l∈⟦e⟧⇒e⤇l (Vee ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁#τ₂) (inj₁ l∈⟦e₁⟧) = Veeˡ (l∈⟦e⟧⇒e⤇l ∙,∙⊢e₁∶τ₁ l∈⟦e₁⟧)
+l∈⟦e⟧⇒e⤇l (Vee ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁#τ₂) (inj₂ l∈⟦e₂⟧) = Veeʳ (l∈⟦e⟧⇒e⤇l ∙,∙⊢e₂∶τ₂ l∈⟦e₂⟧)
-- 
cgit v1.2.3