From 0dc59b43f78654a746ef5baaeabcc767c64ee0df Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 13 Mar 2021 20:06:22 +0000
Subject: Add weakening proofs for type judgements.

---
 src/Cfe/Judgement/Properties.agda | 159 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 159 insertions(+)
 create mode 100644 src/Cfe/Judgement/Properties.agda

(limited to 'src/Cfe/Judgement/Properties.agda')

diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
new file mode 100644
index 0000000..b5183eb
--- /dev/null
+++ b/src/Cfe/Judgement/Properties.agda
@@ -0,0 +1,159 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Setoid)
+
+module Cfe.Judgement.Properties
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open import Cfe.Expression over
+open import Cfe.Judgement.Base over
+open import Cfe.Type over
+open import Data.Empty
+open import Data.Fin as F hiding (cast)
+open import Data.Fin.Properties
+open import Data.Nat as ℕ
+open import Data.Nat.Properties
+open import Data.Vec
+open import Data.Vec.Properties
+open import Function
+open import Relation.Binary.PropositionalEquality
+
+wkn₁ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
+       Γ , Δ ⊢ e ∶ τ →
+       ∀ τ′ i →
+       insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (wkn e (F.cast (+-suc n m) (raise n i))) ∶ τ
+wkn₁ Eps τ′ i = Eps
+wkn₁ (Char c) τ′ i = Char c
+wkn₁ Bot τ′ i = Bot
+wkn₁ {m} {n} {Γ} {Δ} {e} {τ} (Var {i = j} j≥n) τ′ i =
+  subst (insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (Var (punchIn (F.cast (+-suc n m) (raise n i)) j)) ∶_)
+        (eq Γ τ′ i j≥n)
+        (Var (le i j≥n))
+  where
+  toℕ-punchIn : ∀ {m} i j → toℕ j ℕ.≤ toℕ (punchIn {m} i j)
+  toℕ-punchIn zero j = n≤1+n (toℕ j)
+  toℕ-punchIn (suc i) zero = z≤n
+  toℕ-punchIn (suc i) (suc j) = s≤s (toℕ-punchIn i j)
+
+  le : ∀ {m n} i {j} → toℕ j ≥ n → toℕ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) ≥ n
+  le {m} {n} i {j} j≥n = begin
+    n ≤⟨ j≥n ⟩
+    toℕ j ≤⟨ toℕ-punchIn (F.cast (+-suc n m) (raise n i)) j ⟩
+    toℕ (punchIn (F.cast _ (raise n i)) j) ≡˘⟨ toℕ-cast (sym (+-suc n m)) (punchIn (F.cast _ (raise n i)) j) ⟩
+    toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ∎
+    where
+    open ≤-Reasoning
+
+  lookup-cast : ∀ {a A n} l j → lookup {a} {A} {n} l (F.cast refl j) ≡ lookup l j
+  lookup-cast l zero = refl
+  lookup-cast (x ∷ l) (suc j) = lookup-cast l j
+
+  toℕ-reduce : ∀ {m n} i i≥m → toℕ (reduce≥ {m} {n} i i≥m) ≡ toℕ i ∸ m
+  toℕ-reduce {zero} i i≥m = refl
+  toℕ-reduce {suc m} (suc i) (s≤s i≥m) = toℕ-reduce i i≥m
+
+  punchIn-∸ : ∀ {m n} i {j} j≥n → toℕ (punchIn (F.cast (+-suc n m) (raise n i)) j) ∸ n ≡ toℕ (punchIn i (reduce≥ j j≥n))
+  punchIn-∸ {zero} {n} zero {j} j≥n = ⊥-elim (<⇒≱ (begin-strict
+    toℕ j ≡˘⟨ toℕ-cast (+-identityʳ n) j ⟩
+    toℕ (F.cast _ j) <⟨ toℕ<n (F.cast _ j) ⟩
+    n ∎) j≥n)
+    where
+    open ≤-Reasoning
+  punchIn-∸ {suc m} {zero} zero {j} z≤n = refl
+  punchIn-∸ {suc m} {suc n} zero {suc j} (s≤s j≥n) = punchIn-∸ zero j≥n
+  punchIn-∸ {suc m} {zero} (suc i) {zero} z≤n = refl
+  punchIn-∸ {suc m} {zero} (suc i) {suc j} z≤n = cong suc (punchIn-∸ i z≤n)
+  punchIn-∸ {suc m} {suc n} (suc i) {suc j} (s≤s j≥n) = punchIn-∸ (suc i) j≥n
+
+  missing-link : ∀ {m n} i {j} j≥n → reduce≥ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) (le i j≥n) ≡ punchIn i (reduce≥ j j≥n)
+  missing-link {n = n} i {j} j≥n = toℕ-injective (begin
+    toℕ (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n)) ≡⟨ toℕ-reduce (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n) ⟩
+    toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ∸ n ≡⟨ cong (_∸ n) (toℕ-cast _ (punchIn (F.cast _ (raise n i)) j)) ⟩
+    toℕ (punchIn (F.cast _ (raise n i)) j) ∸ n ≡⟨ punchIn-∸ i j≥n ⟩
+    toℕ (punchIn i (reduce≥ j j≥n)) ∎)
+    where
+    open ≡-Reasoning
+
+  eq : ∀ {a} {A : Set a} {m n} (Γ : Vec A m) τ′ i {j} j≥n → lookup (insert Γ i τ′) (reduce≥ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) (le i {j} j≥n)) ≡ lookup Γ (reduce≥ j j≥n)
+  eq {n = n} Γ τ′ i {j} j≥n = begin
+    lookup (insert Γ i τ′) (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n)) ≡⟨ cong (lookup (insert Γ i τ′)) (missing-link i j≥n) ⟩
+    lookup (insert Γ i τ′) (punchIn i (reduce≥ j j≥n)) ≡⟨ insert-punchIn Γ i τ′ (reduce≥ j j≥n) ⟩
+    lookup Γ (reduce≥ j j≥n) ∎
+    where
+    open ≡-Reasoning
+
+wkn₁ (Fix Γ,τ∷Δ⊢e∶τ) τ′ i = Fix (wkn₁ Γ,τ∷Δ⊢e∶τ τ′ i)
+wkn₁{m} {n} {Γ} {Δ} (Cat {e₂ = e₂} {τ₂ = τ₂} Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) τ′ i =
+  Cat (wkn₁ Γ,Δ⊢e₁∶τ₁  τ′ i)
+      (subst (λ x → Δ ++ insert Γ i τ′ , [] ⊢ x ∶ τ₂)
+             (begin
+               cast _ (cast _ (wkn e₂ (F.cast refl (raise zero (F.cast _ (raise n i)))))) ≡⟨⟩
+               cast _ (cast _ (wkn e₂ (F.cast refl (F.cast _ (raise n i))))) ≡⟨ cast-involutive (wkn e₂ (F.cast refl (F.cast _ (raise n i)))) refl (sym (+-suc n m)) (sym (+-suc n m)) ⟩
+               cast _ (wkn e₂ (F.cast refl (F.cast _ (raise n i)))) ≡⟨ cong (λ x → cast (sym (+-suc n m)) (wkn e₂ x)) (fcast-involutive (raise n i) (+-suc n m) refl (+-suc n m)) ⟩
+               cast _ (wkn e₂ (F.cast _ (raise n i))) ∎)
+             (cast₁ (eq Γ Δ τ′ i) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ τ′ (F.cast (+-suc n m) (raise n i)))))
+      τ₁⊛τ₂
+  where
+  open ≡-Reasoning
+  eq : ∀ {a A m n} Γ Δ τ′ i → insert (Δ ++ Γ) (F.cast (+-suc n m) (raise n i)) τ′ ≅ Δ ++ insert {a} {A} {m} Γ i τ′
+  eq Γ [] τ′ zero = ≅-refl
+  eq (x ∷ Γ) [] τ′ (suc i) = refl ∷ eq Γ [] τ′ i
+  eq Γ (x ∷ Δ) τ′ i = refl ∷ (eq Γ Δ τ′ i)
+
+  fcast-involutive : ∀ {k m n} i → .(k≡m : k ≡ m) → .(m≡n : m ≡ n) → .(k≡n : k ≡ n) → F.cast m≡n (F.cast k≡m i) ≡ F.cast k≡n i
+  fcast-involutive i k≡m m≡n k≡n = toℕ-injective (begin
+    toℕ (F.cast m≡n (F.cast k≡m i)) ≡⟨ toℕ-cast m≡n (F.cast k≡m i) ⟩
+    toℕ (F.cast k≡m i) ≡⟨ toℕ-cast k≡m i ⟩
+    toℕ i ≡˘⟨ toℕ-cast k≡n i ⟩
+    toℕ (F.cast k≡n i) ∎)
+
+wkn₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) τ′ i = Vee (wkn₁ Γ,Δ⊢e₁∶τ₁ τ′ i) (wkn₁ Γ,Δ⊢e₂∶τ₂ τ′ i) τ₁#τ₂
+
+wkn₂ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
+       Γ , Δ ⊢ e ∶ τ →
+       ∀ τ′ i →
+       Γ , insert Δ i τ′ ⊢ wkn e (inject+ m i) ∶ τ
+wkn₂ Eps τ′ i = Eps
+wkn₂ (Char c) τ′ i = Char c
+wkn₂ Bot τ′ i = Bot
+wkn₂ {m} {n} {Γ} {Δ} (Var {i = j} j≥n) τ′ i =
+  subst (Γ , insert Δ i τ′ ⊢_∶ lookup Γ (reduce≥ j j≥n))
+        (cong Var (toℕ-injective (begin-equality
+          toℕ (suc j) ≡⟨⟩
+          suc (toℕ j) ≡˘⟨ cong toℕ (punchIn-suc i≤j) ⟩
+          toℕ (punchIn (inject+ m i) j) ∎)))
+        (Var (s≤s j≥n))
+  where
+  open ≤-Reasoning
+
+  m<n+1⇒m≤n : ∀ {m n} → m ℕ.< suc n → m ℕ.≤ n
+  m<n+1⇒m≤n (s≤s m≤n) = m≤n
+
+  i≤j : toℕ (inject+ m i) ℕ.≤ toℕ j
+  i≤j = begin
+    toℕ (inject+ m i) ≡˘⟨ toℕ-inject+ m i ⟩
+    toℕ i ≤⟨ m<n+1⇒m≤n (toℕ<n i) ⟩
+    n ≤⟨ j≥n ⟩
+    toℕ j ∎
+
+  punchIn-suc : ∀ {m i j} → toℕ i ℕ.≤ toℕ j → punchIn {m} i j ≡ suc j
+  punchIn-suc {_} {zero} {j} i≤j = refl
+  punchIn-suc {_} {suc i} {suc j} (s≤s i≤j) = cong suc (punchIn-suc i≤j)
+wkn₂ (Fix Γ,τ∷Δ⊢e∶τ) τ′ i = Fix (wkn₂ Γ,τ∷Δ⊢e∶τ τ′ (suc i))
+wkn₂ {m} {n} {Γ} {Δ} (Cat {e₂ = e₂} {τ₂ = τ₂} Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) τ′ i =
+  Cat (wkn₂ Γ,Δ⊢e₁∶τ₁ τ′ i)
+      (subst (insert Δ i τ′ ++ Γ , [] ⊢_∶ τ₂)
+             (begin
+               cast refl (cast refl (wkn e₂ (F.cast refl (inject+ m i)))) ≡⟨ cast-inverse (wkn e₂ (F.cast refl (inject+ m i))) refl refl ⟩
+               wkn e₂ (F.cast refl (inject+ m i)) ≡⟨ cong (wkn e₂) (toℕ-injective (toℕ-cast refl (inject+ m i))) ⟩
+               wkn e₂ (inject+ m i) ∎)
+             (cast₁ (≅-reflexive (eq Γ Δ τ′ i)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ τ′ (inject+ m i))))
+      τ₁⊛τ₂
+  where
+  open ≡-Reasoning
+
+  eq : ∀ {a A m n} Γ Δ τ i → insert (Δ ++ Γ) (inject+ m i) τ ≡ insert {a} {A} {n} Δ i τ ++ Γ
+  eq Γ Δ τ zero = refl
+  eq Γ (_ ∷ Δ) τ (suc i) = cong₂ _∷_ refl (eq Γ Δ τ i)
+wkn₂ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) τ′ i = Vee (wkn₂ Γ,Δ⊢e₁∶τ₁ τ′ i) (wkn₂ Γ,Δ⊢e₂∶τ₂ τ′ i) τ₁#τ₂
-- 
cgit v1.2.3