Skip to content

Commit

Permalink
FTBFS boehmTheory, finally
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Nov 5, 2024
1 parent ea8623c commit c200ae9
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 71 deletions.
107 changes: 47 additions & 60 deletions examples/lambda/barendregt/boehmScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1548,6 +1548,7 @@ QED
(* ‘subterm X M p r’ w.r.t. different X and r *)
(*****************************************************************************)

(* NOTE: cf. subterm_fresh_tpm_cong for the easier case of fresh tpm *)
Theorem subterm_tpm_lemma :
!X Y p M pi r r'. FINITE X /\ FINITE Y /\
FV M SUBSET X UNION RANK r /\
Expand Down Expand Up @@ -4826,34 +4827,37 @@ Proof
First of all, those assumptions about p1,p2,p3 are no more needed.
*)
>> qunabbrev_tac ‘pi’
>> Q.PAT_X_ASSUM ‘Boehm_transform p1’ K_TAC
>> Q.PAT_X_ASSUM ‘apply p1 M0 == M1’ K_TAC
>> Q.PAT_X_ASSUM ‘Boehm_transform p1’ K_TAC
>> Q.PAT_X_ASSUM ‘apply p1 M0 == M1’ K_TAC
>> qunabbrev_tac ‘p1’
>> Q.PAT_X_ASSUM ‘Boehm_transform p2’ K_TAC
>> Q.PAT_X_ASSUM ‘apply p2 M1 = P @* args'’ K_TAC
>> Q.PAT_X_ASSUM ‘Boehm_transform p2’ K_TAC
>> Q.PAT_X_ASSUM ‘apply p2 M1 = P @* args'’ K_TAC
>> qunabbrev_tac ‘p2’
>> Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC
>> Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC
>> Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC
>> Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC
>> qunabbrev_tac ‘p3’
>> Q.PAT_X_ASSUM ‘h::t <> []’ K_TAC (* too obvious *)
>> Q.PAT_X_ASSUM ‘h::t <> []’ K_TAC
>> qabbrev_tac ‘N = EL h args’
>> qabbrev_tac ‘N' = EL h args'’
(* eliminating N' *)
>> ‘N' = [P/y] N’ by simp [EL_MAP, Abbr ‘m’, Abbr ‘N’, Abbr ‘N'’, Abbr ‘args'’]
>> ‘N' = [P/y] N’
by simp [EL_MAP, Abbr ‘m’, Abbr ‘N’, Abbr ‘N'’, Abbr ‘args'’]
>> POP_ORW
>> qunabbrev_tac ‘N'’
(* cleanup args' *)
>> Q.PAT_X_ASSUM ‘!i. i < m ==> FV (EL i args') SUBSET FV (EL i args)’ K_TAC
>> Q.PAT_X_ASSUM ‘LENGTH args' = m’ K_TAC
>> Q.PAT_X_ASSUM
‘!i. i < m ==>
FV (EL i args') SUBSET FV (EL i args)’ K_TAC
>> Q.PAT_X_ASSUM ‘LENGTH args' = m’ K_TAC
>> qunabbrev_tac ‘args'’
(* cleanup l, as and b *)
>> Q.PAT_X_ASSUM ‘ALL_DISTINCT l’ K_TAC
>> NTAC 2 (Q.PAT_X_ASSUM ‘DISJOINT (set l) _’ K_TAC)
>> Q.PAT_X_ASSUM ‘LENGTH l = q - m + 1’ K_TAC
>> Q.PAT_X_ASSUM ‘l <> []’ K_TAC
>> Q.PAT_X_ASSUM ‘l = SNOC b as’ K_TAC
>> Q.PAT_X_ASSUM ‘~MEM y l’ K_TAC
>> Q.PAT_X_ASSUM ‘LENGTH as = q - m’ K_TAC
>> Q.PAT_X_ASSUM ‘ALL_DISTINCT l’ K_TAC
>> NTAC 2 (Q.PAT_X_ASSUM ‘DISJOINT (set l) _’ K_TAC)
>> Q.PAT_X_ASSUM ‘LENGTH l = q - m + 1’ K_TAC
>> Q.PAT_X_ASSUM ‘l <> []’ K_TAC
>> Q.PAT_X_ASSUM ‘l = SNOC b as’ K_TAC
>> Q.PAT_X_ASSUM ‘~MEM y l’ K_TAC
>> Q.PAT_X_ASSUM ‘LENGTH as = q - m’ K_TAC
>> qunabbrevl_tac [‘l’, ‘as’, ‘b’]
(* applying subterm_headvar_lemma *)
>> Know ‘hnf_headvar M1 IN X UNION RANK (SUC r)’
Expand Down Expand Up @@ -4887,7 +4891,8 @@ Proof
MATCH_MP_TAC subterm_induction_lemma' \\
qexistsl_tac [‘M’, ‘M0’, ‘n’, ‘m’, ‘vs’, ‘M1’] >> simp [])
>> DISCH_TAC
>> ‘t IN ltree_paths (BT' X N (SUC r))’ by PROVE_TAC [subterm_imp_ltree_paths]
>> ‘t IN ltree_paths (BT' X N (SUC r))’
by PROVE_TAC [subterm_imp_ltree_paths]
>> simp [] >> DISCH_THEN K_TAC
(* applying SUBSET_MAX_SET *)
>> MATCH_MP_TAC SUBSET_MAX_SET
Expand Down Expand Up @@ -5830,9 +5835,8 @@ Proof
by rw [Abbr ‘l’, Abbr ‘m’, Abbr ‘args2’, Abbr ‘args'’, Abbr ‘d_max’]
>> ‘!i. d_max < LENGTH (l i)’ by rw []
(* applying TAKE_DROP_SUC to break l into 3 pieces *)
>> MP_TAC
(Q.GEN ‘i’
(ISPECL [“d_max :num”, “l (i :num) :term list”] (GSYM TAKE_DROP_SUC)))
>> MP_TAC (Q.GEN ‘i’ (ISPECL [“d_max :num”, “l (i :num) :term list”]
(GSYM TAKE_DROP_SUC)))
>> simp [] >> Rewr'
>> REWRITE_TAC [appstar_APPEND, appstar_SING]
(* The segmentation of list l(i) - apply (p3 ++ p2 ++ p1) (M i)
Expand Down Expand Up @@ -6407,7 +6411,7 @@ Proof
DISCH_THEN (Q.X_CHOOSE_THEN ‘j1’ STRIP_ASSUME_TAC) \\
DISCH_THEN (Q.X_CHOOSE_THEN ‘j2’ STRIP_ASSUME_TAC) \\
rpt STRIP_TAC (* this asserts q *) \\
Q.PAT_X_ASSUM ‘!q. q <<= p ==> _’ (MP_TAC o Q.SPEC ‘q’) >> simp [] \\
Q.PAT_X_ASSUM ‘!q. q <<= p ==> _ = _’ (MP_TAC o Q.SPEC ‘q’) >> simp [] \\
Q.PAT_X_ASSUM ‘M2 = M j1’ (rfs o wrap) \\
Q.PAT_X_ASSUM ‘N2 = M j2’ (rfs o wrap) \\
Q.PAT_X_ASSUM ‘M2' = apply pi (M j1)’ K_TAC \\
Expand All @@ -6428,7 +6432,7 @@ Proof
MATCH_MP_TAC BT_of_principle_hnf \\
simp [Abbr ‘M'’] \\
METIS_TAC [lameq_solvable_cong]) >> Rewr' \\
simp [Abbr ‘M'’] \\
simp [Abbr ‘M'’] >> T_TAC \\
(* NOTE: now we are still missing some important connections:
- ltree_el (BT W M2) q ~1~ subterm' W M2 q
- ltree_el (BT W N2) q ~1~ subterm' W N2 q
Expand Down Expand Up @@ -6539,31 +6543,29 @@ Proof
TODO: Do we know ‘subterm X N t (SUC r) <> NONE’?
*)
Q_TAC (RNEWS_TAC (“ys :string list”, “r :num”, “n_max :num”)) ‘X’ \\
qabbrev_tac ‘pm = ZIP (REVERSE ys, REVERSE vs)’ \\
qabbrev_tac ‘pm = ZIP (vs,ys)’ \\
Know ‘!i. i < k ==>
subterm X (H i) p r <> NONE /\
subterm' X (H i) p r = (tpm pm (subterm' X (M i) p r)) ISUB ss’
subterm' X (H i) p r =
(tpm (REVERSE pm) (subterm' X (M i) p r)) ISUB ss’
>- (Q.X_GEN_TAC ‘i’ >> DISCH_TAC \\
Cases_on ‘p’ >> FULL_SIMP_TAC list_ss [] \\
Q.PAT_X_ASSUM ‘!i q. _ ==> subterm X (M i) q r <> NONE’
(MP_TAC o Q.SPECL [‘i’, ‘p’]) >> simp [] \\
Cases_on ‘p’ >> FULL_SIMP_TAC list_ss [] >> T_TAC \\
Q_TAC (UNBETA_TAC [subterm_of_solvables]) ‘subterm X (H i) (h::t) r’ \\
Know ‘principle_hnf (H i) = H i’
>- (MATCH_MP_TAC principle_hnf_reduce \\
simp [Abbr ‘H’, GSYM appstar_APPEND, hnf_appstar]) \\
DISCH_TAC \\
Know ‘LAMl_size (H i) = 0’
>- (rw [Abbr ‘H’, LAMl_size_appstar, GSYM appstar_APPEND]) \\
DISCH_TAC \\
simp [] \\
(* NOTE: popping this assume will eventually bring us ‘h < m i’ *)
Q.PAT_X_ASSUM ‘!i. i < k ==> h::t IN ltree_paths (BT' X (M i) r)’
(MP_TAC o Q.SPEC ‘i’) \\
(* unfolding ‘BT' X (M i) r’ *)
simp [BT_def, BT_generator_def, Once ltree_unfold, subterm_of_solvables] \\
Q_TAC (RNEWS_TAC (“ys' :string list”, “r :num”, “(n :num -> num) i”)) ‘X’ \\
DISCH_TAC >> simp [] \\
simp [subterm_of_solvables] \\
Q_TAC (RNEWS_TAC (“ys' :string list”, “r :num”,
“(n :num -> num) i”)) ‘X’ \\
qabbrev_tac ‘vs' = TAKE (n i) vs’ \\
‘ALL_DISTINCT vs' /\ LENGTH vs' = n i’ by rw [ALL_DISTINCT_TAKE, Abbr ‘vs'’] \\
simp [ltree_paths_def, ltree_lookup_def] \\
simp [LMAP_fromList, GSYM BT_def, LNTH_fromList, EL_MAP] \\
‘ALL_DISTINCT vs' /\ LENGTH vs' = n i’
by rw [ALL_DISTINCT_TAKE, Abbr ‘vs'’] \\
qabbrev_tac ‘t0 = VAR (y i) @* args i’ \\
Know ‘DISJOINT (set vs') (set ys')’
>- (MATCH_MP_TAC DISJOINT_SUBSET' \\
Expand All @@ -6576,7 +6578,8 @@ Proof
CONJ_TAC >- rw [Abbr ‘vs’, RNEWS_SUBSET_ROW] \\
MATCH_MP_TAC ROW_SUBSET_RANK >> art []) >> DISCH_TAC \\
(* applying for principle_hnf_tpm_reduce *)
Know ‘principle_hnf (LAMl vs' t0 @* MAP VAR ys') = tpm (ZIP (vs',ys')) t0’
Know ‘principle_hnf (LAMl vs' t0 @* MAP VAR ys') =
tpm (ZIP (vs',ys')) t0’
>- (‘hnf t0’ by rw [Abbr ‘t0’, hnf_appstar] \\
MATCH_MP_TAC principle_hnf_tpm_reduce' >> art [] \\
MATCH_MP_TAC subterm_disjoint_lemma \\
Expand Down Expand Up @@ -6608,34 +6611,18 @@ Proof
REWRITE_TAC [GSYM APPEND_ASSOC] \\
MATCH_MP_TAC EL_APPEND1 \\
simp [Abbr ‘args'’]) >> Rewr' \\
qabbrev_tac ‘f = \t. t ISUB ss’ \\
fs [Abbr ‘args'’, EL_MAP] \\
qabbrev_tac ‘N = EL h (args i)’ \\
(* applying subterm_isub_permutator_cong' and subterm_tpm_lemma' *)
fs [Abbr ‘args'’, EL_MAP] \\
qabbrev_tac ‘pm' = ZIP (vs',ys')’ \\
‘ltree_lookup (BT' X (tpm pm' N) (SUC r)) t <> NONE <=>
t IN ltree_paths (BT' X (tpm pm' N) (SUC r))’ by simp [ltree_paths_def] \\
POP_ORW >> DISCH_TAC \\
(* applying fresh_tpm_isub *)
Know ‘tpm pm' N = N ISUB ZIP (MAP VAR (REVERSE ys'),REVERSE vs')’
>- (qunabbrev_tac ‘pm'’ \\
MATCH_MP_TAC fresh_tpm_isub >> art [] \\
MATCH_MP_TAC subterm_disjoint_lemma \\
qexistsl_tac [‘X’, ‘r’, ‘n i’] >> simp [] \\
Q_TAC (TRANS_TAC SUBSET_TRANS) ‘Z’ >> art [] \\
qunabbrev_tac ‘N’ \\
Q.PAT_X_ASSUM ‘!i. i < k ==> y i IN Z /\ _’ (MP_TAC o Q.SPEC ‘i’) \\
rw [SUBSET_DEF] \\
FIRST_X_ASSUM MATCH_MP_TAC \\
Q.EXISTS_TAC ‘FV (EL h (args i))’ >> art [] \\
Q.EXISTS_TAC ‘EL h (args i)’ >> simp [EL_MEM]) >> Rewr' \\
simp [Abbr ‘pm'’, Abbr ‘f’] \\
(* applying subterm_fresh_tpm_cong *)
(* subterm_isub_permutator_cong' *)
cheat) >> DISCH_TAC \\
Know ‘unsolvable (subterm' X (H j1) p r) /\
unsolvable (subterm' X (H j2) p r)’
>- (ASM_SIMP_TAC std_ss [] \\
CONJ_TAC \\ (* 2 subgoals, same tactics *)
MATCH_MP_TAC unsolvable_ISUB >> art []) >> STRIP_TAC \\
CONJ_TAC (* 2 subgoals, same tactics *) \\
MATCH_MP_TAC unsolvable_ISUB \\
simp [solvable_tpm]) >> STRIP_TAC \\
Know ‘unsolvable (subterm' X (H j1) p r) <=>
ltree_el (BT' X (H j1) r) p = SOME bot’
>- (MATCH_MP_TAC BT_ltree_el_of_unsolvables >> art [] \\
Expand Down
20 changes: 9 additions & 11 deletions examples/probability/central_limitScript.sml
View file
Original file line number Diff line number Diff line change
@@ -1,36 +1,34 @@
(* ========================================================================= *)
(* The Central Limit Theorems *)
(* The Central Limit Theorem (CLT) *)
(* ========================================================================= *)

open HolKernel Parse boolLib bossLib;

open pairTheory combinTheory optionTheory prim_recTheory arithmeticTheory
pred_setTheory pred_setLib topologyTheory hurdUtils;
pred_setTheory pred_setLib topologyTheory hurdUtils;

open realTheory realLib iterateTheory seqTheory transcTheory real_sigmaTheory
real_topologyTheory;
real_topologyTheory derivativeTheory;

open util_probTheory extrealTheory sigma_algebraTheory measureTheory
real_borelTheory borelTheory lebesgueTheory martingaleTheory
probabilityTheory derivativeTheory;
probabilityTheory;

val _ = new_theory "central_limit";


Definition mgf_def:
mgf p X s =
expectation p (\x. exp (Normal s * X x))
mgf p X s = expectation p (\x. exp (Normal s * X x))
End

Theorem mgf_0:
!p X. prob_space p ==> mgf p X 0 = 1
!p X. prob_space p ==> mgf p X 0 = 1
Proof
RW_TAC std_ss [mgf_def, mul_lzero, exp_0, normal_0]
>> MATCH_MP_TAC expectation_const >> art[]
RW_TAC std_ss [mgf_def, mul_lzero, exp_0, normal_0]
>> MATCH_MP_TAC expectation_const >> art []
QED

Theorem real_random_variable_exp:
∀p X r. prob_space p ∧ real_random_variable X p ⇒ real_random_variable (λx. exp (X x)) p
!p X r. prob_space p ∧ real_random_variable X p ⇒ real_random_variable (λx. exp (X x)) p
Proof
rpt GEN_TAC
>> simp [real_random_variable, prob_space_def, p_space_def, events_def]
Expand Down

0 comments on commit c200ae9

Please sign in to comment.