-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathTypedRule.v
225 lines (201 loc) · 8.9 KB
/
TypedRule.v
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
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
Require Import HoTT.
Require Import Syntax.ScopeSystem.
Require Import Auxiliary.Family.
Require Import Auxiliary.WellFounded.
Require Import Auxiliary.Coproduct.
Require Import Syntax.All.
Require Import Typing.Context.
Require Import Typing.Judgement.
Require Import Presented.AlgebraicExtension.
Require Import Typing.RawRule.
Require Import Typing.RawTypeTheory.
Require Import Presented.PresentedRawRule.
Require Import Presented.PresentedRawTypeTheory.
Require Import Presented.CongruenceRule.
Require Import Typing.Presuppositions.
(** In this file: definition of well-typedness of an algebraic extension, and a (well-presented) rule. *)
Section WellTypedRule.
Context {σ : scope_system}.
(* TODO: upstream to new file [TypedAlgebraicExtension]. *)
Definition is_well_typed_algebraic_extension
{Σ : signature σ} (T : raw_type_theory Σ)
{a} (A : algebraic_extension Σ a)
: Type.
Proof.
refine (forall r : A, _).
exact (forall
(i : presupposition_of_boundary (AlgebraicExtension.premise_boundary r)),
RawTypeTheory.derivation
(RawTypeTheory.fmap include_symbol T)
(AlgebraicExtension.flatten (AlgebraicExtension.initial_segment A r))
(presupposition_of_boundary _ i)).
Defined.
(* NOTE: when checking we want to add the earlier premises of [A] to [T], and typecheck [r] over that. There are (at least) three ways to do this:
(1) take earlier premises just as judgements, and allow them as hypotheses in the derivation;
(2) take earlier premise as judgements, then add no-premise raw rules to [T], giving these judgements as axioms;
(3) give the extension of [T] by the preceding part of [A] as a type theory, i.e. turn premises of [A] into genuine raw rules, with the variables of their contexts turned into term premises, and conclusion just the head of the given premise of [A].
In any case we must first translate [T] up to the extended signature of [R].
(1) would nicely fit into the monadic view of derivations.
(3) would nicely factorise into “take initial segment of an alg ext”, and “extend TT by an alg ext”; also avoids the need to frequently use “cut” when invoking the earlier premises in the derivations
We currently take option (1).
*)
(* TODO: consider naming. Currently a bit out of step with our general convention of using e.g. [derivation] not [is_derivable]; but [derivation] would be misleading here, since this is the type of derivations showing that the rule is well-formed, not “derivations of the rule” in the usual sense of derivations showing it’s a derivable rule. *)
Local Definition is_well_typed
{Σ : signature σ} (T : raw_type_theory Σ)
{a} {jf_concl}
(R : rule Σ a jf_concl)
: Type.
Proof.
refine (is_well_typed_algebraic_extension T (rule_premise R) * _).
(* well-typedness of conclusion *)
exact
(forall (i : presupposition_of_boundary (PresentedRawRule.conclusion_boundary R)),
RawTypeTheory.derivation
(RawTypeTheory.fmap include_symbol T)
(AlgebraicExtension.flatten (rule_premise R))
(presupposition_of_boundary _ i)).
Defined.
End WellTypedRule.
Section Functoriality.
Context {σ : scope_system} `{Funext}.
Definition fmap_is_well_typed_algebraic_extension
{Σ Σ' : signature σ} (f : Signature.map Σ Σ')
{a} {A : algebraic_extension Σ a}
{T} (D : is_well_typed_algebraic_extension T A)
: is_well_typed_algebraic_extension
(RawTypeTheory.fmap f T) (AlgebraicExtension.fmap f A).
Proof.
unfold is_well_typed_algebraic_extension.
intros p.
change (AlgebraicExtension.premise_boundary p)
with (Judgement.fmap_boundary
(Metavariable.fmap1 f _)
(@AlgebraicExtension.premise_boundary _ _ _ A p)).
intros i.
set (Di := D p (presupposition_fmap_boundary _ _ i)).
(* [Di] is essentially what we want, modulo some translation. *)
refine (transport _
(Family.map_commutes (presupposition_fmap_boundary _ _) i) _).
match goal with
| [|- RawTypeTheory.derivation _ _ ?JJ ] => set (J := (JJ)) in *
| _ => fail
end.
unfold Family.fmap, family_element in J.
subst J.
refine (RawTypeTheory.derivation_fmap_over_simple _ _ _ Di).
- (* map in type theory *)
(* TODO: refactor to be higher-level, eg using [RawTypeTheory.fmap_compose]? *)
exists idmap.
intros r; simpl.
eapply concat. { apply inverse, RawRule.fmap_compose. }
eapply concat. 2: { apply RawRule.fmap_compose. }
apply ap10, ap.
apply Metavariable.include_symbol_after_map.
- (* map in hypotheses *)
cbn. exists idmap; intros j.
eapply concat. 2: { apply AlgebraicExtension.flatten_fmap. }
apply AlgebraicExtension.flatten_initial_segment_fmap_applied.
Defined.
(** Well-typedness is _covariant_ in the signature *)
Local Definition fmap_is_well_typed
{Σ Σ' : signature σ} (f : Signature.map Σ Σ')
{a} {jf_concl} {R : rule Σ a jf_concl}
{T} (D : is_well_typed T R)
: is_well_typed (RawTypeTheory.fmap f T) (PresentedRawRule.fmap f R).
Proof.
split.
(* premises *)
{ apply fmap_is_well_typed_algebraic_extension, (fst D). }
(* conclusion *)
set (fR_concl := PresentedRawRule.conclusion_boundary (PresentedRawRule.fmap f R)).
assert (e_concl : fR_concl = Judgement.fmap_boundary
(Metavariable.fmap1 f _)
(PresentedRawRule.conclusion_boundary R)).
{ apply PresentedRawRule.conclusion_boundary_fmap. }
clearbody fR_concl. destruct e_concl^.
intros i.
set (Di := (snd D) (presupposition_fmap_boundary _ _ i)).
(* [Di] is essentially what we want, modulo some translation. *)
refine (transport _
(Family.map_commutes (presupposition_fmap_boundary _ _) i) _).
match goal with
| [|- RawTypeTheory.derivation _ _ ?JJ ] => set (J := (JJ)) in *
| _ => fail
end.
unfold Family.fmap, family_element in J.
subst J.
refine (RawTypeTheory.derivation_fmap_over_simple _ _ _ Di).
- (* map in type theory *)
(* TODO: refactor using [RawTypeTheory.fmap_compose]? *)
exists idmap.
intros r; simpl.
eapply concat. { apply inverse, RawRule.fmap_compose. }
eapply concat. 2: { apply RawRule.fmap_compose. }
apply ap10, ap.
apply Metavariable.include_symbol_after_map.
- (* map in hypotheses *)
cbn. exists idmap.
apply AlgebraicExtension.flatten_fmap.
Defined.
(** Well-typedness is _contravariantly_ functorial in the ambient theory. *)
(* TODO: consider naming! *)
Definition fmap_is_well_typed_algebraic_extension_in_theory {Σ : signature σ}
{T T' : raw_type_theory Σ} (f : RawTypeTheory.map T T')
{a} {A : algebraic_extension Σ a}
: is_well_typed_algebraic_extension T A
-> is_well_typed_algebraic_extension T' A.
Proof.
intros A_WT r p.
refine (RawTypeTheory.derivation_fmap1 _ (A_WT r p)).
apply RawTypeTheory.map_fmap, f.
Defined.
(** Well-typedness is _contravariantly_ functorial in the ambient theory. *)
(* TODO: consider naming! *)
Definition fmap_is_well_typed_in_theory {Σ : signature σ}
{T T' : raw_type_theory Σ} (f : RawTypeTheory.map T T')
{a} {jf_concl} {R : rule Σ a jf_concl}
: is_well_typed T R -> is_well_typed T' R.
Proof.
intros R_WT.
split.
{ exact (fmap_is_well_typed_algebraic_extension_in_theory f (fst R_WT)). }
intros p.
refine (RawTypeTheory.derivation_fmap1 _ (snd R_WT p)).
apply RawTypeTheory.map_fmap, f.
Defined.
End Functoriality.
Section Flattening.
Context {σ : scope_system} `{Funext}.
Definition weakly_presuppositive_flatten
{Σ : signature σ} {T : raw_type_theory Σ}
{a} {jf_concl}
{R : rule Σ a jf_concl}
(T_WT : is_well_typed T R)
(Sr : Judgement.is_object jf_concl ->
{S : Σ.(family_index) &
(symbol_arity S = a) * (symbol_class S = Judgement.class_of jf_concl)})
: weakly_presuppositive_raw_rule T (PresentedRawRule.flatten R Sr).
Proof.
apply snd in T_WT.
intros i.
refine (Closure.graft' (T_WT i) _ _).
- recursive_destruct jf_concl; apply idpath.
- clear i. intros i.
exact (Closure.hypothesis _ (_+_) (inl i)).
Qed.
(* NOTE: in fact, we should be able to extend this to showing
that [flatten R] is _strongly_ presuppositive. *)
End Flattening.
Section Congruence_Rules.
Context {σ : scope_system} `{Funext}.
Definition congruence_rule_is_well_typed
{Σ : signature σ} {T : raw_type_theory Σ}
{a} {jf_concl} {R : rule Σ a jf_concl} (R_WT : is_well_typed T R)
(R_is_ob : Judgement.is_object jf_concl)
(S : Σ)
(e_a : symbol_arity S = a)
(e_cl : symbol_class S = class_of jf_concl)
: is_well_typed T (congruence_rule R R_is_ob S e_a e_cl).
Proof.
Admitted. (* [congruence_rule_is_well_typed]: large, key stress test of functoriality framework for derivability *)
End Congruence_Rules.