diff options
Diffstat (limited to 'src/Cfe/Context/Properties.agda')
| -rw-r--r-- | src/Cfe/Context/Properties.agda | 244 |
1 files changed, 191 insertions, 53 deletions
diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda index b718518..569b72e 100644 --- a/src/Cfe/Context/Properties.agda +++ b/src/Cfe/Context/Properties.agda @@ -6,7 +6,7 @@ module Cfe.Context.Properties {c ℓ} (over : Setoid c ℓ) where -open import Cfe.Context.Base over as C +open import Cfe.Context.Base over open import Cfe.Fin open import Cfe.Type over using () renaming @@ -21,7 +21,7 @@ open import Cfe.Type over using () ; ≤-antisym to ≤ᵗ-antisym ) open import Data.Fin hiding (pred; _≟_) renaming (_≤_ to _≤ᶠ_) -open import Data.Fin.Properties using (toℕ-inject₁; toℕ<n) +open import Data.Fin.Properties using (toℕ<n; toℕ-injective; toℕ-inject₁) renaming ( ≤-refl to ≤ᶠ-refl ; ≤-reflexive to ≤ᶠ-reflexive @@ -29,12 +29,17 @@ open import Data.Fin.Properties using (toℕ-inject₁; toℕ<n) ; ≤-antisym to ≤ᶠ-antisym ) open import Data.Nat renaming (_≤_ to _≤ⁿ_) -open import Data.Nat.Properties using (module ≤-Reasoning) renaming (≤-reflexive to ≤ⁿ-reflexive) +open import Data.Nat.Properties using (<⇒≤pred; pred-mono; module ≤-Reasoning) + renaming + ( ≤-refl to ≤ⁿ-refl + ; ≤-reflexive to ≤ⁿ-reflexive + ; ≤-trans to ≤ⁿ-trans + ) open import Data.Product -open import Data.Vec using ([]; _∷_; Vec; insert) +open import Data.Vec using ([]; _∷_; Vec; insert; remove) open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pw using ([]; _∷_; Pointwise) open import Function -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) +open import Relation.Binary.PropositionalEquality hiding (setoid) open import Relation.Nullary.Decidable using (True; toWitness; fromWitness) private @@ -52,13 +57,22 @@ private pw-antisym antisym (x ∷ xs) (y ∷ ys) = antisym x y ∷ pw-antisym antisym xs ys pw-insert : - ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} {n} {xs : Vec A n} {ys : Vec B n} → + ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} {m n} {xs : Vec A m} {ys : Vec B n} → ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} {x y} → x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (insert xs i x) (insert ys j y) pw-insert zero zero x xs = x ∷ xs pw-insert (suc i) (suc j) {i≡j} x (y ∷ xs) = y ∷ pw-insert i j {i≡j |> toWitness |> cong pred |> fromWitness} x xs + pw-remove : + ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} → + ∀ {m n} {xs : Vec A (suc m)} {ys : Vec B (suc n)} → + ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} → + Pointwise _∼_ xs ys → Pointwise _∼_ (remove xs i) (remove ys j) + pw-remove zero zero (_ ∷ xs) = xs + pw-remove (suc i) (suc j) {i≡j} (x ∷ y ∷ xs) = + x ∷ pw-remove i j {i≡j |> toWitness |> cong pred |> fromWitness} (y ∷ xs) + ------------------------------------------------------------------------ -- Properties of _≈_ ------------------------------------------------------------------------ @@ -142,7 +156,6 @@ setoid {n} = record { isEquivalence = ≈-isEquivalence {n} } ------------------------------------------------------------------------ -- Properties of wkn₂ ------------------------------------------------------------------------ --- Algebraic Properties wkn₂-mono : ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} {τ₁ τ₂} → @@ -150,8 +163,8 @@ wkn₂-mono : wkn₂-mono i j {i≡j} τ₁≤τ₂ (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) = s≤s g₂≤g₁ , pw-insert - (inject<! i) (inject<! j) - {i≡j |> toWitness |> inject<!-cong |> cong toℕ |> fromWitness} + (inject!< i) (inject!< j) + {i≡j |> toWitness |> inject!<-cong |> fromWitness} τ₁≤τ₂ Γ,Δ₁≤Γ,Δ₂ @@ -166,17 +179,22 @@ wkn₂-cong i j {i≡j} τ₁≈τ₂ ctx₁≈ctx₂ = (≤ᵗ-reflexive (≈ᵗ-sym τ₁≈τ₂)) (≤-reflexive (≈-sym ctx₁≈ctx₂))) +wkn₂-cong-≡ : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} {τ₁ τ₂} → + τ₁ ≡ τ₂ → ctx₁ ≡ ctx₂ → wkn₂ {n} ctx₁ i τ₁ ≡ wkn₂ ctx₂ j τ₂ +wkn₂-cong-≡ {ctx₁ = Γ,Δ ⊐ g} i j {i≡j} {τ} refl refl = + i≡j |> toWitness |> inject!<-cong |> toℕ-injective |> cong (λ x → insert Γ,Δ x τ ⊐ suc g) + wkn₂-comm : ∀ ctx i j τ τ′ → - wkn₂ (wkn₂ {n} ctx (inject<!′ {j = suc i} j) τ′) (suc i) τ ≈ wkn₂ (wkn₂ ctx i τ) (inject<′ j) τ′ -wkn₂-comm (Γ,Δ ⊐ g) i zero τ τ′ = ≈-refl + wkn₂ (wkn₂ {n} ctx (inject!<< {j = suc i} j) τ′) (suc i) τ ≡ wkn₂ (wkn₂ ctx i τ) (inject<< j) τ′ +wkn₂-comm (Γ,Δ ⊐ g) i zero τ τ′ = refl wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) τ τ′ = - wkn₂-cong zero zero ≈ᵗ-refl (wkn₂-comm (Γ,Δ ⊐ g) i j τ τ′) + wkn₂-cong-≡ zero zero refl (wkn₂-comm (Γ,Δ ⊐ g) i j τ τ′) ------------------------------------------------------------------------ -- Properties of wkn₁ ------------------------------------------------------------------------ --- Algebraic Properties wkn₁-mono : ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} → @@ -188,15 +206,15 @@ wkn₁-mono {_} {_ ⊐ g₁} {_ ⊐ g₂} i j {i≡j} τ₁≤τ₂ (g₂≤g₁ toℕ g₁ ≡˘⟨ toℕ-inject₁ g₁ ⟩ toℕ (inject₁ g₁) ∎) , pw-insert - (raise> i) (raise> j) - {i≡j |> toWitness |> raise>-cong |> cong toℕ |> fromWitness} + (raise!> i) (raise!> j) + {i≡j |> toWitness |> raise!>-cong |> fromWitness} τ₁≤τ₂ Γ,Δ₁≤Γ,Δ₂ where open ≤-Reasoning wkn₁-cong : - ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} → - ∀ {τ₁ τ₂} → τ₁ ≈ᵗ τ₂ → ctx₁ ≈ ctx₂ → wkn₁ {n} ctx₁ i τ₁ ≈ wkn₁ ctx₂ j τ₂ + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} {τ₁ τ₂} → + τ₁ ≈ᵗ τ₂ → ctx₁ ≈ ctx₂ → wkn₁ {n} ctx₁ i τ₁ ≈ wkn₁ ctx₂ j τ₂ wkn₁-cong i j {i≡j} τ₁≈τ₂ ctx₁≈ctx₂ = ≤-antisym (wkn₁-mono i j {i≡j} (≤ᵗ-reflexive τ₁≈τ₂) (≤-reflexive ctx₁≈ctx₂)) @@ -205,40 +223,38 @@ wkn₁-cong i j {i≡j} τ₁≈τ₂ ctx₁≈ctx₂ = (≤ᵗ-reflexive (≈ᵗ-sym τ₁≈τ₂)) (≤-reflexive (≈-sym ctx₁≈ctx₂))) +wkn₁-cong-≡ : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} {τ₁ τ₂} → + τ₁ ≡ τ₂ → ctx₁ ≡ ctx₂ → wkn₁ {n} ctx₁ i τ₁ ≡ wkn₁ ctx₂ j τ₂ +wkn₁-cong-≡ {ctx₁ = Γ,Δ ⊐ g} i j {i≡j} {τ} refl refl = + i≡j |> toWitness |> raise!>-cong |> toℕ-injective |> cong (λ x → insert Γ,Δ x τ ⊐ inject₁ g) + wkn₁-comm : ∀ ctx i j τ τ′ → - let g = guard ctx in - wkn₁ (wkn₁ {n} ctx (inject>!′ {j = suc> i} j) τ′) (suc> i) τ ≈ wkn₁ (wkn₁ ctx i τ) (inject>′ j) τ′ --- wkn₁-comm = {!!} -wkn₁-comm (Γ,Δ ⊐ zero) zero zero τ τ′ = ≈-refl + wkn₁ (wkn₁ {n} ctx (inject!>< {j = suc> i} j) τ′) (suc> i) τ ≡ wkn₁ (wkn₁ ctx i τ) (inject>< j) τ′ +wkn₁-comm (Γ,Δ ⊐ zero) zero zero τ τ′ = refl wkn₁-comm (Γ,Δ ⊐ zero) (suc i) zero τ τ′ = - wkn₁-cong zero zero ≈ᵗ-refl - (wkn₁-cong (suc> i) (suc i) {toℕ>-suc> i |> fromWitness } ≈ᵗ-refl ≈-refl) + wkn₁-cong-≡ zero zero refl + (wkn₁-cong-≡ (suc> i) (suc i) {toℕ-suc> i |> fromWitness } refl refl) wkn₁-comm (_ ∷ Γ,Δ ⊐ zero) (suc i) (suc j) τ τ′ = - wkn₁-cong zero zero ≈ᵗ-refl (wkn₁-comm (Γ,Δ ⊐ zero) i j τ τ′) + wkn₁-cong-≡ zero zero refl (wkn₁-comm (Γ,Δ ⊐ zero) i j τ τ′) wkn₁-comm (_ ∷ Γ,Δ ⊐ suc g) (inj i) (inj j) τ τ′ = - wkn₂-cong zero zero ≈ᵗ-refl (wkn₁-comm (Γ,Δ ⊐ g) i j τ τ′) + wkn₂-cong-≡ zero zero refl (wkn₁-comm (Γ,Δ ⊐ g) i j τ τ′) wkn₁-wkn₂-comm : ∀ ctx i j τ τ′ → - wkn₁ (wkn₂ {n} ctx j τ′) (inj i) τ ≈ wkn₂ (wkn₁ ctx i τ) (cast<-inject₁ j) τ′ -wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i zero τ τ′ = ≈-refl + wkn₁ (wkn₂ {n} ctx j τ′) (inj i) τ ≡ + wkn₂ (wkn₁ ctx i τ) (cast< (guard ctx |> toℕ-inject₁ |> cong suc |> sym) j) τ′ +wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i zero τ τ′ = refl wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (inj i) (suc j) τ τ′ = - wkn₂-cong zero zero ≈ᵗ-refl (wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i j τ τ′) + wkn₂-cong-≡ zero zero refl (wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i j τ τ′) ------------------------------------------------------------------------ -- Properties of shift ------------------------------------------------------------------------ shift-mono : ∀ {ctx₁ ctx₂ i j} → toℕ< j ≤ⁿ toℕ< i → ctx₁ ≤ ctx₂ → shift {n} ctx₁ i ≤ shift ctx₂ j -shift-mono {i = i} {j} j≤i (_ , Γ,Δ₁≤Γ,Δ₂) = - (begin - toℕ (inject<! j) ≡⟨ toℕ<-inject<! j ⟩ - toℕ< j ≤⟨ j≤i ⟩ - toℕ< i ≡˘⟨ toℕ<-inject<! i ⟩ - toℕ (inject<! i) ∎) , - Γ,Δ₁≤Γ,Δ₂ - where open ≤-Reasoning +shift-mono {i = i} {j} j≤i (_ , Γ,Δ₁≤Γ,Δ₂) = inject!<-mono j≤i , Γ,Δ₁≤Γ,Δ₂ shift-cong : ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} → ctx₁ ≈ ctx₂ → shift {n} ctx₁ i ≈ shift ctx₂ j @@ -247,35 +263,157 @@ shift-cong i j {i≡j} ctx₁≈ctx₂ = (shift-mono (i≡j |> toWitness |> sym |> ≤ⁿ-reflexive) (≤-reflexive ctx₁≈ctx₂)) (shift-mono (i≡j |> toWitness |> ≤ⁿ-reflexive) (≤-reflexive (≈-sym ctx₁≈ctx₂))) -shift-identity : ∀ ctx → shift {n} ctx (strengthen< (guard ctx)) ≈ ctx -shift-identity (Γ,Δ ⊐ zero) = ≈-refl -shift-identity (_ ∷ Γ,Δ ⊐ suc g) = wkn₂-cong zero zero ≈ᵗ-refl (shift-identity (Γ,Δ ⊐ g)) +shift-cong-≡ : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} → ctx₁ ≡ ctx₂ → shift {n} ctx₁ i ≡ shift ctx₂ j +shift-cong-≡ {ctx₁ = Γ,Δ ⊐ _} i j {i≡j} refl = + i≡j |> toWitness |> inject!<-cong |> toℕ-injective |> cong (Γ,Δ ⊐_) -shift-trans : ∀ ctx i j → shift (shift {n} ctx i) (inject<!′-inject! j) ≈ shift {n} ctx (inject<!′ j) -shift-trans (Γ,Δ ⊐ _) _ zero = ≈-refl +shift-identity : ∀ ctx → shift {n} ctx (strengthen< (guard ctx)) ≡ ctx +shift-identity (Γ,Δ ⊐ zero) = refl +shift-identity (_ ∷ Γ,Δ ⊐ suc g) = wkn₂-cong-≡ zero zero refl (shift-identity (Γ,Δ ⊐ g)) + +shift-trans : + ∀ ctx i j → + shift (shift {n} ctx i) (inject!<< (cast<< (strengthen<-inject!< i |> cong suc |> sym) j)) ≡ + shift ctx (inject!<< j) +shift-trans (Γ,Δ ⊐ _) _ zero = refl shift-trans (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) = - wkn₂-cong zero zero ≈ᵗ-refl (shift-trans (Γ,Δ ⊐ g) i j) + wkn₂-cong-≡ zero zero refl (shift-trans (Γ,Δ ⊐ g) i j) shift-wkn₁-comm : ∀ ctx i j τ → - shift (wkn₁ {n} ctx j τ) (cast<-inject₁ i) ≈ wkn₁ (shift ctx i) (cast>-inject<! i j) τ + let i≤g = ≤ⁿ-trans (≤ⁿ-reflexive (toℕ-inject!< i)) (pred-mono (toℕ<<i i)) in + shift (wkn₁ {n} ctx j τ) (cast< (toℕ-inject₁ (guard ctx) |> cong suc |> sym) i) ≡ + wkn₁ (shift ctx i) (cast> (inject₁-mono i≤g) j) τ shift-wkn₁-comm (Γ,Δ ⊐ zero) zero j τ = - wkn₁-cong j (cast>-inject<! zero j) {toℕ>-cast>-inject<! zero j |> fromWitness} ≈ᵗ-refl ≈-refl + wkn₁-cong-≡ j (cast> ≤ⁿ-refl j) {toℕ-cast> ≤ⁿ-refl j |> sym |> fromWitness} refl refl shift-wkn₁-comm (_ ∷ Γ,Δ ⊐ suc g) zero (inj j) τ = - wkn₁-cong zero zero ≈ᵗ-refl (shift-wkn₁-comm (Γ,Δ ⊐ g) zero j τ) + wkn₁-cong-≡ zero zero refl (shift-wkn₁-comm (Γ,Δ ⊐ g) zero j τ) shift-wkn₁-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (inj j) τ = - wkn₂-cong zero zero ≈ᵗ-refl (shift-wkn₁-comm (Γ,Δ ⊐ g) i j τ) + wkn₂-cong-≡ zero zero refl (shift-wkn₁-comm (Γ,Δ ⊐ g) i j τ) shift-wkn₂-comm : ∀ ctx i j τ → - shift (wkn₂ {n} ctx (inject<!′ j) τ) (suc i) ≈ wkn₂ (shift ctx i) (inject<!′-inject! j) τ -shift-wkn₂-comm (Γ,Δ ⊐ g) i zero τ = ≈-refl + shift (wkn₂ {n} ctx (inject!<< j) τ) (suc i) ≡ + wkn₂ (shift ctx i) (inject!<< (cast<< (strengthen<-inject!< i |> cong suc |> sym) j)) τ +shift-wkn₂-comm (Γ,Δ ⊐ g) i zero τ = refl shift-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) τ = - wkn₂-cong zero zero ≈ᵗ-refl (shift-wkn₂-comm (Γ,Δ ⊐ g) i j τ) + wkn₂-cong-≡ zero zero refl (shift-wkn₂-comm (Γ,Δ ⊐ g) i j τ) shift-wkn₁-wkn₂-comm : ∀ ctx i j τ → - shift (wkn₂ {n} ctx i τ) (inject<′ j) ≈ wkn₁ (shift ctx (inject<!′ j)) (reflect i j) τ -shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) zero zero τ = ≈-refl -shift-wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) zero τ = wkn₁-cong zero zero ≈ᵗ-refl (shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i zero τ) -shift-wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) τ = wkn₂-cong zero zero ≈ᵗ-refl (shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i j τ) + shift (wkn₂ {n} ctx i τ) (inject<< j) ≡ wkn₁ (shift ctx (inject!<< j)) (reflect! i j) τ +shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) zero zero τ = refl +shift-wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) zero τ = + wkn₁-cong-≡ zero zero refl (shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i zero τ) +shift-wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) τ = + wkn₂-cong-≡ zero zero refl (shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i j τ) + +------------------------------------------------------------------------ +-- Properties of remove₂ +------------------------------------------------------------------------ + +remove₂-mono : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} → + ctx₁ ≤ ctx₂ → remove₂ {n} ctx₁ i ≤ remove₂ ctx₂ j +remove₂-mono i j {i≡j} (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) = + predⁱ<-mono j i g₂≤g₁ , + pw-remove (inject!< i) (inject!< j) {i≡j |> toWitness |> inject!<-cong |> fromWitness} Γ,Δ₁≤Γ,Δ₂ + +remove₂-cong : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} → + ctx₁ ≈ ctx₂ → remove₂ {n} ctx₁ i ≈ remove₂ ctx₂ j +remove₂-cong i j {i≡j} ctx₁≈ctx₂ = + ≤-antisym + (remove₂-mono i j {i≡j} (≤-reflexive ctx₁≈ctx₂)) + (remove₂-mono j i {i≡j |> toWitness |> sym |> fromWitness} (≤-reflexive (≈-sym ctx₁≈ctx₂))) + +remove₂-cong-≡ : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} → + ctx₁ ≡ ctx₂ → remove₂ {n} ctx₁ i ≡ remove₂ ctx₂ j +remove₂-cong-≡ {ctx₁ = Γ,Δ ⊐ _} i j {i≡j} refl = + i≡j |> toWitness |> λ i≡j → + cong₂ + _⊐_ + (i≡j |> inject!<-cong |> toℕ-injective |> cong (remove Γ,Δ)) + (predⁱ<-cong i j refl |> toℕ-injective) + +remove₂-wkn₂-comm : + ∀ ctx i j τ → + remove₂ (wkn₂ {suc n} ctx (inject<< {j = suc i} j) τ) (suc i) ≡ + wkn₂ (remove₂ ctx i) (cast< (sym (toℕ-predⁱ< i)) (inject!<< j)) τ +remove₂-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) i zero τ = refl +remove₂-wkn₂-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (suc i) (suc zero) τ = refl +remove₂-wkn₂-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (suc i) (suc (suc j)) τ = + wkn₂-cong-≡ zero zero refl (remove₂-wkn₂-comm (τ′ ∷ Γ,Δ ⊐ suc g) i (suc j) τ) + +------------------------------------------------------------------------ +-- Properties of remove₁ +------------------------------------------------------------------------ + +remove₁-mono : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} → + ctx₁ ≤ ctx₂ → remove₁ {n} ctx₁ i ≤ remove₁ ctx₂ j +remove₁-mono i j {i≡j} (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) = + inject₁ⁱ>-mono j i g₂≤g₁ , + pw-remove (raise!> i) (raise!> j) {i≡j |> toWitness |> raise!>-cong |> fromWitness} Γ,Δ₁≤Γ,Δ₂ + +remove₁-cong : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} → + ctx₁ ≈ ctx₂ → remove₁ {n} ctx₁ i ≈ remove₁ ctx₂ j +remove₁-cong i j {i≡j} ctx₁≈ctx₂ = + ≤-antisym + (remove₁-mono i j {i≡j} (≤-reflexive ctx₁≈ctx₂)) + (remove₁-mono j i {i≡j |> toWitness |> sym |> fromWitness} (≤-reflexive (≈-sym ctx₁≈ctx₂))) + +remove₁-cong-≡ : + ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} → + ctx₁ ≡ ctx₂ → remove₁ {n} ctx₁ i ≡ remove₁ ctx₂ j +remove₁-cong-≡ {ctx₁ = Γ,Δ ⊐ _} i j {i≡j} refl = + i≡j |> toWitness |> λ i≡j → + cong₂ + _⊐_ + (i≡j |> raise!>-cong |> toℕ-injective |> cong (remove Γ,Δ)) + (inject₁ⁱ>-cong i j refl |> toℕ-injective) + +remove₁-wkn₂-comm : + ∀ ctx i j τ → + remove₁ (wkn₂ {suc n} ctx j τ) (inj i) ≡ + wkn₂ (remove₁ ctx i) (cast< (toℕ-inject₁ⁱ> i |> cong suc |> sym) j) τ +remove₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ g) _ zero τ = refl +remove₁-wkn₂-comm (_ ∷ _ ∷ Γ,Δ ⊐ suc zero) (inj i) (suc zero) τ = refl +remove₁-wkn₂-comm (_ ∷ _ ∷ Γ,Δ ⊐ suc (suc g)) (inj i) (suc zero) τ = refl +remove₁-wkn₂-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (inj i) (suc (suc j)) τ = + wkn₂-cong-≡ zero zero refl (remove₁-wkn₂-comm ((τ′ ∷ Γ,Δ) ⊐ suc g) i (suc j) τ) + +remove₁-shift-comm : + ∀ ctx i j → + remove₁ (shift ctx i) (cast> (≤ⁿ-trans (≤ⁿ-reflexive (toℕ-inject!< i)) (<⇒≤pred (toℕ<<i i))) j) ≡ + shift (remove₁ {n} ctx j) (cast< (toℕ-inject₁ⁱ> j |> cong suc |> sym) i) +remove₁-shift-comm (Γ,Δ ⊐ g) zero zero = refl +remove₁-shift-comm (Γ,Δ ⊐ g) zero (suc j) = + toℕ-cast> z≤n j |> raise!>-cong |> toℕ-injective |> cong ((_⊐ zero) ∘ remove Γ,Δ ∘ suc) +remove₁-shift-comm (Γ,Δ ⊐ g) zero (inj j) = + toℕ-cast> z≤n j |> raise!>-cong |> toℕ-injective |> cong ((_⊐ zero) ∘ remove Γ,Δ ∘ suc) +remove₁-shift-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc zero) (suc i) (inj j) = + wkn₂-cong-≡ zero zero refl (remove₁-shift-comm (τ′ ∷ Γ,Δ ⊐ zero) i j) +remove₁-shift-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (suc i) (inj j) = + wkn₂-cong-≡ zero zero refl (remove₁-shift-comm (τ′ ∷ Γ,Δ ⊐ suc g) i j) + +-- remove₁ (shift ctx zero) (reflect i zero) ≡ shift (remove ctx i) zero +remove₁-remove₂-shift-comm : + ∀ ctx i j → + let eq = inject-square j |> cong toℕ |> sym |> ≤ⁿ-reflexive in + remove₁ (shift {suc n} ctx (inject<< j)) (cast> eq (reflect i j)) ≡ + shift (remove₂ ctx i) (cast< (sym (toℕ-predⁱ< i)) (inject!<< j)) +remove₁-remove₂-shift-comm (Γ,Δ ⊐ suc g) zero zero = refl +remove₁-remove₂-shift-comm (Γ,Δ ⊐ suc (suc g)) (suc i) zero = + cong ((_⊐ zero) ∘ remove Γ,Δ ∘ suc) (toℕ-injective (begin + toℕ (raise!> (cast> _ (reflect i zero))) ≡⟨ toℕ-raise!> (cast> _ (reflect i zero)) ⟩ + toℕ> (cast> _ (reflect i zero)) ≡⟨ toℕ-cast> z≤n (reflect i zero) ⟩ + toℕ> (reflect i zero) ≡⟨ toℕ-reflect i zero ⟩ + toℕ< i ≡˘⟨ toℕ-inject!< i ⟩ + toℕ (inject!< i) ∎)) + where open ≡-Reasoning +remove₁-remove₂-shift-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (suc i) (suc j) = + wkn₂-cong-≡ zero zero refl (remove₁-remove₂-shift-comm (τ′ ∷ Γ,Δ ⊐ suc g) i j) |