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