Prove derivations are structurally unique.HEADmaster

4 files changed, 105 insertions, 26 deletions

diff --git a/README.org b/README.org
index 666898e..b4d808c 100644
--- a/README.org
+++ b/README.org
@@ -9,7 +9,7 @@ Parsing]].
 - [X] Proposition 3.2 :: ~Cfe.Expression.Properties.⟦⟧-mono-env~
 - [X] Lemma 3.3 :: ~Cfe.Language.Properties.∪-selective~
 - [X] Lemma 3.4 :: ~Cfe.Language.Properties.∙-unique~
-- [ ] Lemma 3.5 :: throughout ~Cfe.Language.Properties~. In the paper, statement
+- [-] Lemma 3.5 :: throughout ~Cfe.Language.Properties~. In the paper, statement
   2 is false; a language satisfying \(\tau_\epsilon\) is at most \(\{\epsilon\}\).
   - [X] 1
   - [X] 2
@@ -22,9 +22,6 @@ Parsing]].
 - [X] Lemma 4.2 :: throughout ~Cfe.Judgement.Properties~
 - [X] Theorem 4.3 :: ~Cfe.Judgement.Properties.soundness~
 - [X] Lemma 4.4 :: ~Cfe.Judgement.Properties.subst₂-pres-rank~
-- [ ] Theorem 4.5 :: throughout ~Cfe.Derivation.Properties~
-    - [X] Semantics to derivation
-    - [X] Derivation to semantics
-    - [ ] Uniqueness of derivation
+- [X] Theorem 4.5 :: throughout ~Cfe.Derivation.Properties~
 - [ ] Theorem 4.6 ::
 - [ ] Theorem 4.7 ::
diff --git a/src/Cfe/Derivation/Base.agda b/src/Cfe/Derivation/Base.agda
index 0432c3d..373b6b5 100644
--- a/src/Cfe/Derivation/Base.agda
+++ b/src/Cfe/Derivation/Base.agda
@@ -13,6 +13,7 @@ open import Data.Fin using (zero)
 open import Data.List using (List; []; [_]; _++_)
 open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_)
 open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
 
 infix 5 _⤇_
 infix 4 _≈_
@@ -29,10 +30,10 @@ data _≈_ : ∀ {e w w′} → REL (e ⤇ w) (e ⤇ w′) (c ⊔ ℓ) where
   Eps  : Eps ≈ Eps
   Char : ∀ {c y y′} → (c∼y : c ∼ y) → (c∼y′ : c ∼ y′) → Char c∼y ≈ Char c∼y′
   Cat  :
-    ∀ {e₁ e₂ w w₁ w₂ w₁′ w₂′ e₁⤇w₁ e₁⤇w₁′ e₂⤇w₂ e₂⤇w₂′} →
+    ∀ {e₁ e₂ w w′ w₁ w₂ w₁′ w₂′ e₁⤇w₁ e₁⤇w₁′ e₂⤇w₂ e₂⤇w₂′} →
     (e₁⤇w₁≈e₁⤇w′ : _≈_ {e₁} {w₁} {w₁′} e₁⤇w₁ e₁⤇w₁′) →
     (e₂⤇w₂≈e₂⤇w′ : _≈_ {e₂} {w₂} {w₂′} e₂⤇w₂ e₂⤇w₂′) →
-    (eq : w₁ ++ w₂ ≋ w) → (eq′ : w₁′ ++ w₂′ ≋ w) →
+    (eq : w₁ ++ w₂ ≋ w) → (eq′ : w₁′ ++ w₂′ ≋ w′) →
     Cat e₁⤇w₁ e₂⤇w₂ eq ≈ Cat e₁⤇w₁′ e₂⤇w₂′ eq′
   Veeˡ :
     ∀ {e₁ e₂ w w′ e₁⤇w e₁⤇w′} →
diff --git a/src/Cfe/Derivation/Properties.agda b/src/Cfe/Derivation/Properties.agda
index 99be370..7167465 100644
--- a/src/Cfe/Derivation/Properties.agda
+++ b/src/Cfe/Derivation/Properties.agda
@@ -10,24 +10,24 @@ open Setoid over using () renaming (Carrier to C)
 
 open import Cfe.Context over using (_⊐_; Γ,Δ; ∙,∙; remove₁) renaming (wkn₂ to wkn₂ᶜ)
 open import Cfe.Derivation.Base over
-open import Cfe.Expression over
+open import Cfe.Expression over hiding (_≈_)
 open import Cfe.Fin using (zero; inj; raise!>; cast>)
 open import Cfe.Judgement over
 open import Cfe.Language over hiding (_∙_)
   renaming (_≈_ to _≈ˡ_; ≈-refl to ≈ˡ-refl; ≈-reflexive to ≈ˡ-reflexive; ≈-sym to ≈ˡ-sym)
-open import Cfe.Type over using (_⊛_; _⊨_)
+open import Cfe.Type over using (_⊛_; _⊨_; #⇒selective; ⊛⇒uniqueₗ; ⊛⇒uniqueᵣ)
 open import Cfe.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-insert)
 open import Data.Empty using (⊥-elim)
 open import Data.Fin using (Fin; zero; suc; _≟_; punchOut; punchIn)
 open import Data.Fin.Properties using (punchIn-punchOut)
 open import Data.List using (List; []; length; _++_)
 open import Data.List.Properties using (length-++)
-open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_; []; _∷_)
+open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_; []; _∷_; ≋-refl)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise-length)
 open import Data.Nat using (ℕ; zero; suc; z≤n; s≤s; _+_) renaming (_≤_ to _≤ⁿ_)
 open import Data.Nat.Properties using (n<1+n; m≤m+n; m≤n+m; m≤n⇒m<n∨m≡n; module ≤-Reasoning)
 open import Data.Product using (_×_; _,_; -,_; ∃-syntax; map₂; proj₁; proj₂)
-open import Data.Sum using (inj₁; inj₂; [_,_]′)
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec using ([]; _∷_; [_]; lookup; insert)
 open import Data.Vec.Properties using (insert-lookup; insert-punchIn)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pw using ([]; _∷_)
@@ -39,6 +39,14 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable using (fromWitness)
 
+-- Lemma
+w,e[μe/0]<ₗₑₓw,μe : ∀ {e τ} → [ τ ] ⊐ suc zero ⊢ e ∶ τ → ∀ w → (w , e [ μ e / zero ]) <ₗₑₓ (w , μ e)
+w,e[μe/0]<ₗₑₓw,μe {e} ctx⊢e∶τ w = inj₂ (refl , (begin-strict
+  rank (e [ μ e / zero ]) ≡⟨ subst₂-pres-rank ctx⊢e∶τ zero (Fix ctx⊢e∶τ) ⟩
+  rank e                  <⟨ rank-μ e ⟩
+  rank (μ e)              ∎))
+  where open ≤-Reasoning
+
 parse : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w} → w ∈ ⟦ e ⟧ [] → e ⤇ w
 parse {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ-wellFounded _ Pred go (w , e) ctx⊢e∶τ w∈⟦e⟧
   where
@@ -51,17 +59,10 @@ parse {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ-wellFounded _
   go (w  , μ e)     rec (Fix ctx⊢e∶τ) w∈⟦e⟧ =
     Fix (rec
       (w , e [ μ e / zero ])
-      w,e[μe/0]<ₗₑₓw,μe
+      (w,e[μe/0]<ₗₑₓw,μe ctx⊢e∶τ w)
       (subst₂ ctx⊢e∶τ zero (Fix ctx⊢e∶τ))
       (∈-resp-⊆ ⟦μe⟧⊆⟦e[μe/0]⟧ w∈⟦e⟧))
     where
-    w,e[μe/0]<ₗₑₓw,μe : (w , e [ μ e / zero ]) <ₗₑₓ (w , μ e)
-    w,e[μe/0]<ₗₑₓw,μe = inj₂ (refl , (begin-strict
-      rank (e [ μ e / zero ]) ≡⟨ subst₂-pres-rank ctx⊢e∶τ zero (Fix ctx⊢e∶τ) ⟩
-      rank e                  <⟨ rank-μ e ⟩
-      rank (μ e)              ∎))
-      where open ≤-Reasoning
-
     ⟦μe⟧⊆⟦e[μe/0]⟧ : ⟦ μ e ⟧ [] ⊆ ⟦ e [ μ e / zero ] ⟧ []
     ⟦μe⟧⊆⟦e[μe/0]⟧ = begin
       ⟦ μ e ⟧ []              ⊆⟨  ⋃-unroll (⟦⟧-mono-env e ∘ (_∷ [])) ⟩
@@ -93,15 +94,9 @@ generate {e = e} ctx⊢e∶τ {w} e⤇w = All.wfRec <ₗₑₓ-wellFounded _ Pre
   go (w , Char c)  rec (Char c) (Char c∼y) = c∼y ∷ []
   go (w , μ e)     rec (Fix ctx⊢e∶τ) (Fix e[μe/0]⤇w) = ∈-resp-≈ (μ-roll e []) w∈⟦e[μe/0]⟧
     where
-    w,e[μe/0]<ₗₑₓw,μe : (w , e [ μ e / zero ]) <ₗₑₓ (w , μ e)
-    w,e[μe/0]<ₗₑₓw,μe = inj₂ (refl , (begin-strict
-      rank (e [ μ e / zero ]) ≡⟨ subst₂-pres-rank ctx⊢e∶τ zero (Fix ctx⊢e∶τ) ⟩
-      rank e                  <⟨ rank-μ e ⟩
-      rank (μ e)              ∎))
-      where open ≤-Reasoning
 
     w∈⟦e[μe/0]⟧ : w ∈ ⟦ e [ μ e / zero ] ⟧ []
-    w∈⟦e[μe/0]⟧ = rec (w , e [ μ e / zero ]) w,e[μe/0]<ₗₑₓw,μe (subst₂ ctx⊢e∶τ zero (Fix ctx⊢e∶τ)) e[μe/0]⤇w
+    w∈⟦e[μe/0]⟧ = rec (w , e [ μ e / zero ]) (w,e[μe/0]<ₗₑₓw,μe ctx⊢e∶τ w) (subst₂ ctx⊢e∶τ zero (Fix ctx⊢e∶τ)) e[μe/0]⤇w
   go (w , e₁ ∙ e₂) rec (Cat ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁⊛τ₂) (Cat {w₁ = w₁} {w₂} e₁⤇w₁ e₂⤇w₂ eq) =
     w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq
     where
@@ -115,3 +110,62 @@ generate {e = e} ctx⊢e∶τ {w} e⤇w = All.wfRec <ₗₑₓ-wellFounded _ Pre
     inj₁ (rec (w , e₁) (inj₂ (refl , rank-∨ˡ e₁ e₂)) ctx⊢e₁∶τ₁ e₁⤇w)
   go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) (Veeʳ e₂⤇w) =
     inj₂ (rec (w , e₂) (inj₂ (refl , rank-∨ʳ e₁ e₂)) ctx⊢e₂∶τ₂ e₂⤇w)
+
+parse-unique : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w} (d₁ d₂ : e ⤇ w) → d₁ ≈ d₂
+parse-unique {e = e} ctx⊢e∶τ {w} d₁ d₂ =
+  All.wfRec <ₗₑₓ-wellFounded _ Pred go (w , e) ctx⊢e∶τ ≋-refl d₁ d₂
+  where
+  Pred : (List C × Expression 0) → Set _
+  Pred (w , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w′} → w ≋ w′ → (d₁ : e ⤇ w) → (d₂ : e ⤇ w′) → d₁ ≈ d₂
+
+  go : ∀ w,e → WfRec _<ₗₑₓ_ Pred w,e → Pred w,e
+  go (w , ε)       rec Eps           eq Eps        Eps         = Eps
+  go (w , Char c)  rec (Char c)      eq (Char c∼y) (Char c∼y′) = Char c∼y c∼y′
+  go (w , μ e)     rec (Fix ctx⊢e∶τ) eq (Fix d₁)   (Fix d₂)    =
+    Fix (rec
+      (w , e [ μ e / zero ])
+      (w,e[μe/0]<ₗₑₓw,μe ctx⊢e∶τ w)
+      (subst₂ ctx⊢e∶τ zero (Fix ctx⊢e∶τ))
+      eq d₁ d₂)
+  go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) eq (Veeˡ d₁) (Veeˡ d₂) =
+    Veeˡ (rec (w , e₁) (inj₂ (refl , rank-∨ˡ e₁ e₂)) ctx⊢e₁∶τ₁ eq d₁ d₂)
+  go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) eq (Veeˡ d₁) (Veeʳ d₂) =
+    let w∈⟦e₁⟧ = ⟦ e₁ ⟧ [] .∈-resp-≋ eq (generate ctx⊢e₁∶τ₁ d₁) in
+    let w∈⟦e₂⟧ = generate ctx⊢e₂∶τ₂ d₂ in
+    let ⟦e₁⟧⊨τ₁ = soundness ctx⊢e₁∶τ₁ [] [] in
+    let ⟦e₂⟧⊨τ₂ = soundness ctx⊢e₂∶τ₂ [] [] in
+    ⊥-elim (#⇒selective τ₁#τ₂ ⟦e₁⟧⊨τ₁ ⟦e₂⟧⊨τ₂ (w∈⟦e₁⟧ , w∈⟦e₂⟧))
+    where open Language
+  go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) eq (Veeʳ d₁) (Veeˡ d₂) =
+    let w∈⟦e₁⟧ = generate ctx⊢e₁∶τ₁ d₂ in
+    let w∈⟦e₂⟧ = ⟦ e₂ ⟧ [] .∈-resp-≋ eq (generate ctx⊢e₂∶τ₂ d₁) in
+    let ⟦e₁⟧⊨τ₁ = soundness ctx⊢e₁∶τ₁ [] [] in
+    let ⟦e₂⟧⊨τ₂ = soundness ctx⊢e₂∶τ₂ [] [] in
+    ⊥-elim (#⇒selective τ₁#τ₂ ⟦e₁⟧⊨τ₁ ⟦e₂⟧⊨τ₂ (w∈⟦e₁⟧ , w∈⟦e₂⟧))
+    where open Language
+  go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) eq (Veeʳ d₁) (Veeʳ d₂) =
+    Veeʳ (rec (w , e₂) (inj₂ (refl , rank-∨ʳ e₁ e₂)) ctx⊢e₂∶τ₂ eq d₁ d₂)
+  go (w , e₁ ∙ e₂) rec ctx⊢e₁∙e₂:τ₁∙τ₂@(Cat ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁⊛τ₂) eq
+    d₁@(Cat {w₁ = w₁} {w₂} d₁₁ d₁₂ eq₁)
+    d₂@(Cat {w₁ = w₃} {w₄} d₂₁ d₂₂ eq₂) =
+    Cat
+      (rec (w₁ , e₁) (lex-∙ˡ e₁ e₂ w₁ eq₁) ctx⊢e₁∶τ₁ w₁≋w₃ d₁₁ d₂₁)
+      (rec (w₂ , e₂) (lex-∙ʳ e₁ e₂ [] ε∉⟦e₁⟧ w₁∈⟦e₁⟧ eq₁) ctx⊢e₂∶τ₂ w₂≋w₄ d₁₂ d₂₂)
+      eq₁
+      eq₂
+    where
+    open _⊛_ using (¬n₁); open _⊨_ using (n⇒n); open Language
+    ⟦e₁⟧⊨τ₁ = soundness ctx⊢e₁∶τ₁ [] []
+    ⟦e₂⟧⊨τ₂ = soundness ctx⊢e₂∶τ₂ [] []
+
+    ε∉⟦e₁⟧ = τ₁⊛τ₂ .¬n₁ ∘ ⟦e₁⟧⊨τ₁ .n⇒n
+
+    w₁w₂∈⟦e₁∙e₂⟧ = ⟦ e₁ ∙ e₂ ⟧ [] .∈-resp-≋ eq (generate ctx⊢e₁∙e₂:τ₁∙τ₂ d₁)
+    w₃w₄∈⟦e₁∙e₂⟧ = generate ctx⊢e₁∙e₂:τ₁∙τ₂ d₂
+    w₁∈⟦e₁⟧ = generate ctx⊢e₁∶τ₁ d₁₁
+
+    w₁≋w₃ : w₁ ≋ w₃
+    w₁≋w₃ = ⊛⇒uniqueₗ τ₁⊛τ₂ ⟦e₁⟧⊨τ₁ ⟦e₂⟧⊨τ₂ w₁w₂∈⟦e₁∙e₂⟧ w₃w₄∈⟦e₁∙e₂⟧
+
+    w₂≋w₄ : w₂ ≋ w₄
+    w₂≋w₄ = ⊛⇒uniqueᵣ τ₁⊛τ₂ ⟦e₁⟧⊨τ₁ ⟦e₂⟧⊨τ₂ w₁w₂∈⟦e₁∙e₂⟧ w₃w₄∈⟦e₁∙e₂⟧
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 4b38c1e..985219f 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -55,6 +55,7 @@ open import Data.Empty using (⊥-elim)
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.List using ([]; _∷_; _++_)
 open import Data.List.Properties using (++-assoc; ++-identityʳ)
+open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_)
 open import Data.List.Relation.Binary.Pointwise as Pw hiding (refl; setoid; map)
 open import Data.Nat using (suc; zero; _+_; z≤n; s≤s) renaming (_≤_ to _≤ⁿ_)
 open import Data.Nat.Properties using (m≤m+n; m≤n+m)
@@ -759,6 +760,24 @@ L⊨τε⇒L≤｛ε｝ {A = A} A⊨τε = ∄[First[A]]⇒A⊆｛ε｝ λ _ xw�
       y ∷ w₁ ++ u ∷ w′′  ≈˘⟨ ++⁺ (∼-refl ∷ Pw.refl ∼-refl) (y′∼u ∷ Pw.refl ∼-refl) ⟩
       y ∷ w₁ ++ y′ ∷ w′′ ∎
 
+⊛⇒uniqueₗ :
+  τ₁ ⊛ τ₂ → A ⊨ τ₁ → B ⊨ τ₂ →
+  ∀ {w} → (p q : w ∈ A ∙ˡ B) → (_≋_ on proj₁) p q
+⊛⇒uniqueₗ {A = A} {B = B} τ₁⊛τ₂ A⊨τ₁ B⊨τ₂ =
+  ∙-uniqueₗ A B
+    (λ (c∈l[A] , c∈f[B]) → ∄[l₁∩f₂] (A⊨τ₁ .l⇒l c∈l[A] , B⊨τ₂ .f⇒f c∈f[B]))
+    (λ ε∈A → ¬n₁ (A⊨τ₁ .n⇒n ε∈A))
+  where open _⊛_ τ₁⊛τ₂; open _⊨_
+
+⊛⇒uniqueᵣ :
+  τ₁ ⊛ τ₂ → A ⊨ τ₁ → B ⊨ τ₂ →
+  ∀ {w} → (p q : w ∈ A ∙ˡ B) → (_≋_ on proj₁ ∘ proj₂) p q
+⊛⇒uniqueᵣ {A = A} {B = B} τ₁⊛τ₂ A⊨τ₁ B⊨τ₂ =
+  ∙-uniqueᵣ A B
+    (λ (c∈l[A] , c∈f[B]) → ∄[l₁∩f₂] (A⊨τ₁ .l⇒l c∈l[A] , B⊨τ₂ .f⇒f c∈f[B]))
+    (λ ε∈A → ¬n₁ (A⊨τ₁ .n⇒n ε∈A))
+  where open _⊛_ τ₁⊛τ₂; open _⊨_
+
 ------------------------------------------------------------------------
 -- Properties of _∨_
 ------------------------------------------------------------------------
@@ -986,3 +1005,11 @@ L⊨τε⇒L≤｛ε｝ {A = A} A⊨τε = ∄[First[A]]⇒A⊆｛ε｝ λ _ xw�
   open _#_ τ₁#τ₂
   module A⊨τ₁ = _⊨_ A⊨τ₁
   module B⊨τ₂ = _⊨_ B⊨τ₂
+
+#⇒selective : τ₁ # τ₂ → A ⊨ τ₁ → B ⊨ τ₂ → ∀ {w} → ¬ (w ∈ A × w ∈ B)
+#⇒selective τ₁#τ₂ A⊨τ₁ B⊨τ₂ {[]}    (ε∈A  , ε∈B)  =
+  ¬n₁∨¬n₂ (A⊨τ₁ .n⇒n ε∈A , B⊨τ₂ .n⇒n ε∈B)
+  where open _#_ τ₁#τ₂; open _⊨_
+#⇒selective τ₁#τ₂ A⊨τ₁ B⊨τ₂ {c ∷ w} (cw∈A , cw∈B) =
+  ∄[f₁∩f₂] (A⊨τ₁ .f⇒f (w , cw∈A) , B⊨τ₂ .f⇒f (w , cw∈B))
+  where open _#_ τ₁#τ₂; open _⊨_