1(* interactive mode
2loadPath := ["../ho_prover","../subtypes","../formalize"] @ !loadPath;
3app load
4  ["bossLib","realLib","ho_proverTools","extra_pred_setTools",
5   "sequenceTools","prob_canonTools","prob_algebraTheory","probTheory"];
6quietdec := true;
7*)
8
9open HolKernel Parse boolLib bossLib arithmeticTheory pred_setTheory
10     listTheory state_transformerTheory
11     HurdUseful extra_numTheory combinTheory
12     pairTheory realTheory realLib extra_boolTheory
13     extra_pred_setTheory sumTheory
14     extra_realTheory extra_pred_setTools numTheory
15     simpLib seqTheory res_quanTheory;
16
17open sequenceTheory sequenceTools subtypeTheory;
18open util_probTheory measureTheory probabilityTheory;
19open prob_algebraTheory probTheory;
20
21(* interactive mode
22quietdec := false;
23*)
24
25val _ = new_theory "prob_bernoulli";
26
27val EXISTS_DEF = boolTheory.EXISTS_DEF;
28val std_ss' = std_ss ++ boolSimps.ETA_ss;
29val Rewr = DISCH_THEN (REWRITE_TAC o wrap);
30val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap);
31val STRONG_DISJ_TAC = CONV_TAC (REWR_CONV (GSYM IMP_DISJ_THM)) >> STRIP_TAC;
32val Cond =
33  DISCH_THEN
34  (fn mp_th =>
35   let
36     val cond = fst (dest_imp (concl mp_th))
37   in
38     KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)]
39   end);
40
41(* ------------------------------------------------------------------------- *)
42(* The definition of the Bernoulli(p) sampling algorithm.                    *)
43(* ------------------------------------------------------------------------- *)
44
45val prob_bernoulli_iter_def = Define
46  `prob_bernoulli_iter p =
47   BIND sdest
48   (\b.
49    UNIT
50    (if b then (if p <= (1 :real) / 2 then INR F else INL (2 * p - 1))
51     else (if p <= 1 / 2 then INL (2 * p) else INR T)))`;
52
53val prob_bernoulli_loop_def = new_definition
54  ("prob_bernoulli_loop_def",
55   ``prob_bernoulli_loop = prob_while ISL (prob_bernoulli_iter o OUTL)``);
56
57val prob_bernoulli_def = Define
58  `prob_bernoulli p = BIND (prob_bernoulli_loop (INL p)) (\a. UNIT (OUTR a))`;
59
60(* ------------------------------------------------------------------------- *)
61(* Theorems leading to:                                                      *)
62(* 1. !p. 0 <= p /\ p <= 1 ==> prob bern {s | FST (prob_bernoulli p s)} = p  *)
63(* ------------------------------------------------------------------------- *)
64
65val INDEP_FN_PROB_BERNOULLI_ITER = store_thm
66  ("INDEP_FN_PROB_BERNOULLI_ITER",
67   ``!p. prob_bernoulli_iter p IN indep_fn``,
68   RW_TAC std_ss [INDEP_FN_BIND, INDEP_FN_UNIT, prob_bernoulli_iter_def,
69                  INDEP_FN_SDEST]);
70
71val PROB_TERMINATES_BERNOULLI = store_thm
72  ("PROB_TERMINATES_BERNOULLI",
73   ``prob_while_terminates ISL (prob_bernoulli_iter o OUTL)``,
74   RW_TAC std_ss [PROB_TERMINATES_HART, o_THM, INDEP_FN_PROB_BERNOULLI_ITER]
75   >> Q.EXISTS_TAC `1 / 2`
76   >> RW_TAC std_ss [HALF_POS, GBIGUNION_IMAGE]
77   >> MATCH_MP_TAC REAL_LE_TRANS
78   >> Q.EXISTS_TAC
79      `prob bern
80       ({x | ~ISL x} o FST o
81        prob_while_cut ISL (prob_bernoulli_iter o OUTL) 1 a)`
82   >> REVERSE CONJ_TAC
83   >- (MATCH_MP_TAC PROB_INCREASING
84       >> RW_TAC std_ss [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_BERNOULLI_ITER,
85                         PROB_SPACE_BERN, INDEP_FN_PROB_WHILE_CUT, o_THM] >|
86       [MATCH_MP_TAC EVENTS_COUNTABLE_UNION
87        >> RW_TAC std_ss [PROB_SPACE_BERN, SUBSET_DEF, IN_UNIV, COUNTABLE_NUM,
88                          IN_IMAGE, image_countable]
89        >> Know
90           `{s |
91             ISR (FST (prob_while_cut
92                        ISL (prob_bernoulli_iter o OUTL) n a s))} =
93            {x | ISR x} o FST o
94            prob_while_cut ISL (prob_bernoulli_iter o OUTL) n a`
95        >- (SET_EQ_TAC
96            >> RW_TAC std_ss [GSPECIFICATION, IN_o, o_THM])
97        >> Rewr
98        >> RW_TAC std_ss [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_BERNOULLI_ITER,
99                          PROB_SPACE_BERN, INDEP_FN_PROB_WHILE_CUT, o_THM],
100        RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION_IMAGE, IN_UNIV, GSPECIFICATION,
101                       IN_o, o_THM]
102        >> PROVE_TAC []])
103   >> REVERSE (Cases_on `a`)
104   >- (RW_TAC std_ss [PROB_WHILE_CUT_ID, UNIT_DEF]
105       >> Suff
106          `{(x:real+bool) | ~ISL x} o FST o (\s. (INR y, s)) =
107           (UNIV:(num->bool)->bool)`
108       >- RW_TAC std_ss [PROB_BERN_UNIV, REAL_LT_IMP_LE, HALF_LT_1]
109       >> SET_EQ_TAC
110       >> RW_TAC std_ss [IN_UNIV, GSPECIFICATION, IN_o, o_THM])
111   >> RW_TAC bool_ss [ONE]
112   >> RW_TAC std_ss [prob_while_cut_def, PROB_WHILE_CUT_0,
113                      BIND_RIGHT_UNIT, o_THM]
114   >> MP_TAC (Q.SPEC `{x | ISR x} o FST o prob_bernoulli_iter x`
115              (GSYM PROB_BERN_INTER_HALVES))
116   >> Cond >- RW_TAC std_ss [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_BERNOULLI_ITER]
117   >> Rewr'
118   >> RW_TAC std_ss [prob_bernoulli_iter_def] \\ (* 2 sub-goals here *)
119 ( Know `!f b.
120         halfspace b INTER {x:real+bool | ISR x} o FST o BIND sdest (\b. f b) =
121         halfspace b INTER ({x | ISR x} o FST o f b) o stl`
122   >- (SET_EQ_TAC
123       >> RW_TAC std_ss [IN_o, o_THM, IN_HALFSPACE, IN_INTER, GSPECIFICATION,
124                         BIND_DEF, UNCURRY, sdest_def]
125       >> Cases_on `shd x'`
126       >> Cases_on `b`
127       >> RW_TAC std_ss [])
128   >> DISCH_THEN (fn th => RW_TAC std_ss [th])
129   >> RW_TAC bool_ss [REWRITE_RULE [o_ASSOC] INDEP_FN_FST_EVENTS,
130                      PROB_BERN_STL_HALFSPACE, INDEP_FN_UNIT, o_ASSOC]
131   >> RW_TAC bool_ss [GSYM o_ASSOC]
132   >> Know
133      `!x:real+bool.
134         {x | ISR x} o FST o UNIT x =
135         if ISL x then {} else (UNIV:(num->bool)->bool)`
136   >- (SET_EQ_TAC
137       >> RW_TAC std_ss [GSPECIFICATION, IN_o, o_THM, UNIT_DEF, IN_UNIV,
138                         NOT_IN_EMPTY]
139       >> FULL_SIMP_TAC (srw_ss()) [])
140   >> Rewr
141   >> RW_TAC std_ss [PROB_BERN_UNIV, PROB_BERN_EMPTY, GSYM ONE]
142   >> RW_TAC real_ss [REAL_LE_REFL] ));
143
144val INDEP_FN_PROB_BERNOULLI_LOOP = store_thm
145  ("INDEP_FN_PROB_BERNOULLI_LOOP",
146   ``!a. prob_bernoulli_loop a IN indep_fn``,
147   RW_TAC std_ss [prob_bernoulli_loop_def, INDEP_FN_PROB_WHILE,
148                  PROB_TERMINATES_BERNOULLI, INDEP_FN_PROB_BERNOULLI_ITER,
149                  o_THM]);
150
151val INDEP_FN_PROB_BERNOULLI = store_thm
152  ("INDEP_FN_PROB_BERNOULLI",
153   ``!p. prob_bernoulli p IN indep_fn``,
154   RW_TAC std_ss [prob_bernoulli_def, INDEP_FN_BIND, INDEP_FN_UNIT,
155                  INDEP_FN_PROB_BERNOULLI_LOOP]);
156
157val PROB_BERNOULLI_ALT = store_thm
158  ("PROB_BERNOULLI_ALT",
159   ``prob_bernoulli p =
160     BIND sdest
161     (\b.
162      if b then (if p <= 1 / 2 then UNIT F else prob_bernoulli (2 * p - 1))
163      else (if p <= 1 / 2 then prob_bernoulli (2 * p) else UNIT T))``,
164   SIMP_TAC std_ss [prob_bernoulli_def, prob_bernoulli_loop_def]
165   >> MP_TAC (Q.SPECL [`ISL`, `prob_bernoulli_iter o OUTL`, `INL p`]
166              (INST_TYPE [alpha |-> ``:real+bool``] PROB_WHILE_ADVANCE))
167   >> Cond
168   >- RW_TAC std_ss [INDEP_FN_PROB_BERNOULLI_ITER, PROB_TERMINATES_BERNOULLI,
169                     o_THM]
170   >> Rewr
171   >> RW_TAC std_ss [o_THM, prob_bernoulli_iter_def, GSYM BIND_ASSOC,
172                     BIND_LEFT_UNIT]
173   >> RW_TAC (std_ss ++ boolSimps.COND_elim_ss) []
174   >> RW_TAC std_ss [PROB_WHILE_ADVANCE, INDEP_FN_PROB_BERNOULLI_ITER, o_THM,
175                     PROB_TERMINATES_BERNOULLI]
176   >> RW_TAC (std_ss ++ boolSimps.COND_elim_ss) []
177   >> RW_TAC std_ss [BIND_LEFT_UNIT]);
178
179val PROB_BERNOULLI = store_thm
180  ("PROB_BERNOULLI",
181   ``!p. 0 <= p /\ p <= 1 ==> (prob bern {s | FST (prob_bernoulli p s)} = p)``,
182   Know `!p. {s | FST (prob_bernoulli p s)} = I o FST o prob_bernoulli p`
183   >- (SET_EQ_TAC
184       >> RW_TAC std_ss [GSPECIFICATION, IN_o, o_THM, IN_I])
185   >> Rewr
186   >> Know `!p. 0 <= prob bern (I o FST o prob_bernoulli p)`
187   >- RW_TAC std_ss [PROB_POSITIVE, PROB_SPACE_BERN, INDEP_FN_FST_EVENTS,
188                     INDEP_FN_PROB_BERNOULLI]
189   >> STRIP_TAC
190   >> Know `!p. prob bern (I o FST o prob_bernoulli p) <= 1`
191   >- RW_TAC std_ss [PROB_LE_1, PROB_SPACE_BERN, INDEP_FN_FST_EVENTS,
192                     INDEP_FN_PROB_BERNOULLI]
193   >> STRIP_TAC
194   >> RW_TAC bool_ss []
195   >> MATCH_MP_TAC ABS_EQ
196   >> RW_TAC bool_ss []
197   >> MP_TAC (Q.SPEC `e` POW_HALF_SMALL)
198   >> RW_TAC bool_ss []
199   >> MATCH_MP_TAC REAL_LET_TRANS
200   >> Q.EXISTS_TAC `(1 / 2) pow n`
201   >> RW_TAC bool_ss []
202   >> NTAC 2 (POP_ASSUM K_TAC)
203   >> NTAC 2 (POP_ASSUM MP_TAC)
204   >> REWRITE_TAC [AND_IMP_INTRO]
205   >> Q.SPEC_TAC (`p`, `p`)
206   >> Induct_on `n`
207   >- (RW_TAC bool_ss [pow, abs]
208       >> Q.PAT_X_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)
209       >> Q.PAT_X_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)
210       >> REPEAT (POP_ASSUM MP_TAC)
211       >> REAL_ARITH_TAC)
212   >> GEN_TAC
213   >> MP_TAC (Q.SPEC `I o FST o prob_bernoulli p` (GSYM PROB_BERN_INTER_HALVES))
214   >> Cond >- RW_TAC std_ss [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_BERNOULLI]
215   >> Rewr'
216   >> REPEAT DISCH_TAC
217   >> Know `!x y : real. abs 2 * x <= 2 * y ==> x <= y`
218   >- (SIMP_TAC arith_ss [abs, REAL_LE]
219       >> REAL_ARITH_TAC)
220   >> DISCH_THEN MATCH_MP_TAC
221   >> RW_TAC bool_ss [GSYM ABS_MUL, pow, REAL_MUL_ASSOC, HALF_CANCEL,
222                      REAL_MUL_LID, REAL_SUB_LDISTRIB]
223   >> ONCE_REWRITE_TAC [PROB_BERNOULLI_ALT]
224   >> Know
225      `!f b.
226         halfspace b INTER I o FST o BIND sdest (\b. f b) =
227         halfspace b INTER (I o FST o f b) o stl`
228   >- (SET_EQ_TAC
229       >> RW_TAC std_ss [IN_o, o_THM, IN_HALFSPACE, IN_INTER, GSPECIFICATION,
230                         BIND_DEF, UNCURRY, sdest_def, IN_I]
231       >> Cases_on `shd x`
232       >> Cases_on `b`
233       >> RW_TAC std_ss [])
234   >> DISCH_THEN
235      (fn th =>
236       RW_TAC bool_ss [th, PROB_BERN_STL_HALFSPACE, INDEP_FN_PROB_BERNOULLI,
237                       INDEP_FN_FST_EVENTS, INDEP_FN_UNIT]
238       >> RW_TAC bool_ss [GSYM REAL_ADD_LDISTRIB, REAL_MUL_ASSOC,
239                          REAL_MUL_LID, HALF_CANCEL]) >|
240   [Know `(I o FST o UNIT F) = ({}:(num->bool)->bool)`
241    >- (SET_EQ_TAC
242        >> RW_TAC std_ss [NOT_IN_EMPTY, IN_o, o_THM, IN_I, UNIT_DEF])
243    >> Rewr
244    >> RW_TAC bool_ss [PROB_BERN_EMPTY, REAL_ADD_LID]
245    >> Q.PAT_X_ASSUM `!p. P p` MATCH_MP_TAC
246    >> CONJ_TAC >- (Q.PAT_X_ASSUM `0 <= p` MP_TAC >> REAL_ARITH_TAC)
247    >> Suff `2 * p <= 2 * (1 / 2)` >- RW_TAC std_ss [HALF_CANCEL]
248    >> RW_TAC arith_ss [REAL_LE_LMUL, REAL_LT],
249    Know `(I o FST o UNIT T) = (UNIV:(num->bool)->bool)`
250    >- (SET_EQ_TAC
251        >> RW_TAC std_ss [IN_UNIV, IN_o, o_THM, IN_I, UNIT_DEF])
252    >> Rewr
253    >> RW_TAC bool_ss [PROB_BERN_UNIV]
254    >> Know `!x y : real. (x + 1) - y = x - (y - 1)` >- REAL_ARITH_TAC
255    >> Rewr'
256    >> Q.PAT_X_ASSUM `!p. P p` MATCH_MP_TAC
257    >> REVERSE CONJ_TAC >- (Q.PAT_X_ASSUM `p <= 1` MP_TAC >> REAL_ARITH_TAC)
258    >> Suff `~(2 * p <= 1)` >- REAL_ARITH_TAC
259    >> STRIP_TAC
260    >> Q.PAT_X_ASSUM `~x` MP_TAC
261    >> RW_TAC std_ss []
262    >> Know `2 * p <= 2 * (1 / 2)` >- RW_TAC std_ss [HALF_CANCEL]
263    >> RW_TAC arith_ss [REAL_LE_LMUL, REAL_LT]]);
264
265val _ = export_theory ();
266