Skip to content

Commit

Permalink
Added subterm_width_inclusive, etc.
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Nov 9, 2024
1 parent 34e621e commit 0198ba9
Showing 1 changed file with 78 additions and 12 deletions.
90 changes: 78 additions & 12 deletions examples/lambda/barendregt/boehmScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2897,6 +2897,57 @@ Proof
Q.EXISTS_TAC ‘q’ >> art [] ]
QED

Theorem subterm_width_inclusive :
!M p q. q <<= p /\ subterm_width M p <= d ==> subterm_width M q <= d
Proof
rpt STRIP_TAC
>> Cases_on ‘p = []’ >- fs []
>> Cases_on ‘q = []’ >- rw []
>> Cases_on ‘p’ >> fs [subterm_width_def]
>> Cases_on ‘q’ >> fs [subterm_width_def]
>> T_TAC
>> Q.PAT_X_ASSUM ‘h' = h’ K_TAC
>> rename1 ‘t0 <<= t’
>> Q_TAC (TRANS_TAC LESS_EQ_TRANS)
‘MAX_SET
(IMAGE (hnf_children_size o principle_hnf)
{subterm' (FV M) M q 0 |
q |
q <<= FRONT (h::t) /\ solvable (subterm' (FV M) M q 0)})’
>> POP_ASSUM (REWRITE_TAC o wrap)
>> MATCH_MP_TAC SUBSET_MAX_SET
>> CONJ_TAC
>- (MATCH_MP_TAC IMAGE_FINITE \\
MATCH_MP_TAC FINITE_SUBSET \\
Q.EXISTS_TAC ‘{subterm' (FV M) M q 0 | q | q <<= FRONT (h::t0)}’ \\
reverse CONJ_TAC
>- (rw [SUBSET_DEF] \\
Q.EXISTS_TAC ‘q’ >> art []) \\
Know ‘{subterm' (FV M) M q 0 | q <<= FRONT (h::t0)} =
IMAGE (\q. subterm' (FV M) M q 0) {q | q <<= FRONT (h::t0)}’
>- (rw [Once EXTENSION] >> EQ_TAC >> rw []) >> Rewr' \\
MATCH_MP_TAC IMAGE_FINITE \\
rw [FINITE_prefix])
>> CONJ_TAC
>- (MATCH_MP_TAC IMAGE_FINITE \\
MATCH_MP_TAC FINITE_SUBSET \\
Q.EXISTS_TAC ‘{subterm' (FV M) M q 0 | q | q <<= FRONT (h::t)}’ \\
reverse CONJ_TAC
>- (rw [SUBSET_DEF] \\
Q.EXISTS_TAC ‘q’ >> art []) \\
Know ‘{subterm' (FV M) M q 0 | q <<= FRONT (h::t)} =
IMAGE (\q. subterm' (FV M) M q 0) {q | q <<= FRONT (h::t)}’
>- (rw [Once EXTENSION] >> EQ_TAC >> rw []) >> Rewr' \\
MATCH_MP_TAC IMAGE_FINITE \\
rw [FINITE_prefix])
>> rw [SUBSET_DEF]
>> Q.EXISTS_TAC ‘subterm' (FV M) M q 0’ >> art []
>> Q.EXISTS_TAC ‘q’ >> art []
>> Q_TAC (TRANS_TAC isPREFIX_TRANS) ‘FRONT (h::t0)’ >> art []
>> MATCH_MP_TAC IS_PREFIX_FRONT_MONO
>> simp []
QED

(* NOTE: ‘p <> []’ is necessary for ‘FRONT p’ to be meaningful, and then
subterm_valid_path_lemma makes sure that all involved ‘subterm X M q r’
are meaningful (IS_SOME).
Expand Down Expand Up @@ -6919,9 +6970,10 @@ Proof
>- (Q.X_GEN_TAC ‘i’ >> DISCH_TAC \\
Q.PAT_X_ASSUM ‘!i q. i < k /\ q <<= p ==> subterm X (M i) q r <> NONE’
(MP_TAC o Q.SPECL [‘i’, ‘q’]) >> simp [] \\
Cases_on ‘q’ >> fs [] \\
Q.PAT_X_ASSUM ‘!i. i < k ==> subterm_width (M i) p <= d’ drule \\
Cases_on ‘p’ >> fs [] \\
Q.PAT_X_ASSUM ‘h = h'’ (fs o wrap o SYM) \\
Cases_on ‘q’ >> fs [] \\
Q.PAT_X_ASSUM ‘h' = h’ (fs o wrap) >> T_TAC \\
simp [subterm_of_solvables] \\
Know ‘principle_hnf (H i) = H i’
>- (MATCH_MP_TAC principle_hnf_reduce \\
Expand All @@ -6931,7 +6983,8 @@ Proof
>- (rw [Abbr ‘H’, LAMl_size_appstar, GSYM appstar_APPEND]) \\
DISCH_TAC \\
simp [] \\
NTAC 2 (POP_ASSUM K_TAC) >> T_TAC \\
NTAC 2 (POP_ASSUM K_TAC) \\
DISCH_TAC \\
RNEWS_TAC (“ys' :string list”, “r :num”, “(n :num -> num) i”)
“X :string set” \\
qabbrev_tac ‘vs' = TAKE (n i) vs’ \\
Expand Down Expand Up @@ -7084,7 +7137,7 @@ Proof
DISCH_TAC \\
(* applying subterm_fresh_tpm_cong *)
DISCH_TAC (* subterm X (tpm pm N) t (SUC r) <> NONE *) \\
MP_TAC (Q.SPECL [‘pm’, ‘X’, ‘N’, ‘t’, ‘SUC r’] subterm_fresh_tpm_cong) \\
MP_TAC (Q.SPECL [‘pm’, ‘X’, ‘N’, ‘t'’, ‘SUC r’] subterm_fresh_tpm_cong) \\
impl_tac >- simp [Abbr ‘pm’, MAP_ZIP] \\
simp [] >> STRIP_TAC \\
POP_ASSUM K_TAC (* already used *) \\
Expand All @@ -7106,12 +7159,13 @@ Proof
simp [Abbr ‘ss’, Abbr ‘sub’] \\
simp [MAP_REVERSE, MAP_GENLIST, o_DEF]) \\
(* subterm_width N t <= d_max *)
Know ‘subterm_width (M i) (h::t) <= d’
>- cheat \\
Know ‘subterm_width (M i) (h::t') <= d’
>- (MATCH_MP_TAC subterm_width_inclusive \\
Q.EXISTS_TAC ‘h::t’ >> simp []) \\
qabbrev_tac ‘Ms' = args i ++ DROP (n i) (MAP VAR vs)’ \\
(* applying subterm_width_induction_lemma (the general one) *)
Suff ‘subterm_width (M i) (h::t) <= d <=>
m i <= d /\ subterm_width (EL h Ms') t <= d’
Suff ‘subterm_width (M i) (h::t') <= d <=>
m i <= d /\ subterm_width (EL h Ms') t' <= d’
>- (Rewr' \\
Know ‘EL h Ms' = N’
>- (simp [Abbr ‘Ms'’, Abbr ‘N’] \\
Expand All @@ -7128,7 +7182,7 @@ Proof
Q.EXISTS_TAC ‘M i’ >> art [] \\
rw [Abbr ‘M’, EL_MEM]) \\
MATCH_MP_TAC ltree_paths_inclusive \\
Q.EXISTS_TAC ‘h::t'’ >> simp []) >> DISCH_TAC \\
Q.EXISTS_TAC ‘h::t’ >> simp []) >> DISCH_TAC \\
(* NOTE: ‘solvable (subterm' X (M i) q r)’ only holds when ‘q <<= FRONT p’.
The case that ‘unsolvable (subterm' X (M j1/j2) q r)’ (p = q) must be
treated specially. In this case, ltree_el (BT' X (M i) r q = SOME bot.
Expand Down Expand Up @@ -7234,10 +7288,22 @@ Proof
Know ‘y i IN Z’ >- rw [] \\
Suff ‘Z SUBSET X UNION RANK r’ >- METIS_TAC [SUBSET_DEF] \\
FIRST_X_ASSUM ACCEPT_TAC) >> DISCH_TAC \\
Know ‘FV (tpm (REVERSE pm) N) SUBSET X UNION RANK r1 /\
(* some properties needed by the next "solvable" subgoal *)
Know ‘set vs SUBSET X UNION RANK r1’
>- (Suff ‘set vs SUBSET RANK r1’ >- SET_TAC [] \\
qunabbrev_tac ‘vs’ \\
MATCH_MP_TAC RNEWS_SUBSET_RANK >> simp [Abbr ‘r1’]) >> DISCH_TAC \\
Know ‘set ys SUBSET X UNION RANK r1’
>- (Suff ‘set ys SUBSET RANK r1’ >- SET_TAC [] \\
qunabbrev_tac ‘ys’ \\
MATCH_MP_TAC RNEWS_SUBSET_RANK >> simp [Abbr ‘r1’] \\
rw [LENGTH_NON_NIL]) >> DISCH_TAC \\
Know ‘FV (tpm (REVERSE pm) N) SUBSET X UNION RANK r1 /\
FV (tpm (REVERSE pm) N') SUBSET X UNION RANK r1’
>- (
cheat) >> STRIP_TAC \\
>- (CONJ_TAC \\
MATCH_MP_TAC FV_tpm_lemma \\
Q.EXISTS_TAC ‘r1’ >> simp [Abbr ‘pm’, MAP_REVERSE, MAP_ZIP]) \\
STRIP_TAC \\
Know ‘hnf_children_size N0 <= d_max /\ hnf_children_size N0' <= d_max’
>- (
cheat) >> STRIP_TAC \\
Expand Down

0 comments on commit 0198ba9

Please sign in to comment.