blob: 241669f8f827341b521634dba687037d74fedacc (
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
190
|
module Core.Reduction
import Core.Context
import Core.Declarative
import Core.Environment
import Core.Term
import Core.Term.NormalForm
import Core.Term.Substitution
import Core.Thinning
public export
data TermStep : Env sx -> Term sx -> Term sx -> Term sx -> Type where
PiBeta :
TypeWf env f ->
TermWf (env :< f) t g ->
TermWf env u f ->
---
TermStep env (App (Abs n t) u) (subst t $ sub1 u) (subst g $ sub1 u)
AppStep :
TermStep env t u (Pi n f g) ->
TermWf env a f ->
---
TermStep env (App t a) (App u a) (subst g $ sub1 a)
StepConv :
TermStep env t u a ->
TypeConv env a b ->
---
TermStep env t u b
public export
TypeStep : Env sx -> Term sx -> Term sx -> Type
TypeStep env a b = TermStep env a b Set
namespace Type
public export
data TypeRed : Env sx -> Term sx -> Term sx -> Type where
Stay : TypeWf env a -> TypeRed env a a
(::) : TypeStep env a b -> TypeRed env b c -> TypeRed env a c
namespace Term
public export
data TermRed : Env sx -> Term sx -> Term sx -> Term sx -> Type where
Stay : TermWf env t a -> TermRed env t t a
(::) : TermStep env t u a -> TermRed env u v a -> TermRed env t v a
%name TypeStep step
%name TermStep step
%name TypeRed steps
%name TermRed steps
-- Reduction Subsumed by Conversion --------------------------------------------
termStepImpliesTermConv : TermStep env t u a -> TermConv env t u a
termStepImpliesTermConv (PiBeta wf wf1 wf2) = PiBeta wf wf1 wf2
termStepImpliesTermConv (AppStep step wf) = AppConv (termStepImpliesTermConv step) (ReflTerm wf)
termStepImpliesTermConv (StepConv step conv) = ConvTermConv (termStepImpliesTermConv step) conv
typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b
typeStepImpliesTypeConv step = LiftConv (termStepImpliesTermConv step)
export
typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b
typeRedImpliesTypeConv (Stay wf) = ReflType wf
typeRedImpliesTypeConv (step :: steps) =
TransType
(typeStepImpliesTypeConv step)
(typeRedImpliesTypeConv steps)
export
termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a
termRedImpliesTermConv (Stay wf) = ReflTerm wf
termRedImpliesTermConv (step :: steps) =
TransTerm
(termStepImpliesTermConv step)
(termRedImpliesTermConv steps)
-- Subject Typing --------------------------------------------------------------
termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
termStepImpliesSubjectWf (PiBeta wf wf1 wf2) = AppTerm (AbsTerm wf wf1) wf2
termStepImpliesSubjectWf (AppStep step wf) = AppTerm (termStepImpliesSubjectWf step) wf
termStepImpliesSubjectWf (StepConv step conv) = ConvTerm (termStepImpliesSubjectWf step) conv
typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
typeStepImpliesSubjectWf step = LiftType (termStepImpliesSubjectWf step)
-- Whnfs Do Not Reduce ---------------------------------------------------------
-- Cannot step from whnf
termStepWhnfImpossible : Whnf t -> Not (TermStep env t u a)
termStepWhnfImpossible n (StepConv step conv) = termStepWhnfImpossible n step
termStepWhnfImpossible (Ntrl (App n)) (PiBeta wf wf1 wf2) impossible
termStepWhnfImpossible (Ntrl (App n)) (AppStep step wf) = termStepWhnfImpossible (Ntrl n) step
typeStepWhnfImpossible : Whnf a -> Not (TypeStep env a b)
typeStepWhnfImpossible = termStepWhnfImpossible
-- Reduction starting from whnf goes nowhere
typeRedWhnfStays : Whnf a -> TypeRed env a b -> a = b
typeRedWhnfStays n (Stay wf) = Refl
typeRedWhnfStays n (step :: steps) = absurd $ typeStepWhnfImpossible n step
termRedWhnfStays : Whnf t -> TermRed env t u a -> t = u
termRedWhnfStays n (Stay wf) = Refl
termRedWhnfStays n (step :: steps) = absurd $ termStepWhnfImpossible n step
-- Reduction is Deterministic --------------------------------------------------
termStepDeterministic : TermStep env t u a -> TermStep env t v b -> u = v
termStepDeterministic (StepConv step conv) step1 = termStepDeterministic step step1
termStepDeterministic step (StepConv step1 conv) = termStepDeterministic step step1
termStepDeterministic (PiBeta _ _ _) (PiBeta _ _ _) = Refl
termStepDeterministic (PiBeta _ _ _) (AppStep step _) = absurd $ termStepWhnfImpossible Abs step
termStepDeterministic (AppStep step _) (PiBeta _ _ _) = absurd $ termStepWhnfImpossible Abs step
termStepDeterministic (AppStep step _) (AppStep step1 _) =
cong (flip App _) $
termStepDeterministic step step1
typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c
typeStepDeterministic = termStepDeterministic
typeRedDeterministic : TypeRed env a b -> TypeRed env a c -> Whnf b -> Whnf c -> b = c
typeRedDeterministic (Stay _) red n m = typeRedWhnfStays n red
typeRedDeterministic red (Stay _) n m = sym $ typeRedWhnfStays m red
typeRedDeterministic (step :: steps) (step1 :: steps1) n m =
let steps1' = rewrite typeStepDeterministic step step1 in steps1 in
typeRedDeterministic steps steps1' n m
termRedDeterministic : TermRed env t u a -> TermRed env t v b -> Whnf u -> Whnf v -> u = v
termRedDeterministic (Stay _) red n m = termRedWhnfStays n red
termRedDeterministic red (Stay _) n m = sym $ termRedWhnfStays m red
termRedDeterministic (step :: steps) (step1 :: steps1) n m =
let steps1' : TermRed env _ v b = rewrite termStepDeterministic step step1 in steps1 in
termRedDeterministic steps steps1' n m
-- Weakening Preservation ------------------------------------------------------
wknPresTermStep :
{0 env1 : Env sx} ->
TermStep env1 t u a ->
EnvWf env2 ->
IsExtension thin env2 env1 ->
TermStep env2 (wkn t thin) (wkn u thin) (wkn a thin)
wknPresTermStep (PiBeta {f, g, n, t, u} wf wf1 wf2) envWf ext =
rewrite wknSub1 g u thin in
rewrite wknSub1 t u thin in
let wf' = wknPresTypeWf wf envWf ext in
PiBeta wf'
(termWfRespEnvEq
(wknPresTermWf wf1 (envWf :< wf') $
replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
(compRightIdentity thin)
(KeepWf ext))
((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin)))
(wknPresTermWf wf2 envWf ext)
wknPresTermStep (AppStep {g, a} step wf) envWf ext =
rewrite wknSub1 g a thin in
AppStep (wknPresTermStep step envWf ext) (wknPresTermWf wf envWf ext)
wknPresTermStep (StepConv step conv) envWf ext =
StepConv (wknPresTermStep step envWf ext) (wknPresTypeConv conv envWf ext)
wknPresTypeStep :
{0 env1 : Env sx} ->
TypeStep env1 a b ->
EnvWf env2 ->
IsExtension thin env2 env1 ->
TypeStep env2 (wkn a thin) (wkn b thin)
wknPresTypeStep = wknPresTermStep
wknPresTypeRed :
{0 env1 : Env sx} ->
TypeRed env1 a b ->
EnvWf env2 ->
IsExtension thin env2 env1 ->
TypeRed env2 (wkn a thin) (wkn b thin)
wknPresTypeRed (Stay wf) envWf ext = Stay (wknPresTypeWf wf envWf ext)
wknPresTypeRed (step :: steps) envWf ext =
wknPresTypeStep step envWf ext :: wknPresTypeRed steps envWf ext
wknPresTermRed :
{0 env1 : Env sx} ->
TermRed env1 t u a ->
EnvWf env2 ->
IsExtension thin env2 env1 ->
TermRed env2 (wkn t thin) (wkn u thin) (wkn a thin)
wknPresTermRed (Stay wf) envWf ext = Stay (wknPresTermWf wf envWf ext)
wknPresTermRed (step :: steps) envWf ext =
wknPresTermStep step envWf ext :: wknPresTermRed steps envWf ext
|
