blob: 9e1d318a5d36cc3cdc31e0bf409ad0d701a90dc8 (
plain)
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
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
|
module Core.Reduction
import Core.Environment
import Core.Declarative
import Core.Term
import Core.Term.NormalForm
import Core.Term.Substitution
import Core.Term.Thinned
import Core.Thinning
%prefix_record_projections off
-- Definition ------------------------------------------------------------------
public export
data TermStep : Env n -> Term n -> Term n -> Term n -> Type where
AppStep :
TermStep env t u (Pi a b) ->
TermWf env v a ->
---
TermStep env (App t v) (App u v) (subst b $ Wkn (id _) :< pure v)
PiBeta :
TypeWf env a ->
TermWf (env :< pure a) t b ->
TermWf env u a ->
---
TermStep env
(App (Abs t) u)
(subst t $ Wkn (id _) :< pure u)
(subst b $ Wkn (id _) :< pure u)
ConvStep :
TermStep env t u a ->
TypeConv env a b ->
---
TermStep env t u b
public export
TypeStep : Env n -> Term n -> Term n -> Type
TypeStep env a b = TermStep env a b Set
public export
data ReflTransClosure : (refl : a -> Type) -> (step : a -> a -> Type) -> a -> a -> Type where
Refl :
{0 refl : a -> Type} ->
refl x ->
---
ReflTransClosure refl step x x
Step :
{0 step : a -> a -> Type} ->
step x y ->
ReflTransClosure refl step y z ->
---
ReflTransClosure refl step x z
public export
TypeReduce : Env n -> Term n -> Term n -> Type
TypeReduce env = ReflTransClosure (TypeWf env) (TypeStep env)
public export
TermReduce : Env n -> Term n -> Term n -> Term n -> Type
TermReduce env t u a = ReflTransClosure (\t => TermWf env t a) (\t, u => TermStep env t u a) t u
%name TermStep step
%name ReflTransClosure steps
-- Respects Environment Quotient -----------------------------------------------
export
termStepRespEq : TermStep env1 t u a -> env1 =~= env2 -> TermStep env2 t u a
termStepRespEq (AppStep step tmWf) prf =
AppStep
(termStepRespEq step prf)
(termWfRespEq tmWf prf)
termStepRespEq (PiBeta tyWf tmWf tmWf1) prf =
PiBeta
(typeWfRespEq tyWf prf)
(termWfRespEq tmWf $ prf :< Refl)
(termWfRespEq tmWf1 prf)
termStepRespEq (ConvStep step tyConv) prf =
ConvStep
(termStepRespEq step prf)
(typeConvRespEq tyConv prf)
export
typeStepRespEq : TypeStep env1 a b -> env1 =~= env2 -> TypeStep env2 a b
typeStepRespEq = termStepRespEq
export
typeRedRespEq : TypeReduce env1 a b -> env1 =~= env2 -> TypeReduce env2 a b
typeRedRespEq (Refl tyWf) prf = Refl (typeWfRespEq tyWf prf)
typeRedRespEq (Step step steps) prf = Step (typeStepRespEq step prf) (typeRedRespEq steps prf)
export
termRedRespEq : TermReduce env1 t u a -> env1 =~= env2 -> TermReduce env2 t u a
termRedRespEq (Refl tmWf) prf = Refl (termWfRespEq tmWf prf)
termRedRespEq (Step step steps) prf = Step (termStepRespEq step prf) (termRedRespEq steps prf)
-- Reduction Subsumed by Conversion --------------------------------------------
export
termStepImpliesConv : TermStep env t u a -> TermConv env t u a
termStepImpliesConv (AppStep step tmWf) = AppConv (termStepImpliesConv step) (ReflTm tmWf)
termStepImpliesConv (PiBeta tyWf tmWf tmWf1) = PiBeta tyWf tmWf tmWf1
termStepImpliesConv (ConvStep step tyConv) = ConvConv (termStepImpliesConv step) tyConv
export
typeStepImpliesConv : TypeStep env a b -> TypeConv env a b
typeStepImpliesConv = LiftConv . termStepImpliesConv
export
typeRedImpliesConv : TypeReduce env a b -> TypeConv env a b
typeRedImpliesConv (Refl tyWf) = ReflTy tyWf
typeRedImpliesConv (Step step steps) =
TransTy
(typeStepImpliesConv step)
(typeRedImpliesConv steps)
export
termRedImpliesConv : TermReduce env t u a -> TermConv env t u a
termRedImpliesConv (Refl tmWf) = ReflTm tmWf
termRedImpliesConv (Step step steps) =
TransTm
(termStepImpliesConv step)
(termRedImpliesConv steps)
-- Subject Typing --------------------------------------------------------------
export
termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
termStepImpliesSubjectWf (AppStep step tmWf) = AppWf (termStepImpliesSubjectWf step) tmWf
termStepImpliesSubjectWf (PiBeta tyWf tmWf tmWf1) = AppWf (AbsWf tyWf tmWf) tmWf1
termStepImpliesSubjectWf (ConvStep step tyConv) = ConvWf (termStepImpliesSubjectWf step) tyConv
export
typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
typeStepImpliesSubjectWf = LiftWf . termStepImpliesSubjectWf
-- Whnfs Do Not Reduce ---------------------------------------------------------
export
whnfNoTermStep : Whnf t -> Not (TermStep env t u a)
whnfNoTermStep (Ntrl (App n)) (AppStep step tmWf) = whnfNoTermStep (Ntrl n) step
whnfNoTermStep (Ntrl (App n)) (PiBeta tyWf tmWf tmWf1) impossible
whnfNoTermStep n (ConvStep step tyConv) = whnfNoTermStep n step
export
whnfNoTypeStep : Whnf a -> Not (TypeStep env a b)
whnfNoTypeStep = whnfNoTermStep
export
whnfTypeRedStays : Whnf a -> TypeReduce env a b -> a = b
whnfTypeRedStays n (Refl tyWf) = Refl
whnfTypeRedStays n (Step step steps) = absurd (whnfNoTypeStep n step)
export
whnfTermRedStays : Whnf t -> TermReduce env t u a -> t = u
whnfTermRedStays n (Refl tmWf) = Refl
whnfTermRedStays n (Step step steps) = absurd (whnfNoTermStep n step)
-- Reduction is Deterministic --------------------------------------------------
export
termStepDeterministic : TermStep env t u a -> TermStep env t v b -> u = v
termStepDeterministic (ConvStep step1 tyConv) step2 = termStepDeterministic step1 step2
termStepDeterministic step1 (ConvStep step2 tyConv) = termStepDeterministic step1 step2
termStepDeterministic (AppStep step1 _) (AppStep step2 _) =
cong (flip App _) $
termStepDeterministic step1 step2
termStepDeterministic (AppStep step1 _) (PiBeta _ _ _) = absurd (whnfNoTermStep Abs step1)
termStepDeterministic (PiBeta _ _ _) (AppStep step2 _) = absurd (whnfNoTermStep Abs step2)
termStepDeterministic (PiBeta _ _ _) (PiBeta _ _ _) = Refl
export
typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c
typeStepDeterministic = termStepDeterministic
export
typeRedDeterministic : TypeReduce env a b -> TypeReduce env a c -> Whnf b -> Whnf c -> b = c
typeRedDeterministic (Refl _) steps2 n m = whnfTypeRedStays n steps2
typeRedDeterministic steps1 (Refl _) n m = sym $ whnfTypeRedStays m steps1
typeRedDeterministic (Step step1 steps1) (Step step2 steps2) n m =
typeRedDeterministic steps1 (rewrite typeStepDeterministic step1 step2 in steps2) n m
export
termRedDeterministic : TermReduce env t u a -> TermReduce env t v b -> Whnf u -> Whnf v -> u = v
termRedDeterministic (Refl _) steps2 n m = whnfTermRedStays n steps2
termRedDeterministic steps1 (Refl _) n m = sym $ whnfTermRedStays m steps1
termRedDeterministic (Step step1 steps1) (Step step2 steps2) n m =
termRedDeterministic steps1 (rewrite termStepDeterministic step1 step2 in steps2) n m
|
