Prove judgement weakening.

4 files changed, 141 insertions, 16 deletions

diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda
index dcd8056..6b7a9dc 100644
--- a/src/Cfe/Context/Base.agda
+++ b/src/Cfe/Context/Base.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary using (Setoid; Rel)
 
 module Cfe.Context.Base
   {c ℓ} (over : Setoid c ℓ)
@@ -8,18 +8,23 @@ module Cfe.Context.Base
 
 open import Cfe.Type over
 open import Data.Empty
-open import Data.Fin as F
+open import Data.Fin as F hiding (cast)
 open import Data.Fin.Properties hiding (≤-trans)
 open import Data.Nat as ℕ hiding (_⊔_)
 open import Data.Nat.Properties
+open import Data.Product
 open import Data.Vec
 open import Level renaming (suc to lsuc)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary
 
-reduce≥′ : ∀ {m n} → .(m ℕ.≤ n) → (i : Fin n) → .(toℕ i ≥ m) → Fin (n ∸ m)
+cast : ∀ {a A m n} → .(m ≡ n) → Vec {a} A m → Vec {a} A n
+cast {m = 0} {0} eq [] = []
+cast {m = suc _} {suc n} eq (x ∷ xs) = x ∷ cast (cong ℕ.pred eq) xs
+
+reduce≥′ : ∀ {m n} → .(m ℕ.≤ n) → (i : Fin n) → toℕ i ≥ m → Fin (n ∸ m)
 reduce≥′ {ℕ.zero} {n} m≤n i i≥m = i
-reduce≥′ {suc m} {suc n} m≤n (suc i) i≥m = reduce≥′ (pred-mono m≤n) i (pred-mono i≥m)
+reduce≥′ {suc m} {suc n} m≤n (suc i) (s≤s i≥m) = reduce≥′ (pred-mono m≤n) i i≥m
 
 private
   insert′ : ∀ {a A m n} → Vec {a} A (n ∸ m) → m ℕ.≤ n → m ≢ 0 → (i : Fin (n ∸ ℕ.pred m)) → A → Vec A (n ∸ ℕ.pred m)
@@ -29,9 +34,9 @@ private
   insert′ {a} {A} {suc (suc m)} {suc ℕ.zero} xs m≤n _ i x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) m≤n)
   insert′ {a} {A} {suc (suc m)} {suc (suc n)} xs m≤n _ i x = insert′ {m = suc m} xs (pred-mono m≤n) (λ ()) i x
 
-  reduce≥′-mono : ∀ {m n} → .(m≤n : m ℕ.≤ n) → (i j : Fin n) → .(i≥m : toℕ i ≥ m) → (i≤j : i F.≤ j) → reduce≥′ m≤n i i≥m F.≤ reduce≥′ m≤n j (≤-trans i≥m i≤j)
+  reduce≥′-mono : ∀ {m n} → .(m≤n : m ℕ.≤ n) → (i j : Fin n) → (i≥m : toℕ i ≥ m) → (i≤j : i F.≤ j) → reduce≥′ m≤n i i≥m F.≤ reduce≥′ m≤n j (≤-trans i≥m i≤j)
   reduce≥′-mono {ℕ.zero} {n} m≤n i j i≥m i≤j = i≤j
-  reduce≥′-mono {suc m} {suc n} m≤n (suc i) (suc j) i≥m i≤j = reduce≥′-mono (pred-mono m≤n) i j (pred-mono i≥m) (pred-mono i≤j)
+  reduce≥′-mono {suc m} {suc n} m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = reduce≥′-mono (pred-mono m≤n) i j i≥m i≤j
 
   remove′ : ∀ {a A m} → Vec {a} A m → .(m ≢ 0) → Fin m → Vec A (ℕ.pred m)
   remove′ (x ∷ xs) m≢0 F.zero = xs
@@ -48,25 +53,25 @@ record Context n : Set (c ⊔ lsuc ℓ) where
     Γ : Vec (Type ℓ ℓ) (n ∸ m)
     Δ : Vec (Type ℓ ℓ) m
 
-wkn₁ : ∀ {n} → (Γ,Δ : Context n) → (i : Fin (suc n)) → .(toℕ i ≥ Context.m Γ,Δ) → Type ℓ ℓ → Context (suc n)
+wkn₁ : ∀ {n} → (Γ,Δ : Context n) → (i : Fin (suc n)) → (toℕ i ≥ Context.m Γ,Δ) → Type ℓ ℓ → Context (suc n)
 wkn₁ Γ,Δ i i≥m τ = record
   { m≤n = ≤-step m≤n
-  ; Γ = subst (Vec (Type ℓ ℓ)) (sym (+-∸-assoc 1 m≤n)) (insert Γ (F.cast (+-∸-assoc 1 m≤n) (reduce≥′ (≤-step m≤n) i i≥m)) τ)
+  ; Γ = cast (sym (+-∸-assoc 1 m≤n)) (insert Γ (F.cast (+-∸-assoc 1 m≤n) (reduce≥′ (≤-step m≤n) i i≥m)) τ)
   ; Δ = Δ
   }
   where
   open Context Γ,Δ
 
 wkn₂ : ∀ {n} → (Γ,Δ : Context n) → (i : Fin (suc n)) → toℕ i ℕ.≤ Context.m Γ,Δ → Type ℓ ℓ → Context (suc n)
-wkn₂ Γ,Δ i i<m τ = record
+wkn₂ Γ,Δ i i≤m τ = record
   { m≤n = s≤s m≤n
   ; Γ = Γ
-  ; Δ = insert Δ (fromℕ< (s≤s i<m)) τ
+  ; Δ = insert Δ (fromℕ< (s≤s i≤m)) τ
   }
   where
   open Context Γ,Δ
 
-rotate₁ : ∀ {n} → (Γ,Δ : Context n) → (i j : Fin n) → toℕ i ≥ Context.m Γ,Δ → .(i F.≤ j) → Context n
+rotate₁ : ∀ {n} → (Γ,Δ : Context n) → (i j : Fin n) → toℕ i ≥ Context.m Γ,Δ → (i F.≤ j) → Context n
 rotate₁ {n} Γ,Δ i j i≥m i≤j = record
   { m≤n = m≤n
   ; Γ = rotate (reduce≥′ m≤n i i≥m) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) (reduce≥′-mono m≤n i j i≥m i≤j) Γ
@@ -104,8 +109,8 @@ transfer {n} Γ,Δ i j i<m 1+j≥m with Context.m Γ,Δ ℕ.≟ 0
   where
   open Context Γ,Δ
 
-cons : ∀ {n} → Type ℓ ℓ → Context n → Context (suc n)
-cons {n} τ Γ,Δ = record
+cons : ∀ {n} → Context n → Type ℓ ℓ → Context (suc n)
+cons {n} Γ,Δ τ = record
   { m≤n = s≤s m≤n
   ; Γ = Γ
   ; Δ = τ ∷ Δ
@@ -116,8 +121,11 @@ cons {n} τ Γ,Δ = record
 shift : ∀ {n} → Context n → Context n
 shift {n} Γ,Δ = record
   { m≤n = z≤n
-  ; Γ = subst (Vec (Type ℓ ℓ)) (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (Δ ++ Γ)
+  ; Γ = cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (Δ ++ Γ)
   ; Δ = []
   }
   where
   open Context Γ,Δ
+
+_≋_ : ∀ {n} → Rel (Context n) (c ⊔ lsuc ℓ)
+Γ,Δ ≋ Γ,Δ′ = Σ (Context.m Γ,Δ ≡ Context.m Γ,Δ′) λ {refl → Context.Γ Γ,Δ ≡ Context.Γ Γ,Δ′ × Context.Δ Γ,Δ ≡ Context.Δ Γ,Δ′}
diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda
index 2acaf72..2761fae 100644
--- a/src/Cfe/Context/Properties.agda
+++ b/src/Cfe/Context/Properties.agda
@@ -1,7 +1,64 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary using (Setoid; Symmetric)
 
 module Cfe.Context.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
+
+open import Cfe.Context.Base over as C
+open import Cfe.Type over
+open import Data.Fin as F
+open import Data.Nat as ℕ
+open import Data.Nat.Properties
+open import Data.Product
+open import Data.Vec
+open import Function
+open import Relation.Binary.PropositionalEquality
+
+≋-sym : ∀ {n} → Symmetric (_≋_ {n})
+≋-sym (refl , refl , refl) = refl , refl , refl
+
+cast-involutive : ∀ {a A k m n} .(k≡m : k ≡ m) .(m≡n : m ≡ n) .(k≡n : _) xs → C.cast m≡n (C.cast {a} {A} k≡m xs) ≡ C.cast k≡n xs
+cast-involutive {k = zero} {zero} {zero} k≡m m≡n k≡n [] = refl
+cast-involutive {k = suc _} {suc _} {suc _} k≡m m≡n k≡n (x ∷ xs) = cong (x ∷_) (cast-involutive (cong ℕ.pred k≡m) (cong ℕ.pred m≡n) (cong ℕ.pred k≡n) xs)
+
+wkn₁-shift : ∀ {n} (Γ,Δ : Context n) i i≥m τ → shift (wkn₁ Γ,Δ i i≥m τ) ≋ wkn₁ (shift Γ,Δ) i z≤n τ
+wkn₁-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i i≥m τ =
+  refl ,
+  eq Δ Γ m≤n i i≥m τ ,
+  refl
+  where
+  eq : ∀ {a A m n} xs ys .(m≤n : m ℕ.≤ n) i (i≥m : toℕ i ≥ m) y →
+       C.cast {a} {A}
+         (trans (sym (+-∸-assoc m (≤-step m≤n))) (m+n∸m≡n m (suc n)))
+         (xs ++ C.cast (sym (+-∸-assoc 1 m≤n)) (insert ys (F.cast (+-∸-assoc 1 m≤n) (reduce≥′ (≤-step m≤n) i i≥m)) y)) ≡
+       C.cast refl (insert (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (xs ++ ys)) (F.cast refl i) y)
+  eq [] [] m≤n zero i≥m y = refl
+  eq [] (x ∷ ys) m≤n zero i≥m y = refl
+  eq [] (x ∷ ys) m≤n (suc i) i≥m y = cong (x ∷_) (eq [] ys z≤n i z≤n y)
+  eq {m = suc m} {suc n} (x ∷ xs) ys m≤n (suc i) (s≤s i≥m) y = cong (x ∷_) (eq xs ys (pred-mono m≤n) i i≥m y)
+
+wkn₂-shift : ∀ {n} (Γ,Δ : Context n) i i≤m τ → shift (wkn₂ Γ,Δ i i≤m τ) ≋ wkn₁ (shift Γ,Δ) i z≤n τ
+wkn₂-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i i≤m τ =
+  refl ,
+  eq Δ Γ m≤n i i≤m τ ,
+  refl
+  where
+  eq : ∀ {a A m n} xs ys .(m≤n : m ℕ.≤ n) i (i≤m : toℕ i ℕ.≤ m) y →
+       C.cast {a} {A}
+         (trans (sym (+-∸-assoc (suc m) (s≤s m≤n))) (m+n∸m≡n (suc m) (suc n)))
+         (insert xs (fromℕ< (s≤s i≤m)) y ++ ys) ≡
+       C.cast
+         (sym (+-∸-assoc 1 z≤n))
+         (insert (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (xs ++ ys))
+                 (F.cast (+-∸-assoc 1 z≤n) (reduce≥′ (≤-step z≤n) i z≤n)) y)
+  eq [] [] m≤n zero i≤m y = refl
+  eq [] (x ∷ ys) m≤n zero i≤m y = cong (λ z → y ∷ x ∷ z) (sym (cast-involutive refl refl refl ys))
+  eq {m = suc m} {suc n} (x ∷ xs) ys m≤n zero i≤m y =
+    cong (λ z → y ∷ x ∷ z)
+         (sym (cast-involutive (trans (sym (+-∸-assoc m (pred-mono m≤n))) (m+n∸m≡n m n))
+                               refl
+                               (trans (sym (+-∸-assoc m (pred-mono m≤n))) (m+n∸m≡n m n))
+                               (xs ++ ys)))
+  eq {m = suc m} {suc n} (x ∷ xs) ys m≤n (suc i) (s≤s i≤m) y = cong (x ∷_) (eq xs ys (pred-mono m≤n) i i≤m y)
diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda
index 6b42598..0e5417a 100644
--- a/src/Cfe/Judgement/Base.agda
+++ b/src/Cfe/Judgement/Base.agda
@@ -22,6 +22,6 @@ data _⊢_∶_ : {n : ℕ} → Context n → Expression n → Type ℓ ℓ → S
   Char : ∀ {n} {Γ,Δ : Context n} c → Γ,Δ ⊢ Char c ∶ Lift ℓ ℓ τ[ c ]
   Bot : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ⊥ ∶ Lift ℓ ℓ τ⊥
   Var : ∀ {n} {Γ,Δ : Context n} {i} (i≥m : toℕ i ≥ _) → Γ,Δ ⊢ Var i ∶ lookup (Context.Γ Γ,Δ) (reduce≥′ (Context.m≤n Γ,Δ) i i≥m)
-  Fix : ∀ {n} {Γ,Δ : Context n} {e τ} → cons τ Γ,Δ ⊢ e ∶ τ → Γ,Δ ⊢ μ e ∶ τ
+  Fix : ∀ {n} {Γ,Δ : Context n} {e τ} → cons Γ,Δ τ ⊢ e ∶ τ → Γ,Δ ⊢ μ e ∶ τ
   Cat : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → shift Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁⊛τ₂ : τ₁ ⊛ τ₂) → Γ,Δ ⊢ e₁ ∙ e₂ ∶ τ₁ ∙ₜ τ₂
   Vee : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ,Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
index b901ced..7f357f0 100644
--- a/src/Cfe/Judgement/Properties.agda
+++ b/src/Cfe/Judgement/Properties.agda
@@ -5,3 +5,63 @@ open import Relation.Binary using (Setoid)
 module Cfe.Judgement.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
+
+open import Cfe.Context over renaming (wkn₁ to cwkn₁; wkn₂ to cwkn₂; _≋_ to _≋ᶜ_)
+open import Cfe.Expression over
+open import Cfe.Judgement.Base over
+open import Data.Fin
+open import Data.Nat as ℕ
+open import Data.Nat.Properties
+open import Data.Product
+open import Data.Vec
+open import Relation.Binary.PropositionalEquality
+
+toℕ-punchIn : ∀ {n} i j → toℕ j ℕ.≤ toℕ (punchIn {n} i j)
+toℕ-punchIn zero j = n≤1+n (toℕ j)
+toℕ-punchIn (suc i) zero = ≤-refl
+toℕ-punchIn (suc i) (suc j) = s≤s (toℕ-punchIn i j)
+
+congᶜ : ∀ {n} {Γ,Δ Γ,Δ′ : Context n} {e τ} → Γ,Δ ≋ᶜ Γ,Δ′ → Γ,Δ ⊢ e ∶ τ → Γ,Δ′ ⊢ e ∶ τ
+congᶜ {Γ,Δ = Γ,Δ} {Γ,Δ′} (refl , refl , refl) Γ,Δ⊢e∶τ with ≤-irrelevant (Context.m≤n Γ,Δ) (Context.m≤n Γ,Δ′)
+... | refl = Γ,Δ⊢e∶τ
+
+congᵗ : ∀ {n} {Γ,Δ : Context n} {e τ τ′} → τ ≡ τ′ → Γ,Δ ⊢ e ∶ τ → Γ,Δ ⊢ e ∶ τ′
+congᵗ refl Γ,Δ⊢e∶τ = Γ,Δ⊢e∶τ
+
+wkn₁ : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ i τ′ i≥m → cwkn₁ Γ,Δ i i≥m τ′ ⊢ wkn e i ∶ τ
+wkn₁ Eps i τ′ i≥m = Eps
+wkn₁ (Char c) i τ′ i≥m = Char c
+wkn₁ Bot i τ′ i≥m = Bot
+wkn₁ {Γ,Δ = Γ,Δ} (Var {i = j} j≥m) i τ′ i≥m = congᵗ (τ≡τ′ Γ,Δ i j i≥m j≥m τ′) (Var (≤-trans j≥m (toℕ-punchIn i j)))
+  where
+  open Context Γ,Δ
+  τ≡τ′ : ∀ {n} (Γ,Δ : Context n) i j i≥m j≥m τ → lookup (Context.Γ (cwkn₁ Γ,Δ i i≥m τ)) (reduce≥′ (≤-step (Context.m≤n Γ,Δ)) (punchIn i j) (≤-trans j≥m (toℕ-punchIn i j))) ≡ lookup (Context.Γ Γ,Δ) (reduce≥′ (Context.m≤n Γ,Δ) j j≥m)
+  τ≡τ′ {suc _} record { m = zero ; m≤n = _ ; Γ = (_ ∷ _) ; Δ = _ } zero zero _ _ _ = refl
+  τ≡τ′ {suc n} record { m = zero ; m≤n = _ ; Γ = (_ ∷ Γ) ; Δ = Δ } zero (suc j) _ _ τ = τ≡τ′ (record { m≤n = z≤n ; Γ = Γ ; Δ = Δ }) zero j z≤n z≤n τ
+  τ≡τ′ {suc n} record { m = zero ; m≤n = _ ; Γ = (_ ∷ _) ; Δ = _ } (suc _) zero _ _ τ = refl
+  τ≡τ′ {suc n} record { m = zero ; m≤n = _ ; Γ = (_ ∷ Γ) ; Δ = Δ } (suc i) (suc j) _ _ τ = τ≡τ′ (record { m≤n = z≤n ; Γ = Γ ; Δ = Δ}) i j z≤n z≤n τ
+  τ≡τ′ {suc n} record { m = (suc m) ; m≤n = (s≤s m≤n) ; Γ = Γ ; Δ = (_ ∷ Δ) } (suc i) (suc j) (s≤s i≥m) (s≤s j≥m) τ = τ≡τ′ (record { m≤n = m≤n ; Γ = Γ ; Δ = Δ}) i j i≥m j≥m τ
+wkn₁ (Fix Γ,Δ⊢e∶τ) i τ′ i≥m = Fix (wkn₁ Γ,Δ⊢e∶τ (suc i) τ′ (s≤s i≥m))
+wkn₁ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i τ′ i≥m = Cat (wkn₁ Γ,Δ⊢e₁∶τ₁ i τ′ i≥m) (congᶜ (≋-sym (wkn₁-shift Γ,Δ i i≥m τ′)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ i τ′ z≤n)) τ₁⊛τ₂
+wkn₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i τ′ i≥m = Vee (wkn₁ Γ,Δ⊢e₁∶τ₁ i τ′ i≥m) (wkn₁ Γ,Δ⊢e₂∶τ₂ i τ′ i≥m) τ₁#τ₂
+
+wkn₂ : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ i τ′ i≤m → cwkn₂ Γ,Δ i i≤m τ′ ⊢ wkn e i ∶ τ
+wkn₂ Eps i τ′ i≤m = Eps
+wkn₂ (Char c) i τ′ i≤m = Char c
+wkn₂ Bot i τ′ i≤m = Bot
+wkn₂ {Γ,Δ = Γ,Δ} (Var {i = j} j≥m) i τ′ i≤m =
+  congᵗ
+    (τ≡τ′ (Context.Γ Γ,Δ) (Context.m≤n Γ,Δ) i j i≤m j≥m)
+    (Var (punchIn[i,j]≥m i j i≤m j≥m))
+  where
+  punchIn[i,j]≥m : ∀ {m n} i j → toℕ i ℕ.≤ m → toℕ j ≥ m → toℕ (punchIn {n} i j) ≥ suc m
+  punchIn[i,j]≥m {m} zero j i≤m j≥m = s≤s j≥m
+  punchIn[i,j]≥m {suc m} (suc i) (suc j) (s≤s i≤m) (s≤s j≥m) = s≤s (punchIn[i,j]≥m i j i≤m j≥m)
+
+  τ≡τ′ : ∀ {a A m n} xs m≤n i j i≤m j≥m → lookup {a} {A} xs (reduce≥′ {suc m} (s≤s m≤n) (punchIn {n} i j) (punchIn[i,j]≥m i j i≤m j≥m)) ≡ lookup xs (reduce≥′ m≤n j j≥m)
+  τ≡τ′ {m = zero} xs m≤n zero j i≤m j≥m = refl
+  τ≡τ′ {m = suc _} xs m≤n zero (suc j) i≤m (s≤s j≥m) = τ≡τ′ xs (pred-mono m≤n) zero j z≤n j≥m
+  τ≡τ′ {m = suc _} xs m≤n (suc i) (suc j) (s≤s i≤m) (s≤s j≥m) = τ≡τ′ xs (pred-mono m≤n) i j i≤m j≥m
+wkn₂ (Fix Γ,Δ⊢e∶τ) i τ′ i≤m = Fix (wkn₂ Γ,Δ⊢e∶τ (suc i) τ′ (s≤s i≤m))
+wkn₂ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i τ′ i≤m = Cat (wkn₂ Γ,Δ⊢e₁∶τ₁ i τ′ i≤m) (congᶜ (≋-sym (wkn₂-shift Γ,Δ i i≤m τ′)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ i τ′ z≤n)) τ₁⊛τ₂
+wkn₂ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i τ′ i≤m = Vee (wkn₂ Γ,Δ⊢e₁∶τ₁ i τ′ i≤m) (wkn₂ Γ,Δ⊢e₂∶τ₂ i τ′ i≤m) τ₁#τ₂