Introduce non-terminating proof of derivation existence.

6 files changed, 83 insertions, 5 deletions

diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda
index 2814a64..a428d3c 100644
--- a/src/Cfe/Context/Base.agda
+++ b/src/Cfe/Context/Base.agda
@@ -54,6 +54,8 @@ record Context n : Set (c ⊔ lsuc ℓ) where
     Γ : Vec (Type ℓ ℓ) (n ∸ m)
     Δ : Vec (Type ℓ ℓ) m
 
+∙,∙ : Context 0
+∙,∙ = record { m≤n = z≤n ; Γ = [] ; Δ = [] }
 
 toVec : ∀ {n} → Context n → Vec (Type ℓ ℓ) n
 toVec record { m = .0 ; m≤n = _ ; Γ = Γ ; Δ = [] } = Γ
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index c3367c2..dd9e9b4 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -88,3 +88,12 @@ rotate (μ e) i j i≤j = μ (rotate e (suc i) (suc j) (s≤s i≤j))
 
 _≋_ : {n : ℕ} → Expression n → Expression n → Set (lsuc (c ⊔ ℓ))
 e₁ ≋ e₂ = ∀ γ → ⟦ e₁ ⟧ γ 𝕃.≈ ⟦ e₂ ⟧ γ
+
+rank : {n : ℕ} → Expression n → ℕ
+rank ⊥ = 0
+rank ε = 0
+rank (Char _) = 0
+rank (e₁ ∨ e₂) = suc (rank e₁ ℕ.+ rank e₂)
+rank (e₁ ∙ _) = suc (rank e₁)
+rank (Var _) = 0
+rank (μ e) = suc (rank e)
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
index 9ccdf7c..aff4ae0 100644
--- a/src/Cfe/Judgement/Properties.agda
+++ b/src/Cfe/Judgement/Properties.agda
@@ -189,3 +189,24 @@ soundness (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) γ γ⊨Γ
   ∪-⊨ (soundness Γ,Δ⊢e₁∶τ₁ γ γ⊨Γ,Δ)
       (soundness Γ,Δ⊢e₂∶τ₂ γ γ⊨Γ,Δ)
       τ₁#τ₂
+
+subst-preserves-rank : ∀ {n} {Γ,Δ : Context n} {e τ i τ′} (i≤m : toℕ i ℕ.≤ _) →
+  C.wkn₂ Γ,Δ i≤m τ′ ⊢ e ∶ τ →
+  ∀ {e′} → shift Γ,Δ ⊢ e′ ∶ τ′ →
+  rank (e [ e′ / i ]) ≡ rank e
+subst-preserves-rank i≤m Eps Γ,Δ⊢e′∶τ′ = refl
+subst-preserves-rank i≤m (Char c) Γ,Δ⊢e′∶τ′ = refl
+subst-preserves-rank i≤m Bot Γ,Δ⊢e′∶τ′ = refl
+subst-preserves-rank {i = i} i≤m (Var {i = j} j>m) Γ,Δ⊢e′∶τ′ with i F.≟ j
+... | yes refl = ⊥-elim (<⇒≱ j>m i≤m)
+... | no i≢j = refl
+subst-preserves-rank {Γ,Δ = Γ,Δ} {τ = τ} {τ′ = τ′} i≤m (Fix Γ,Δ⊢e∶τ) Γ,Δ⊢e′∶τ′ =
+  cong suc (subst-preserves-rank {Γ,Δ = cons Γ,Δ τ} (s≤s i≤m)
+    (congᶜ (≋ᶜ-sym (wkn₂-comm Γ,Δ z≤n i≤m τ τ′)) Γ,Δ⊢e∶τ)
+    (congᶜ (≋ᶜ-sym (shift≤-wkn₂-comm-≤ Γ,Δ z≤n z≤n τ)) (wkn₁ Γ,Δ⊢e′∶τ′ z≤n τ)))
+subst-preserves-rank i≤m (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) Γ,Δ⊢e′∶τ′ =
+  cong suc (subst-preserves-rank i≤m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′)
+subst-preserves-rank i≤m (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) Γ,Δ⊢e′∶τ′ =
+  cong₂ (λ x y → suc (x ℕ.+ y))
+        (subst-preserves-rank i≤m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′)
+        (subst-preserves-rank i≤m Γ,Δ⊢e₂∶τ₂ Γ,Δ⊢e′∶τ′)
diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
index 1a37326..0ae9100 100644
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda
@@ -73,6 +73,9 @@ module _
     where
     module Iter = IndexedLanguage (Iterate f)
 
+  fⁿ≤⋃f : ∀ f n → (f ^ n) (Lift a ∅) ≤ ⋃ f
+  fⁿ≤⋃f f n = record { f = n ,_ }
+
   ⋃-cong : ∀ {f g} → (∀ {x y} → x ≈ y → f x ≈ g y) → ⋃ f ≈ ⋃ g
   ⋃-cong f≈g = record
     { f = λ { (n , l∈fn) → n , _≈_.f (f≈g⇒fn≈gn (L.setoid a) f≈g n (Lift a ∅)) l∈fn}
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₂⟧)