diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Cfe/Context/Base.agda | 113 | ||||
| -rw-r--r-- | src/Cfe/Context/Properties.agda | 224 | ||||
| -rw-r--r-- | src/Cfe/Judgement/Base.agda | 2 | ||||
| -rw-r--r-- | src/Cfe/Judgement/Properties.agda | 223 |
4 files changed, 262 insertions, 300 deletions
diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda index 1a37aa0..6b34a67 100644 --- a/src/Cfe/Context/Base.agda +++ b/src/Cfe/Context/Base.agda @@ -18,36 +18,34 @@ open import Level renaming (suc to lsuc) open import Relation.Binary.PropositionalEquality open import Relation.Nullary -≤-recomputable : ∀ {m n} → .(m ℕ.≤ n) → m ℕ.≤ n -≤-recomputable {ℕ.zero} {n} m≤n = z≤n -≤-recomputable {suc m} {suc n} m≤n = s≤s (≤-recomputable (pred-mono m≤n)) +drop′ : ∀ {a A n m i} → m ℕ.≤ n → i ℕ.≤ m → Vec {a} A (m ℕ.+ (n ∸ m)) → Vec A (n ∸ i) +drop′ z≤n z≤n xs = xs +drop′ (s≤s m≤n) z≤n (x ∷ xs) = x ∷ drop′ m≤n z≤n xs +drop′ (s≤s m≤n) (s≤s i≤m) (x ∷ xs) = drop′ m≤n i≤m xs -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 +take′ : ∀ {a A m i} → i ℕ.≤ m → Vec {a} A m → Vec A i +take′ z≤n xs = [] +take′ (s≤s i≤m) (x ∷ xs) = x ∷ (take′ i≤m 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≥′ : ∀ {n m i} → m ℕ.≤ n → toℕ {n} i ≥ m → Fin (n ∸ m) +reduce≥′ {i = i} z≤n i≥m = i +reduce≥′ {i = suc i} (s≤s m≤n) (s≤s i≥m) = reduce≥′ m≤n i≥m -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) (s≤s i≥m) (s≤s i≤j) = reduce≥′-mono (pred-mono m≤n) i j i≥m i≤j +reduce≥′-mono : ∀ {n m i j} → (m≤n : m ℕ.≤ n) → (i≥m : toℕ i ≥ m) → (i≤j : i F.≤ j) → reduce≥′ m≤n i≥m F.≤ reduce≥′ m≤n (≤-trans i≥m i≤j) +reduce≥′-mono z≤n i≥m i≤j = i≤j +reduce≥′-mono {i = suc i} {suc j} (s≤s m≤n) (s≤s i≥m) (s≤s i≤j) = reduce≥′-mono m≤n i≥m i≤j -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) -insert′ {a} {A} {ℕ.zero} xs m≤n m≢0 i x = ⊥-elim (m≢0 refl) -insert′ {a} {A} {suc ℕ.zero} xs _ _ F.zero x = x ∷ xs -insert′ {a} {A} {suc ℕ.zero} (y ∷ xs) _ _ (suc i) x = y ∷ insert′ xs (s≤s z≤n) (λ ()) i x -insert′ {a} {A} {suc (suc m)} {suc ℕ.zero} xs m≤n _ i x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable m≤n)) -insert′ {a} {A} {suc (suc m)} {suc (suc _)} xs m≤n _ i x = insert′ {m = suc m} xs (pred-mono m≤n) (λ ()) i x +insert′ : ∀ {a A n m} → Vec {a} A (n ∸ suc m) → suc m ℕ.≤ n → Fin (n ∸ m) → A → Vec A (n ∸ m) +insert′ xs (s≤s z≤n) i x = insert xs i x +insert′ xs (s≤s (s≤s m≤n)) i x = insert′ xs (s≤s m≤n) i x -rotate : ∀ {a A n} → (i j : Fin n) → .(i F.≤ j) → Vec {a} A n → Vec A n -rotate F.zero j i≤j (x ∷ xs) = insert xs j x -rotate (suc i) (suc j) i≤j (x ∷ xs) = x ∷ (rotate i j (pred-mono i≤j) xs) +rotate : ∀ {a A n} {i j : Fin n} → Vec {a} A n → i F.≤ j → Vec A n +rotate {i = F.zero} {j} (x ∷ xs) z≤n = insert xs j x +rotate {i = suc i} {suc j} (x ∷ xs) (s≤s i≤j) = x ∷ (rotate xs 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 -remove′ (x ∷ y ∷ xs) m≢0 (suc i) = x ∷ remove′ (y ∷ xs) (λ ()) i +remove′ : ∀ {a A n} → Vec {a} A n → Fin n → Vec A (ℕ.pred n) +remove′ (x ∷ xs) F.zero = xs +remove′ (x ∷ y ∷ xs) (suc i) = x ∷ remove′ (y ∷ xs) i record Context n : Set (c ⊔ lsuc ℓ) where field @@ -56,17 +54,17 @@ 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₁ Γ,Δ i i≥m τ = record +wkn₁ : ∀ {n i} → (Γ,Δ : Context n) → toℕ {suc n} i ≥ Context.m Γ,Δ → Type ℓ ℓ → Context (suc n) +wkn₁ Γ,Δ i≥m τ = record { m≤n = ≤-step m≤n - ; Γ = cast (sym (+-∸-assoc 1 m≤n)) (insert Γ (F.cast (+-∸-assoc 1 m≤n) (reduce≥′ (≤-step m≤n) i i≥m)) τ) + ; Γ = insert′ Γ (s≤s m≤n) (reduce≥′ (≤-step m≤n) 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₂ : ∀ {n i} → (Γ,Δ : Context n) → toℕ {suc n} i ℕ.≤ Context.m Γ,Δ → Type ℓ ℓ → Context (suc n) +wkn₂ Γ,Δ i≤m τ = record { m≤n = s≤s m≤n ; Γ = Γ ; Δ = insert Δ (fromℕ< (s≤s i≤m)) τ @@ -74,61 +72,18 @@ wkn₂ Γ,Δ i i≤m τ = record where open Context Γ,Δ -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) Γ - ; Δ = Δ +shift≤ : ∀ {n i} (Γ,Δ : Context n) → i ℕ.≤ Context.m Γ,Δ → Context n +shift≤ {n} {i} record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤m = record + { m≤n = ≤-trans i≤m m≤n + ; Γ = drop′ m≤n i≤m (Δ ++ Γ) + ; Δ = take′ i≤m Δ } - where - open Context Γ,Δ - -rotate₂ : ∀ {n} → (Γ,Δ : Context n) → (i j : Fin n) → (toℕ j ℕ.< Context.m Γ,Δ) → (i F.≤ j) → Context n -rotate₂ {n} Γ,Δ i j j<m i≤j = record - { m≤n = m≤n - ; Γ = Γ - ; Δ = rotate - (fromℕ< (≤-trans (s≤s i≤j) j<m)) - (fromℕ< j<m) - (begin - toℕ (fromℕ< (≤-trans (s≤s i≤j) j<m)) ≡⟨ toℕ-fromℕ< (≤-trans (s≤s i≤j) j<m) ⟩ - toℕ i ≤⟨ i≤j ⟩ - toℕ j ≡˘⟨ toℕ-fromℕ< j<m ⟩ - toℕ (fromℕ< j<m) ∎) - Δ - } - where - open Context Γ,Δ - open ≤-Reasoning - -transfer : ∀ {n} → (Γ,Δ : Context n) → (i j : Fin n) → (toℕ i ℕ.< Context.m Γ,Δ) → (suc (toℕ j) ≥ Context.m Γ,Δ) → Context n -transfer {n} Γ,Δ i j i<m 1+j≥m with Context.m Γ,Δ ℕ.≟ 0 -... | yes m≡0 = ⊥-elim (m<n⇒n≢0 i<m m≡0) -... | no m≢0 = record - { m≤n = pred-mono (≤-step m≤n) - ; Γ = insert′ Γ m≤n m≢0 (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m)) (lookup Δ (fromℕ< i<m)) - ; Δ = remove′ Δ m≢0 (fromℕ< i<m) - } - where - open Context Γ,Δ cons : ∀ {n} → Context n → Type ℓ ℓ → Context (suc n) -cons {n} Γ,Δ τ = record - { m≤n = s≤s m≤n - ; Γ = Γ - ; Δ = τ ∷ Δ - } - where - open Context Γ,Δ +cons Γ,Δ τ = wkn₂ Γ,Δ z≤n τ shift : ∀ {n} → Context n → Context n -shift {n} Γ,Δ = record - { m≤n = z≤n - ; Γ = cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (Δ ++ Γ) - ; Δ = [] - } - where - open Context Γ,Δ +shift Γ,Δ = shift≤ Γ,Δ z≤n _≋_ : ∀ {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 230c18b..11441a7 100644 --- a/src/Cfe/Context/Properties.agda +++ b/src/Cfe/Context/Properties.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary using (Setoid; Symmetric) +open import Relation.Binary using (Setoid; Symmetric; Transitive) module Cfe.Context.Properties {c ℓ} (over : Setoid c ℓ) @@ -20,102 +20,138 @@ 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) +≋-trans : ∀ {n} → Transitive (_≋_ {n}) +≋-trans (refl , refl , refl) (refl , refl , refl) = refl , refl , refl -cast-insert : ∀ {a A m n} xs .(m≡n : _) i j .(_ : toℕ i ≡ toℕ j) y → C.cast {a} {A} {suc m} {suc n} (cong suc m≡n) (insert xs i y) ≡ insert (C.cast m≡n xs) j y -cast-insert [] m≡n zero zero _ y = refl -cast-insert (x ∷ xs) m≡n zero zero _ y = refl -cast-insert {m = suc _} {n = suc _} (x ∷ xs) m≡n (suc i) (suc j) i≡j y = cong (x ∷_) (cast-insert xs (cong ℕ.pred m≡n) i j (cong ℕ.pred i≡j) 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 +shift≤-wkn₁-comm : ∀ {n i j} Γ,Δ i≤m j≥m τ → + shift≤ {i = i} (wkn₁ {n} {j} Γ,Δ j≥m τ) i≤m ≋ + wkn₁ (shift≤ Γ,Δ i≤m) (≤-trans i≤m j≥m) τ +shift≤-wkn₁-comm record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤m j≥m τ = + refl , eq Γ Δ m≤n i≤m j≥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 + eq : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤m : i ℕ.≤ m) (j≥m : toℕ {suc n} j ≥ m) y → + drop′ {a} {A} (≤-step m≤n) i≤m (ys ++ (insert′ xs (s≤s m≤n) (reduce≥′ (≤-step m≤n) j≥m) y)) ≡ + insert′ (drop′ m≤n i≤m (ys ++ xs)) (s≤s (≤-trans i≤m m≤n)) (reduce≥′ (≤-step (≤-trans i≤m m≤n)) (≤-trans i≤m j≥m)) y + eq _ [] z≤n z≤n _ _ = refl + eq {j = suc _} xs (x ∷ ys) (s≤s m≤n) z≤n (s≤s j≥m) y = cong (x ∷_) (eq xs ys m≤n z≤n j≥m y) + eq {j = suc _} xs (_ ∷ ys) (s≤s m≤n) (s≤s i≤m) (s≤s j≥m) y = eq xs ys m≤n i≤m j≥m y + +shift≤-wkn₂-comm-≤ : ∀ {n i j} Γ,Δ i≤j j≤m τ → + shift≤ {i = i} (wkn₂ {n} {j} Γ,Δ j≤m τ) (≤-trans i≤j (≤-step j≤m)) ≋ + wkn₁ (shift≤ Γ,Δ (≤-trans i≤j j≤m)) i≤j τ +shift≤-wkn₂-comm-≤ record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤j j≤m τ = + refl , eq₁ Γ Δ m≤n i≤j j≤m τ , eq₂ Δ i≤j j≤m τ 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) - -rotate₁-shift : ∀ {n} (Γ,Δ : Context n) i j i≥m i≤j → rotate₁ (shift Γ,Δ) i j z≤n i≤j ≋ shift (rotate₁ Γ,Δ i j i≥m i≤j) -rotate₁-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i≥m i≤j = - refl , - eq Γ Δ m≤n i j i≥m i≤j , - refl + eq₁ : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤j : i ℕ.≤ toℕ {suc n} j) (j≤m : toℕ j ℕ.≤ m) y → + drop′ {a} {A} (s≤s m≤n) (≤-trans i≤j (≤-step j≤m)) (insert ys (fromℕ< (s≤s j≤m)) y ++ xs) ≡ + insert′ + (drop′ m≤n (≤-trans i≤j j≤m) (ys ++ xs)) + (s≤s (≤-trans (≤-trans i≤j j≤m) m≤n)) + (reduce≥′ (≤-step (≤-trans (≤-trans i≤j j≤m) m≤n)) i≤j) + y + eq₁ {j = zero} _ _ _ z≤n _ _ = refl + eq₁ {j = suc j} xs (x ∷ ys) (s≤s m≤n) z≤n (s≤s j≤m) y = cong (x ∷_) (eq₁ xs ys m≤n z≤n j≤m y) + eq₁ {j = suc j} xs (x ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) y = eq₁ xs ys m≤n i≤j j≤m y + + eq₂ : ∀ {a A n m i j} ys (i≤j : i ℕ.≤ toℕ {suc n} j) (j≤m : toℕ j ℕ.≤ m) y → + take′ {a} {A} (≤-trans i≤j (≤-step j≤m)) (insert ys (fromℕ< (s≤s j≤m)) y) ≡ + take′ (≤-trans i≤j j≤m) ys + eq₂ {j = zero} _ z≤n _ _ = refl + eq₂ {j = suc _} _ z≤n _ _ = refl + eq₂ {j = suc zero} (_ ∷ _) (s≤s z≤n) (s≤s _) _ = refl + eq₂ {j = suc (suc _)} (x ∷ ys) (s≤s i≤j) (s≤s j≤m) y = cong (x ∷_) (eq₂ ys i≤j j≤m y) + +shift≤-wkn₂-comm-> : ∀ {n i j} Γ,Δ i≤j j≤m τ → + shift≤ {i = suc j} (wkn₂ {n} {i} Γ,Δ (≤-trans i≤j j≤m) τ) (s≤s j≤m) ≋ + wkn₂ (shift≤ Γ,Δ j≤m) i≤j τ +shift≤-wkn₂-comm-> record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤j j≤m τ = refl , eq₁ Γ Δ m≤n i≤j j≤m τ , eq₂ Δ m≤n i≤j j≤m τ where - eq : ∀ {a A m n} xs ys .(m≤n : m ℕ.≤ n) i j i≥m i≤j → - rotate {a} {A} i j i≤j (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ xs)) ≡ - C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ 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) xs) - eq {m = zero} {suc _} (x ∷ xs) [] _ zero j _ _ = sym (cast-insert xs refl j j refl x) - eq {m = zero} (x ∷ xs) [] _ (suc i) (suc j) _ i≤j = cong (x ∷_) (eq xs [] z≤n i j z≤n (pred-mono i≤j)) - eq {m = suc _} {suc _} xs (y ∷ ys) m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = cong (y ∷_) (eq xs ys (pred-mono m≤n) i j i≥m i≤j) - -transfer-cons : ∀ {n} (Γ,Δ : Context n) i j i<m 1+j≥m τ → transfer (cons Γ,Δ τ) (suc i) (suc j) (s≤s i<m) (s≤s 1+j≥m) ≋ cons (transfer Γ,Δ i j i<m 1+j≥m) τ -transfer-cons record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i<m 1+j≥m τ = - refl , eq₁ Γ Δ m≤n (fromℕ< i<m) j 1+j≥m τ , eq₂ Δ (fromℕ< i<m) τ + eq₁ : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤j : toℕ {suc n} i ℕ.≤ j) (j≤m : j ℕ.≤ m) y → + drop′ {a} {A} (s≤s m≤n) (s≤s j≤m) (insert ys (fromℕ< (s≤s (≤-trans i≤j j≤m))) y ++ xs) ≡ + drop′ m≤n j≤m (ys ++ xs) + eq₁ {i = zero} _ _ _ _ _ _ = refl + eq₁ {i = suc _} xs (_ ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) y = eq₁ xs ys m≤n i≤j j≤m y + + eq₂ : ∀ {a A n m i j} ys (m≤n : m ℕ.≤ n) (i≤j : toℕ {suc n} i ℕ.≤ j) (j≤m : j ℕ.≤ m) y → + take′ {a} {A} (s≤s j≤m) (insert ys (fromℕ< (s≤s (≤-trans i≤j j≤m))) y) ≡ + insert (take′ j≤m ys) (fromℕ< (s≤s i≤j)) y + eq₂ {i = zero} _ _ _ _ _ = refl + eq₂ {i = suc _} (x ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) y = cong (x ∷_) (eq₂ ys m≤n i≤j j≤m y) + +shift≤-identity : ∀ {n} Γ,Δ → shift≤ {n} Γ,Δ ≤-refl ≋ Γ,Δ +shift≤-identity record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } = refl , eq₁ Γ Δ m≤n , eq₂ Δ where - eq₁ : ∀ {a A m n} xs ys .(m≤n : suc m ℕ.≤ n) (i : Fin (suc m)) j .(1+j≥m : _) y → - insert′ {a} {A} xs (s≤s m≤n) (λ ()) (reduce≥′ (≤-step m≤n) (suc j) 1+j≥m) (lookup (y ∷ ys) (suc i)) ≡ - insert′ xs m≤n (λ ()) (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m)) (lookup ys i) - eq₁ {m = zero} {suc _} xs ys m≤n i j 1+j≥m y = refl - eq₁ {m = suc m} xs ys m≤n i zero 1+j≥m x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m)) - eq₁ {m = suc m} {suc _} xs (x ∷ ys) m≤n i (suc j) 1+j≥m y = refl - - eq₂ : ∀ {a A m} ys (i : Fin (suc m)) y → - remove′ {a} {A} (y ∷ ys) (λ ()) (suc i) ≡ y ∷ remove′ ys (λ ()) i - eq₂ (x ∷ ys) i y = refl - -transfer-shift : ∀ {n} (Γ,Δ : Context n) i j i<m 1+j≥m → rotate₁ (shift Γ,Δ) i j z≤n (pred-mono (≤-trans i<m 1+j≥m)) ≋ shift (transfer Γ,Δ i j i<m 1+j≥m) -transfer-shift record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i<m 1+j≥m = - refl , - eq Γ Δ m≤n i j i<m 1+j≥m , - refl + eq₁ : ∀ {a A n m} xs ys (m≤n : m ℕ.≤ n) → drop′ {a} {A} m≤n ≤-refl (ys ++ xs) ≡ xs + eq₁ xs [] z≤n = refl + eq₁ xs (_ ∷ ys) (s≤s m≤n) = eq₁ xs ys m≤n + + eq₂ : ∀ {a A m} ys → take′ {a} {A} {m} ≤-refl ys ≡ ys + eq₂ [] = refl + eq₂ (x ∷ ys) = cong (x ∷_) (eq₂ ys) + +shift≤-idem : ∀ {n i j} Γ,Δ i≤j j≤m → shift≤ {n} {i} (shift≤ {i = j} Γ,Δ j≤m) i≤j ≋ shift≤ Γ,Δ (≤-trans i≤j j≤m) +shift≤-idem record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤j j≤m = refl , eq₁ Γ Δ m≤n i≤j j≤m , eq₂ Δ i≤j j≤m where - eq : ∀ {a A m n} xs ys .(m≤n : suc m ℕ.≤ n) i j i<m .(1+j≥m : _) → - rotate {a} {A} i j - (pred-mono {_} {suc (toℕ j)} (≤-trans i<m 1+j≥m)) - (C.cast (trans (sym (+-∸-assoc (suc m) m≤n)) (m+n∸m≡n (suc m) n)) (ys ++ xs)) ≡ - C.cast - (trans (sym (+-∸-assoc m (pred-mono (≤-step m≤n)))) (m+n∸m≡n (suc m) n)) - ( remove′ ys (λ ()) (fromℕ< i<m) ++ - insert′ xs m≤n (λ ()) - (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m)) - (lookup ys (fromℕ< i<m))) - eq {m = zero} {suc _} xs (y ∷ []) m≤n zero zero i<m 1+j≥m = refl - eq {m = zero} {suc (suc _)} (x ∷ xs) (y ∷ []) _ zero (suc j) _ _ = cong (x ∷_) (eq xs (y ∷ []) (s≤s z≤n) zero j (s≤s z≤n) (s≤s z≤n)) - eq {m = zero} {suc _} _ (_ ∷ []) _ (suc _) _ (s≤s ()) _ - eq {m = suc _} {suc _} _ (_ ∷ _) _ _ zero _ 1+j≥m = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m)) - eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n zero (suc j) i<m 1+j≥m = cong (y ∷_) (eq xs (x ∷ ys) (pred-mono m≤n) zero j (s≤s z≤n) (pred-mono 1+j≥m)) - eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n (suc i) (suc j) (s≤s i<m) 1+j≥m = cong (x ∷_) (eq xs (y ∷ ys) (pred-mono m≤n) i j i<m (pred-mono 1+j≥m)) + eq₁ : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤j : i ℕ.≤ j) (j≤m : j ℕ.≤ m) → + drop′ {a} {A} (≤-trans j≤m m≤n) i≤j (take′ j≤m ys ++ drop′ m≤n j≤m (ys ++ xs)) ≡ + drop′ m≤n (≤-trans i≤j j≤m) (ys ++ xs) + eq₁ _ _ _ z≤n z≤n = refl + eq₁ xs (y ∷ ys) (s≤s m≤n) z≤n (s≤s j≤m) = cong (y ∷_) (eq₁ xs ys m≤n z≤n j≤m) + eq₁ xs (_ ∷ ys) (s≤s m≤n) (s≤s i≤j) (s≤s j≤m) = eq₁ xs ys m≤n i≤j j≤m + + eq₂ : ∀ {a A m i j} ys (i≤j : i ℕ.≤ j) (j≤m : j ℕ.≤ m) → take′ {a} {A} i≤j (take′ j≤m ys) ≡ take′ (≤-trans i≤j j≤m) ys + eq₂ ys z≤n j≤m = refl + eq₂ (y ∷ ys) (s≤s i≤j) (s≤s j≤m) = cong (y ∷_) (eq₂ ys i≤j j≤m) + +-- rotate₁-shift : ∀ {n i j} Γ,Δ i≥m i≤j → rotate₁ {n} {i} {j} (shift Γ,Δ) z≤n i≤j ≋ shift (rotate₁ Γ,Δ i≥m i≤j) +-- rotate₁-shift record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≥m i≤j = +-- refl , +-- eq Γ Δ m≤n i≥m i≤j , +-- refl +-- where +-- eq : ∀ {a A m n i j} xs ys (m≤n : m ℕ.≤ n) i≥m i≤j → ? +-- -- rotate {a} {A} i j i≤j (C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ xs)) ≡ +-- -- C.cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (ys ++ 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) xs) +-- eq xs ys m≤n i≥m i≤j = ? +-- -- eq {m = zero} {suc _} (x ∷ xs) [] _ zero j _ _ = sym (cast-insert xs refl j j refl x) +-- -- eq {m = zero} (x ∷ xs) [] _ (suc i) (suc j) _ i≤j = cong (x ∷_) (eq xs [] z≤n i j z≤n (pred-mono i≤j)) +-- -- eq {m = suc _} {suc _} xs (y ∷ ys) m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = cong (y ∷_) (eq xs ys (pred-mono m≤n) i j i≥m i≤j) + +-- transfer-cons : ∀ {n i j} Γ,Δ i<m 1+j≥m τ → transfer {suc n} {suc i} {suc j} (cons Γ,Δ τ) (s≤s i<m) 1+j≥m ≋ cons (transfer Γ,Δ i<m (pred-mono 1+j≥m)) τ +-- transfer-cons record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i<m 1+j≥m τ = +-- refl , eq₁ Γ Δ m≤n (fromℕ< i<m) 1+j≥m τ , eq₂ Δ (fromℕ< i<m) τ +-- where +-- eq₁ : ∀ {a A m n j} xs ys (m≤n : suc m ℕ.≤ n) i 1+j≥m y → ? ≡ ? +-- -- insert′ {a} {A} xs (s≤s m≤n) (reduce≥′ (≤-step m≤n) 1+j≥m) (lookup (y ∷ ys) (suc i)) ≡ +-- -- insert′ xs m≤n (reduce≥′ (pred-mono (≤-step m≤n)) (pred-mono 1+j≥m)) (lookup ys i) +-- eq₁ xs ys m≤n i 1+j≥m y = ? +-- -- eq₁ {m = zero} {suc _} xs ys m≤n i j 1+j≥m y = refl +-- -- eq₁ {m = suc m} xs ys m≤n i zero 1+j≥m x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m)) +-- -- eq₁ {m = suc m} {suc _} xs (x ∷ ys) m≤n i (suc j) 1+j≥m y = refl + +-- eq₂ : ∀ {a A m} ys (i : Fin (suc m)) y → +-- remove′ {a} {A} (y ∷ ys) (suc i) ≡ y ∷ remove′ ys i +-- eq₂ (x ∷ ys) i y = refl + +-- transfer-shift : ∀ {n i j} (Γ,Δ : Context n) i j i<m 1+j≥m → rotate₁ (shift Γ,Δ) z≤n (pred-mono (≤-trans i<m 1+j≥m)) ≋ shift (transfer Γ,Δ i j i<m 1+j≥m) +-- transfer-shift record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i j i<m 1+j≥m = +-- refl , +-- eq Γ Δ m≤n i j i<m 1+j≥m , +-- refl +-- where +-- eq : ∀ {a A m n} xs ys .(m≤n : suc m ℕ.≤ n) i j i<m .(1+j≥m : _) → +-- rotate {a} {A} i j +-- (pred-mono {_} {suc (toℕ j)} (≤-trans i<m 1+j≥m)) +-- (C.cast (trans (sym (+-∸-assoc (suc m) m≤n)) (m+n∸m≡n (suc m) n)) (ys ++ xs)) ≡ +-- C.cast +-- (trans (sym (+-∸-assoc m (pred-mono (≤-step m≤n)))) (m+n∸m≡n (suc m) n)) +-- ( remove′ ys (λ ()) (fromℕ< i<m) ++ +-- insert′ xs m≤n (λ ()) +-- (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m)) +-- (lookup ys (fromℕ< i<m))) +-- eq {m = zero} {suc _} xs (y ∷ []) m≤n zero zero i<m 1+j≥m = refl +-- eq {m = zero} {suc (suc _)} (x ∷ xs) (y ∷ []) _ zero (suc j) _ _ = cong (x ∷_) (eq xs (y ∷ []) (s≤s z≤n) zero j (s≤s z≤n) (s≤s z≤n)) +-- eq {m = zero} {suc _} _ (_ ∷ []) _ (suc _) _ (s≤s ()) _ +-- eq {m = suc _} {suc _} _ (_ ∷ _) _ _ zero _ 1+j≥m = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m)) +-- eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n zero (suc j) i<m 1+j≥m = cong (y ∷_) (eq xs (x ∷ ys) (pred-mono m≤n) zero j (s≤s z≤n) (pred-mono 1+j≥m)) +-- eq {m = suc _} {suc (suc _)} xs (x ∷ y ∷ ys) m≤n (suc i) (suc j) (s≤s i<m) 1+j≥m = cong (x ∷_) (eq xs (y ∷ ys) (pred-mono m≤n) i j i<m (pred-mono 1+j≥m)) diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda index 0e5417a..4be0256 100644 --- a/src/Cfe/Judgement/Base.agda +++ b/src/Cfe/Judgement/Base.agda @@ -21,7 +21,7 @@ data _⊢_∶_ : {n : ℕ} → Context n → Expression n → Type ℓ ℓ → S Eps : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ε ∶ Lift ℓ ℓ τε 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) + Var : ∀ {n} {Γ,Δ : Context n} {i} (i≥m : toℕ i ≥ _) → Γ,Δ ⊢ Var i ∶ lookup (Context.Γ Γ,Δ) (reduce≥′ (Context.m≤n Γ,Δ) i≥m) 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 053ab73..1e79a81 100644 --- a/src/Cfe/Judgement/Properties.agda +++ b/src/Cfe/Judgement/Properties.agda @@ -6,19 +6,14 @@ module Cfe.Judgement.Properties {c ℓ} (over : Setoid c ℓ) where -open import Cfe.Context over - renaming - ( wkn₁ to cwkn₁ - ; wkn₂ to cwkn₂ - ; rotate to crotate - ; rotate₁ to crotate₁ - ; transfer to ctransfer - ; _≋_ to _≋ᶜ_ - ) -open import Cfe.Expression over +open import Cfe.Context over as C + hiding + ( shift≤ ; wkn₁ ; wkn₂ ) + renaming (_≋_ to _≋ᶜ_; ≋-sym to ≋ᶜ-sym; ≋-trans to ≋ᶜ-trans ) +open import Cfe.Expression over as E open import Cfe.Judgement.Base over open import Data.Empty -open import Data.Fin as F +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.Properties @@ -29,10 +24,19 @@ open import Function open import Relation.Binary.PropositionalEquality open import Relation.Nullary -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) +private + 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) + + punchIn[i,j]≥m : ∀ {n m i j} → toℕ i ℕ.≤ m → toℕ j ≥ m → toℕ (punchIn {n} i j) ≥ suc m + punchIn[i,j]≥m {i = zero} i≤m j≥m = s≤s j≥m + punchIn[i,j]≥m {i = suc i} {suc j} (s≤s i≤m) (s≤s j≥m) = s≤s (punchIn[i,j]≥m i≤m j≥m) + + punchOut≥m : ∀ {n m i j} → (i≢j : i ≢ j) → toℕ {suc n} i ≥ m → toℕ j ≥ m → toℕ (punchOut i≢j) ≥ m + punchOut≥m {m = zero} _ z≤n _ = z≤n + punchOut≥m {n = suc _} {.(suc _)} {suc _} {suc _} i≢j (s≤s i≥m) (s≤s j≥m) = s≤s (punchOut≥m (i≢j ∘ cong suc) i≥m j≥m) congᶜ : ∀ {n} {Γ,Δ Γ,Δ′ : Context n} {e τ} → Γ,Δ ≋ᶜ Γ,Δ′ → Γ,Δ ⊢ e ∶ τ → Γ,Δ′ ⊢ e ∶ τ congᶜ {Γ,Δ = Γ,Δ} {Γ,Δ′} (refl , refl , refl) Γ,Δ⊢e∶τ with ≤-irrelevant (Context.m≤n Γ,Δ) (Context.m≤n Γ,Δ′) @@ -41,121 +45,88 @@ congᶜ {Γ,Δ = Γ,Δ} {Γ,Δ′} (refl , refl , refl) Γ,Δ⊢e∶τ with ≤- 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))) +wkn₁ : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ {i} i≥m τ′ → C.wkn₁ {i = i} Γ,Δ i≥m τ′ ⊢ wkn e i ∶ τ +wkn₁ Eps i≥m τ′ = Eps +wkn₁ (Char c) i≥m τ′ = Char c +wkn₁ Bot i≥m τ′ = Bot +wkn₁ {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} (Var {i = j} j≥m) {i = i} i≥m τ′ = + congᵗ (τ≡τ′ Γ m≤n 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) τ₁#τ₂ + τ≡τ′ : ∀ {a A n m i j} xs (m≤n : m ℕ.≤ n) (i≥m : toℕ i ≥ _) j≥m x → + lookup {a} {A} + (insert′ xs (s≤s m≤n) (reduce≥′ (≤-step m≤n) i≥m) x) + (reduce≥′ (≤-step m≤n) (≤-trans j≥m (toℕ-punchIn i j))) ≡ + lookup xs (reduce≥′ m≤n j≥m) + τ≡τ′ {i = zero} {j} (y ∷ xs) z≤n z≤n z≤n x = refl + τ≡τ′ {i = suc i} {zero} (y ∷ xs) z≤n z≤n z≤n x = refl + τ≡τ′ {i = suc i} {suc j} (y ∷ xs) z≤n z≤n z≤n x = τ≡τ′ {i = i} xs z≤n z≤n z≤n x + τ≡τ′ {i = suc i} {suc j} xs (s≤s m≤n) (s≤s i≥m) (s≤s j≥m) x = τ≡τ′ xs m≤n i≥m j≥m x +wkn₁ (Fix Γ,Δ⊢e∶τ) i≥m τ′ = Fix (wkn₁ Γ,Δ⊢e∶τ (s≤s i≥m) τ′) +wkn₁ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i≥m τ′ = Cat (wkn₁ Γ,Δ⊢e₁∶τ₁ i≥m τ′) (congᶜ (≋ᶜ-sym (shift≤-wkn₁-comm Γ,Δ z≤n i≥m τ′)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ z≤n τ′)) τ₁⊛τ₂ +wkn₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i≥m τ′ = Vee (wkn₁ Γ,Δ⊢e₁∶τ₁ i≥m τ′) (wkn₁ Γ,Δ⊢e₂∶τ₂ 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)) +wkn₂ : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ {i} i≤m τ′ → C.wkn₂ {i = i} Γ,Δ i≤m τ′ ⊢ wkn e i ∶ τ +wkn₂ Eps i≤m τ′ = Eps +wkn₂ (Char c) i≤m τ′ = Char c +wkn₂ Bot i≤m τ′ = Bot +wkn₂ {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }}(Var {i = j} j≥m) i≤m τ′ = congᵗ (τ≡τ′ Γ m≤n i≤m j≥m) (Var (punchIn[i,j]≥m 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 n m i j} xs (m≤n : m ℕ.≤ n) (i≤m : toℕ i ℕ.≤ _) (j≥m : toℕ j ≥ _) → + lookup {a} {A} xs (reduce≥′ (s≤s m≤n) (punchIn[i,j]≥m i≤m j≥m)) ≡ + lookup xs (reduce≥′ m≤n j≥m) + τ≡τ′ {i = zero} _ z≤n _ _ = refl + τ≡τ′ {i = zero} _ (s≤s _) _ _ = refl + τ≡τ′ {i = suc i} {suc j} xs (s≤s m≤n) (s≤s i≤m) (s≤s j≥m) = τ≡τ′ xs m≤n i≤m j≥m +wkn₂ (Fix Γ,Δ⊢e∶τ) i≤m τ′ = Fix (wkn₂ Γ,Δ⊢e∶τ (s≤s i≤m) τ′) +wkn₂ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i≤m τ′ = Cat (wkn₂ Γ,Δ⊢e₁∶τ₁ i≤m τ′) (congᶜ (≋ᶜ-sym (shift≤-wkn₂-comm-≤ Γ,Δ z≤n i≤m τ′)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ z≤n τ′)) τ₁⊛τ₂ +wkn₂ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i≤m τ′ = Vee (wkn₂ Γ,Δ⊢e₁∶τ₁ i≤m τ′) (wkn₂ Γ,Δ⊢e₂∶τ₂ i≤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) τ₁#τ₂ - -rotate₁ : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ i j i≥m i≤j → crotate₁ Γ,Δ i j i≥m i≤j ⊢ rotate e i j i≤j ∶ τ -rotate₁ Eps i j i≥m i≤j = Eps -rotate₁ (Char c) i j i≥m i≤j = Char c -rotate₁ Bot i j i≥m i≤j = Bot -rotate₁ {suc n} {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} (Var {i = k} k≥m) i j i≥m i≤j with i F.≟ k -... | yes refl = congᵗ (τ≡τ′ Γ m≤n i j i≥m i≤j) (Var (≤-trans i≥m i≤j)) - where - τ≡τ′ : ∀ {a A m n} xs m≤n i j i≥m i≤j → lookup {a} {A} (crotate (reduce≥′ {m} {n} m≤n i i≥m) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) (reduce≥′-mono m≤n i j i≥m i≤j) xs) (reduce≥′ m≤n j (≤-trans i≥m i≤j)) ≡ lookup xs (reduce≥′ m≤n i i≥m) - τ≡τ′ {m = zero} (x ∷ xs) m≤n zero j i≥m i≤j = insert-lookup xs j x - τ≡τ′ {m = zero} (x ∷ xs) m≤n (suc i) (suc j) i≥m i≤j = τ≡τ′ xs z≤n i j z≤n (pred-mono i≤j) - τ≡τ′ {m = suc m} {suc n} xs m≤n (suc i) (suc j) (s≤s i≥m) (s≤s i≤j) = τ≡τ′ xs (pred-mono m≤n) i j i≥m i≤j -... | no i≢k = congᵗ (τ≡τ′ Γ m≤n i j k i≢k i≥m i≤j k≥m) (Var (punchIn-punchOut≥m i j k i≢k i≥m i≤j k≥m)) +shift≤ : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ {i} (i≤m : i ℕ.≤ _) → C.shift≤ Γ,Δ i≤m ⊢ e ∶ τ +shift≤ Eps i≤m = Eps +shift≤ (Char c) i≤m = Char c +shift≤ Bot i≤m = Bot +shift≤ {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} (Var {i = j} j≥m) i≤m = + congᵗ (τ≡τ′ Γ Δ m≤n i≤m j≥m) (Var (≤-trans i≤m j≥m)) where - punchIn-punchOut≥m : ∀ {m n} (i j k : Fin (suc n)) (i≢k : i ≢ k) → toℕ i ≥ m → i F.≤ j → toℕ k ≥ m → toℕ (punchIn j (punchOut i≢k)) ≥ m - punchIn-punchOut≥m {zero} _ _ _ _ _ _ _ = z≤n - punchIn-punchOut≥m {suc _} zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl) - punchIn-punchOut≥m {suc _} zero zero (suc _) _ _ _ k≥m = k≥m - punchIn-punchOut≥m {suc _} {suc _} (suc i) (suc j) (suc k) i≢k (s≤s i≥m) (s≤s i≤j) (s≤s k≥m) = s≤s (punchIn-punchOut≥m i j k (i≢k ∘ cong suc) i≥m i≤j k≥m) + τ≡τ′ : ∀ {a A n m i j} xs ys (m≤n : m ℕ.≤ n) (i≤m : i ℕ.≤ m) (j≥m : toℕ j ≥ m) → + lookup {a} {A} (drop′ m≤n i≤m (ys ++ xs)) (reduce≥′ (≤-trans i≤m m≤n) (≤-trans i≤m j≥m)) ≡ + lookup xs (reduce≥′ m≤n j≥m) + τ≡τ′ xs [] z≤n z≤n z≤n = refl + τ≡τ′ {j = suc j} xs (x ∷ ys) (s≤s m≤n) z≤n (s≤s j≥m) = τ≡τ′ xs ys m≤n z≤n j≥m + τ≡τ′ {j = suc j} xs (x ∷ ys) (s≤s m≤n) (s≤s i≤m) (s≤s j≥m) = τ≡τ′ xs ys m≤n i≤m j≥m +shift≤ {Γ,Δ = Γ,Δ} {τ = τ} (Fix Γ,Δ⊢e∶τ) {i} i≤m = Fix (congᶜ (shift≤-wkn₂-comm-> Γ,Δ z≤n i≤m τ) (shift≤ Γ,Δ⊢e∶τ (s≤s i≤m))) +shift≤ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i≤m = + Cat (shift≤ Γ,Δ⊢e₁∶τ₁ i≤m) + (congᶜ (≋ᶜ-trans (shift≤-identity (shift Γ,Δ)) + (≋ᶜ-sym (shift≤-idem Γ,Δ z≤n i≤m))) + (shift≤ Δ++Γ,∙⊢e₂∶τ₂ z≤n)) + τ₁⊛τ₂ +shift≤ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i≤m = Vee (shift≤ Γ,Δ⊢e₁∶τ₁ i≤m) (shift≤ Γ,Δ⊢e₂∶τ₂ i≤m) τ₁#τ₂ - τ≡τ′ : ∀ {a A m n} xs m≤n i j k i≢k i≥m i≤j k≥m → - lookup {a} {A} - (crotate - (reduce≥′ {m} {suc n} m≤n i i≥m) - (reduce≥′ m≤n j (≤-trans i≥m i≤j)) - (reduce≥′-mono m≤n i j i≥m i≤j) xs) - (reduce≥′ - m≤n - (punchIn j (punchOut i≢k)) - (punchIn-punchOut≥m i j k i≢k i≥m i≤j k≥m)) ≡ - lookup xs (reduce≥′ m≤n k k≥m) - τ≡τ′ {m = zero} _ _ zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl) - τ≡τ′ {m = zero} (_ ∷ _) _ zero zero (suc _) _ _ _ _ = refl - τ≡τ′ {m = zero} (_ ∷ _ ∷ _) _ zero (suc _) (suc zero) _ _ _ _ = refl - τ≡τ′ {m = zero} (x ∷ _ ∷ xs) _ zero (suc j) (suc (suc k)) _ _ _ _ = τ≡τ′ (x ∷ xs) z≤n zero j (suc k) (λ ()) z≤n z≤n z≤n - τ≡τ′ {m = zero} (_ ∷ _ ∷ _) _ (suc _) (suc _) zero _ _ _ _ = refl - τ≡τ′ {m = zero} (_ ∷ x ∷ xs) _ (suc i) (suc j) (suc k) i≢k _ i≤j _ = τ≡τ′ (x ∷ xs) z≤n i j k (i≢k ∘ cong suc) z≤n (pred-mono i≤j) z≤n - τ≡τ′ {m = suc m} {suc _} xs m≤n (suc i) (suc j) (suc k) i≢k i≥m i≤j k≥m = τ≡τ′ xs (pred-mono m≤n) i j k (i≢k ∘ cong suc) (pred-mono i≥m) (pred-mono i≤j) (pred-mono k≥m) -rotate₁ (Fix Γ,Δ⊢e∶τ) i j i≥m i≤j = Fix (rotate₁ Γ,Δ⊢e∶τ (suc i) (suc j) (s≤s i≥m) (s≤s i≤j)) -rotate₁ {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i j i≥m i≤j = Cat (rotate₁ Γ,Δ⊢e₁∶τ₁ i j i≥m i≤j) (congᶜ (rotate₁-shift Γ,Δ i j i≥m i≤j) (rotate₁ Δ++Γ,∙⊢e₂∶τ₂ i j z≤n i≤j)) τ₁⊛τ₂ -rotate₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i j i≥m i≤j = Vee (rotate₁ Γ,Δ⊢e₁∶τ₁ i j i≥m i≤j) (rotate₁ Γ,Δ⊢e₂∶τ₂ i j i≥m i≤j) τ₁#τ₂ - -transfer : ∀ {n} {Γ,Δ : Context n} {e τ} → Γ,Δ ⊢ e ∶ τ → ∀ i j i<m 1+j≥m → ctransfer Γ,Δ i j i<m 1+j≥m ⊢ rotate e i j (pred-mono (≤-trans i<m 1+j≥m)) ∶ τ -transfer Eps i j i<m 1+j≥m = Eps -transfer (Char c) i j i<m 1+j≥m = Char c -transfer Bot i j i<m 1+j≥m = Bot -transfer {suc n} {Γ,Δ = record { m = suc m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} (Var {i = k} k≥m) i j i<m 1+j≥m with suc m ℕ.≟ 0 | i F.≟ k -... | no m≢0 | yes refl = ⊥-elim (<⇒≱ i<m k≥m) -... | no m≢0 | no i≢k = congᵗ (τ≡τ′ Γ (lookup Δ (fromℕ< i<m)) m≢0 m≤n i j k i<m 1+j≥m k≥m i≢k) (Var (punchIn≥m i j k i≢k i<m 1+j≥m k≥m)) +subst₁ : ∀ {n} {Γ,Δ : Context n} {e τ i τ′} (i≥m : toℕ i ≥ _) → C.wkn₁ Γ,Δ i≥m τ′ ⊢ e ∶ τ → ∀ {e′} → Γ,Δ ⊢ e′ ∶ τ′ → Γ,Δ ⊢ e [ e′ / i ] ∶ τ +subst₁ _ Eps Γ,Δ⊢e′∶τ′ = Eps +subst₁ _ (Char c) Γ,Δ⊢e′∶τ′ = Char c +subst₁ _ Bot Γ,Δ⊢e′∶τ′ = Bot +subst₁ {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} {i = i} {τ′} i≥m (Var {i = j} j≥m) Γ,Δ⊢e′∶τ′ with i F.≟ j +... | no i≢j = + congᵗ (sym (τ≡τ′ Γ m≤n i≢j i≥m j≥m τ′)) (Var (punchOut≥m i≢j i≥m j≥m)) where - punchIn≥m : ∀ {m n} (i j k : Fin (suc n)) (i≢k : i ≢ k) → toℕ i ℕ.< m → .(suc (toℕ j) ≥ m) → toℕ k ≥ m → toℕ (punchIn j (punchOut i≢k)) ≥ ℕ.pred m - punchIn≥m {suc zero} _ _ _ _ _ _ _ = z≤n - punchIn≥m {suc (suc _)} zero _ zero i≢k _ _ _ = ⊥-elim (i≢k refl) - punchIn≥m {suc (suc _)} zero zero (suc _) _ _ _ (s≤s k≥m) = ≤-step k≥m - punchIn≥m {suc (suc _)} {suc _} (suc i) zero (suc k) i≢k (s≤s i<m) 1+j≥m (s≤s k≥m) = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m)) - punchIn≥m {suc (suc _)} zero (suc _) (suc zero) _ _ _ (s≤s k≥m) = k≥m - punchIn≥m {suc (suc _)} zero (suc j) (suc (suc k)) _ _ 1+j≥m (s≤s k≥m) = s≤s (punchIn≥m zero j (suc k) (λ ()) (s≤s z≤n) (pred-mono 1+j≥m) k≥m) - punchIn≥m {suc (suc _)} {suc _} (suc i) (suc j) (suc k) i≢k (s≤s i<m) 1+j≥m (s≤s k≥m) = s≤s (punchIn≥m i j k (i≢k ∘ cong suc) i<m (pred-mono 1+j≥m) k≥m) - - τ≡τ′ : ∀ {a A m n} xs y m≢0 .(m≤n : _) i j k i<m .(1+j≥m : _) k≥m i≢k → - lookup - (insert′ {a} {A} {m} {suc n} xs m≤n m≢0 - (reduce≥′ (pred-mono (≤-step m≤n)) j (pred-mono 1+j≥m)) - y) - (reduce≥′ - (pred-mono (≤-step m≤n)) - (punchIn j (punchOut i≢k)) - (punchIn≥m i j k i≢k i<m 1+j≥m k≥m)) ≡ - lookup xs (reduce≥′ m≤n k k≥m) - τ≡τ′ {m = suc zero} _ _ _ _ zero zero (suc _) _ _ (s≤s z≤n) _ = refl - τ≡τ′ {m = suc zero} _ _ _ _ (suc _) zero (suc _) (s≤s ()) _ _ _ - τ≡τ′ {m = suc zero} (_ ∷ _) _ _ _ zero (suc _) (suc zero) _ _ (s≤s z≤n) _ = refl - τ≡τ′ {m = suc zero} (_ ∷ xs) y _ _ zero (suc j) (suc (suc k)) _ _ (s≤s z≤n) _ = τ≡τ′ xs y (λ ()) (s≤s (z≤n)) zero j (suc k) (s≤s z≤n) (s≤s z≤n) (s≤s z≤n) (λ ()) - τ≡τ′ {m = suc (suc _)} _ _ _ _ _ zero _ _ 1+j≥m _ _ = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) (≤-recomputable 1+j≥m)) - τ≡τ′ {m = suc (suc _)} _ _ _ _ zero _ (suc zero) _ _ (s≤s ()) _ - τ≡τ′ {m = suc (suc _)} {suc (suc _)} xs y _ m≤n zero (suc j) (suc (suc k)) _ 1+j≥m (s≤s k≥m) _ = τ≡τ′ xs y (λ ()) (pred-mono m≤n) zero j (suc k) (s≤s z≤n) (pred-mono 1+j≥m) k≥m (λ ()) - τ≡τ′ {m = suc (suc m)} xs y m≢0 m≤n (suc i) (suc j) (suc zero) (s≤s i<m) 1+j≥m (s≤s k≥m) i≢k = τ≡τ′ xs y (λ ()) (pred-mono m≤n) i j zero i<m (pred-mono 1+j≥m) k≥m (i≢k ∘ cong suc) - τ≡τ′ {m = suc (suc m)} xs y m≢0 m≤n (suc i) (suc j) (suc (suc k)) (s≤s i<m) 1+j≥m (s≤s k≥m) i≢k = τ≡τ′ xs y (λ ()) (pred-mono m≤n) i j (suc k) i<m (pred-mono 1+j≥m) k≥m (i≢k ∘ cong suc) -transfer {Γ,Δ = Γ,Δ} {τ = τ} (Fix Γ,Δ⊢e∶τ) i j i<m 1+j≥m = Fix (congᶜ (transfer-cons Γ,Δ i j i<m 1+j≥m τ) (transfer Γ,Δ⊢e∶τ (suc i) (suc j) (s≤s i<m) (s≤s 1+j≥m))) -transfer {Γ,Δ = Γ,Δ} (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) i j i<m 1+j≥m = Cat (transfer Γ,Δ⊢e₁∶τ₁ i j i<m 1+j≥m) (congᶜ (transfer-shift Γ,Δ i j i<m 1+j≥m) (rotate₁ Δ++Γ,∙⊢e₂∶τ₂ i j z≤n (pred-mono (≤-trans i<m 1+j≥m)))) τ₁⊛τ₂ -transfer (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) i j i<m 1+j≥m = Vee (transfer Γ,Δ⊢e₁∶τ₁ i j i<m 1+j≥m) (transfer Γ,Δ⊢e₂∶τ₂ i j i<m 1+j≥m) τ₁#τ₂ + τ≡τ′ : ∀ {a A n m i j} xs (m≤n : m ℕ.≤ n) (i≢j : i ≢ j) (i≥m : toℕ i ≥ m) (j≥m : toℕ j ≥ m) x → + lookup {a} {A} (insert′ xs (s≤s m≤n) (reduce≥′ (≤-step m≤n) i≥m) x) (reduce≥′ (≤-step m≤n) j≥m) ≡ + lookup xs (reduce≥′ m≤n (punchOut≥m i≢j i≥m j≥m)) + τ≡τ′ {i = zero} {zero} xs m≤n i≢j i≥m j≥m x = ⊥-elim (i≢j refl) + τ≡τ′ {n = suc n} {i = zero} {suc j} xs z≤n i≢j z≤n z≤n x = refl + τ≡τ′ {n = suc n} {i = suc i} {zero} (y ∷ xs) z≤n i≢j z≤n z≤n x = refl + τ≡τ′ {n = suc n} {i = suc i} {suc j} (y ∷ xs) z≤n i≢j z≤n z≤n x = τ≡τ′ xs z≤n (i≢j ∘ cong suc) z≤n z≤n x + τ≡τ′ {n = suc n} {i = suc i} {suc j} xs (s≤s m≤n) i≢j (s≤s i≥m) (s≤s j≥m) x = τ≡τ′ xs m≤n (i≢j ∘ cong suc) i≥m j≥m x +... | yes refl with ≤-irrelevant i≥m j≥m +... | refl = congᵗ (sym (τ≡τ′ Γ m≤n i≥m τ′)) Γ,Δ⊢e′∶τ′ + where + τ≡τ′ : ∀ {a A n m i} xs (m≤n : m ℕ.≤ n) (i≥m : toℕ i ≥ m) x → + lookup {a} {A} (insert′ xs (s≤s m≤n) (reduce≥′ (≤-step m≤n) i≥m) x) (reduce≥′ (≤-step m≤n) i≥m) ≡ x + τ≡τ′ {i = zero} xs z≤n z≤n x = refl + τ≡τ′ {i = suc i} (y ∷ xs) z≤n z≤n x = insert-lookup xs i x + τ≡τ′ {i = suc i} xs (s≤s m≤n) (s≤s i≥m) = τ≡τ′ xs m≤n i≥m +subst₁ {τ = τ} i≥m (Fix Γ,Δ⊢e∶τ) Γ,Δ⊢e′∶τ′ = Fix (subst₁ (s≤s i≥m) Γ,Δ⊢e∶τ (wkn₂ Γ,Δ⊢e′∶τ′ z≤n τ)) +subst₁ {Γ,Δ = Γ,Δ} {i = i} {τ′} i≥m (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) Γ,Δ⊢e′∶τ′ = Cat (subst₁ i≥m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′) (subst₁ z≤n (congᶜ (shift≤-wkn₁-comm Γ,Δ z≤n i≥m τ′) Δ++Γ,∙⊢e₂∶τ₂) (shift≤ Γ,Δ⊢e′∶τ′ z≤n)) τ₁⊛τ₂ +subst₁ i≥m (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) Γ,Δ⊢e′∶τ′ = Vee (subst₁ i≥m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′) (subst₁ i≥m Γ,Δ⊢e₂∶τ₂ Γ,Δ⊢e′∶τ′) τ₁#τ₂ |