errorStateMonadScript.sml

1Theory errorStateMonad
2Ancestors
3  pair combin option list
4Libs
5  pairSyntax simpLib BasicProvers boolSimps metisLib BasicProvers
6
7(* ------------------------------------------------------------------------- *)
8(* Definitions.                                                              *)
9(* ------------------------------------------------------------------------- *)
10
11Type M[local] = “:'state -> ('a # 'state) option”
12
13Definition UNIT_DEF:   UNIT (x:'b) : ('b,'a) M = \(s:'a). SOME (x, s)
14End
15
16Definition BIND_DEF:
17  BIND (g: ('b, 'a) M) (f: 'b -> ('c, 'a) M) (s0:'a) =
18    case g s0 of
19      NONE => NONE
20    | SOME (b,s) => f b s
21End
22
23Definition IGNORE_BIND_DEF:
24  IGNORE_BIND (f:('a,'b)M) (g:('c,'b)M) : ('c,'b)M = BIND f (\x. g)
25End
26
27Definition MMAP_DEF:   MMAP (f: 'c -> 'b) (m: ('c, 'a) M) = BIND m (UNIT o f)
28End
29
30Definition JOIN_DEF:   JOIN (z: (('b, 'a) M, 'a) M) = BIND z I
31End
32
33Definition EXT_DEF:   EXT g m = BIND m g
34End
35
36(* composition in the Kleisli category:
37  can compose any monad with the state transformer monad in this way *)
38Definition MCOMP_DEF:   MCOMP g f = CURRY (OPTION_MCOMP (UNCURRY g) (UNCURRY f))
39End
40
41Definition FOR_def:
42 (FOR : num # num # (num -> (unit, 'state) M) -> (unit, 'state) M) (i, j, a) =
43     if i = j then
44        a i
45     else
46        BIND (a i) (\u. FOR (if i < j then i + 1 else i - 1, j, a))
47Termination
48  WF_REL_TAC `measure (\(i, j, a). if i < j then j - i else i - j)`
49End
50
51Definition FOREACH_def:
52   ((FOREACH : 'a list # ('a -> (unit, 'state) M) -> (unit, 'state) M) ([], a) =
53       UNIT ()) /\
54   (FOREACH (h :: t, a) = BIND (a h) (\u. FOREACH (t, a)))
55End
56
57Definition READ_def:
58   (READ : ('state -> 'a) -> ('a, 'state) M) f = \s. SOME (f s, s)
59End
60
61Definition WRITE_def:
62   (WRITE : ('state -> 'state) -> (unit, 'state) M) f = \s. SOME ((), f s)
63End
64
65Definition NARROW_def:
66   (NARROW : 'b -> ('a, 'b # 'state) M -> ('a, 'state) M) v f =
67   \s. case f (v, s) of
68           NONE => NONE
69         | SOME (r, s1) => SOME (r, SND s1)
70End
71
72Definition WIDEN_def:
73   (WIDEN : ('a, 'state) M -> ('a, 'b # 'state) M) f =
74   \(s1, s2). case f s2 of
75                  NONE => NONE
76                | SOME (r, s3) => SOME (r, (s1, s3))
77End
78
79Definition sequence_def:
80   sequence = FOLDR (\m ms. BIND m (\x. BIND ms (\xs. UNIT (x::xs)))) (UNIT [])
81End
82
83Definition mapM_def:
84   mapM f = sequence o MAP f
85End
86
87Definition mwhile_step_def:
88  mwhile_step P g x 0 s = BIND (P x) (\b. UNIT (b,x)) s /\
89  mwhile_step P g x (SUC n) s = BIND (P x)
90    (\b. if b then BIND (g x) (\gx. mwhile_step P g gx n) else UNIT (b,x)) s
91End
92
93Theorem mwhile_exists[local]:
94  !P g. ?f .
95    !x s. f x s = BIND (P x) (\b. if b then BIND (g x) f else UNIT x) s
96Proof
97  qx_gen_tac `P` >> qx_gen_tac `g` >>
98  qexists_tac `\x s.
99    if ?n. !y t. mwhile_step P g x n s <> SOME ((T,y), t) then
100      let n = @n. !y t. mwhile_step P g x n s <> SOME ((T,y), t) /\
101        !m. m < n ==> ?y t. mwhile_step P g x m s = SOME ((T,y), t) in
102      case mwhile_step P g x n s of NONE => NONE | SOME ((_,y),t) => SOME (y,t)
103    else ARB` >>
104  qx_gen_tac `x` >> qx_gen_tac `s` >> BETA_TAC >>
105  reverse (IF_CASES_TAC)
106  >- (
107    fs[BIND_DEF, UNIT_DEF, COND_RATOR] >>
108    first_assum (qspec_then `0` assume_tac) >>
109    fs[mwhile_step_def, BIND_DEF, UNIT_DEF] >>
110    full_case_tac >> fs[] >> full_case_tac >> fs[] >>
111    rpt (var_eq_tac) >>
112    first_assum (qspec_then `SUC 0` assume_tac) >>
113    fs[mwhile_step_def, BIND_DEF, UNIT_DEF] >> rfs[BIND_DEF] >>
114    full_case_tac >> fs[] >> full_case_tac >> fs[] >>
115    IF_CASES_TAC >> simp[LET_DEF] >>
116    pop_assum (qx_choose_then `n` assume_tac) >>
117    first_x_assum (qspec_then `SUC n` assume_tac) >>
118    fs[mwhile_step_def, BIND_DEF, UNIT_DEF] >> rfs[BIND_DEF]
119    ) >>
120  pop_assum (qx_choose_then `n` assume_tac) >>
121  SELECT_ELIM_TAC >> conj_tac
122  >- (
123    completeInduct_on `n` >> strip_tac >>
124    Cases_on `!m. m < n ==> ?y t. mwhile_step P g x m s = SOME ((T,y), t)` >>
125    fs[BIND_DEF, mwhile_step_def] >- (qexists_tac `n` >> fs[]) >>
126    first_x_assum irule >> goal_assum drule >>
127    asm_rewrite_tac []
128    ) >>
129  fs[BIND_DEF, UNIT_DEF, COND_RATOR, LET_DEF] >>
130  pop_assum kall_tac >> qx_gen_tac `n` >> rpt strip_tac >>
131  fs[GSYM PULL_FORALL] >> Cases_on `n`
132  >- (
133    fs[mwhile_step_def, BIND_DEF, UNIT_DEF] >>
134    Cases_on `P x s` >> simp[] >> rename1 `P x s = SOME y` >>
135    PairCases_on `y` >> fs[]
136    ) >>
137  rename1 `SUC n` >> fs[mwhile_step_def, BIND_DEF, UNIT_DEF, COND_RATOR] >>
138  Cases_on `P x s` >> simp[] >>
139  rename1 `P x s = SOME y` >> PairCases_on `y` >> Cases_on `y0` >> fs[] >>
140  Cases_on `g x y1` >> fs[] >> rename1 `g x y1 = SOME z` >>
141  PairCases_on `z` >> fs[] >>
142  reverse (IF_CASES_TAC)
143  >- (fs[] >> pop_assum (qspec_then `n` assume_tac) >> rfs[]) >>
144  SELECT_ELIM_TAC >> conj_tac
145  >- (
146    ntac 4 (last_x_assum kall_tac) >>
147    pop_assum (qx_choose_then `n` assume_tac) >>
148    completeInduct_on `n` >> strip_tac >>
149    Cases_on `!m. m < n ==> ?y t. mwhile_step P g z0 m z1 = SOME ((T,y),t)`
150    >- (goal_assum drule >> fs[]) >>
151    pop_assum mp_tac >> simp[]
152    ) >>
153  qx_gen_tac `m` >> strip_tac >>
154  qsuff_tac `m = n` >> fs[] >>
155  fs[arithmeticTheory.EQ_LESS_EQ, GSYM arithmeticTheory.NOT_LESS] >>
156  conj_tac >> CCONTR_TAC >> fs[]
157  >- (first_x_assum drule >> strip_tac >> rfs[]) >>
158  last_x_assum (qspec_then `SUC m` assume_tac) >>
159  rfs[mwhile_step_def, BIND_DEF, UNIT_DEF]
160QED
161
162val MWHILE_DEF = new_specification(
163  "MWHILE_DEF", ["MWHILE"],
164  mwhile_exists |> SIMP_RULE bool_ss [SKOLEM_THM]);
165
166Definition mwhile_unit_step_def:
167  mwhile_unit_step P g 0 s = P s /\
168  mwhile_unit_step P g (SUC n) s = BIND P
169    (\b. if b then IGNORE_BIND g (mwhile_unit_step P g n) else UNIT b) s
170End
171
172Theorem mwhile_unit_exists[local]:
173  !P g. ?f. !s.
174    f s = BIND P (\b. if b then IGNORE_BIND g f else UNIT ()) s
175Proof
176  qx_gen_tac `P` >> qx_gen_tac `g` >>
177  qexists_tac `\s.
178    if ?n. !t. mwhile_unit_step P g n s <> SOME (T, t) then
179      let n = @n. !t. mwhile_unit_step P g n s <> SOME (T, t) /\
180        !m. m < n ==> ?t. mwhile_unit_step P g m s = SOME (T, t) in
181      case mwhile_unit_step P g n s of NONE => NONE | SOME (_,t) => SOME ((),t)
182    else ARB` >>
183  qx_gen_tac `s` >> BETA_TAC >>
184  reverse (IF_CASES_TAC)
185  >- (
186    fs[BIND_DEF, UNIT_DEF, COND_RATOR] >>
187    first_assum (qspec_then `0` assume_tac) >>
188    fs[mwhile_unit_step_def, BIND_DEF, IGNORE_BIND_DEF, UNIT_DEF] >>
189    first_assum (qspec_then `SUC 0` assume_tac) >>
190    fs[mwhile_unit_step_def, BIND_DEF, UNIT_DEF, COND_RATOR, IGNORE_BIND_DEF] >>
191    rfs[] >> full_case_tac >> fs[] >> full_case_tac >> fs[] >>
192    IF_CASES_TAC >> simp[] >>
193    pop_assum (qx_choose_then `n` assume_tac) >>
194    first_x_assum (qspec_then `SUC n` assume_tac) >>
195    fs[mwhile_unit_step_def, BIND_DEF, IGNORE_BIND_DEF, UNIT_DEF, COND_RATOR] >>
196    rfs[]
197    ) >>
198  pop_assum (qx_choose_then `n` assume_tac) >>
199  SELECT_ELIM_TAC >> conj_tac
200  >- (
201    completeInduct_on `n` >> strip_tac >>
202    Cases_on `!m. m < n ==> ?t. mwhile_unit_step P g m s = SOME (T, t)` >>
203    fs[BIND_DEF, mwhile_unit_step_def] >- (qexists_tac `n` >> fs[]) >>
204    first_x_assum irule >> goal_assum drule >>
205    asm_rewrite_tac []
206    ) >>
207  fs[BIND_DEF, UNIT_DEF, COND_RATOR, IGNORE_BIND_DEF] >>
208  pop_assum kall_tac >> qx_gen_tac `n` >> rpt strip_tac >>
209  fs[GSYM PULL_FORALL] >> Cases_on `n`
210  >- (
211    fs[mwhile_unit_step_def, BIND_DEF, UNIT_DEF] >>
212    Cases_on `P s` >> simp[] >> rename1 `P s = SOME y` >>
213    PairCases_on `y` >> fs[]
214    ) >>
215  rename1 `SUC n` >>
216  fs[mwhile_unit_step_def, BIND_DEF, UNIT_DEF, COND_RATOR, IGNORE_BIND_DEF] >>
217  Cases_on `P s` >> simp[] >>
218  rename1 `P s = SOME y` >> PairCases_on `y` >> Cases_on `y0` >> fs[] >>
219  Cases_on `g y1` >> fs[] >> rename1 `g y1 = SOME z` >>
220  PairCases_on `z` >> fs[] >>
221  reverse (IF_CASES_TAC)
222  >- (fs[] >> pop_assum (qspec_then `n` assume_tac) >> rfs[]) >>
223  SELECT_ELIM_TAC >> conj_tac
224  >- (
225    ntac 4 (last_x_assum kall_tac) >>
226    pop_assum (qx_choose_then `n` assume_tac) >>
227    completeInduct_on `n` >> strip_tac >>
228    Cases_on `!m. m < n ==> ?t. mwhile_unit_step P g m z1 = SOME (T,t)`
229    >- (goal_assum drule >> fs[]) >>
230    pop_assum mp_tac >> simp[]
231    ) >>
232  qx_gen_tac `m` >> strip_tac >>
233  qsuff_tac `m = n` >> fs[] >>
234  fs[arithmeticTheory.EQ_LESS_EQ, GSYM arithmeticTheory.NOT_LESS] >>
235  conj_tac >> CCONTR_TAC >> fs[]
236  >- (first_x_assum drule >> strip_tac >> rfs[]) >>
237  last_x_assum (qspec_then `SUC m` assume_tac) >>
238  rfs[mwhile_unit_step_def, BIND_DEF, UNIT_DEF, IGNORE_BIND_DEF]
239QED
240
241val MWHILE_UNIT_DEF = new_specification(
242  "MWHILE_UNIT_DEF", ["MWHILE_UNIT"],
243  mwhile_unit_exists |> SIMP_RULE bool_ss [SKOLEM_THM]);
244
245
246(* ------------------------------------------------------------------------- *)
247(* Theorems.                                                                 *)
248(* ------------------------------------------------------------------------- *)
249
250Theorem BIND_LEFT_UNIT[simp]:
251     !k x. BIND (UNIT x) k = k x
252Proof
253   SRW_TAC [][BIND_DEF, UNIT_DEF, FUN_EQ_THM]
254QED
255
256val option_case_eq = prove_case_eq_thm{
257  case_def= option_case_def,
258  nchotomy = option_CASES
259               |> ONCE_REWRITE_RULE [DISJ_COMM]
260};
261
262Theorem MCOMP_THM:
263    MCOMP g f = EXT g o f
264Proof
265  REWRITE_TAC [MCOMP_DEF, EXT_DEF, FUN_EQ_THM, o_THM,
266      OPTION_MCOMP_def, CURRY_DEF, UNCURRY_DEF]
267    THEN REPEAT GEN_TAC
268    THEN Cases_on `f x x'`
269    THEN ASM_SIMP_TAC bool_ss [ OPTION_BIND_def, BIND_DEF, UNCURRY_VAR,
270      option_case_def, pair_CASE_def]
271QED
272
273Theorem MCOMP_ASSOC:
274     MCOMP f (MCOMP g h) = MCOMP (MCOMP f g) h
275Proof
276  REWRITE_TAC [MCOMP_DEF, OPTION_MCOMP_ASSOC, UNCURRY_CURRY_THM]
277QED
278
279Theorem UNIT_CURRY:
280    UNIT = CURRY SOME
281Proof
282  REWRITE_TAC [FUN_EQ_THM, UNIT_DEF, CURRY_DEF]
283    THEN BETA_TAC THEN REPEAT GEN_TAC THEN REFL_TAC
284QED
285
286Theorem MCOMP_ID:
287     (MCOMP g UNIT = g) /\ (MCOMP UNIT f = f)
288Proof
289  REWRITE_TAC [MCOMP_DEF, UNIT_CURRY, OPTION_MCOMP_ID,
290    UNCURRY_CURRY_THM, CURRY_UNCURRY_THM]
291QED
292
293(* could also derive following two theorems from MCOMP_ASSOC and MCOMP_ID,
294  using MCOMP_THM and EXT_DEF *)
295
296Theorem BIND_RIGHT_UNIT[simp]:
297     !k. BIND k UNIT = k
298Proof
299   SRW_TAC [boolSimps.CONJ_ss]
300           [BIND_DEF, UNIT_DEF, FUN_EQ_THM, option_case_eq, pair_case_eq] THEN
301   (Q.RENAME1_TAC `k v = NONE` ORELSE Q.RENAME1_TAC `NONE = k v`) THEN
302   Cases_on `k v` THEN SRW_TAC [][] THEN
303   metisLib.METIS_TAC [TypeBase.nchotomy_of ``:'a # 'b``]
304QED
305
306Theorem BIND_ASSOC:
307     !k m n. BIND k (\a. BIND (m a) n) = BIND (BIND k m) n
308Proof
309   SRW_TAC [][BIND_DEF, FUN_EQ_THM] THEN
310   Q.RENAME1_TAC `option_CASE (k v) NONE _` THEN
311   Cases_on `k v` THEN SRW_TAC [][] THEN
312   Q.RENAME1_TAC `pair_CASE p _` THEN Cases_on `p` THEN
313   SRW_TAC [][]
314QED
315
316Theorem MMAP_ID[simp]:
317     MMAP I = I
318Proof
319   SRW_TAC[][FUN_EQ_THM, MMAP_DEF]
320QED
321
322Theorem MMAP_COMP:
323     !f g. MMAP (f o g) = MMAP f o MMAP g
324Proof
325   SRW_TAC[][FUN_EQ_THM, MMAP_DEF, o_DEF, GSYM BIND_ASSOC]
326QED
327
328Theorem MMAP_UNIT:
329     !f. MMAP f o UNIT = UNIT o f
330Proof
331   SRW_TAC[][FUN_EQ_THM, MMAP_DEF]
332QED
333
334Theorem MMAP_JOIN:
335     !f. MMAP f o JOIN = JOIN o MMAP (MMAP f)
336Proof
337   SRW_TAC [][MMAP_DEF, o_DEF, JOIN_DEF, FUN_EQ_THM, GSYM BIND_ASSOC]
338QED
339
340Theorem JOIN_UNIT:
341     JOIN o UNIT = I
342Proof
343   SRW_TAC[][FUN_EQ_THM, JOIN_DEF, o_DEF]
344QED
345
346Theorem JOIN_MMAP_UNIT[simp]:
347     JOIN o MMAP UNIT = I
348Proof
349   SRW_TAC[boolSimps.ETA_ss]
350          [JOIN_DEF, o_DEF, MMAP_DEF, FUN_EQ_THM, GSYM BIND_ASSOC]
351QED
352
353Theorem JOIN_MAP_JOIN:
354     JOIN o MMAP JOIN = JOIN o JOIN
355Proof
356   SRW_TAC [][FUN_EQ_THM, JOIN_DEF, o_DEF, MMAP_DEF, GSYM BIND_ASSOC]
357QED
358
359Theorem JOIN_MAP:
360     !k m. BIND k m = JOIN (MMAP m k)
361Proof
362   SRW_TAC [boolSimps.ETA_ss]
363           [JOIN_DEF, o_DEF, MMAP_DEF, FUN_EQ_THM, GSYM BIND_ASSOC]
364QED
365
366Theorem sequence_nil[simp]:
367    sequence [] = UNIT []
368Proof
369  SRW_TAC[][sequence_def]
370QED
371
372Theorem mapM_nil[simp]:
373    mapM f [] = UNIT []
374Proof
375  SRW_TAC[][mapM_def]
376QED
377
378Theorem mapM_cons:
379    mapM f (x::xs) = BIND (f x) (\y. BIND (mapM f xs) (\ys. UNIT (y::ys)))
380Proof
381  SRW_TAC[][mapM_def,sequence_def]
382QED
383
384(* fail and choice *)
385Definition ES_FAIL_DEF:
386  ES_FAIL s = NONE
387End
388
389Definition ES_CHOICE_DEF:
390  ES_CHOICE xM yM s =
391    case xM s of
392       NONE => yM s
393     | xr => xr
394End
395
396Definition ES_GUARD_DEF:
397  ES_GUARD b = if b then UNIT () else ES_FAIL
398End
399
400val _ =
401    monadsyntax.declare_monad (
402      "errorState",
403      { bind = “BIND”, ignorebind = SOME “IGNORE_BIND”, unit = “UNIT”,
404        choice = SOME “ES_CHOICE”, fail = SOME “ES_FAIL”,
405        guard = SOME “ES_GUARD”
406      }
407    )
408
409
410Theorem ES_CHOICE_ASSOC:
411    ES_CHOICE xM (ES_CHOICE yM zM) = ES_CHOICE (ES_CHOICE xM yM) zM
412Proof
413  SRW_TAC[][FUN_EQ_THM, ES_CHOICE_DEF] THEN
414  Q.RENAME1_TAC `option_CASE (xM s)` THEN Cases_on `xM s` THEN SRW_TAC[][]
415QED
416
417Theorem ES_CHOICE_FAIL_LID[simp]:
418    ES_CHOICE ES_FAIL xM = xM
419Proof
420  SRW_TAC[][FUN_EQ_THM, ES_CHOICE_DEF, ES_FAIL_DEF]
421QED
422
423Theorem ES_CHOICE_FAIL_RID[simp]:
424    ES_CHOICE xM ES_FAIL = xM
425Proof
426  SRW_TAC[][FUN_EQ_THM, ES_CHOICE_DEF, ES_FAIL_DEF] THEN
427  Q.RENAME1_TAC `option_CASE (xM s)` THEN Cases_on `xM s` THEN SRW_TAC[][]
428QED
429
430Theorem BIND_FAIL_L[simp]:
431    BIND ES_FAIL fM = ES_FAIL
432Proof
433  SRW_TAC[][FUN_EQ_THM, ES_FAIL_DEF, BIND_DEF]
434QED
435
436Theorem BIND_ESGUARD[simp]:
437    (BIND (ES_GUARD F) fM = ES_FAIL) /\
438    (BIND (ES_GUARD T) fM = fM ())
439Proof
440  SRW_TAC[][ES_GUARD_DEF]
441QED
442
443Theorem IGNORE_BIND_ESGUARD[simp]:
444    (IGNORE_BIND (ES_GUARD F) xM = ES_FAIL) /\
445    (IGNORE_BIND (ES_GUARD T) xM = xM)
446Proof
447  SRW_TAC[][ES_GUARD_DEF, IGNORE_BIND_DEF]
448QED
449
450Theorem IGNORE_BIND_FAIL[simp]:
451    (IGNORE_BIND ES_FAIL xM = ES_FAIL) /\
452    (IGNORE_BIND xM ES_FAIL = ES_FAIL)
453Proof
454  SRW_TAC[][IGNORE_BIND_DEF] THEN
455  SRW_TAC[][ES_FAIL_DEF, BIND_DEF, FUN_EQ_THM] THEN
456  Q.RENAME1_TAC `option_CASE (xM s)` THEN Cases_on `xM s` THEN
457  SRW_TAC [][] THEN Q.RENAME1_TAC `xM s = SOME rs` THEN Cases_on `rs` THEN
458  SRW_TAC[][]
459QED
460
461(* applicative *)
462Definition ES_APPLY_DEF:
463  ES_APPLY fM xM = BIND fM (\f. BIND xM (\x. UNIT (f x)))
464End
465Overload APPLICATIVE_FAPPLY = ``ES_APPLY``
466
467Theorem APPLY_UNIT:
468    UNIT f <*> xM = MMAP f xM
469Proof
470  SRW_TAC[][ES_APPLY_DEF, MMAP_DEF, o_DEF]
471QED
472
473Theorem APPLY_UNIT_UNIT[simp]:
474    UNIT f <*> UNIT x = UNIT (f x)
475Proof
476  SRW_TAC[][ES_APPLY_DEF]
477QED
478
479Definition ES_LIFT2_DEF:
480  ES_LIFT2 f xM yM = MMAP f xM <*> yM
481End
482
483
484(* ------------------------------------------------------------------------- *)