Skip to content

Commit

Permalink
Stage work removing is_ready'
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Jan 1, 2025
1 parent cb069ef commit 7bc2db5
Show file tree
Hide file tree
Showing 2 changed files with 113 additions and 143 deletions.
188 changes: 75 additions & 113 deletions examples/lambda/barendregt/boehmScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,29 +49,6 @@ fun PRINT_TAC pfx g = (print (pfx ^ "\n"); ALL_TAC g);
Overload FV = “supp term_pmact”
Overload VAR = “term$VAR”

(*---------------------------------------------------------------------------*
* ltreeTheory extras
*---------------------------------------------------------------------------*)

(* ltree_subset A B <=> A results from B by "cutting off" some subtrees. Thus,
1) The paths of A is a subset of paths of B
2) The node contents for all paths of A is identical to those of B, but the number
of successors at those nodes of B may be different (B may have more successors)
NOTE: Simply defining ‘ltree_subset A B <=> subtrees A SUBSET subtrees B’ is wrong,
as A may appear as a non-root subtree of B, i.e. ‘A IN subtrees B’ but there's
no way to "cut off" B to get A, the resulting subtree in B always have some
more path prefixes.
*)
Definition ltree_subset_def :
ltree_subset A B <=>
(ltree_paths A) SUBSET (ltree_paths B) /\
!p. p IN ltree_paths A ==>
ltree_node (THE (ltree_lookup A p)) =
ltree_node (THE (ltree_lookup B p))
End

(*---------------------------------------------------------------------------*
* Boehm Trees (and subterms) - name after Corrado_Böhm [2] UOK *
*---------------------------------------------------------------------------*)
Expand Down Expand Up @@ -1053,6 +1030,17 @@ Proof
>> qexistsl_tac [‘M’, ‘M0’, ‘n’, ‘m’, ‘vs’, ‘M1’] >> simp []
QED

(* p <> [] is required because ‘[] IN ltree_paths (BT' X M r)’ always holds. *)
Theorem ltree_paths_imp_solvable :
!p X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ p <> [] /\
p IN ltree_paths (BT' X M r) ==> solvable M
Proof
rw [ltree_paths_def]
>> Cases_on ‘p’ >> fs []
>> CCONTR_TAC
>> fs [BT_of_unsolvables, ltree_lookup_def]
QED

(* ltree_lookup returns more information (the entire subtree), thus can be
used to construct the return value of ltree_el.
Expand Down Expand Up @@ -2878,19 +2866,23 @@ Proof
>> rw [Boehm_apply_MAP_rightctxt]
QED

(* NOTE: if M is solvable, ‘apply pi M’ may not be solvable. *)
Theorem Boehm_apply_unsolvable :
(* |- !M N. solvable (M @@ N) ==> solvable M *)
Theorem solvable_APP_E[local] =
has_hnf_APP_E |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
|> Q.GENL [‘M’, ‘N’]

Theorem Boehm_transform_of_unsolvables :
!pi M. Boehm_transform pi /\ unsolvable M ==> unsolvable (apply pi M)
Proof
SNOC_INDUCT_TAC >> rw []
>> FIRST_X_ASSUM MATCH_MP_TAC >> art []
>> fs [solving_transform_def, solvable_iff_has_hnf] (* 2 subgaols *)
>| [ (* goal 1 (of 2) *)
CCONTR_TAC >> fs [] \\
METIS_TAC [has_hnf_APP_E],
(* goal 2 (of 2) *)
CCONTR_TAC >> fs [] \\
METIS_TAC [has_hnf_SUB_E] ]
Induct_on ‘pi’ using SNOC_INDUCT
>- rw []
>> simp [FOLDR_SNOC, Boehm_transform_SNOC]
>> qx_genl_tac [‘t’, ‘M’]
>> reverse (rw [solving_transform_def])
>- (FIRST_X_ASSUM MATCH_MP_TAC >> art [] \\
MATCH_MP_TAC unsolvable_subst >> art [])
>> FIRST_X_ASSUM MATCH_MP_TAC >> simp []
>> PROVE_TAC [solvable_APP_E]
QED

(* Definition 10.3.5 (ii) *)
Expand All @@ -2914,10 +2906,6 @@ Definition is_ready_def :
?N. M -h->* N /\ hnf N /\ ~is_abs N /\ head_original N
End

Definition is_ready'_def :
is_ready' M <=> is_ready M /\ solvable M
End

(* NOTE: This alternative definition of ‘is_ready’ consumes ‘head_original’
and eliminated the ‘principle_hnf’ inside it.
*)
Expand Down Expand Up @@ -2952,15 +2940,6 @@ Proof
>> qexistsl_tac [‘y’, ‘args’] >> art []
QED

Theorem is_ready_alt' :
!M. is_ready' M <=> solvable M /\
?y Ns. M -h->* VAR y @* Ns /\ EVERY (\e. y # e) Ns
Proof
(* NOTE: this proof relies on the new [NOT_AND'] in boolSimps.BOOL_ss *)
rw [is_ready'_def, is_ready_alt, RIGHT_AND_OVER_OR]
>> REWRITE_TAC [Once CONJ_COMM]
QED

(* ‘subterm_width M p’ is the maximal number of children of all subterms of form
‘subterm X M q r’ such that ‘q <<= p’, irrelevant with particular X and r.
Expand Down Expand Up @@ -5261,7 +5240,8 @@ QED
Theorem Boehm_transform_exists_lemma :
!X M p r. FINITE X /\ FV M SUBSET X UNION RANK r /\
p <> [] /\ subterm X M p r <> NONE ==>
?pi. Boehm_transform pi /\ is_ready' (apply pi M) /\
?pi. Boehm_transform pi /\
solvable (apply pi M) /\ is_ready (apply pi M) /\
FV (apply pi M) SUBSET X UNION RANK (SUC r) /\
?v P. closed P /\
!q. q <<= p /\ q <> [] ==>
Expand Down Expand Up @@ -5391,15 +5371,16 @@ Proof
>> CONJ_ASM1_TAC
>- (MATCH_MP_TAC Boehm_transform_APPEND >> art [] \\
MATCH_MP_TAC Boehm_transform_APPEND >> art [])
>> Know ‘apply (p3 ++ p2 ++ p1) M == VAR b @* args' @* MAP VAR as’
>> qabbrev_tac ‘pi = p3 ++ p2 ++ p1’
>> Know ‘apply pi M == VAR b @* args' @* MAP VAR as’
>- (MATCH_MP_TAC lameq_TRANS \\
Q.EXISTS_TAC ‘apply (p3 ++ p2 ++ p1) M0’ \\
Q.EXISTS_TAC ‘apply pi M0’ \\
CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong \\
CONJ_TAC >- art [] \\
qunabbrev_tac ‘M0’ \\
MATCH_MP_TAC lameq_SYM \\
MATCH_MP_TAC lameq_principle_hnf' >> art []) \\
ONCE_REWRITE_TAC [Boehm_apply_APPEND] \\
SIMP_TAC std_ss [Once Boehm_apply_APPEND, Abbr ‘pi’] \\
MATCH_MP_TAC lameq_TRANS \\
Q.EXISTS_TAC ‘apply (p3 ++ p2) M1’ \\
CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> art [] \\
Expand All @@ -5409,18 +5390,23 @@ Proof
Q.EXISTS_TAC ‘apply p3 (P @* args')’ >> art [] \\
MATCH_MP_TAC Boehm_apply_lameq_cong >> rw [])
>> DISCH_TAC
>> CONJ_ASM1_TAC
>- (Suff ‘solvable (VAR b @* args' @* MAP VAR as)’
>- METIS_TAC [lameq_solvable_cong] \\
simp [solvable_iff_has_hnf, GSYM appstar_APPEND] \\
MATCH_MP_TAC hnf_has_hnf >> simp [hnf_appstar])
(* stage work *)
>> Know ‘principle_hnf (apply (p3 ++ p2 ++ p1) M) = VAR b @* args' @* MAP VAR as’
>- (Q.PAT_X_ASSUM ‘Boehm_transform (p3 ++ p2 ++ p1)’ K_TAC \\
Q.PAT_X_ASSUM ‘Boehm_transform p1’ K_TAC \\
Q.PAT_X_ASSUM ‘Boehm_transform p2’ K_TAC \\
Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC \\
Q.PAT_X_ASSUM ‘apply p1 M0 == M1’ K_TAC \\
Q.PAT_X_ASSUM ‘apply p2 M1 = P @* args'’ K_TAC \\
Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\
>> Know ‘principle_hnf (apply pi M) = VAR b @* args' @* MAP VAR as’
>- (Q.PAT_X_ASSUM ‘Boehm_transform pi’ K_TAC \\
Q.PAT_X_ASSUM ‘Boehm_transform p1’ K_TAC \\
Q.PAT_X_ASSUM ‘Boehm_transform p2’ K_TAC \\
Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC \\
Q.PAT_X_ASSUM ‘apply p1 M0 == M1’ K_TAC \\
Q.PAT_X_ASSUM ‘apply p2 M1 = P @* args'’ K_TAC \\
Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\
(* preparing for principle_hnf_denude_thm *)
Q.PAT_X_ASSUM ‘apply (p3 ++ p2 ++ p1) M == _’ MP_TAC \\
simp [Boehm_apply_APPEND, Abbr ‘p1’, Abbr ‘p2’, Abbr ‘p3’,
Q.PAT_X_ASSUM ‘apply pi M == _’ MP_TAC \\
simp [Boehm_apply_APPEND, Abbr ‘pi’, Abbr ‘p1’, Abbr ‘p2’, Abbr ‘p3’,
Boehm_apply_MAP_rightctxt'] \\
Know ‘[P/y] (M @* MAP VAR vs) @* MAP VAR (SNOC b as) =
[P/y] (M @* MAP VAR vs @* MAP VAR (SNOC b as))’
Expand Down Expand Up @@ -5500,17 +5486,9 @@ Proof
*)
MATCH_MP_TAC principle_hnf_denude_thm >> rw [])
>> DISCH_TAC
>> simp [is_ready'_def, GSYM CONJ_ASSOC]
(* extra subgoal: solvable (apply (p3 ++ p2 ++ p1) M) *)
>> ONCE_REWRITE_TAC [TAUT ‘P /\ Q /\ R <=> Q /\ P /\ R’]
>> CONJ_ASM1_TAC
>- (Suff ‘solvable (VAR b @* args' @* MAP VAR as)’
>- PROVE_TAC [lameq_solvable_cong] \\
REWRITE_TAC [solvable_iff_has_hnf] \\
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar])
(* applying is_ready_alt *)
>> CONJ_TAC
>- (simp [is_ready_alt] \\
>- (simp [is_ready_alt, Abbr ‘pi’] \\
qexistsl_tac [‘b’, ‘args' ++ MAP VAR as’] \\
CONJ_TAC
>- (MP_TAC (Q.SPEC ‘VAR b @* args' @* MAP VAR as’
Expand Down Expand Up @@ -5541,12 +5519,12 @@ Proof
Q.EXISTS_TAC ‘e’ >> art [])
(* extra goal *)
>> CONJ_TAC
>- (Q.PAT_X_ASSUM ‘apply (p3 ++ p2 ++ p1) M == _’ K_TAC \\
Q.PAT_X_ASSUM ‘principle_hnf (apply (p3 ++ p2 ++ p1) M) = _’ K_TAC \\
Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\
rpt (Q.PAT_X_ASSUM ‘Boehm_transform _’ K_TAC) \\
Q.PAT_X_ASSUM ‘solvable (apply (p3 ++ p2 ++ p1) M)’ K_TAC \\
simp [Boehm_apply_APPEND, Abbr ‘p1’, Abbr ‘p2’, Abbr ‘p3’,
>- (Q.PAT_X_ASSUM ‘apply pi M == _’ K_TAC \\
Q.PAT_X_ASSUM ‘principle_hnf (apply pi M) = _’ K_TAC \\
Q.PAT_X_ASSUM ‘apply p3 (P @* args') == _’ K_TAC \\
rpt (Q.PAT_X_ASSUM ‘Boehm_transform _’ K_TAC) \\
Q.PAT_X_ASSUM ‘solvable (apply pi M)’ K_TAC \\
simp [Boehm_apply_APPEND, Abbr ‘pi’, Abbr ‘p1’, Abbr ‘p2’, Abbr ‘p3’,
Boehm_apply_MAP_rightctxt'] \\
POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM) \\
reverse CONJ_TAC
Expand All @@ -5567,7 +5545,6 @@ Proof
Suff ‘RANK r SUBSET RANK (SUC r)’ >- SET_TAC [] \\
rw [RANK_MONO])
(* stage work, there's the textbook choice of y and P *)
>> qabbrev_tac ‘pi = p3 ++ p2 ++ p1’
>> qexistsl_tac [‘y’, ‘P’] >> art []
>> NTAC 2 STRIP_TAC (* push ‘q <<= p’ to assumptions *)
(* RHS rewriting from M to M0 *)
Expand Down Expand Up @@ -5758,17 +5735,17 @@ Proof
>> POP_ASSUM (MP_TAC o (Q.SPEC ‘p’)) (* put q = p *)
>> rw []
>> qabbrev_tac ‘M' = apply p0 M’
>> ‘solvable M' /\ ?y Ms. M' -h->* VAR y @* Ms /\ EVERY (\e. y # e) Ms’
by METIS_TAC [is_ready_alt']
>> ‘principle_hnf M' = VAR y @* Ms’ by rw [principle_hnf_thm', hnf_appstar]
>> Q.PAT_X_ASSUM ‘is_ready M'’ (MP_TAC o REWRITE_RULE [is_ready_alt])
>> STRIP_TAC
>> ‘principle_hnf M' = VAR y @* Ns’ by rw [principle_hnf_thm', hnf_appstar]
(* stage work *)
>> qunabbrev_tac ‘p’
>> Know ‘h < LENGTH Ms’
>> Know ‘h < LENGTH Ns’
>- (Q.PAT_X_ASSUM ‘subterm X M' (h::t) r <> NONE’ MP_TAC \\
RW_TAC std_ss [subterm_of_solvables] >> fs [])
>> DISCH_TAC
>> qabbrev_tac ‘m = LENGTH Ms’
>> qabbrev_tac ‘N = EL h Ms’
>> qabbrev_tac ‘m = LENGTH Ns’
>> qabbrev_tac ‘N = EL h Ns’
(* stage work *)
>> Know ‘subterm X N t (SUC r) <> NONE /\
subterm' X M' (h::t) r = subterm' X N t (SUC r)’
Expand All @@ -5795,10 +5772,10 @@ Proof
MATCH_MP_TAC lameq_SYM \\
MATCH_MP_TAC lameq_principle_hnf' >> art []) \\
rw [Abbr ‘p1’, appstar_SUB] \\
Know ‘MAP [U/y] Ms = Ms’
Know ‘MAP [U/y] Ns = Ns’
>- (rw [LIST_EQ_REWRITE, EL_MAP] \\
MATCH_MP_TAC lemma14b \\
Q.PAT_X_ASSUM ‘EVERY (\e. y # e) Ms’ MP_TAC \\
Q.PAT_X_ASSUM ‘EVERY (\e. y # e) Ns’ MP_TAC \\
rw [EVERY_MEM, MEM_EL] \\
POP_ASSUM MATCH_MP_TAC >> rename1 ‘i < m’ \\
Q.EXISTS_TAC ‘i’ >> art []) >> Rewr' \\
Expand All @@ -5812,12 +5789,12 @@ Proof
MATCH_MP_TAC SUBSET_TRANS \\
Q.EXISTS_TAC ‘FV (apply p0 M)’ >> art [] \\
MATCH_MP_TAC SUBSET_TRANS \\
Q.EXISTS_TAC ‘FV (VAR y @* Ms)’ \\
Q.EXISTS_TAC ‘FV (VAR y @* Ns)’ \\
reverse CONJ_TAC >- (MATCH_MP_TAC hreduce_FV_SUBSET >> art []) \\
rw [SUBSET_DEF, FV_appstar, IN_UNION] \\
DISJ2_TAC \\
Q.EXISTS_TAC ‘FV (EL h Ms)’ >> art [] \\
Q.EXISTS_TAC ‘EL h Ms’ >> rw [EL_MEM])
Q.EXISTS_TAC ‘FV (EL h Ns)’ >> art [] \\
Q.EXISTS_TAC ‘EL h Ns’ >> rw [EL_MEM])
>> RW_TAC std_ss []
>> rename1 ‘apply p2 N == _ ISUB ss'’
>> qabbrev_tac ‘N' = subterm' X M (h::t) r’
Expand Down Expand Up @@ -6009,10 +5986,10 @@ Theorem subtree_equiv_lemma_explicit :
!X Ms p r.
FINITE X /\ p <> [] /\ 0 < r /\ Ms <> [] /\
BIGUNION (IMAGE FV (set Ms)) SUBSET X UNION RANK r /\
EVERY (\M. subterm X M p r <> NONE) Ms ==>
EVERY (\M. p IN ltree_paths (BT' X M r)) Ms ==>
let pi = Boehm_construction X Ms p in
Boehm_transform pi /\
EVERY is_ready' (MAP (apply pi) Ms) /\
EVERY is_ready (MAP (apply pi) Ms) /\
EVERY (\M. p IN ltree_paths (BT' X M r)) (MAP (apply pi) Ms) /\
!M N q. MEM M Ms /\ MEM N Ms /\ q <<= p ==>
(subtree_equiv X M N q r <=>
Expand All @@ -6037,27 +6014,7 @@ Proof
FIRST_X_ASSUM MATCH_MP_TAC >> Q.EXISTS_TAC ‘M i’ >> art [] \\
rw [Abbr ‘M’, EL_MEM])
>> DISCH_TAC
(* now derive some non-trivial assumptions *)
>> ‘!i. i < k ==> (!q. q <<= p ==> subterm X (M i) q r <> NONE) /\
!q. q <<= FRONT p ==> solvable (subterm' X (M i) q r)’
by METIS_TAC [subterm_solvable_lemma]
(* convert previous assumption into easier forms for MATCH_MP_TAC *)
>> ‘(!i q. i < k /\ q <<= p ==> subterm X (M i) q r <> NONE) /\
(!i q. i < k /\ q <<= FRONT p ==> solvable (subterm' X (M i) q r))’
by PROVE_TAC []
>> Q.PAT_X_ASSUM ‘!i. i < k ==> P /\ Q’ K_TAC
(* In the original antecedents of this theorem, some M may be unsolvable,
and that's the easy case.
*)
>> Know ‘!i. i < k ==> solvable (M i)’
>- (rpt STRIP_TAC \\
Q.PAT_X_ASSUM ‘!i q. i < k /\ q <<= FRONT p ==> solvable _’
(MP_TAC o Q.SPECL [‘i’, ‘[]’]) >> simp [])
>> DISCH_TAC
>> Know ‘!i. i < k ==> p IN ltree_paths (BT' X (M i) r)’
>- (rpt STRIP_TAC \\
MATCH_MP_TAC subterm_imp_ltree_paths >> rw [])
>> DISCH_TAC
>> ‘!i. i < k ==> solvable (M i)’ by METIS_TAC [ltree_paths_imp_solvable]
(* define M0 *)
>> qabbrev_tac ‘M0 = \i. principle_hnf (M i)’
>> Know ‘!i. i < k ==> hnf (M0 i)’
Expand Down Expand Up @@ -6663,12 +6620,12 @@ Proof
MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar, GSYM appstar_APPEND])
>> DISCH_TAC
>> PRINT_TAC "stage work on subtree_equiv_lemma: L6560"
>> CONJ_TAC (* EVERY is_ready' ... *)
>> CONJ_TAC (* EVERY is_ready ... *)
>- (rpt (Q.PAT_X_ASSUM ‘Boehm_transform _’ K_TAC) \\
simp [EVERY_EL, EL_MAP] \\
Q.X_GEN_TAC ‘i’ >> DISCH_TAC \\
(* now expanding ‘is_ready’ using [is_ready_alt] *)
ASM_SIMP_TAC std_ss [is_ready_alt'] \\
ASM_SIMP_TAC std_ss [is_ready_alt] \\
qexistsl_tac [‘b i’, ‘Ns i ++ tl i’] \\
(* subgoal: apply pi (M i) -h->* VAR (b i) @* (Ns i ++ tl i) *)
CONJ_TAC
Expand Down Expand Up @@ -6834,6 +6791,10 @@ Proof
(* This subgoal was due to modifications of agree_upto_def. It's still kept
in case this extra subgoal may be later needed.
*)


>> cheat
(* TODO
>> Know ‘!i. i < k ==> p IN ltree_paths (BT' X (apply pi (M i)) r)’
>- (rpt STRIP_TAC \\
simp [BT_def, BT_generator_def, Once ltree_unfold,
Expand Down Expand Up @@ -10228,6 +10189,7 @@ Proof
>> Q.PAT_X_ASSUM ‘_ = m3’ (REWRITE_TAC o wrap o SYM)
>> Q.PAT_X_ASSUM ‘_ = m4’ (REWRITE_TAC o wrap o SYM)
>> simp [Abbr ‘d_max'’]
*)
QED

val _ = export_theory ();
Expand Down
Loading

0 comments on commit 7bc2db5

Please sign in to comment.