bnfMutualScript.sml
1Theory bnfMutual[bare]
2Ancestors
3 bnfFixBNF pred_set
4Libs
5 HolKernel Parse boolLib BasicProvers simpLib boolSimps metisLib numLib
6 pred_setLib pairLib QLib TotalDefn[qualified]
7
8(* ----------------------------------------------------------------------
9 bossLib is not built yet — the package has to be, so that Datatype
10 can use it, and so this is the part of bossLib's environment these
11 proofs need. The same emulation cardinalScript uses.
12 ---------------------------------------------------------------------- *)
13
14fun simp ths = simpLib.ASM_SIMP_TAC (srw_ss()) ths
15fun csimp ths = simp (SF CONJ_ss :: ths)
16fun dsimp ths = simp (SF DNF_ss :: ths)
17fun gs ths = simpLib.global_simp_tac
18 {elimvars = false, strip = true, droptrues = true,
19 oldestfirst = true} (srw_ss()) ths
20fun gvs ths = simpLib.global_simp_tac
21 {elimvars = true, strip = true, droptrues = true,
22 oldestfirst = true} (srw_ss()) ths
23fun rw ths = BasicProvers.SRW_TAC [] ths
24val metis_tac = metisLib.METIS_TAC
25fun SRULE ths th = SIMP_RULE (srw_ss()) ths th
26val qexists = Q.EXISTS_TAC
27val op >~ = Q.>~
28val op >>~ = Q.>>~
29
30
31(* ----------------------------------------------------------------------
32 Mutual recursion, from nested recursion.
33
34 A mutually recursive pair arrives from the specification as one
35 functor per type with the sibling as an extra argument:
36
37 T1 = F1(T1, T2) T2 = F2(T2, T1)
38
39 Nothing new has to be constructed for it. Take T2's fixed point with
40 the *sibling's* slot left as a parameter — an ordinary datatype,
41 T2' α — and then define
42
43 T1 = μβ. F1(β, T2' β) T2 = T2' T1
44
45 which is a recursion nested through T2', and that already works. What
46 is left is to turn the nested recursion principle for T1, and T2''s
47 own, into the principle for the pair, and that is what is proved here
48 — once, over parameters, so no datatype replays it.
49
50 Throughout, 'n1 and 'n2 are the two types and 'c1 and 'c2 the answer
51 types a pair of functions maps them to; 'm2 is T2' 'c1, the sibling's
52 type over the answers rather than over T1. smap is T2''s map in that
53 argument, which is where the two recursions meet.
54 ---------------------------------------------------------------------- *)
55
56(* the equations a pair of functions defined by mutual recursion
57 satisfies: each type's constructor takes a value of that type's functor,
58 whose occurrences of *either* type have been mapped by the
59 corresponding function *)
60Definition MUTREC_def:
61 bnfMUTREC (cn1 : 'fn1 -> 'n1) (cn2 : 'fn2 -> 'n2) mpK mpQ t1 t2 h1 h2 ⇔
62 (∀af. h1 (cn1 af) = t1 (mpK h1 h2 af)) ∧
63 (∀af. h2 (cn2 af) = t2 (mpQ h1 h2 af))
64End
65
66(* the recursion principle a type's own construction produced, as a
67 predicate: the map is the one over that type's functor, so the
68 hypotheses below can name it *)
69Definition SREC_def:
70 bnfSREC (cn : 'f -> 'n) (mp : ('n -> 'c) -> 'f -> 'g) ⇔
71 ∀t. ∃!h. ∀af. h (cn af) = t (mp h af)
72End
73
74(* and the sibling's map, at every function it might be given: not
75 bnfFIXMAP, because the map operator here is the sibling's map itself
76 rather than a parameter to be solved for *)
77Definition SMAP_def:
78 bnfSMAP (cn2 : 'fn2 -> 'n2) cm2 mpBg smap ⇔
79 ∀g af. smap g (cn2 af) = cm2 (mpBg g af)
80End
81
82(* the principle a pair of types has once the reduction is done: for any
83 pair of target functions there is exactly one pair of functions
84 satisfying the two equations *)
85Definition MUTITER_def:
86 bnfMUTITER (cn1 : 'fn1 -> 'n1) (cn2 : 'fn2 -> 'n2) mpK mpQ ⇔
87 ∀t1 t2.
88 (∃h1 h2. bnfMUTREC cn1 cn2 mpK mpQ t1 t2 h1 h2) ∧
89 ∀h1 h2 k1 k2.
90 bnfMUTREC cn1 cn2 mpK mpQ t1 t2 h1 h2 ∧
91 bnfMUTREC cn1 cn2 mpK mpQ t1 t2 k1 k2 ⇒ h1 = k1 ∧ h2 = k2
92End
93
94(* Mapping a functor's own argument and then the sibling's answers is
95 mapping both at once, with the sibling's map composed in. Both
96 functors need this, in the same shape: for F1 the first map is its own
97 recursion, and for F2 it is the sibling's map at the same time. *)
98Definition MUTMAP_def:
99 bnfMUTMAP (mpG : ('n1 -> 'c1) -> 'fn1 -> 'fg1) mpH mpK smap ⇔
100 ∀g k af. mpH k (mpG g af) = mpK g (k o smap g) af
101End
102
103(* the two functors' composition laws, as rewrites in either direction:
104 the map through the sibling is what has to be introduced on one side
105 and eliminated on the other *)
106val f1fwd = qpat_assum ‘bnfMUTMAP mpG mpH mpK smap’
107 (fn th => REWRITE_TAC[SRULE [MUTMAP_def] th])
108val f1bwd = qpat_assum ‘bnfMUTMAP mpG mpH mpK smap’
109 (fn th => REWRITE_TAC[GSYM (SRULE [MUTMAP_def] th)])
110val f2bwd = qpat_assum ‘bnfMUTMAP mpBg mp2c mpQ smap’
111 (fn th => REWRITE_TAC[GSYM (SRULE [MUTMAP_def] th)])
112
113(* mapping a functor's own argument and the sibling's separately is
114 mapping both at once *)
115Definition MUTSPLIT_def:
116 bnfMUTSPLIT (mpQ : ('n1 -> 'c1) -> ('n2 -> 'c2) -> 'fn2 -> 'fc2) mp1a mp2n ⇔
117 ∀g k af. mpQ g k af = mp1a g (mp2n k af)
118End
119
120Theorem MUTUAL_RECURSION:
121 (* T1's recursion, nested through the sibling *)
122 bnfSREC cn1 mpG ∧
123 (* the sibling's own recursion, over the answers and over T1 *)
124 bnfSREC cm2 mp2c ∧ bnfSREC cn2 mp2n ∧
125 (* the sibling's map, and the functors' composition laws *)
126 bnfSMAP cn2 cm2 mpBg smap ∧
127 bnfMUTMAP mpG mpH mpK smap ∧ bnfMUTMAP mpBg mp2c mpQ smap ∧
128 bnfMUTSPLIT mpQ mp1a mp2n ⇒
129 bnfMUTITER cn1 cn2 mpK mpQ
130Proof
131 simp[MUTITER_def] >> strip_tac >>
132 (* the predicates are there so that a driver's facts can be matched
133 against them; the proof wants what they say *)
134 RULE_ASSUM_TAC (PURE_REWRITE_RULE [SREC_def, SMAP_def, MUTSPLIT_def]) >>
135 rpt gen_tac >>
136 (* the fold over the sibling's structure that the answers call for *)
137 qpat_assum ‘∀s. ∃!k. ∀af. k (cm2 af) = s (mp2c k af)’
138 (qspec_then ‘t2’ (strip_assume_tac o SRULE[EXISTS_UNIQUE_THM])) >>
139 rename [‘∀af. fold (cm2 af) = t2 (mp2c fold af)’] >>
140 (* whatever T1's function is, the sibling's is that fold after it *)
141 ‘∀g af. (fold o smap g) (cn2 af) = t2 (mpQ g (fold o smap g) af)’
142 by (rpt gen_tac >> f2bwd >> simp[]) >>
143 ‘∀h1 h2. (∀af. h2 (cn2 af) = t2 (mpQ h1 h2 af)) ⇒ h2 = fold o smap h1’
144 by (rpt strip_tac >>
145 qpat_assum ‘∀s. ∃!k. ∀af. k (cn2 af) = s (mp2n k af)’
146 (qspec_then ‘t2 o mp1a h1’
147 (strip_assume_tac o SRULE[EXISTS_UNIQUE_THM])) >>
148 first_x_assum irule >> simp[]) >>
149 (* and T1's is the solution of its own recursion at that fold *)
150 qpat_assum ‘∀t. ∃!h. ∀af. h (cn1 af) = t (mpG h af)’
151 (qspec_then ‘t1 o mpH fold’
152 (strip_assume_tac o SRULE[EXISTS_UNIQUE_THM])) >>
153 rename [‘∀af. hh (cn1 af) = t1 (mpH fold (mpG hh af))’] >>
154 (* so there is only one solution, and this is it *)
155 ‘∀h1 h2. bnfMUTREC cn1 cn2 mpK mpQ t1 t2 h1 h2 ⇒
156 h1 = hh ∧ h2 = fold o smap hh’
157 by (simp[MUTREC_def] >> rpt gen_tac >> strip_tac >>
158 ‘h2 = fold o smap h1’
159 by (qpat_assum ‘∀h1 h2. (∀af. h2 (cn2 af) = _) ⇒ _’ irule >>
160 simp[]) >>
161 ‘h1 = hh’
162 by (qpat_assum ‘∀h h'. (∀af. h (cn1 af) = t1 (mpH fold _)) ∧ _ ⇒ _’
163 irule >> simp[] >> qx_gen_tac ‘af’ >> f1fwd >> simp[]) >>
164 simp[]) >>
165 conj_tac
166 >- (qexistsl_tac [‘hh’, ‘fold o smap hh’] >> simp[MUTREC_def] >>
167 qx_gen_tac ‘af’ >> f1bwd >> simp[]) >>
168 rpt gen_tac >> strip_tac >> res_tac >> simp[]
169QED
170
171(* ----------------------------------------------------------------------
172 Mutual induction.
173
174 Each type's own principle covers *its* sub-terms, and the two are
175 tied together by the second type's set function for the first type's
176 slot: the values of one type inside a value of the other. What the
177 pair's principle needs beyond the two is that this set decomposes the
178 way the nesting says — the first type's own sub-terms are its direct
179 occurrences together with those the sibling holds.
180 ---------------------------------------------------------------------- *)
181
182Definition NESTSET_def:
183 bnfNESTSET (stn1 : 'fn1 -> 'n1 set) sb1 sa1 S21 ⇔
184 ∀af. stn1 af = sb1 af ∪ BIGUNION (IMAGE S21 (sa1 af))
185End
186
187Theorem MUTUAL_INDUCTION:
188 bnfFIXIND cn1 stn1 ∧ bnfFIXIND cn2 st2 ∧
189 bnfNESTSET stn1 sb1 sa1 S21 ∧ bnfFIXSET cn2 st2 sb2 S21 ⇒
190 ∀P1 P2.
191 (∀af. (∀y. y ∈ sb1 af ⇒ P1 y) ∧ (∀z. z ∈ sa1 af ⇒ P2 z) ⇒ P1 (cn1 af)) ∧
192 (∀af. (∀y. y ∈ sb2 af ⇒ P1 y) ∧ (∀z. z ∈ st2 af ⇒ P2 z) ⇒ P2 (cn2 af)) ⇒
193 (∀n. P1 n) ∧ ∀m. P2 m
194Proof
195 strip_tac >>
196 RULE_ASSUM_TAC (PURE_REWRITE_RULE [FIXIND_def, FIXSET_def, NESTSET_def]) >>
197 rpt gen_tac >> strip_tac >>
198 (* a value of the second type satisfies P2 once the first type's values
199 inside it satisfy P1 — which is its own induction *)
200 ‘∀m. (∀y. y ∈ S21 m ⇒ P1 y) ⇒ P2 m’
201 by (qpat_assum ‘∀P. (∀af. (∀z. z ∈ st2 af ⇒ P z) ⇒ P (cn2 af)) ⇒ ∀m. P m’
202 ho_match_mp_tac >>
203 rpt strip_tac >>
204 qpat_assum ‘∀af. (∀y. y ∈ sb2 af ⇒ P1 y) ∧ _ ⇒ _’ irule >> conj_tac
205 >- (rpt strip_tac >>
206 qpat_assum ‘∀y. y ∈ S21 (cn2 af) ⇒ P1 y’ irule >> simp[]) >>
207 rpt strip_tac >>
208 qpat_assum ‘∀m. m ∈ st2 af ⇒ _ ⇒ P2 m’ (drule_then irule) >>
209 rpt strip_tac >>
210 qpat_assum ‘∀y. y ∈ S21 (cn2 af) ⇒ P1 y’ irule >> simp[] >>
211 disj2_tac >> qexists_tac ‘S21 z’ >> simp[] >> qexists_tac ‘z’ >>
212 simp[]) >>
213 (* and then the first type's own induction covers both *)
214 ‘∀n. P1 n’
215 by (qpat_assum ‘∀P. (∀af. (∀y. y ∈ stn1 af ⇒ P y) ⇒ P (cn1 af)) ⇒ ∀n. P n’
216 ho_match_mp_tac >>
217 rpt strip_tac >>
218 qpat_assum ‘∀af. (∀y. y ∈ sb1 af ⇒ P1 y) ∧ _ ⇒ _’ irule >> conj_tac
219 >- (rpt strip_tac >>
220 qpat_assum ‘∀y. y ∈ stn1 af ⇒ P1 y’ irule >> simp[]) >>
221 rpt strip_tac >>
222 qpat_assum ‘∀m. (∀y. y ∈ S21 m ⇒ P1 y) ⇒ P2 m’ irule >>
223 rpt strip_tac >>
224 qpat_assum ‘∀y. y ∈ stn1 af ⇒ P1 y’ irule >> simp[] >>
225 disj2_tac >> qexists_tac ‘S21 z’ >> simp[] >> qexists_tac ‘z’ >>
226 simp[]) >>
227 simp[]
228QED
229
230(* ----------------------------------------------------------------------
231 Primitive recursion for the pair.
232
233 The principle above is an iterator: each function only ever sees the
234 results of the recursive calls. HOL's datatype axioms hand the
235 function the constructor's arguments as well, and the two are bridged
236 by the standard pairing trick — iterate into 'n1 # 'c1 and 'n2 # 'c2,
237 rebuilding the arguments alongside the answers, and observe that
238 rebuilding is the identity because it and the constructors solve the
239 same iteration. Both types go through it at once, so the maps here
240 take a function per type rather than one.
241 ---------------------------------------------------------------------- *)
242
243Definition MapId2_def:
244 bnfMapId2 (mp : ('a -> 'a) -> ('b -> 'b) -> 'f -> 'f) ⇔ ∀x. mp I I x = x
245End
246
247Definition MapComp2_def:
248 bnfMapComp2 (mp_ab : ('a1 -> 'b1) -> ('a2 -> 'b2) -> 'f -> 'g)
249 (mp_bc : ('b1 -> 'c1) -> ('b2 -> 'c2) -> 'g -> 'h)
250 (mp_ac : ('a1 -> 'c1) -> ('a2 -> 'c2) -> 'f -> 'h) ⇔
251 ∀f1 f2 g1 g2 x. mp_bc g1 g2 (mp_ab f1 f2 x) = mp_ac (g1 o f1) (g2 o f2) x
252End
253
254Theorem MUTUAL_PRIM_REC:
255 bnfMUTITER cn1 cn2
256 (mpq1 : ('n1 -> 'n1 # 'c1) -> ('n2 -> 'n2 # 'c2) -> 'fn1 -> 'fq1)
257 mpq2 ∧
258 bnfMUTITER cn1 cn2 mpn1 mpn2 ∧
259 bnfMapComp2 mpq1 mpqn1 mpn1 ∧ bnfMapComp2 mpq1 mpqc1 mpc1 ∧ bnfMapId2 mpn1 ∧
260 bnfMapComp2 mpq2 mpqn2 mpn2 ∧ bnfMapComp2 mpq2 mpqc2 mpc2 ∧ bnfMapId2 mpn2 ⇒
261 ∀t1 t2.
262 (∃(h1 : 'n1 -> 'c1) (h2 : 'n2 -> 'c2).
263 (∀af. h1 (cn1 af) = t1 af (mpc1 h1 h2 af)) ∧
264 (∀af. h2 (cn2 af) = t2 af (mpc2 h1 h2 af))) ∧
265 ∀h1 h2 k1 k2.
266 ((∀af. h1 (cn1 af) = t1 af (mpc1 h1 h2 af)) ∧
267 (∀af. h2 (cn2 af) = t2 af (mpc2 h1 h2 af))) ∧
268 ((∀af. k1 (cn1 af) = t1 af (mpc1 k1 k2 af)) ∧
269 (∀af. k2 (cn2 af) = t2 af (mpc2 k1 k2 af))) ⇒ h1 = k1 ∧ h2 = k2
270Proof
271 strip_tac >> rpt gen_tac >>
272 (* the paired iterator: alongside the answer it rebuilds its argument *)
273 qpat_assum ‘bnfMUTITER cn1 cn2 mpq1 mpq2’
274 (fn th =>
275 qspecl_then
276 [‘λv. (cn1 (mpqn1 FST FST v),
277 t1 (mpqn1 FST FST v) (mpqc1 SND SND v))’,
278 ‘λv. (cn2 (mpqn2 FST FST v),
279 t2 (mpqn2 FST FST v) (mpqc2 SND SND v))’]
280 (strip_assume_tac o SRULE [])
281 (SRULE [MUTITER_def, MUTREC_def] th)) >>
282 (* and rebuilding is the identity: it and the constructors solve the
283 iteration at the types themselves, which has one solution *)
284 qpat_assum ‘bnfMUTITER cn1 cn2 mpn1 mpn2’
285 (fn th =>
286 qspecl_then [‘cn1’, ‘cn2’] (strip_assume_tac o SRULE [])
287 (SRULE [MUTITER_def, MUTREC_def] th)) >>
288 ‘FST o h1 = I ∧ FST o h2 = I’
289 by (qpat_x_assum ‘∀h1 h2 k1 k2. _ ∧ _ ⇒ h1 = k1 ∧ h2 = k2’
290 (qspecl_then [‘FST o h1’, ‘FST o h2’, ‘I’, ‘I’] mp_tac) >>
291 impl_tac >- (rpt conj_tac >> gen_tac >> simp[] >>
292 gs[MapId2_def, MapComp2_def]) >>
293 simp[]) >>
294 conj_tac
295 >- (qexistsl_tac [‘SND o h1’, ‘SND o h2’] >> rpt conj_tac >> gen_tac >>
296 simp[] >> gs[MapComp2_def] >> gs[MapId2_def]) >>
297 (* uniqueness: a solution paired with the identity solves the paired
298 iteration, and those solutions are unique *)
299 ‘∀g1 g2. (∀af. g1 (cn1 af) = t1 af (mpc1 g1 g2 af)) ∧
300 (∀af. g2 (cn2 af) = t2 af (mpc2 g1 g2 af)) ⇒
301 h1 = (λx. (x, g1 x)) ∧ h2 = (λx. (x, g2 x))’
302 by (rpt gen_tac >> strip_tac >>
303 qpat_assum ‘∀h1 h2 k1 k2. _ ∧ _ ⇒ h1 = k1 ∧ h2 = k2’
304 (qspecl_then [‘h1’, ‘h2’, ‘λx. (x, g1 x)’, ‘λx. (x, g2 x)’]
305 mp_tac) >>
306 impl_tac
307 >- (simp[] >> gs[MapComp2_def] >>
308 simp[combinTheory.o_DEF, GSYM combinTheory.I_EQ_IDABS, ETA_AX] >>
309 gs[MapId2_def]) >>
310 simp[]) >>
311 qx_genl_tac [‘g1’, ‘g2’, ‘j1’, ‘j2’] >> strip_tac >>
312 ‘(λx. (x, g1 x)) = (λx. (x, j1 x)) ∧ (λx. (x, g2 x)) = (λx. (x, j2 x))’
313 by metis_tac[] >>
314 gs[FUN_EQ_THM]
315QED