Prove substitution into guarded variable.

2 files changed, 75 insertions, 83 deletions

diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda
index 11441a7..b3037b2 100644
--- a/src/Cfe/Context/Properties.agda
+++ b/src/Cfe/Context/Properties.agda
@@ -23,6 +23,44 @@ open import Relation.Binary.PropositionalEquality
 ≋-trans : ∀ {n} → Transitive (_≋_ {n})
 ≋-trans (refl , refl , refl) (refl , refl , refl) = refl , refl , refl
 
+i≤j⇒inject₁[i]≤1+j : ∀ {n i j} → i F.≤ j → inject₁ {n} i F.≤ suc j
+i≤j⇒inject₁[i]≤1+j {i = zero} i≤j = z≤n
+i≤j⇒inject₁[i]≤1+j {i = suc i} {suc j} (s≤s i≤j) = s≤s (i≤j⇒inject₁[i]≤1+j i≤j)
+
+wkn₂-comm : ∀ {n i j} Γ,Δ i≤j j≤m τ₁ τ₂ → wkn₂ (wkn₂ {n} {i} Γ,Δ (≤-trans i≤j j≤m) τ₁) (s≤s j≤m) τ₂ ≋ wkn₂ (wkn₂ {i = j} Γ,Δ j≤m τ₂) (≤-trans (i≤j⇒inject₁[i]≤1+j i≤j) (s≤s j≤m)) τ₁
+wkn₂-comm record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤j j≤m τ₁ τ₂ = refl , refl , eq Δ i≤j j≤m τ₁ τ₂
+  where
+  eq : ∀ {a A n m i j} ys (i≤j : i F.≤ j) (j≤m : toℕ {n} j ℕ.≤ m) y₁ y₂ →
+       insert {a} {A} (insert ys (fromℕ< (s≤s (≤-trans i≤j j≤m))) y₁) (fromℕ< (s≤s (s≤s j≤m))) y₂ ≡
+       insert (insert ys (fromℕ< (s≤s j≤m)) y₂) (fromℕ< (s≤s (≤-trans (i≤j⇒inject₁[i]≤1+j i≤j) (s≤s j≤m)))) y₁
+  eq {i = zero} _ _ _ _ _ = refl
+  eq {i = suc i} {j = suc j} (x ∷ ys) (s≤s i≤j) (s≤s j≤m) y₁ y₂ = cong (x ∷_) (eq ys i≤j j≤m y₁ 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 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 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)
+
 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) τ
@@ -77,81 +115,3 @@ shift≤-wkn₂-comm-> record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤
         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 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 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/Properties.agda b/src/Cfe/Judgement/Properties.agda
index 1e79a81..ab4fda9 100644
--- a/src/Cfe/Judgement/Properties.agda
+++ b/src/Cfe/Judgement/Properties.agda
@@ -21,7 +21,7 @@ open import Data.Product
 open import Data.Vec
 open import Data.Vec.Properties
 open import Function
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality hiding (subst₂)
 open import Relation.Nullary
 
 private
@@ -34,10 +34,6 @@ private
   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 Γ,Δ′)
 ... | refl = Γ,Δ⊢e∶τ
@@ -111,6 +107,10 @@ subst₁ {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} {i = i}
 ... | no i≢j =
   congᵗ (sym (τ≡τ′ Γ m≤n i≢j i≥m j≥m τ′)) (Var (punchOut≥m i≢j i≥m j≥m))
   where
+  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)
+
   τ≡τ′ : ∀ {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))
@@ -130,3 +130,35 @@ subst₁ {Γ,Δ = record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ }} {i = i}
 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′∶τ′) τ₁#τ₂
+
+
+subst₂ : ∀ {n} {Γ,Δ : Context n} {e τ i τ′} (i≤m : toℕ i ℕ.≤ _) → C.wkn₂ Γ,Δ i≤m τ′ ⊢ e ∶ τ → ∀ {e′} → shift Γ,Δ ⊢ e′ ∶ τ′ → Γ,Δ ⊢ e [ e′ / i ] ∶ τ
+subst₂ i≤m Eps Γ,Δ⊢e′∶τ′ = Eps
+subst₂ i≤m (Char c) Γ,Δ⊢e′∶τ′ = Char c
+subst₂ i≤m 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
+... | yes refl = ⊥-elim (<⇒≱ j>m i≤m)
+... | no i≢j = congᵗ (cong (lookup Γ) (τ≡τ′ m≤n i≢j i≤m j>m)) (Var (punchOut≥m i≢j i≤m j>m))
+  where
+  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} i≢j i≤m j>m = z≤n
+  punchOut≥m {m = suc _} {zero} {suc _} _ _ (s≤s j>m) = j>m
+  punchOut≥m {n = suc _} {i = suc _} {suc _} i≢j (s≤s i≤m) (s≤s j>m) = s≤s (punchOut≥m (i≢j ∘ cong suc) i≤m j>m)
+
+  τ≡τ′ : ∀ {n m i j} (m≤n : m ℕ.≤ n) (i≢j : i ≢ j) (i≤m : toℕ i ℕ.≤ m) (j>m : toℕ j > m) →
+    reduce≥′ m≤n (punchOut≥m i≢j i≤m j>m) ≡ reduce≥′ (s≤s m≤n) j>m
+  τ≡τ′ {m = zero} {zero} {suc _} m≤n i≢j z≤n (s≤s z≤n) = refl
+  τ≡τ′ {m = suc _} {zero} {suc _} m≤n i≢j z≤n (s≤s j>m) = refl
+  τ≡τ′ {n = suc _} {i = suc _} {suc _} (s≤s m≤n) i≢j (s≤s i≤m) (s≤s j>m) = τ≡τ′ m≤n (i≢j ∘ cong suc) i≤m j>m
+
+subst₂ {Γ,Δ = Γ,Δ} {τ = τ} {τ′ = τ′} i≤m (Fix Γ,Δ⊢e∶τ) Γ,Δ⊢e′∶τ′ =
+  Fix (subst₂ (s≤s i≤m)
+              (congᶜ (≋ᶜ-sym (wkn₂-comm Γ,Δ z≤n i≤m τ τ′)) Γ,Δ⊢e∶τ)
+              (congᶜ (≋ᶜ-sym (shift≤-wkn₂-comm-≤ Γ,Δ z≤n z≤n τ)) (wkn₁ Γ,Δ⊢e′∶τ′ z≤n τ)))
+subst₂ {Γ,Δ = Γ,Δ} {τ′ = τ′} i≤m (Cat Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) Γ,Δ⊢e′∶τ′ =
+  Cat (subst₂ i≤m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′)
+      (subst₁ z≤n
+              (congᶜ (shift≤-wkn₂-comm-≤ Γ,Δ z≤n i≤m τ′) Δ++Γ,∙⊢e₂∶τ₂)
+              Γ,Δ⊢e′∶τ′)
+      τ₁⊛τ₂
+subst₂ i≤m (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) Γ,Δ⊢e′∶τ′ = Vee (subst₂ i≤m Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e′∶τ′) (subst₂ i≤m Γ,Δ⊢e₂∶τ₂ Γ,Δ⊢e′∶τ′) τ₁#τ₂