Begin soundness proof.

6 files changed, 84 insertions, 29 deletions

diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda
index 6b34a67..2814a64 100644
--- a/src/Cfe/Context/Base.agda
+++ b/src/Cfe/Context/Base.agda
@@ -54,6 +54,11 @@ record Context n : Set (c ⊔ lsuc ℓ) where
     Γ : Vec (Type ℓ ℓ) (n ∸ m)
     Δ : Vec (Type ℓ ℓ) m
 
+
+toVec : ∀ {n} → Context n → Vec (Type ℓ ℓ) n
+toVec record { m = .0 ; m≤n = _ ; Γ = Γ ; Δ = [] } = Γ
+toVec {suc n} record { m = .(suc _) ; m≤n = (s≤s m≤n) ; Γ = Γ ; Δ = (x ∷ Δ) } = x ∷ toVec (record { m≤n = m≤n ; Γ = Γ ; Δ = Δ })
+
 wkn₁ : ∀ {n i} → (Γ,Δ : Context n) → toℕ {suc n} i ≥ Context.m Γ,Δ → Type ℓ ℓ → Context (suc n)
 wkn₁ Γ,Δ i≥m τ = record
   { m≤n = ≤-step m≤n
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index 0b1ae2c..22dc18f 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -55,29 +55,29 @@ isSemiring n = record
       { isSemigroup = record
         { isMagma = record
           { isEquivalence = isEquivalence n
-          ; ∙-cong = λ x≋y u≋v γ → ∙-mon.∙-cong (x≋y γ) (u≋v γ)
+          ; ∙-cong = λ x≋y u≋v γ → ∙.∙-cong {c ⊔ ℓ} (x≋y γ) (u≋v γ)
           }
-        ; assoc = λ x y z γ → ∙-mon.assoc (⟦ x ⟧ γ) (⟦ y ⟧ γ) (⟦ z ⟧ γ)
+        ; assoc = λ x y z γ → ∙.∙-assoc (⟦ x ⟧ γ) (⟦ y ⟧ γ) (⟦ z ⟧ γ)
         }
-      ; identity = (λ x γ → ∙-mon.identityˡ (⟦ x ⟧ γ)) , (λ x γ → ∙-mon.identityʳ (⟦ x ⟧ γ))
+      ; identity = (λ x γ → ∙.∙-identityˡ {ℓ} (⟦ x ⟧ γ)) , (λ x γ → ∙.∙-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)
+        { record { l₁∈A = l₁∈⟦x⟧ ; l₂∈B = inj₁ l₂∈⟦y⟧ ; eq = eq } → inj₁ record { l₁∈A = l₁∈⟦x⟧ ; l₂∈B = l₂∈⟦y⟧ ; eq = eq }
+        ; record { l₁∈A = l₁∈⟦x⟧ ; l₂∈B = inj₂ l₂∈⟦z⟧ ; eq = eq } → inj₂ record { l₁∈A = l₁∈⟦x⟧ ; l₂∈B = l₂∈⟦z⟧ ; eq = eq }
         }
       ; 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
+        { (inj₁ record { l₁∈A = l₁∈⟦x⟧ ; l₂∈B = l₂∈⟦y⟧ ; eq = eq }) → record { l₁∈A = l₁∈⟦x⟧ ; l₂∈B = inj₁ l₂∈⟦y⟧ ; eq = eq }
+        ; (inj₂ record { l₁∈A = l₁∈⟦x⟧ ; l₂∈B = l₂∈⟦z⟧ ; eq = eq }) → record { l₁∈A = l₁∈⟦x⟧ ; l₂∈B = inj₂ l₂∈⟦z⟧ ; eq = eq }
         }
       }) , (λ 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)
+        { record { l₁∈A = inj₁ l₁∈⟦y⟧ ; l₂∈B = l₂∈⟦x⟧ ; eq = eq } → inj₁ record { l₁∈A = l₁∈⟦y⟧ ; l₂∈B = l₂∈⟦x⟧ ; eq = eq }
+        ; record { l₁∈A = inj₂ l₁∈⟦z⟧ ; l₂∈B = l₂∈⟦x⟧ ; eq = eq } → inj₂ record { l₁∈A = l₁∈⟦z⟧ ; l₂∈B = l₂∈⟦x⟧ ; eq = eq }
         }
       ; 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
+        { (inj₁ record { l₁∈A = l₁∈⟦y⟧ ; l₂∈B = l₂∈⟦x⟧ ; eq = eq }) → record { l₁∈A = inj₁ l₁∈⟦y⟧ ; l₂∈B = l₂∈⟦x⟧ ; eq = eq }
+        ; (inj₂ record { l₁∈A = l₁∈⟦z⟧ ; l₂∈B = l₂∈⟦x⟧ ; eq = eq }) → record { l₁∈A = inj₂ l₁∈⟦z⟧ ; l₂∈B = l₂∈⟦x⟧ ; eq = eq }
         }
       })
     }
@@ -91,7 +91,6 @@ isSemiring n = record
   }
   where
   module ∪-comm = IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ})
-  module ∙-mon = IsMonoid (∙.isMonoid {ℓ})
 
 module _ where
   open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ)) as VE
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
index ab4fda9..7e5659d 100644
--- a/src/Cfe/Judgement/Properties.agda
+++ b/src/Cfe/Judgement/Properties.agda
@@ -12,15 +12,19 @@ open import Cfe.Context over as C
   renaming (_≋_ to _≋ᶜ_; ≋-sym to ≋ᶜ-sym; ≋-trans to ≋ᶜ-trans )
 open import Cfe.Expression over as E
 open import Cfe.Judgement.Base over
+open import Cfe.Type over
+open import Cfe.Type.Construct.Lift over
 open import Data.Empty
 open import Data.Fin as F hiding (splitAt)
 open import Data.Fin.Properties hiding (≤-refl; ≤-trans; ≤-irrelevant)
-open import Data.Nat as ℕ
+open import Data.Nat as ℕ hiding (_⊔_)
 open import Data.Nat.Properties
 open import Data.Product
 open import Data.Vec
 open import Data.Vec.Properties
+import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
 open import Function
+open import Level renaming (suc to lsuc)
 open import Relation.Binary.PropositionalEquality hiding (subst₂)
 open import Relation.Nullary
 
@@ -162,3 +166,17 @@ subst₂ {Γ,Δ = Γ,Δ} {τ′ = τ′} i≤m (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,
               Γ,Δ⊢e′∶τ′)
       τ₁⊛τ₂
 subst₂ i≤m (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) Γ,Δ⊢e′∶τ′ = Vee (subst₂ i≤m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′) (subst₂ i≤m Γ,Δ⊢e₂∶τ₂ Γ,Δ⊢e′∶τ′) τ₁#τ₂
+
+soundness : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ γ → PW.Pointwise _⊨_ γ (toVec Γ,Δ) → ⟦ e ⟧ γ ⊨ τ
+soundness Eps γ γ⊨Γ,Δ = ⊨-liftˡ ℓ (⊨-liftʳ ℓ ℓ (｛ε｝⊨τε))
+soundness (Char c) γ γ⊨Γ,Δ = ⊨-liftˡ ℓ (⊨-liftʳ ℓ ℓ (｛c｝⊨τ[c] c))
+soundness Bot γ γ⊨Γ,Δ = ⊨-liftˡ (c ⊔ ℓ) (⊨-liftʳ ℓ ℓ (∅⊨τ⊥))
+soundness {Γ,Δ = Γ,Δ} (Var {i = i} i≥m) γ γ⊨Γ,Δ = subst (⟦ Var i ⟧ γ ⊨_) (sym (τ≡τ′ Γ,Δ i≥m)) (PW.Pointwise.app γ⊨Γ,Δ i)
+  where
+  τ≡τ′ : ∀ {n i} (Γ,Δ : Context n) i≥m → lookup (Context.Γ Γ,Δ) (reduce≥′ {i = i} (Context.m≤n Γ,Δ) i≥m) ≡ lookup (toVec Γ,Δ) i
+  τ≡τ′ {.(suc _)} record { m = .0 ; m≤n = z≤n ; Γ = (x ∷ Γ) ; Δ = [] } i≥m = refl
+  τ≡τ′ {.(suc _)} {suc i} record { m = .(suc _) ; m≤n = (s≤s m≤n) ; Γ = Γ ; Δ = (x ∷ Δ) } (s≤s i≥m) = τ≡τ′ (record { m≤n = m≤n ; Γ = Γ ; Δ = Δ}) i≥m
+-- ⋃ (λ X → ⟦ e ⟧ (X ∷ y)) ⊨ τ
+soundness (Fix Γ,Δ⊢e∶τ) γ γ⊨Γ,Δ = {!!}
+soundness (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) γ γ⊨Γ,Δ = {!!}
+soundness (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) γ γ⊨Γ,Δ = {!!}
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index c4a5670..c7baa48 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -179,8 +179,36 @@ module _
   where
   module X = Language X
 
-∙-unique-prefix : ∀ {a b} (A : Language a) (B : Language b) → Empty (flast A ∩ first B) → ¬ (null A) → ∀ {l} → (l∈A∙B l∈A∙B′ : l ∈ A ∙ B) → Concat.l₁ l∈A∙B ≋ Concat.l₁ l∈A∙B′ × Concat.l₂ l∈A∙B ≋ Concat.l₂ l∈A∙B′
-∙-unique-prefix A B ∄[l₁∩f₂] ¬n₁ l∈A∙B l∈A∙B′ with Compare.compare (Concat.l₁ l∈A∙B) (Concat.l₂ l∈A∙B) (Concat.l₁ l∈A∙B′) (Concat.l₂ l∈A∙B′) (≋-trans (Concat.eq l∈A∙B) (≋-sym (Concat.eq l∈A∙B′)))
+∙-identityʳ : ∀ {a} → RightIdentity _≈_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) _∙_
+∙-identityʳ X = record
+  { f = λ
+    { record { l₁ = l₁ ; l₂ = [] ; l₁∈A = l∈X ; eq = eq } → X.∈-resp-≋ (≋-trans (≋-sym (≋-reflexive (++-identityʳ l₁))) eq) l∈X
+    }
+  ; f⁻¹ = λ {l} l∈X → record
+    { l₁∈A = l∈X
+    ; l₂∈B = lift ≡.refl
+    ; eq = ≋-reflexive (++-identityʳ l)
+    }
+  }
+  where
+  module X = Language X
+
+∙-mono : ∀ {a b} → _∙_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
+∙-mono X≤Y U≤V = record
+  { f = λ
+    { record { l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = eq } → record
+      { l₁∈A = X≤Y.f l₁∈A
+      ; l₂∈B = U≤V.f l₂∈B
+      ; eq = eq
+      }
+    }
+  }
+  where
+  module X≤Y = _≤_ X≤Y
+  module U≤V = _≤_ U≤V
+
+∙-unique : ∀ {a b} (A : Language a) (B : Language b) → Empty (flast A ∩ first B) → ¬ (null A) → ∀ {l} → (l∈A∙B l∈A∙B′ : l ∈ A ∙ B) → Concat.l₁ l∈A∙B ≋ Concat.l₁ l∈A∙B′ × Concat.l₂ l∈A∙B ≋ Concat.l₂ l∈A∙B′
+∙-unique A B ∄[l₁∩f₂] ¬n₁ l∈A∙B l∈A∙B′ with Compare.compare (Concat.l₁ l∈A∙B) (Concat.l₂ l∈A∙B) (Concat.l₁ l∈A∙B′) (Concat.l₂ l∈A∙B′) (≋-trans (Concat.eq l∈A∙B) (≋-sym (Concat.eq l∈A∙B′)))
 ... | cmp with Compare.<?> cmp
 ... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] w ((-, (λ { ≡.refl → ¬n₁ (Concat.l₁∈A l∈A∙B′)}) , (Concat.l₁∈A l∈A∙B′) , -, A.∈-resp-≋ eq₃ (Concat.l₁∈A l∈A∙B)) , (-, B.∈-resp-≋ (≋-sym eq₄) (Concat.l₂∈B l∈A∙B′))))
   where
@@ -200,20 +228,6 @@ module _
   eq₃ = (proj₁ ∘ proj₂ ∘ proj₂) rsplit
   eq₄ = (proj₂ ∘ proj₂ ∘ proj₂) rsplit
 
-∙-identityʳ : ∀ {a} → RightIdentity _≈_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) _∙_
-∙-identityʳ X = record
-  { f = λ
-    { record { l₁ = l₁ ; l₂ = [] ; l₁∈A = l∈X ; eq = eq } → X.∈-resp-≋ (≋-trans (≋-sym (≋-reflexive (++-identityʳ l₁))) eq) l∈X
-    }
-  ; f⁻¹ = λ {l} l∈X → record
-    { l₁∈A = l∈X
-    ; l₂∈B = lift ≡.refl
-    ; eq = ≋-reflexive (++-identityʳ l)
-    }
-  }
-  where
-  module X = Language X
-
 isMagma : ∀ {a} → IsMagma _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
 isMagma {a} = record
   { isEquivalence = ≈-isEquivalence
diff --git a/src/Cfe/Type/Construct/Lift.agda b/src/Cfe/Type/Construct/Lift.agda
index 9f8e439..e26359f 100644
--- a/src/Cfe/Type/Construct/Lift.agda
+++ b/src/Cfe/Type/Construct/Lift.agda
@@ -7,6 +7,7 @@ module Cfe.Type.Construct.Lift
   where
 
 open import Cfe.Type over
+open import Cfe.Language over using (Language)
 open import Level as L hiding (Lift)
 open import Function
 
@@ -18,3 +19,12 @@ Lift fℓ₂ lℓ₂ τ = record
   }
   where
   module τ = Type τ
+
+⊨-liftʳ : ∀ {a fℓ₁ lℓ₁} {L : Language a} {τ : Type fℓ₁ lℓ₁} fℓ₂ lℓ₂ → L ⊨ τ → L ⊨ Lift fℓ₂ lℓ₂ τ
+⊨-liftʳ _ _ L⊨τ = record
+  { n⇒n = n⇒n
+  ; f⇒f = lift ∘ f⇒f
+  ; l⇒l = lift ∘ l⇒l
+  }
+  where
+  open _⊨_ L⊨τ
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index e9ed634..2554ddd 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -67,6 +67,15 @@ L⊨τ+¬N⇒ε∉L {L = L} {τ} L⊨τ ¬n ε∈L = case ∃[ b ] ((null L →
   open _≤_ τ₁≤τ₂
   module A⊨τ₁ = _⊨_ A⊨τ₁
 
+⊨-liftˡ : ∀ {a fℓ lℓ} {L : Language a} {τ : Type fℓ lℓ} b → L ⊨ τ → Lift b L ⊨ τ
+⊨-liftˡ _ L⊨τ = record
+  { n⇒n = λ { ( L.lift ε∈L ) → n⇒n ε∈L }
+  ; f⇒f = λ { ( l , L.lift xl∈L ) → f⇒f (-, xl∈L)}
+  ; l⇒l = λ { ( l , l≢[] , L.lift l∈L , l′ , L.lift lxl′∈L ) → l⇒l (-, l≢[] , l∈L , -, lxl′∈L)}
+  }
+  where
+  open _⊨_ L⊨τ
+
 L⊨τ⊥⇒L≈∅ : ∀ {a} {L : Language a} → L ⊨ τ⊥ → L ≈ˡ ∅
 L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   { f = λ {l} → elim l