@@ -12,9 +12,9 @@ open import Data.Fin.Substitution
12
12
open import Data.Nat hiding (_⊔_; _/_)
13
13
open import Data.Fin.Base using (Fin; zero; suc; lift)
14
14
open import Data.Vec.Base
15
- import Data.Vec.Properties as VecProp
15
+ import Data.Vec.Properties as Vec
16
16
open import Function.Base as Fun using (_∘_; _$_; flip)
17
- open import Relation.Binary.PropositionalEquality.Core as PropEq
17
+ open import Relation.Binary.PropositionalEquality.Core as ≡
18
18
using (_≡_; refl; sym; cong; cong₂)
19
19
open import Relation.Binary.PropositionalEquality.Properties
20
20
using (module ≡-Reasoning )
@@ -68,9 +68,9 @@ record Lemmas₀ (T : Pred ℕ ℓ) : Set ℓ where
68
68
lookup-map-weaken-↑⋆ zero x = refl
69
69
lookup-map-weaken-↑⋆ (suc k) zero = refl
70
70
lookup-map-weaken-↑⋆ (suc k) (suc x) {ρ} = begin
71
- lookup (map weaken (map weaken ρ ↑⋆ k)) x ≡⟨ VecProp .lookup-map x weaken (map weaken ρ ↑⋆ k) ⟩
71
+ lookup (map weaken (map weaken ρ ↑⋆ k)) x ≡⟨ Vec .lookup-map x weaken (map weaken ρ ↑⋆ k) ⟩
72
72
weaken (lookup (map weaken ρ ↑⋆ k) x) ≡⟨ cong weaken (lookup-map-weaken-↑⋆ k x) ⟩
73
- weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x)) ≡⟨ sym $ VecProp .lookup-map (lift k suc x) weaken ((ρ ↑) ↑⋆ k) ⟩
73
+ weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x)) ≡⟨ sym $ Vec .lookup-map (lift k suc x) weaken ((ρ ↑) ↑⋆ k) ⟩
74
74
lookup (map weaken ((ρ ↑) ↑⋆ k)) (lift k suc x) ∎
75
75
76
76
record Lemmas₁ (T : Pred ℕ ℓ) : Set ℓ where
@@ -85,7 +85,7 @@ record Lemmas₁ (T : Pred ℕ ℓ) : Set ℓ where
85
85
lookup ρ x ≡ var y →
86
86
lookup (map weaken ρ) x ≡ var (suc y)
87
87
lookup-map-weaken x {y} {ρ} hyp = begin
88
- lookup (map weaken ρ) x ≡⟨ VecProp .lookup-map x weaken ρ ⟩
88
+ lookup (map weaken ρ) x ≡⟨ Vec .lookup-map x weaken ρ ⟩
89
89
weaken (lookup ρ x) ≡⟨ cong weaken hyp ⟩
90
90
weaken (var y) ≡⟨ weaken-var ⟩
91
91
var (suc y) ∎
@@ -153,7 +153,7 @@ record Lemmas₂ (T : Pred ℕ ℓ) : Set ℓ where
153
153
154
154
lookup-⊙ : ∀ x {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} →
155
155
lookup (ρ₁ ⊙ ρ₂) x ≡ lookup ρ₁ x / ρ₂
156
- lookup-⊙ x {ρ₁} {ρ₂} = VecProp .lookup-map x (λ t → t / ρ₂) ρ₁
156
+ lookup-⊙ x {ρ₁} {ρ₂} = Vec .lookup-map x (λ t → t / ρ₂) ρ₁
157
157
158
158
lookup-⨀ : ∀ x (ρs : Subs T m n) →
159
159
lookup (⨀ ρs) x ≡ var x /✶ ρs
@@ -239,8 +239,8 @@ record Lemmas₃ (T : Pred ℕ ℓ) : Set ℓ where
239
239
240
240
⊙-id : {ρ : Sub T m n} → ρ ⊙ id ≡ ρ
241
241
⊙-id {ρ = ρ} = begin
242
- map (λ t → t / id) ρ ≡⟨ VecProp .map-cong id-vanishes ρ ⟩
243
- map Fun.id ρ ≡⟨ VecProp .map-id ρ ⟩
242
+ map (λ t → t / id) ρ ≡⟨ Vec .map-cong id-vanishes ρ ⟩
243
+ map Fun.id ρ ≡⟨ Vec .map-id ρ ⟩
244
244
ρ ∎
245
245
246
246
open Lemmas₂ lemmas₂ public hiding (wk-⊙-sub′)
@@ -264,13 +264,13 @@ record Lemmas₄ (T : Pred ℕ ℓ) : Set ℓ where
264
264
ρ₁ ↑ ⊙ ρ₂ ↑ ∎
265
265
where
266
266
lemma = begin
267
- map weaken (map (λ t → t / ρ₂) ρ₁) ≡⟨ sym (VecProp .map-∘ _ _ _) ⟩
268
- map (λ t → weaken (t / ρ₂)) ρ₁ ≡⟨ VecProp .map-cong (λ t → begin
267
+ map weaken (map (λ t → t / ρ₂) ρ₁) ≡⟨ sym (Vec .map-∘ _ _ _) ⟩
268
+ map (λ t → weaken (t / ρ₂)) ρ₁ ≡⟨ Vec .map-cong (λ t → begin
269
269
weaken (t / ρ₂) ≡⟨ sym /-wk ⟩
270
270
t / ρ₂ / wk ≡⟨ hyp t ⟩
271
271
t / wk / ρ₂ ↑ ≡⟨ cong₂ _/_ /-wk refl ⟩
272
272
weaken t / ρ₂ ↑ ∎) ρ₁ ⟩
273
- map (λ t → weaken t / ρ₂ ↑) ρ₁ ≡⟨ VecProp .map-∘ _ _ _ ⟩
273
+ map (λ t → weaken t / ρ₂ ↑) ρ₁ ≡⟨ Vec .map-∘ _ _ _ ⟩
274
274
map (λ t → t / ρ₂ ↑) (map weaken ρ₁) ∎
275
275
276
276
↑⋆-distrib′ : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} →
@@ -284,7 +284,7 @@ record Lemmas₄ (T : Pred ℕ ℓ) : Set ℓ where
284
284
285
285
map-weaken : {ρ : Sub T m n} → map weaken ρ ≡ ρ ⊙ wk
286
286
map-weaken {ρ = ρ} = begin
287
- map weaken ρ ≡⟨ VecProp .map-cong (λ _ → sym /-wk) ρ ⟩
287
+ map weaken ρ ≡⟨ Vec .map-cong (λ _ → sym /-wk) ρ ⟩
288
288
map (λ t → t / wk) ρ ≡⟨ refl ⟩
289
289
ρ ⊙ wk ∎
290
290
@@ -324,8 +324,8 @@ record Lemmas₄ (T : Pred ℕ ℓ) : Set ℓ where
324
324
⊙-assoc : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} {ρ₃ : Sub T o p} →
325
325
ρ₁ ⊙ (ρ₂ ⊙ ρ₃) ≡ (ρ₁ ⊙ ρ₂) ⊙ ρ₃
326
326
⊙-assoc {ρ₁ = ρ₁} {ρ₂} {ρ₃} = begin
327
- map (λ t → t / ρ₂ ⊙ ρ₃) ρ₁ ≡⟨ VecProp .map-cong /-⊙ ρ₁ ⟩
328
- map (λ t → t / ρ₂ / ρ₃) ρ₁ ≡⟨ VecProp .map-∘ _ _ _ ⟩
327
+ map (λ t → t / ρ₂ ⊙ ρ₃) ρ₁ ≡⟨ Vec .map-cong /-⊙ ρ₁ ⟩
328
+ map (λ t → t / ρ₂ / ρ₃) ρ₁ ≡⟨ Vec .map-∘ _ _ _ ⟩
329
329
map (λ t → t / ρ₃) (map (λ t → t / ρ₂) ρ₁) ∎
330
330
331
331
map-weaken-⊙-sub : ∀ {ρ : Sub T m n} {t} → map weaken ρ ⊙ sub t ≡ ρ
@@ -560,7 +560,7 @@ record TermLemmas (T : ℕ → Set) : Set₁ where
560
560
(∀ x → lookup ρ₂ x ≡ T.var (f x)) →
561
561
map T.var ρ₁ ≡ ρ₂
562
562
map-var≡ {ρ₁ = ρ₁} {ρ₂ = ρ₂} {f = f} hyp₁ hyp₂ = extensionality λ x →
563
- lookup (map T.var ρ₁) x ≡⟨ VecProp .lookup-map x _ ρ₁ ⟩
563
+ lookup (map T.var ρ₁) x ≡⟨ Vec .lookup-map x _ ρ₁ ⟩
564
564
T.var (lookup ρ₁ x) ≡⟨ cong T.var $ hyp₁ x ⟩
565
565
T.var (f x) ≡⟨ sym $ hyp₂ x ⟩
566
566
lookup ρ₂ x ∎
@@ -577,15 +577,15 @@ record TermLemmas (T : ℕ → Set) : Set₁ where
577
577
↑≡↑ : {ρ : Sub Fin m n} → map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑
578
578
↑≡↑ {ρ = ρ} = map-var≡
579
579
(VarLemmas.lookup-↑⋆ (lookup ρ) (λ _ → refl) 1 )
580
- (lookup-↑⋆ (lookup ρ) (λ _ → VecProp .lookup-map _ _ ρ) 1 )
580
+ (lookup-↑⋆ (lookup ρ) (λ _ → Vec .lookup-map _ _ ρ) 1 )
581
581
582
582
/Var≡/ : ∀ {ρ : Sub Fin m n} {t} → t /Var ρ ≡ t T./ map T.var ρ
583
583
/Var≡/ {ρ = ρ} {t = t} =
584
584
/✶-↑✶ (ε ▻ ρ) (ε ▻ map T.var ρ)
585
585
(λ k x →
586
586
T.var x /Var ρ VarSubst.↑⋆ k ≡⟨ app-var ⟩
587
587
T.var (lookup (ρ VarSubst.↑⋆ k) x) ≡⟨ cong T.var $ VarLemmas.lookup-↑⋆ _ (λ _ → refl) k _ ⟩
588
- T.var (lift k (VarSubst._/ ρ) x) ≡⟨ sym $ lookup-↑⋆ _ (λ _ → VecProp .lookup-map _ _ ρ) k _ ⟩
588
+ T.var (lift k (VarSubst._/ ρ) x) ≡⟨ sym $ lookup-↑⋆ _ (λ _ → Vec .lookup-map _ _ ρ) k _ ⟩
589
589
lookup (map T.var ρ T.↑⋆ k) x ≡⟨ sym app-var ⟩
590
590
T.var x T./ map T.var ρ T.↑⋆ k ∎)
591
591
zero t
0 commit comments