diff options
Diffstat (limited to 'src/Cfe/Context')
| -rw-r--r-- | src/Cfe/Context/Base.agda | 36 | ||||
| -rw-r--r-- | src/Cfe/Context/Properties.agda | 59 |
2 files changed, 80 insertions, 15 deletions
diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda index dcd8056..6b7a9dc 100644 --- a/src/Cfe/Context/Base.agda +++ b/src/Cfe/Context/Base.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary using (Setoid) +open import Relation.Binary using (Setoid; Rel) module Cfe.Context.Base {c ℓ} (over : Setoid c ℓ) @@ -8,18 +8,23 @@ module Cfe.Context.Base open import Cfe.Type over open import Data.Empty -open import Data.Fin as F +open import Data.Fin as F hiding (cast) open import Data.Fin.Properties hiding (≤-trans) open import Data.Nat as ℕ hiding (_⊔_) open import Data.Nat.Properties +open import Data.Product open import Data.Vec open import Level renaming (suc to lsuc) open import Relation.Binary.PropositionalEquality open import Relation.Nullary -reduce≥′ : ∀ {m n} → .(m ℕ.≤ n) → (i : Fin n) → .(toℕ i ≥ m) → Fin (n ∸ m) +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 + +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≥′ {suc m} {suc n} m≤n (suc i) (s≤s i≥m) = reduce≥′ (pred-mono m≤n) i i≥m private 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) @@ -29,9 +34,9 @@ private insert′ {a} {A} {suc (suc m)} {suc ℕ.zero} xs m≤n _ i x = ⊥-elim (<⇒≱ (s≤s (s≤s z≤n)) m≤n) insert′ {a} {A} {suc (suc m)} {suc (suc n)} xs m≤n _ i x = insert′ {m = suc m} xs (pred-mono m≤n) (λ ()) i x - 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 : ∀ {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) i≥m i≤j = reduce≥′-mono (pred-mono m≤n) i j (pred-mono i≥m) (pred-mono 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 remove′ : ∀ {a A m} → Vec {a} A m → .(m ≢ 0) → Fin m → Vec A (ℕ.pred m) remove′ (x ∷ xs) m≢0 F.zero = xs @@ -48,25 +53,25 @@ 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₁ : ∀ {n} → (Γ,Δ : Context n) → (i : Fin (suc n)) → (toℕ i ≥ Context.m Γ,Δ) → Type ℓ ℓ → Context (suc n) wkn₁ Γ,Δ i i≥m τ = record { m≤n = ≤-step m≤n - ; Γ = subst (Vec (Type ℓ ℓ)) (sym (+-∸-assoc 1 m≤n)) (insert Γ (F.cast (+-∸-assoc 1 m≤n) (reduce≥′ (≤-step m≤n) i i≥m)) τ) + ; Γ = cast (sym (+-∸-assoc 1 m≤n)) (insert Γ (F.cast (+-∸-assoc 1 m≤n) (reduce≥′ (≤-step m≤n) i 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₂ Γ,Δ i i≤m τ = record { m≤n = s≤s m≤n ; Γ = Γ - ; Δ = insert Δ (fromℕ< (s≤s i<m)) τ + ; Δ = insert Δ (fromℕ< (s≤s i≤m)) τ } where open Context Γ,Δ -rotate₁ : ∀ {n} → (Γ,Δ : Context n) → (i j : Fin n) → toℕ i ≥ Context.m Γ,Δ → .(i F.≤ j) → Context n +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) Γ @@ -104,8 +109,8 @@ transfer {n} Γ,Δ i j i<m 1+j≥m with Context.m Γ,Δ ℕ.≟ 0 where open Context Γ,Δ -cons : ∀ {n} → Type ℓ ℓ → Context n → Context (suc n) -cons {n} τ Γ,Δ = record +cons : ∀ {n} → Context n → Type ℓ ℓ → Context (suc n) +cons {n} Γ,Δ τ = record { m≤n = s≤s m≤n ; Γ = Γ ; Δ = τ ∷ Δ @@ -116,8 +121,11 @@ cons {n} τ Γ,Δ = record shift : ∀ {n} → Context n → Context n shift {n} Γ,Δ = record { m≤n = z≤n - ; Γ = subst (Vec (Type ℓ ℓ)) (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (Δ ++ Γ) + ; Γ = cast (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (Δ ++ Γ) ; Δ = [] } where open Context Γ,Δ + +_≋_ : ∀ {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 2acaf72..2761fae 100644 --- a/src/Cfe/Context/Properties.agda +++ b/src/Cfe/Context/Properties.agda @@ -1,7 +1,64 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary using (Setoid) +open import Relation.Binary using (Setoid; Symmetric) module Cfe.Context.Properties {c ℓ} (over : Setoid c ℓ) where + +open import Cfe.Context.Base over as C +open import Cfe.Type over +open import Data.Fin as F +open import Data.Nat as ℕ +open import Data.Nat.Properties +open import Data.Product +open import Data.Vec +open import Function +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) + +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 + 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 + 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) |