Attempt to prove unrolling.thm4.5a

3 files changed, 97 insertions, 9 deletions

diff --git a/src/Cfe/Derivation/Properties.agda b/src/Cfe/Derivation/Properties.agda
index e89d9f1..b3eae87 100644
--- a/src/Cfe/Derivation/Properties.agda
+++ b/src/Cfe/Derivation/Properties.agda
@@ -8,12 +8,12 @@ module Cfe.Derivation.Properties
 
 open Setoid over renaming (Carrier to C; _≈_ to _∼_)
 
-open import Cfe.Context over hiding (_≋_)
+open import Cfe.Context over hiding (_≋_) renaming (≋-sym to ≋ᶜ-sym)
 open import Cfe.Expression over hiding (_≋_)
 open import Cfe.Language over hiding (≤-refl; _≈_; _<_)
 open import Cfe.Language.Construct.Concatenate over using (Concat)
 open import Cfe.Language.Indexed.Construct.Iterate over
-open import Cfe.Judgement over
+open import Cfe.Judgement over renaming (wkn₁ to wkn₁ⱼ; shift≤ to shift≤ⱼ)
 open import Cfe.Derivation.Base over
 open import Cfe.Type over using (_⊛_; _⊨_)
 open import Data.Bool using (T; not; true; false)
@@ -29,22 +29,58 @@ open import Data.Product.Relation.Binary.Lex.Strict
 open import Data.Sum as Sum
 open import Data.Vec hiding (length; _++_)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive
-open import Data.Vec.Relation.Binary.Pointwise.Extensional
+open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
 open import Function
 open import Induction.WellFounded
-open import Level
+open import Level hiding (Lift)
 open import Relation.Binary
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.PropositionalEquality as ≡ hiding (subst₂; setoid)
 
 private
   infix 4 _<_
-  _<_ : Rel (List C × Expression 0) _
-  _<_ = ×-Lex _≡_ ℕ._<_ _<ᵣₐₙₖ_ on (Product.map₁ length)
+  _<_ : ∀ {m n} → REL (List C × Expression m) (List C × Expression n) _
+  (l , e) < (l′ , e′) = length l ℕ.< length l′ ⊎ length l ≡ length l′ × e <ᵣₐₙₖ e′
 
-  <-wellFounded : WellFounded _<_
+    _<ₙ_ : Rel (∃[ n ] List C × Expression n) _
+  nle <ₙ nle′ = proj₂ nle < proj₂ nle′
+
+  <-wellFounded : ∀ {n} → WellFounded (_<_ {n})
   <-wellFounded = On.wellFounded (Product.map₁ length) (×-wellFounded <ⁿ-wellFounded <ᵣₐₙₖ-wellFounded)
 
+unroll₁ : ∀ {n} {Γ,Δ : Context n} {e e′ τ τ′ i} (i≥m : toℕ i ℕ.≥ _) →
+          wkn₁ Γ,Δ i≥m τ′ ⊢ e ∶ τ → Γ,Δ ⊢ μ e′ ∶ τ′ →
+          ∀ {l} γ → PW.Pointwise _⊨_ γ (toVec Γ,Δ) →
+          l ∈ ⟦ e ⟧ (insert γ i (⟦ μ e′ ⟧ γ)) →
+          ∃[ n ] l ∈ ⟦ e ⟧ (insert γ i (((λ X → ⟦ e′ ⟧ (X ∷ γ)) ^ n) (Lift _ ∅)))
+unroll₁ {e = e} i≥m Γ,Δ⊢e∶τ Γ,Δ⊢e′∶τ′ {l = l} γ γ⊨Γ,Δ l∈⟦e⟧ =
+  All.wfRec <-wellFounded _ Pred {!!} (l , e) i≥m Γ,Δ⊢e∶τ Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ l∈⟦e⟧
+  where
+  Pred : ∀ {n} → List C × Expression (ℕ.suc n) → Set _
+  Pred {n} (l , e) =
+    ∀ {Γ,Δ : Context n} {e′ τ τ′ i} (i≥m : toℕ i ℕ.≥ _) →
+    wkn₁ Γ,Δ i≥m τ′ ⊢ e ∶ τ → Γ,Δ ⊢ μ e′ ∶ τ′ →
+    ∀ γ → PW.Pointwise _⊨_ γ (toVec Γ,Δ) →
+    l ∈ ⟦ e ⟧ (insert γ i (⟦ μ e′ ⟧ γ)) →
+    ∃[ n ] l ∈ ⟦ e ⟧ (insert γ i (((λ X → ⟦ e′ ⟧ (X ∷ γ)) ^ n) (Lift _ ∅)))
+
+  go : ∀ {n} l,e → WfRec _<_ (Pred {n}) l,e → Pred l,e
+  go (l , ε) rec i≥m Γ,Δ⊢e∶τ Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ l∈⟦e⟧ = 1 , l∈⟦e⟧
+  go (l , Char x) rec i≥m Γ,Δ⊢e∶τ Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ l∈⟦e⟧ = 1 , l∈⟦e⟧
+  go (l , (e₁ ∨ e₂)) rec i≥m (Vee Γ,Δ⊢e₁∶τ₁ _ _) Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ (inj₁ l∈⟦e₁⟧) =
+    Product.map₂ inj₁ (rec (l , e₁) {!!} i≥m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ l∈⟦e₁⟧)
+  go (l , (e₁ ∨ e₂)) rec i≥m (Vee _ Γ,Δ⊢e₂∶τ₂ _) Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ (inj₂ l∈⟦e₂⟧) =
+    Product.map₂ inj₂ (rec (l , e₂) {!!} i≥m Γ,Δ⊢e₂∶τ₂ Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ l∈⟦e₂⟧)
+  go (l , (e₁ ∙ e₂)) rec {Γ,Δ} {τ′ = τ′} i≥m (Γ,Δ⊢e∶τ @ (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ _)) Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ l∈⟦e⟧ =
+    Product.zip ℕ._+_ (λ l₁∈⟦e₁⟧ l₂∈⟦e₂⟧ → record { l₁∈A = {!fⁿ≤fⁿ⁺ᵐ!} ; l₂∈B = {!!} ; eq = l∈⟦e⟧.eq }) l₁∈⟦e₁⟧′ l₂∈⟦e₂⟧′
+    where
+    module l∈⟦e⟧ = Concat l∈⟦e⟧
+    l₁∈⟦e₁⟧′ = rec (l∈⟦e⟧.l₁ , e₁) {!!} i≥m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ l∈⟦e⟧.l₁∈A
+    l₂∈⟦e₂⟧′ = rec (l∈⟦e⟧.l₂ , e₂) {!!} z≤n (congᶜ (shift≤-wkn₁-comm Γ,Δ z≤n i≥m τ′) Δ++Γ,∙⊢e₂∶τ₂) (shift≤ⱼ Γ,Δ⊢e′∶τ′ z≤n) γ (subst (PW.Pointwise _⊨_ γ) (≡.sym (shift≤-toVec Γ,Δ z≤n)) γ⊨Γ,Δ) l∈⟦e⟧.l₂∈B
+  go (l , Var x) rec i≥m Γ,Δ⊢e∶τ Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ l∈⟦e⟧ = {!!}
+  go (l , μ e) rec i≥m Γ,Δ⊢e∶τ Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ (suc n , l∈⟦e⟧) =
+    Product.map₂ {!!} (rec (l , e [ μ e / F.zero ]) {!!} i≥m {!!} Γ,Δ⊢e′∶τ′ γ γ⊨Γ,Δ {!!})
+
 l∈⟦e⟧⇒e⤇l : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → l ∈ ⟦ e ⟧ [] → e ⤇ l
 l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-wellFounded _ Pred go (l , e) ∙,∙⊢e∶τ l∈⟦e⟧
   where
@@ -114,3 +150,42 @@ l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-well
     Veeˡ (rec (l , e₁) (inj₂ (≡.refl , e₁<ᵣₐₙₖe₁∨e₂ e₁ e₂)) ∙,∙⊢e₁∶τ₁ l∈⟦e₁⟧)
   go (l , e₁ ∨ e₂) rec (Vee _ ∙,∙⊢e₂∶τ₂ _) (inj₂ l∈⟦e₂⟧) =
     Veeʳ (rec (l , e₂) (inj₂ (≡.refl , e₂<ᵣₐₙₖe₁∨e₂ e₁ e₂)) ∙,∙⊢e₂∶τ₂ l∈⟦e₂⟧)
+
+e⤇l⇒l∈⟦e⟧ : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → e ⤇ l → l ∈ ⟦ e ⟧ []
+e⤇l⇒l∈⟦e⟧ {e} ∙,∙⊢e∶τ {l} e⤇l = All.wfRec <-wellFounded _ Pred go (l , e) ∙,∙⊢e∶τ e⤇l
+  where
+  Pred : List C × Expression 0 → Set _
+  Pred (l , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → e ⤇ l → l ∈ ⟦ e ⟧ []
+
+  go : ∀ l,e → WfRec _<_ Pred l,e → Pred l,e
+  go (l , ε) rec ∙,∙⊢e∶τ Eps = Level.lift ≡.refl
+  go (l , (Char _)) rec ∙,∙⊢e∶τ (Char c∼y) = Level.lift (c∼y ∷ [])
+  go (l , (e₁ ∙ e₂)) rec (∙,∙⊢e₁∙e₂∶τ @ (Cat ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ _)) (Cat {l₁ = l₁} {l₂ = l₂} e₁⤇l₁ e₂⤇l₂ eq) = record
+    { l₁∈A = rec (l₁ , e₁) {!!} ∙,∙⊢e₁∶τ₁ e₁⤇l₁
+    ; l₂∈B = rec (l₂ , e₂) {!!} ∙,∙⊢e₂∶τ₂ e₂⤇l₂
+    ; eq = eq
+    }
+  go (l , (e₁ ∨ e₂)) rec ∙,∙⊢e∶τ (Veeˡ e₁⤇l) = inj₁ (rec {!!} {!!} {!!} e₁⤇l)
+  go (l , (e₁ ∨ e₂)) rec ∙,∙⊢e∶τ (Veeʳ e₂⤇l) = inj₂ (rec {!!} {!!} {!!} e₂⤇l)
+  go (l , (μ e)) rec ∙,∙⊢e∶τ (Fix e⤇l) = {!e!}
+
+derivation-unique : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → l ∈ ⟦ e ⟧ [] → (e⤇l e⤇l′ : e ⤇ l) → e⤇l ≈ e⤇l′
+derivation-unique {e} ∙,∙⊢e∶τ {l} l∈⟦e⟧ e⤇l e⤇l′ = All.wfRec <-wellFounded _ Pred {!!} (l , e) ∙,∙⊢e∶τ l∈⟦e⟧ e⤇l e⤇l′
+  where
+  Pred : List C × Expression 0 → Set _
+  Pred (l , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → l ∈ ⟦ e ⟧ [] → (e⤇l e⤇l′ : e ⤇ l) → e⤇l ≈ e⤇l′
+
+  go : ∀ l,e → WfRec _<_ Pred l,e → Pred l,e
+  go (l , e) rec ∙,∙⊢e∶τ l∈⟦e⟧ Eps Eps = Eps
+  go (l , e) rec ∙,∙⊢e∶τ l∈⟦e⟧ (Char c∼y) (Char c∼y′) = Char c∼y c∼y′
+  go (l , e) rec ∙,∙⊢e∶τ l∈⟦e⟧ (Cat e₁⤇l₁ e₂⤇l₂ eq) (Cat e₁⤇l₁′ e₂⤇l₂′ eq′) = {!!}
+  go (l , e₁ ∨ e₂) rec (Vee ∙,∙⊢e₁∶τ₁ _ _) (inj₁ l∈⟦e₁⟧) (Veeˡ e₁⤇l) (Veeˡ e₁⤇l′) =
+    Veeˡ (rec (l , e₁) (inj₂ (≡.refl , e₁<ᵣₐₙₖe₁∨e₂ e₁ e₂)) ∙,∙⊢e₁∶τ₁ l∈⟦e₁⟧ e₁⤇l e₁⤇l′)
+  go ([] , e₁ ∨ e₂) rec (Vee ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁#τ₂) (inj₁ l∈⟦e⟧) (Veeˡ e₁⤇l) (Veeʳ e₂⤇l′) =
+    ⊥-elim {!!}
+  go (x ∷ l , e₁ ∨ e₂) rec (Vee ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁#τ₂) (inj₁ l∈⟦e⟧) (Veeˡ e₁⤇l) (Veeʳ e₂⤇l′) =
+    ⊥-elim {!!}
+  go (l , e₁ ∨ e₂) rec (Vee ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ τ₁#τ₂) (inj₂ l∈⟦e⟧) (Veeˡ e₁⤇l) _ = {!!}
+  go (l , e₁ ∨ e₂) rec ∙,∙⊢e∶τ l∈⟦e⟧ (Veeʳ e₂⤇l) (Veeˡ e₁⤇l′) = {!!}
+  go (l , e₁ ∨ e₂) rec ∙,∙⊢e∶τ l∈⟦e⟧ (Veeʳ e₂⤇l) (Veeʳ e₂⤇l′) = {!!}
+  go (l , e) rec ∙,∙⊢e∶τ l∈⟦e⟧ (Fix e⤇l) e⤇l′ = {!!}
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index 1cd57a7..aabab1b 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -100,5 +100,5 @@ rank (μ e) = suc (rank e)
 
 infix 4 _<ᵣₐₙₖ_
 
-_<ᵣₐₙₖ_ : ∀ {n} → Rel (Expression n) _
-_<ᵣₐₙₖ_ = ℕ._<_ on rank
+_<ᵣₐₙₖ_ : ∀ {m n} → REL (Expression m) (Expression n) _
+e <ᵣₐₙₖ e′ = rank e ℕ.< rank e′
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index d1e2869..f21fe72 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -231,3 +231,16 @@ e₂<ᵣₐₙₖe₁∨e₂ e₁ e₂ = begin-strict
   rank (e₁ ∨ e₂)            ∎
   where
   open ≤-Reasoning
+
+-- ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) ≤ ⟦ μ e ⟧ []
+-- l ∈ ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) → l ∈ ⟦ μ e ⟧ []
+-- l ∈ ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ []) → l ∈ ⋃ (λ x → ⟦ e ⟧ (x ∷ []))
+-- l ∈ ⟦ e′ ⟧ (⟦ μ e ⟧ [] ∷ []) → ∃[ n ] l ∈ ⟦ e′ ⟧ ((λ X → ⟦ e ⟧ (X ∷ [])) ^ n ∷ [])
+-- e-unroll : ∀ {n} (e : Expression (suc n)) e′ i γ → ⟦ e [ e′ / i ] ⟧ γ L.≤ ∃[ n ] (⟦ e ⟧ )
+-- e-unroll ⊥ = ?
+-- e-unroll ε = ?
+-- e-unroll (Char x) = ?
+-- e-unroll (e ∨ e₁) = {!!}
+-- e-unroll (e ∙ e₁) = {!!}
+-- e-unroll (Var x) = {!!}
+-- e-unroll (μ e) = {!!}