From 02a0f87be944b1d43fda265058b891f419d25b65 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 16 Mar 2021 18:45:27 +0000
Subject: Change Language definition to respects instead of custom congruence.

---
 src/Cfe/Judgement/Base.agda       |   2 +-
 src/Cfe/Judgement/Properties.agda | 112 ++++++++++++++++++++++++--------------
 2 files changed, 73 insertions(+), 41 deletions(-)

(limited to 'src/Cfe/Judgement')

diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda
index 4623066..754d92d 100644
--- a/src/Cfe/Judgement/Base.agda
+++ b/src/Cfe/Judgement/Base.agda
@@ -28,10 +28,10 @@ data _,_⊢_∶_ : {m : ℕ} → {n : ℕ} → Vec (Type ℓ ℓ) m → Vec (Typ
   Vee : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e₁ e₂ τ₁ τ₂} → Γ , Δ ⊢ e₁ ∶ τ₁ → Γ , Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ , Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂
 
 vcast : ∀ {a A m n} → .(m ≡ n) → Vec {a} A m → Vec A n
+vcast {n = ℕ.zero} eq [] = []
 vcast {n = suc n} eq (x ∷ xs) = x ∷ vcast (suc-injective eq) xs
   where
   open import Data.Nat.Properties using (suc-injective)
-vcast {n = ℕ.zero} eq [] = []
 
 data _≅_ {a A} : {m n : ℕ} → Vec {a} A m → Vec A n → Set a where
   []≅[] : [] ≅ []
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
index 101994b..1c06fcd 100644
--- a/src/Cfe/Judgement/Properties.agda
+++ b/src/Cfe/Judgement/Properties.agda
@@ -13,11 +13,65 @@ 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.Nat.Properties as NP
 open import Data.Vec
 open import Data.Vec.Properties
 open import Function
 open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+private
+  raise-mono : ∀ {m n i j} → i F.≤ j → raise {n} m i F.≤ raise m j
+  raise-mono {zero} i≤j = i≤j
+  raise-mono {suc m} i≤j = s≤s (raise-mono i≤j)
+
+  raise≤ : ∀ {m} n i → n ℕ.≤ toℕ (raise {m} n i)
+  raise≤ zero i = z≤n
+  raise≤ (suc n) i = s≤s (raise≤ n i)
+
+  inject+≤raise : ∀ {m n} i j → inject+ {suc n} m i F.≤ F.cast (+-suc n m) (raise {suc m} n j)
+  inject+≤raise {m} {n} i j = begin
+    toℕ (inject+ m i)          ≡˘⟨ toℕ-inject+ m i ⟩
+    toℕ i                      ≤⟨ NP.<⇒≤pred (toℕ<n i) ⟩
+    n                          ≤⟨ m≤m+n n (toℕ j) ⟩
+    n ℕ.+ toℕ j                ≡˘⟨ toℕ-raise n j ⟩
+    toℕ (raise n j)            ≡˘⟨ toℕ-cast (+-suc n m) (raise n j) ⟩
+    toℕ (F.cast _ (raise n j)) ∎
+    where
+    open ≤-Reasoning
+
+  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)
+
+  toℕ-punchOut : ∀ {m i j} → (i≢j : i ≢ j) → toℕ j ℕ.≤ suc (toℕ (punchOut {m} i≢j))
+  toℕ-punchOut {_} {zero} {zero} i≢j = ⊥-elim (i≢j refl)
+  toℕ-punchOut {_} {zero} {suc j} i≢j = NP.≤-refl
+  toℕ-punchOut {suc m} {suc i} {zero} i≢j = z≤n
+  toℕ-punchOut {suc m} {suc i} {suc j} i≢j = s≤s (toℕ-punchOut (i≢j ∘ cong suc))
+
+  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
+
+  <⇒punchOut≤ : ∀ {m n i j} → n ℕ.< toℕ j → (i≢j : i ≢ j) → n ℕ.≤ toℕ (punchOut {m} i≢j)
+  <⇒punchOut≤ {m} {n} {zero} {suc j} (s≤s n<j) i≢j = n<j
+  <⇒punchOut≤ {suc m} {zero} {suc i} {suc j} (s≤s n<j) i≢j = z≤n
+  <⇒punchOut≤ {suc m} {suc n} {suc i} {suc j} (s≤s n<j) i≢j = s≤s (<⇒punchOut≤ n<j (i≢j ∘ cong suc))
+
+  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
 
 ≅-refl : ∀ {a A m} {xs : Vec {a} A m} → xs ≅ xs
 ≅-refl {xs = []} = []≅[]
@@ -30,6 +84,10 @@ open import Relation.Binary.PropositionalEquality
 ≅-length []≅[] = refl
 ≅-length (_ ∷ xs≅ys) = cong suc (≅-length xs≅ys)
 
+≅-vcast : ∀ {a A m n} {xs : Vec {a} A m} → .(m≡n : m ≡ n) → vcast m≡n xs ≅ xs
+≅-vcast {n = zero} {[]} m≡n = []≅[]
+≅-vcast {n = suc n} {x ∷ xs} m≡n = refl ∷ ≅-vcast (NP.suc-injective m≡n)
+
 ≅⇒≡ : ∀ {a A m n} {xs : Vec {a} A m} {ys : Vec _ n} → (xs≅ys : xs ≅ ys) → vcast (≅-length xs≅ys) xs ≡ ys
 ≅⇒≡ []≅[] = refl
 ≅⇒≡ (x≡y ∷ xs≅ys) = cong₂ _∷_ x≡y (≅⇒≡ xs≅ys)
@@ -69,7 +127,7 @@ cast₁ eq (Fix Γ₁,τ∷Δ⊢e∶τ) = Fix (cast₁ eq Γ₁,τ∷Δ⊢e∶τ
 cast₁ {Δ = Δ} eq (Cat Γ₁,Δ⊢e₁∶τ₁ Δ++Γ₁,∙⊢e₂∶τ₂ τ₁⊛τ₂) = Cat (cast₁ eq Γ₁,Δ⊢e₁∶τ₁) (cast₁ (++ˡ Δ eq) Δ++Γ₁,∙⊢e₂∶τ₂) τ₁⊛τ₂
 cast₁ eq (Vee Γ₁,Δ⊢e₁∶τ₁ Γ₁,Δ⊢e₂∶τ₂ τ₁#τ₂) = Vee (cast₁ eq Γ₁,Δ⊢e₁∶τ₁) (cast₁ eq Γ₁,Δ⊢e₂∶τ₂) τ₁#τ₂
 
-wkn₁ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
+wkn₁ : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e τ} →
        Γ , Δ ⊢ e ∶ τ →
        ∀ τ′ i →
        insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (wkn e (F.cast (+-suc n m) (raise n i))) ∶ τ
@@ -78,16 +136,11 @@ 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))
+        eq
+        (Var le)
   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
+  le : toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ≥ n
+  le  = 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) ⟩
@@ -99,35 +152,18 @@ wkn₁ {m} {n} {Γ} {Δ} {e} {τ} (Var {i = j} j≥n) τ′ i =
   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) ⟩
+  missing-link : reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le ≡ punchIn i (reduce≥ j j≥n)
+  missing-link = toℕ-injective (begin
+    toℕ (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le) ≡⟨ toℕ-reduce (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le ⟩
     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) ⟩
+  eq : lookup (insert Γ i τ′) (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le) ≡ lookup Γ (reduce≥ j j≥n)
+  eq = begin
+    lookup (insert Γ i τ′) (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le) ≡⟨ cong (lookup (insert Γ i τ′)) missing-link ⟩
     lookup (insert Γ i τ′) (punchIn i (reduce≥ j j≥n)) ≡⟨ insert-punchIn Γ i τ′ (reduce≥ j j≥n) ⟩
     lookup Γ (reduce≥ j j≥n) ∎
     where
@@ -157,10 +193,9 @@ wkn₁{m} {n} {Γ} {Δ} (Cat {e₂ = e₂} {τ₂ = τ₂} Γ,Δ⊢e₁∶τ₁
     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 τ} →
+wkn₂ : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e τ} →
        Γ , Δ ⊢ e ∶ τ →
        ∀ τ′ i →
        Γ , insert Δ i τ′ ⊢ wkn e (inject+ m i) ∶ τ
@@ -177,13 +212,10 @@ wkn₂ {m} {n} {Γ} {Δ} (Var {i = j} j≥n) τ′ i =
   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) ⟩
+    toℕ i ≤⟨ NP.<⇒≤pred (toℕ<n i) ⟩
     n ≤⟨ j≥n ⟩
     toℕ j ∎
 
-- 
cgit v1.2.3