1(* standard prelude *)
2open HolKernel boolLib Parse
3
4
5(* extra theorem-proving oomph from libraries *)
6open bossLib metisLib ncLib BasicProvers boolSimps
7
8
9
10(* ancestor theories *)
11open fsubtypesTheory pred_setTheory
12
13val _ = new_theory "kernel_subtyping"
14
15
16
17(* set up syntax for subtyping judgements *)
18val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)),
19                  fixity = Infix(NONASSOC, 425),
20                  paren_style = OnlyIfNecessary,
21                  pp_elements = [HardSpace 1, TOK "|-", BreakSpace(1, 0),
22                                 BeginFinalBlock(PP.INCONSISTENT, 2),
23                                 TM, HardSpace 1, TOK "<:", BreakSpace(1,0)],
24                  term_name = "fsubtyping"}
25
26(* define subtyping rules *)
27val (fsubtyping_rules, fsubtyping_ind, fsubtyping_cases) = Hol_reln`
28  (!Gamma ty. wfctxt Gamma /\ ftyFV ty SUBSET cdom Gamma ==>
29              Gamma |- ty <: ty) /\
30  (!Gamma ty1 ty2 ty3. Gamma |- ty1 <: ty2 /\
31                       Gamma |- ty2 <: ty3 ==>
32                       Gamma |- ty1 <: ty3) /\
33  (!Gamma ty. wfctxt Gamma /\ ftyFV ty SUBSET cdom Gamma ==>
34              Gamma |- ty <: Top) /\
35  (!Gamma x ty. wfctxt Gamma /\ MEM (x, ty) Gamma ==>
36                Gamma |- TyVar x <: ty) /\
37  (!Gamma s1 t1 s2 t2.
38          Gamma |- t1 <: s1 /\ Gamma |- s2 <: t2 ==>
39          Gamma |- Fun s1 s2 <: Fun t1 t2) /\
40  (!Gamma x u1 s2 t2.
41          ((x,u1) :: Gamma) |- s2 <: t2 ==>
42          Gamma |- ForallTy x u1 s2 <: ForallTy x u1 t2)
43`;
44
45(* prove that sub-typing relation "respects" permutation *)
46val fsubtyping_swap = store_thm(
47  "fsubtyping_swap",
48  ``!Gamma ty1 ty2.
49        Gamma |- ty1 <: ty2 ==>
50        ctxtswap x y Gamma |- fswap x y ty1 <: fswap x y ty2``,
51  HO_MATCH_MP_TAC fsubtyping_ind THEN
52  REPEAT CONJ_TAC THENL [
53    (* refl *)  SRW_TAC [][SUBSET_DEF, fsubtyping_rules],
54    (* trans *) METIS_TAC [fsubtyping_rules],
55    (* top *)   SRW_TAC [][fsubtyping_rules, SUBSET_DEF],
56    (* tvar *)  SRW_TAC [][fsubtyping_rules],
57    (* fun *)   SRW_TAC [][fsubtyping_rules],
58    (* forall *)SRW_TAC [][fsubtyping_rules, SUBSET_DEF]
59  ]);
60
61val fsubtyping_wfctxt = store_thm(
62  "fsubtyping_wfctxt",
63  ``!G ty1 ty2. G |- ty1 <: ty2 ==> wfctxt G``,
64  HO_MATCH_MP_TAC fsubtyping_ind THEN SRW_TAC [][]);
65
66val strong_fsubtyping_ind =
67    IndDefRules.derive_strong_induction (CONJUNCTS fsubtyping_rules,
68                                         fsubtyping_ind)
69
70val fsubtyping_fv_constraint = store_thm(
71  "fsubtyping_fv_constraint",
72  ``!G ty1 ty2. G |- ty1 <: ty2 ==>
73                ftyFV ty1 SUBSET cdom G /\
74                ftyFV ty2 SUBSET cdom G``,
75  HO_MATCH_MP_TAC strong_fsubtyping_ind THEN
76  SRW_TAC [][SUBSET_DEF] THEN
77  TRY (IMP_RES_TAC fsubtyping_wfctxt) THEN
78  FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [wfctxt_MEM, SUBSET_DEF]);
79
80(* define algorithmic sub-typing, with a depth of derivation parameter *)
81val (algn_subtyping_rules, algn_subtyping_ind, algn_subtyping_cases) =
82  Hol_reln`
83    (!Gamma s. wfctxt Gamma /\ ftyFV s SUBSET cdom Gamma ==>
84               algn_subtyping 0 Gamma s Top) /\
85    (!Gamma x. wfctxt Gamma /\ x IN cdom Gamma ==>
86               algn_subtyping 0 Gamma (TyVar x) (TyVar x)) /\
87    (!Gamma x u t n. MEM (x, u) Gamma /\ algn_subtyping n Gamma u t ==>
88                     algn_subtyping (n + 1) Gamma (TyVar x) t) /\
89    (!Gamma t1 s1 t2 s2 n m.
90                 algn_subtyping n Gamma t1 s1 /\
91                 algn_subtyping m Gamma s2 t2 ==>
92                 algn_subtyping (MAX n m + 1) Gamma (Fun s1 s2) (Fun t1 t2)) /\
93    (!Gamma x u1 s2 t2 n.
94                 algn_subtyping n ((x,u1)::Gamma) s2 t2 ==>
95                 algn_subtyping (n + 1) Gamma (ForallTy x u1 s2)
96                                              (ForallTy x u1 t2))
97`;
98
99(* algorithmic sub-typing also respects permutation *)
100val algn_subtyping_fswap = store_thm(
101  "algn_subtyping_fswap",
102  ``!n G ty1 ty2. algn_subtyping n G ty1 ty2 ==>
103                  !x y. algn_subtyping n (ctxtswap x y G)
104                                         (fswap x y ty1)
105                                         (fswap x y ty2)``,
106  HO_MATCH_MP_TAC algn_subtyping_ind THEN REPEAT CONJ_TAC THEN
107  SRW_TAC [][algn_subtyping_rules] THEN
108  METIS_TAC [algn_subtyping_rules, MEM_ctxtswap, fswap_inv,
109             swapTheory.swapstr_inverse]);
110
111(* this equivalence applies more often than the one above; it removes
112   any permutations that might have appeared on the first argument *)
113val algn_subtyping_fswap1_eq = store_thm(
114  "algn_subtyping_fswap1_eq",
115  ``algn_subtyping n G (fswap x y ty1) ty2 =
116    algn_subtyping n (ctxtswap x y G) ty1 (fswap x y ty2)``,
117  METIS_TAC [algn_subtyping_fswap, fswap_inv, ctxtswap_inv]);
118
119val algn_subtyping_wfctxt = store_thm(
120  "algn_subtyping_wfctxt",
121  ``!n G ty1 ty2. algn_subtyping n G ty1 ty2 ==> wfctxt G``,
122  HO_MATCH_MP_TAC algn_subtyping_ind THEN SRW_TAC [][]);
123
124
125(* set up syntax for algorithmic sub-typing relation without the depth
126   parameter *)
127val _ = remove_rules_for_term "dSUB"
128
129val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)),
130                  fixity = Infix(NONASSOC, 425),
131                  paren_style = OnlyIfNecessary,
132                  pp_elements = [HardSpace 1, TOK "|->", BreakSpace(1, 0),
133                                 BeginFinalBlock(PP.INCONSISTENT, 2),
134                                 TM, HardSpace 1, TOK "<:", BreakSpace(1,0)],
135                  term_name = "alg_subtyping"}
136
137val alg_subtyping_def = Define`
138  Gamma |-> s <: t = ?n. algn_subtyping n Gamma s t
139`;
140
141val alg_subtyping_fswap1_eq = store_thm(
142  "alg_subtyping_fswap1_eq",
143  ``Gamma |-> fswap x y ty1 <: ty2 =
144    ctxtswap x y Gamma |-> ty1 <: fswap x y ty2``,
145  METIS_TAC [alg_subtyping_def, algn_subtyping_fswap1_eq]);
146
147fun derive_rule th0 = let
148  val (vs, base) = strip_forall (concl th0)
149  val th = UNDISCH_ALL (SPEC_ALL th0)
150  val (f, args) = strip_comb (concl th)
151  val n = mk_var("n", numSyntax.num)
152  val pattern = mk_exists(n, list_mk_comb(f, n::tl args))
153  val witness = hd args
154  val ex_thm = EXISTS (pattern, witness) th
155  val discharged =
156      GENL vs (DISCH_ALL (REWRITE_RULE [GSYM alg_subtyping_def] ex_thm))
157  val exs_in = SIMP_RULE bool_ss [LEFT_FORALL_IMP_THM,
158                                  LEFT_EXISTS_AND_THM,
159                                  RIGHT_EXISTS_AND_THM] discharged
160in
161  REWRITE_RULE [GSYM alg_subtyping_def] exs_in
162end
163
164val alg_subtyping_rules = save_thm(
165  "alg_subtyping_rules",
166  LIST_CONJ (map derive_rule (CONJUNCTS algn_subtyping_rules)));
167
168(* derive the rule induction principle for algorithmic sub-typing *)
169val alg_subtyping_ind =
170    (Q.GEN `P` o
171     SIMP_RULE (srw_ss()) [GSYM alg_subtyping_def] o
172     CONV_RULE (RAND_CONV
173                  (SWAP_VARS_CONV THENC
174                   BINDER_CONV (SWAP_VARS_CONV THENC
175                                BINDER_CONV (SWAP_VARS_CONV THENC
176                                             BINDER_CONV FORALL_IMP_CONV)))) o
177     SIMP_RULE (srw_ss()) [] o
178     Q.SPEC `\n G ty1 ty2. P G ty1 ty2`) algn_subtyping_ind
179
180(* likewise for the "cases" or inversion theorem *)
181val alg_subtyping_cases =
182    (REWRITE_CONV [alg_subtyping_def] THENC
183     ONCE_REWRITE_CONV [algn_subtyping_cases] THENC
184     SIMP_CONV (srw_ss()) [EXISTS_OR_THM] THENC
185     SIMP_CONV (srw_ss())
186               (map (INST_TYPE [alpha |-> numSyntax.num])
187                    [LEFT_EXISTS_AND_THM, RIGHT_EXISTS_AND_THM]) THENC
188     REWRITE_CONV [GSYM alg_subtyping_def])
189      ``Gamma |-> ty1 <: ty2``
190
191val alg_subtyping_refl (* lemma 28.3.1 *) = store_thm(
192  "alg_subtyping_refl",
193  ``!ty G. wfctxt G /\ ftyFV ty SUBSET cdom G ==> G |-> ty <: ty``,
194  HO_MATCH_MP_TAC fsubty_ind THEN
195  SRW_TAC [][alg_subtyping_rules] THEN
196  Q_TAC (NEW_TAC "z") `cdom G UNION ftyFV ty UNION ftyFV ty'` THEN
197  `ForallTy v ty ty' = ForallTy z ty (fswap z v ty')`
198    by SRW_TAC [][ForallTy_ALPHA] THEN
199  SRW_TAC [][] THEN
200  MATCH_MP_TAC (last (CONJUNCTS alg_subtyping_rules)) THEN
201  SRW_TAC [][alg_subtyping_fswap1_eq] THEN
202  FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
203  FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
204  METIS_TAC [swapTheory.swapstr_def]);
205val _ = export_rewrites ["alg_subtyping_refl"]
206
207val alg_subtyping_top_left = store_thm(
208  "alg_subtyping_top_left",
209  ``!Gamma t. wfctxt Gamma ==> (Gamma |-> Top <: t = (t = Top))``,
210  SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM, alg_subtyping_rules] THEN
211  ONCE_REWRITE_TAC [alg_subtyping_cases] THEN
212  SRW_TAC [][]);
213val _ = export_rewrites ["alg_subtyping_top_left"]
214
215val alg_subtyping_tyvar_right0 = prove(
216  ``!Gamma ty1 ty2. Gamma |-> ty1 <: ty2 ==>
217                    !x. (ty2 = TyVar x) ==>
218                        ?y. ty1 = TyVar y``,
219  HO_MATCH_MP_TAC alg_subtyping_ind THEN SRW_TAC [][]);
220val alg_subtyping_tyvar_right = save_thm(
221  "alg_subtyping_tyvar_right",
222  SIMP_RULE (bool_ss ++ DNF_ss) [] alg_subtyping_tyvar_right0)
223
224val strong_algn_subtyping_ind =
225    IndDefRules.derive_strong_induction (CONJUNCTS algn_subtyping_rules,
226                                         algn_subtyping_ind)
227
228val algn_subtyping_ftyFVs_in_ctxt = store_thm(
229  "algn_subtyping_ftyFVs_in_ctxt",
230  ``!n G ty1 ty2. algn_subtyping n G ty1 ty2 ==>
231                  ftyFV ty1 SUBSET cdom G /\ ftyFV ty2 SUBSET cdom G``,
232  HO_MATCH_MP_TAC strong_algn_subtyping_ind THEN
233  SRW_TAC [][SUBSET_DEF] THEN
234  TRY (IMP_RES_TAC algn_subtyping_wfctxt) THEN
235  FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [cdom_MEM])
236
237val algn_subtyping_swap = store_thm(
238  "algn_subtyping_swap",
239  ``!n G ty1 ty2.
240     algn_subtyping n G ty1 ty2 ==>
241     !x y. algn_subtyping n (ctxtswap x y G) (fswap x y ty1) (fswap x y ty2)``,
242  HO_MATCH_MP_TAC algn_subtyping_ind THEN
243  SRW_TAC [][algn_subtyping_rules] THEN
244  MATCH_MP_TAC (List.nth(CONJUNCTS algn_subtyping_rules, 2)) THEN
245  Q.EXISTS_TAC `fswap x' y ty1` THEN SRW_TAC [][]);
246val algn_subtyping_swap1_eqn = store_thm(
247  "algn_subtyping_swap1_eqn",
248  ``algn_subtyping n G (fswap x y ty1) ty2 =
249    algn_subtyping n (ctxtswap x y G) ty1 (fswap x y ty2)``,
250  METIS_TAC [algn_subtyping_swap, ctxtswap_inv, fswap_inv]);
251
252
253(* important to have this sort of inversion theorem, where you get the
254   same bound variable in the "other" position of the relation.  By
255   analogy, in the lambda calculus with beta reduction, you have to prove
256   that if
257     LAM v bod --> t
258   then
259     ?bod'. (t = LAM v bod') /\ bod --> bod'
260   In the lambda calculus, it's always possible to get this v (which
261   has to do with the fact that beta reduction doesn't produce extra
262   free variables).  In F<:, your x has to satisfy certain constraints.
263*)
264val algn_subtyping_ForallTy_eqn = store_thm(
265  "algn_subtyping_ForallTy_eqn",
266  ``~(x IN ftyFV bnd) /\ ~(x IN cdom G) ==>
267    (algn_subtyping p G (ForallTy x bnd ty) t =
268       wfctxt G /\
269       ((t = Top) /\ (p = 0) /\ ftyFV (ForallTy x bnd ty) SUBSET cdom G \/
270        (?ty' p0. (t = ForallTy x bnd ty') /\ (p = p0 + 1) /\
271                  algn_subtyping p0 ((x,bnd)::G) ty ty')))``,
272  SIMP_TAC (srw_ss() ++ DNF_ss ++ SatisfySimps.SATISFY_ss)
273           [EQ_IMP_THM, algn_subtyping_rules, algn_subtyping_wfctxt] THEN
274  STRIP_TAC THEN
275  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [algn_subtyping_cases])) THEN
276  SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [ForallTy_11] THEN
277  Q.EXISTS_TAC `fswap x x' t2` THEN
278  `wfctxt ((x',u1)::G)` by METIS_TAC [algn_subtyping_wfctxt] THEN
279  FULL_SIMP_TAC (srw_ss()) [algn_subtyping_swap1_eqn] THEN
280  `ftyFV t2 SUBSET cdom ((x',u1)::G)`
281     by METIS_TAC [algn_subtyping_ftyFVs_in_ctxt] THEN
282  Cases_on `x = x'` THEN1 SRW_TAC [][] THEN
283  `~(x' IN ftyFV u1) /\ ~(x IN ftyFV t2)`
284     by METIS_TAC [SUBSET_DEF, cdom_def, pairTheory.FST, IN_INSERT] THEN
285  SRW_TAC [][ctxtswap_fresh, fswap_fresh, wfctxt_ctxtFV_cdom]);
286
287val algn_subtyping_trans = prove(
288  ``!n m p Gamma s q t.
289         (n = m + p) /\
290         algn_subtyping m Gamma s q /\
291         algn_subtyping p Gamma q t ==>
292         ?r. algn_subtyping r Gamma s t``,
293  HO_MATCH_MP_TAC arithmeticTheory.COMPLETE_INDUCTION THEN
294  REPEAT STRIP_TAC THEN
295  Q.PAT_ASSUM `algn_subtyping m Gamma s q`
296              (MP_TAC o ONCE_REWRITE_RULE [algn_subtyping_cases]) THEN
297  SRW_TAC [][] THENL [
298    METIS_TAC [alg_subtyping_def, alg_subtyping_top_left,
299               algn_subtyping_rules],
300    METIS_TAC [],
301    FULL_SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN
302    `?r. algn_subtyping r Gamma u t`
303       by METIS_TAC [DECIDE ``n + p < n + 1 + p``] THEN
304    METIS_TAC [algn_subtyping_rules],
305    Q.PAT_ASSUM `algn_subtyping p Gamma (Fun t1 t2) t`
306                (MP_TAC o ONCE_REWRITE_RULE [algn_subtyping_cases]) THEN
307    SRW_TAC [][] THEN1 METIS_TAC [algn_subtyping_rules,
308                                  algn_subtyping_ftyFVs_in_ctxt] THEN
309    FULL_SIMP_TAC (srw_ss() ++ DNF_ss) [AND_IMP_INTRO] THEN
310    `?r. algn_subtyping r Gamma t1' s1`
311        by (FIRST_X_ASSUM MATCH_MP_TAC THEN
312            MAP_EVERY Q.EXISTS_TAC [`n'`, `n`, `t1`] THEN
313            ASM_SIMP_TAC arith_ss [arithmeticTheory.MAX_DEF]) THEN
314    `?r'. algn_subtyping r' Gamma s2 t2'`
315        by (FIRST_X_ASSUM MATCH_MP_TAC THEN
316            MAP_EVERY Q.EXISTS_TAC [`m'`, `m`, `t2`] THEN
317            ASM_SIMP_TAC arith_ss [arithmeticTheory.MAX_DEF]) THEN
318    METIS_TAC [algn_subtyping_rules],
319    `wfctxt ((x,u1)::Gamma)` by METIS_TAC [algn_subtyping_wfctxt] THEN
320    FULL_SIMP_TAC (srw_ss()) [] THEN
321    `~(x IN ftyFV u1)` by METIS_TAC [SUBSET_DEF] THEN
322    Q.PAT_ASSUM `algn_subtyping p Gamma (ForallTy x u1 t2) t` MP_TAC THEN
323    ASM_SIMP_TAC (srw_ss()) [algn_subtyping_ForallTy_eqn] THEN
324    SRW_TAC [][] THENL [
325      (* case where it's less than Top *)
326      IMP_RES_TAC algn_subtyping_ftyFVs_in_ctxt THEN
327      FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [],
328      ALL_TAC
329    ] THEN
330    SRW_TAC [][ForallTy_11] THEN
331    METIS_TAC [DECIDE ``n + p0 < n + 1 + (p0 + 1)``]
332  ]);
333
334val alg_subtyping_trans (* lemma 28.3.2 *) = store_thm(
335  "alg_subtyping_trans",
336  ``!Gamma s q. Gamma |-> s <: q /\ Gamma |-> q <: t ==>
337                Gamma |-> s <: t``,
338  METIS_TAC [alg_subtyping_def, algn_subtyping_trans]);
339
340val alg_soundcomplete (* theorem 28.3.3 *) = store_thm(
341  "alg_soundcomplete",
342  ``G |- ty1 <: ty2 = G |-> ty1 <: ty2``,
343  EQ_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`ty2`, `ty1`, `G`] THENL [
344    HO_MATCH_MP_TAC fsubtyping_ind THEN SRW_TAC [][alg_subtyping_rules] THENL [
345      METIS_TAC [alg_subtyping_trans],
346      `Gamma |-> ty <: ty`
347         by METIS_TAC [alg_subtyping_refl, wfctxt_MEM, SUBSET_DEF] THEN
348      METIS_TAC [alg_subtyping_rules]
349    ],
350    HO_MATCH_MP_TAC alg_subtyping_ind THEN SRW_TAC [][fsubtyping_rules] THEN
351    METIS_TAC [fsubtyping_rules, wfctxt_MEM, SUBSET_DEF,
352               fsubtyping_wfctxt]
353  ]);
354
355val _ = export_theory ();
356