1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary using (Setoid)
module Cfe.Judgement.Properties
{c ℓ} (over : Setoid c ℓ)
where
open import Cfe.Expression over
open import Cfe.Judgement.Base over
open import Cfe.Type over
open import Data.Empty
open import Data.Fin as F hiding (cast)
open import Data.Fin.Properties
open import Data.Nat as ℕ
open import Data.Nat.Properties
open import Data.Vec
open import Data.Vec.Properties
open import Function
open import Relation.Binary.PropositionalEquality
wkn₁ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
Γ , Δ ⊢ e ∶ τ →
∀ τ′ i →
insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (wkn e (F.cast (+-suc n m) (raise n i))) ∶ τ
wkn₁ Eps τ′ i = Eps
wkn₁ (Char c) τ′ i = Char c
wkn₁ Bot τ′ i = Bot
wkn₁ {m} {n} {Γ} {Δ} {e} {τ} (Var {i = j} j≥n) τ′ i =
subst (insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (Var (punchIn (F.cast (+-suc n m) (raise n i)) j)) ∶_)
(eq Γ τ′ i j≥n)
(Var (le i j≥n))
where
toℕ-punchIn : ∀ {m} i j → toℕ j ℕ.≤ toℕ (punchIn {m} i j)
toℕ-punchIn zero j = n≤1+n (toℕ j)
toℕ-punchIn (suc i) zero = z≤n
toℕ-punchIn (suc i) (suc j) = s≤s (toℕ-punchIn i j)
le : ∀ {m n} i {j} → toℕ j ≥ n → toℕ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) ≥ n
le {m} {n} i {j} j≥n = begin
n ≤⟨ j≥n ⟩
toℕ j ≤⟨ toℕ-punchIn (F.cast (+-suc n m) (raise n i)) j ⟩
toℕ (punchIn (F.cast _ (raise n i)) j) ≡˘⟨ toℕ-cast (sym (+-suc n m)) (punchIn (F.cast _ (raise n i)) j) ⟩
toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ∎
where
open ≤-Reasoning
lookup-cast : ∀ {a A n} l j → lookup {a} {A} {n} l (F.cast refl j) ≡ lookup l j
lookup-cast l zero = refl
lookup-cast (x ∷ l) (suc j) = lookup-cast l j
toℕ-reduce : ∀ {m n} i i≥m → toℕ (reduce≥ {m} {n} i i≥m) ≡ toℕ i ∸ m
toℕ-reduce {zero} i i≥m = refl
toℕ-reduce {suc m} (suc i) (s≤s i≥m) = toℕ-reduce i i≥m
punchIn-∸ : ∀ {m n} i {j} j≥n → toℕ (punchIn (F.cast (+-suc n m) (raise n i)) j) ∸ n ≡ toℕ (punchIn i (reduce≥ j j≥n))
punchIn-∸ {zero} {n} zero {j} j≥n = ⊥-elim (<⇒≱ (begin-strict
toℕ j ≡˘⟨ toℕ-cast (+-identityʳ n) j ⟩
toℕ (F.cast _ j) <⟨ toℕ<n (F.cast _ j) ⟩
n ∎) j≥n)
where
open ≤-Reasoning
punchIn-∸ {suc m} {zero} zero {j} z≤n = refl
punchIn-∸ {suc m} {suc n} zero {suc j} (s≤s j≥n) = punchIn-∸ zero j≥n
punchIn-∸ {suc m} {zero} (suc i) {zero} z≤n = refl
punchIn-∸ {suc m} {zero} (suc i) {suc j} z≤n = cong suc (punchIn-∸ i z≤n)
punchIn-∸ {suc m} {suc n} (suc i) {suc j} (s≤s j≥n) = punchIn-∸ (suc i) j≥n
missing-link : ∀ {m n} i {j} j≥n → reduce≥ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) (le i j≥n) ≡ punchIn i (reduce≥ j j≥n)
missing-link {n = n} i {j} j≥n = toℕ-injective (begin
toℕ (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n)) ≡⟨ toℕ-reduce (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n) ⟩
toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ∸ n ≡⟨ cong (_∸ n) (toℕ-cast _ (punchIn (F.cast _ (raise n i)) j)) ⟩
toℕ (punchIn (F.cast _ (raise n i)) j) ∸ n ≡⟨ punchIn-∸ i j≥n ⟩
toℕ (punchIn i (reduce≥ j j≥n)) ∎)
where
open ≡-Reasoning
eq : ∀ {a} {A : Set a} {m n} (Γ : Vec A m) τ′ i {j} j≥n → lookup (insert Γ i τ′) (reduce≥ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) (le i {j} j≥n)) ≡ lookup Γ (reduce≥ j j≥n)
eq {n = n} Γ τ′ i {j} j≥n = begin
lookup (insert Γ i τ′) (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n)) ≡⟨ cong (lookup (insert Γ i τ′)) (missing-link i j≥n) ⟩
lookup (insert Γ i τ′) (punchIn i (reduce≥ j j≥n)) ≡⟨ insert-punchIn Γ i τ′ (reduce≥ j j≥n) ⟩
lookup Γ (reduce≥ j j≥n) ∎
where
open ≡-Reasoning
wkn₁ (Fix Γ,τ∷Δ⊢e∶τ) τ′ i = Fix (wkn₁ Γ,τ∷Δ⊢e∶τ τ′ i)
wkn₁{m} {n} {Γ} {Δ} (Cat {e₂ = e₂} {τ₂ = τ₂} Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) τ′ i =
Cat (wkn₁ Γ,Δ⊢e₁∶τ₁ τ′ i)
(subst (λ x → Δ ++ insert Γ i τ′ , [] ⊢ x ∶ τ₂)
(begin
cast _ (cast _ (wkn e₂ (F.cast refl (raise zero (F.cast _ (raise n i)))))) ≡⟨⟩
cast _ (cast _ (wkn e₂ (F.cast refl (F.cast _ (raise n i))))) ≡⟨ cast-involutive (wkn e₂ (F.cast refl (F.cast _ (raise n i)))) refl (sym (+-suc n m)) (sym (+-suc n m)) ⟩
cast _ (wkn e₂ (F.cast refl (F.cast _ (raise n i)))) ≡⟨ cong (λ x → cast (sym (+-suc n m)) (wkn e₂ x)) (fcast-involutive (raise n i) (+-suc n m) refl (+-suc n m)) ⟩
cast _ (wkn e₂ (F.cast _ (raise n i))) ∎)
(cast₁ (eq Γ Δ τ′ i) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ τ′ (F.cast (+-suc n m) (raise n i)))))
τ₁⊛τ₂
where
open ≡-Reasoning
eq : ∀ {a A m n} Γ Δ τ′ i → insert (Δ ++ Γ) (F.cast (+-suc n m) (raise n i)) τ′ ≅ Δ ++ insert {a} {A} {m} Γ i τ′
eq Γ [] τ′ zero = ≅-refl
eq (x ∷ Γ) [] τ′ (suc i) = refl ∷ eq Γ [] τ′ i
eq Γ (x ∷ Δ) τ′ i = refl ∷ (eq Γ Δ τ′ i)
fcast-involutive : ∀ {k m n} i → .(k≡m : k ≡ m) → .(m≡n : m ≡ n) → .(k≡n : k ≡ n) → F.cast m≡n (F.cast k≡m i) ≡ F.cast k≡n i
fcast-involutive i k≡m m≡n k≡n = toℕ-injective (begin
toℕ (F.cast m≡n (F.cast k≡m i)) ≡⟨ toℕ-cast m≡n (F.cast k≡m i) ⟩
toℕ (F.cast k≡m i) ≡⟨ toℕ-cast k≡m i ⟩
toℕ i ≡˘⟨ toℕ-cast k≡n i ⟩
toℕ (F.cast k≡n i) ∎)
wkn₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) τ′ i = Vee (wkn₁ Γ,Δ⊢e₁∶τ₁ τ′ i) (wkn₁ Γ,Δ⊢e₂∶τ₂ τ′ i) τ₁#τ₂
wkn₂ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
Γ , Δ ⊢ e ∶ τ →
∀ τ′ i →
Γ , insert Δ i τ′ ⊢ wkn e (inject+ m i) ∶ τ
wkn₂ Eps τ′ i = Eps
wkn₂ (Char c) τ′ i = Char c
wkn₂ Bot τ′ i = Bot
wkn₂ {m} {n} {Γ} {Δ} (Var {i = j} j≥n) τ′ i =
subst (Γ , insert Δ i τ′ ⊢_∶ lookup Γ (reduce≥ j j≥n))
(cong Var (toℕ-injective (begin-equality
toℕ (suc j) ≡⟨⟩
suc (toℕ j) ≡˘⟨ cong toℕ (punchIn-suc i≤j) ⟩
toℕ (punchIn (inject+ m i) j) ∎)))
(Var (s≤s j≥n))
where
open ≤-Reasoning
m<n+1⇒m≤n : ∀ {m n} → m ℕ.< suc n → m ℕ.≤ n
m<n+1⇒m≤n (s≤s m≤n) = m≤n
i≤j : toℕ (inject+ m i) ℕ.≤ toℕ j
i≤j = begin
toℕ (inject+ m i) ≡˘⟨ toℕ-inject+ m i ⟩
toℕ i ≤⟨ m<n+1⇒m≤n (toℕ<n i) ⟩
n ≤⟨ j≥n ⟩
toℕ j ∎
punchIn-suc : ∀ {m i j} → toℕ i ℕ.≤ toℕ j → punchIn {m} i j ≡ suc j
punchIn-suc {_} {zero} {j} i≤j = refl
punchIn-suc {_} {suc i} {suc j} (s≤s i≤j) = cong suc (punchIn-suc i≤j)
wkn₂ (Fix Γ,τ∷Δ⊢e∶τ) τ′ i = Fix (wkn₂ Γ,τ∷Δ⊢e∶τ τ′ (suc i))
wkn₂ {m} {n} {Γ} {Δ} (Cat {e₂ = e₂} {τ₂ = τ₂} Γ,Δ⊢e₁∶τ₁ Δ++Γ,∙⊢e₂∶τ₂ τ₁⊛τ₂) τ′ i =
Cat (wkn₂ Γ,Δ⊢e₁∶τ₁ τ′ i)
(subst (insert Δ i τ′ ++ Γ , [] ⊢_∶ τ₂)
(begin
cast refl (cast refl (wkn e₂ (F.cast refl (inject+ m i)))) ≡⟨ cast-inverse (wkn e₂ (F.cast refl (inject+ m i))) refl refl ⟩
wkn e₂ (F.cast refl (inject+ m i)) ≡⟨ cong (wkn e₂) (toℕ-injective (toℕ-cast refl (inject+ m i))) ⟩
wkn e₂ (inject+ m i) ∎)
(cast₁ (≅-reflexive (eq Γ Δ τ′ i)) (wkn₁ Δ++Γ,∙⊢e₂∶τ₂ τ′ (inject+ m i))))
τ₁⊛τ₂
where
open ≡-Reasoning
eq : ∀ {a A m n} Γ Δ τ i → insert (Δ ++ Γ) (inject+ m i) τ ≡ insert {a} {A} {n} Δ i τ ++ Γ
eq Γ Δ τ zero = refl
eq Γ (_ ∷ Δ) τ (suc i) = cong₂ _∷_ refl (eq Γ Δ τ i)
wkn₂ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) τ′ i = Vee (wkn₂ Γ,Δ⊢e₁∶τ₁ τ′ i) (wkn₂ Γ,Δ⊢e₂∶τ₂ τ′ i) τ₁#τ₂
|
