Skip to content

Commit

Permalink
Stage work on agree_upto_lemma
Browse files Browse the repository at this point in the history
  • Loading branch information
@binghe
binghe committed Nov 11, 2024
1 parent 60b2af8 commit 09832c3
Showing 1 changed file with 102 additions and 64 deletions.
166 changes: 102 additions & 64 deletions examples/lambda/barendregt/boehmScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1238,14 +1238,16 @@ Theorem BT_subterm_thm :
!p X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\
subterm X M p r <> NONE /\ solvable (subterm' X M p r)
==> do (N,r') <- subterm X M p r;
(t,m) <- ltree_el (BT' X M r) p;
(t,m') <- ltree_el (BT' X M r) p;
(xs,y) <- t;
m <- m';
M0 <<- principle_hnf N;
n <<- LAMl_size M0;
vs <<- RNEWS r' n X;
M1 <<- principle_hnf (M0 @* MAP VAR vs);
return (vs = xs /\
hnf_children_size M0 = THE m /\
LAMl_size M0 = n /\
hnf_children_size M0 = m /\
hnf_headvar M1 = y /\
DISJOINT (set vs) (FV M0) /\
r' = r + LENGTH p /\
Expand Down Expand Up @@ -1284,7 +1286,7 @@ Proof
>- (MATCH_MP_TAC subterm_rank_lemma \\
Q.EXISTS_TAC ‘M’ >> art [])
>> STRIP_TAC
>> simp [Abbr ‘y’]
>> simp [Abbr ‘y’, Once EQ_SYM_EQ]
>> MATCH_MP_TAC hnf_children_size_alt
>> qexistsl_tac [‘X’, ‘N’, ‘r'’, ‘n’, ‘vs’, ‘M1’] >> simp []
QED
Expand Down Expand Up @@ -6979,57 +6981,58 @@ Proof
(* applying BT_subterm_thm *)
MP_TAC (Q.SPECL [‘p’, ‘X’, ‘M (j1 :num)’, ‘r’] BT_subterm_thm) \\
rw [] >> fs [] \\
rename1 ‘(\(N,r). NONE) z = SOME T’ \\
rename1 ‘(\ (N,r). NONE) z = SOME T’ \\
Cases_on ‘z’ >> fs []) \\
(* stage work, now applying BT_subterm_thm on ‘M j1’ *)
MP_TAC (Q.SPECL [‘q’, ‘X’, ‘M (j1 :num)’, ‘r’] BT_subterm_thm) \\
simp [] >> STRIP_TAC (* this asserts ‘x’ *) \\
NTAC 3 (Cases_on ‘x’ >> fs []) \\
rename [‘subterm X (M j1) q r = SOME (N,r + LENGTH q)’,
‘ltree_el (BT' X (M j1) r) q = SOME (SOME (vs1,y1),m1)’] \\
Q.PAT_X_ASSUM ‘_ = SOME (vs1,y1)’ K_TAC >> gs [] \\
qabbrev_tac ‘n1 = LAMl_size (principle_hnf N)’ \\
qabbrev_tac ‘r1 = r + LENGTH q’ \\
rename1 ‘subterm X (M j1) q r = SOME (N,r1)’ \\
qabbrev_tac ‘N0 = principle_hnf N’ \\
qabbrev_tac ‘m1 = hnf_children_size N0’ \\
rename1 ‘ltree_el (BT' X (M j1) r) q = SOME (SOME (vs1,y1),SOME m1)’ \\
Q.PAT_X_ASSUM ‘_ = SOME (vs1,y1)’ K_TAC >> gs [] \\
Q.PAT_X_ASSUM ‘_ = r1’ K_TAC \\
Q.PAT_X_ASSUM ‘_ = SOME m1’ K_TAC \\
qabbrev_tac ‘n1 = LAMl_size N0’ \\
(* applying BT_subterm_thm again *)
MP_TAC (Q.SPECL [‘q’, ‘X’, ‘M (j2 :num)’, ‘r’] BT_subterm_thm) \\
simp [] >> STRIP_TAC (* this asserts ‘x’ *) \\
NTAC 3 (Cases_on ‘x’ >> fs []) \\
rename [‘subterm X (M j2) q r = SOME (N',r1)’,
‘ltree_el (BT' X (M j2) r) q = SOME (SOME (vs2,y2),m2)’] \\
rename1 ‘subterm X (M j2) q r = SOME (N',r1)’ \\
qabbrev_tac ‘N0' = principle_hnf N'’ \\
qabbrev_tac ‘m2 = hnf_children_size N0'’ \\
rename1 ‘ltree_el (BT' X (M j2) r) q = SOME (SOME (vs2,y2),SOME m2)’ \\
Q.PAT_X_ASSUM ‘_ = SOME (vs2,y2)’ K_TAC >> gs [] \\
qabbrev_tac ‘n2 = LAMl_size (principle_hnf N')’ \\
STRIP_TAC (* vs1 = vs2 /\ y1 = y2 /\ m1 = m2 *) \\
NTAC 3 (POP_ASSUM (fs o wrap o SYM)) \\
Q.PAT_X_ASSUM ‘_ = r1’ K_TAC \\
Q.PAT_X_ASSUM ‘_ = SOME m2’ K_TAC \\
qabbrev_tac ‘n2 = LAMl_size N0'’ \\
DISCH_THEN (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [EQ_SYM_EQ])) \\
‘n2 = n1’ by PROVE_TAC [Abbr ‘n2’, RNEWS_11'] \\
(* decompose N *)
Q.PAT_X_ASSUM ‘RNEWS r1 n1 X = vs1’ (fs o wrap o SYM) \\
Q_TAC (RNEWS_TAC (“vs1 :string list”, “r1 :num”, “n1 :num”)) ‘X’ \\
qabbrev_tac ‘N0 = principle_hnf N’ \\
qabbrev_tac ‘N1 = principle_hnf (N0 @* MAP VAR vs1)’ \\
Q_TAC (HNF_TAC (“N0 :term”, “vs1 :string list”,
“y1' :string”, “Ns1 :term list”)) ‘N1’ \\
‘TAKE (LAMl_size N0) vs1 = vs1’ by rw [] \\
POP_ASSUM (rfs o wrap) \\
‘hnf_children_size N0 = LENGTH Ns1 /\
hnf_headvar (principle_hnf (N0 @* MAP VAR vs1)) = y1'’ by gs [] \\
NTAC 2 (POP_ASSUM (fs o wrap)) >> T_TAC \\
POP_ASSUM (rfs o wrap) >> T_TAC \\
‘LENGTH Ns1 = m1 /\ hnf_headvar (principle_hnf (N0 @* MAP VAR vs1)) = y1'’
by gs [Abbr ‘m1’] \\
Q.PAT_X_ASSUM ‘N0 = LAMl vs1 (VAR y1' @* Ns1)’ (ASSUME_TAC o SYM) \\
Q.PAT_X_ASSUM ‘y1' = y1’ (fs o wrap) \\
Q.PAT_X_ASSUM ‘r' = r1’ K_TAC \\
Q.PAT_X_ASSUM ‘r'' = r1’ K_TAC \\
(* decompose N' *)
qabbrev_tac ‘N0' = principle_hnf N'’ \\
qabbrev_tac ‘N1' = principle_hnf (N0' @* MAP VAR vs1)’ \\
Q_TAC (HNF_TAC (“N0' :term”, “vs1 :string list”,
“y2' :string”, “Ns2 :term list”)) ‘N1'’ \\
‘TAKE (LAMl_size N0') vs1 = vs1’ by rw [] \\
POP_ASSUM (rfs o wrap) \\
‘hnf_children_size N0' = LENGTH Ns2 /\
hnf_headvar (principle_hnf (N0' @* MAP VAR vs1)) = y2'’ by gs [] \\
NTAC 2 (POP_ASSUM (fs o wrap)) >> T_TAC \\
‘LENGTH Ns2 = m2 /\ hnf_headvar (principle_hnf (N0' @* MAP VAR vs1)) = y2'’
by gs [Abbr ‘m2’] \\
Q.PAT_X_ASSUM ‘N0' = LAMl vs1 (VAR y2' @* Ns2)’ (ASSUME_TAC o SYM) \\
Q.PAT_X_ASSUM ‘y2' = y1’ (fs o wrap) \\
‘LENGTH Ns2 = LENGTH Ns1’ by rw [] (* THE m1 *) \\
gs [] \\
Q.PAT_X_ASSUM ‘y2' = y1'’ (fs o wrap o SYM) \\
Q.PAT_X_ASSUM ‘y2 = y2'’ (fs o wrap o SYM) \\
(* stage work, preparing for BT_subterm_thm on ‘H j1’ and ‘H j2’*)
Know ‘subterm X (H j1) q r <> NONE /\
subterm X (H j2) q r <> NONE’
Expand Down Expand Up @@ -7063,25 +7066,14 @@ Proof
NOTE: This subgoal is only possible with the latest ‘subterm_width’
*)
Know ‘hnf_children_size N0 <= d_max /\
hnf_children_size N0' <= d_max’
>- (CONJ_TAC >| (* 2 subgoals *)
[ (* goal 1 (of 2) *)
qunabbrev_tac ‘N0’ \\
Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ \\
reverse CONJ_TAC >- rw [Abbr ‘d_max’] \\
Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_width (M j1) p’ \\
reverse CONJ_TAC >- simp [] \\
‘N = subterm' X (M j1) q r’ by rw [] >> POP_ORW \\
MATCH_MP_TAC subterm_width_last >> simp [],
(* goal 2 (of 2) *)
qunabbrev_tac ‘N0'’ \\
Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ \\
reverse CONJ_TAC >- rw [Abbr ‘d_max’] \\
Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_width (M j2) p’ \\
reverse CONJ_TAC >- simp [] \\
‘N' = subterm' X (M j2) q r’ by rw [] >> POP_ORW \\
MATCH_MP_TAC subterm_width_last >> simp [] ]) >> STRIP_TAC \\
Know ‘m1 <= d_max’ (* NOTE: m1 = hnf_children_size N0 *)
>- (Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ \\
reverse CONJ_TAC >- rw [Abbr ‘d_max’] \\
Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_width (M j1) p’ \\
reverse CONJ_TAC >- simp [] \\
qunabbrevl_tac [‘m1’, ‘N0’] \\
‘N = subterm' X (M j1) q r’ by rw [] >> POP_ORW \\
MATCH_MP_TAC subterm_width_last >> simp []) >> DISCH_TAC \\
Know ‘solvable (subterm' X (H j1) q r) /\
solvable (subterm' X (H j2) q r)’
>- (ASM_SIMP_TAC std_ss [] \\
Expand All @@ -7098,37 +7090,42 @@ Proof
MP_TAC (Q.SPECL [‘q’, ‘X’, ‘H (j1 :num)’, ‘r’] BT_subterm_thm) \\
simp [] >> STRIP_TAC (* this asserts ‘x’ *) \\
NTAC 3 (Cases_on ‘x’ >> fs []) >> T_TAC \\
rename [‘subterm X (H j1) q r = SOME (W,r1)’,
‘ltree_el (BT' X (H j1) r) q = SOME (SOME (vs3,y3),m3)’] \\
Q.PAT_X_ASSUM ‘_ = SOME (vs3,y3)’ K_TAC >> fs [] \\
qabbrev_tac ‘n3 = LAMl_size (principle_hnf W)’ \\
rename1 ‘subterm X (H j1) q r = SOME (W,r1)’ \\
qabbrev_tac ‘W0 = principle_hnf W’ \\
qabbrev_tac ‘m3 = hnf_children_size W0’ \\
rename1 ‘ltree_el (BT' X (H j1) r) q = SOME (SOME (vs3,y3),SOME m3)’ \\
Q.PAT_X_ASSUM ‘_ = SOME (vs3,y3)’ K_TAC \\
Q.PAT_X_ASSUM ‘_ = SOME m3’ K_TAC \\
qabbrev_tac ‘n3 = LAMl_size W0’ \\
Q.PAT_X_ASSUM ‘_ = r1’ (fs o wrap) \\
(* decompose W *)
Q.PAT_X_ASSUM ‘RNEWS r1 n3 X = vs3’ (fs o wrap o SYM) \\
Q_TAC (RNEWS_TAC (“vs3 :string list”, “r1 :num”, “n3 :num”)) ‘X’ \\
qabbrev_tac ‘W0 = principle_hnf W’ \\
qabbrev_tac ‘W1 = principle_hnf (W0 @* MAP VAR vs3)’ \\
Q_TAC (HNF_TAC (“W0 :term”, “vs3 :string list”,
“y3' :string”, “Ns3 :term list”)) ‘W1’ \\
Q.PAT_X_ASSUM ‘DISJOINT (set vs3) (FV W0)’ K_TAC \\
‘TAKE (LAMl_size W0) vs3 = vs3’ by rw [] \\
POP_ASSUM (fs o wrap) \\
‘hnf_children_size W0 = LENGTH Ns3 /\
POP_ASSUM (fs o wrap) >> T_TAC \\
‘hnf_children_size W0 = m3 /\
hnf_headvar (principle_hnf (W0 @* MAP VAR vs3)) = y3'’ by gs [] \\
NTAC 2 (POP_ASSUM (fs o wrap)) >> T_TAC \\
Q.PAT_X_ASSUM ‘y3' = y3’ (fs o wrap) \\
Q.PAT_X_ASSUM ‘W0 = LAMl vs3 (VAR y3 @* Ns3)’ (ASSUME_TAC o SYM) \\
(* applying BT_subterm_thm on ‘H j2’ *)
MP_TAC (Q.SPECL [‘q’, ‘X’, ‘H (j2 :num)’, ‘r’] BT_subterm_thm) \\
simp [] >> STRIP_TAC (* this asserts ‘x’ *) \\
NTAC 3 (Cases_on ‘x’ >> fs []) >> T_TAC \\
rename [‘subterm X (H j2) q r = SOME (W',r1)’,
‘ltree_el (BT' X (H j2) r) q = SOME (SOME (vs4,y4),m4)’] \\
Q.PAT_X_ASSUM ‘_ = SOME (vs4,y4)’ K_TAC >> fs [] \\
qabbrev_tac ‘n4 = LAMl_size (principle_hnf W')’ \\
rename1 ‘subterm X (H j2) q r = SOME (W',r1)’ \\
qabbrev_tac ‘W0' = principle_hnf W'’ \\
qabbrev_tac ‘m4 = hnf_children_size W0'’ \\
rename1 ‘ltree_el (BT' X (H j2) r) q = SOME (SOME (vs4,y4),SOME m4)’ \\
Q.PAT_X_ASSUM ‘_ = SOME (vs4,y4)’ K_TAC \\
Q.PAT_X_ASSUM ‘_ = SOME m4’ K_TAC \\
qabbrev_tac ‘n4 = LAMl_size W0'’ \\
Q.PAT_X_ASSUM ‘_ = r1’ (fs o wrap) \\
(* decompose W' *)
Q.PAT_X_ASSUM ‘RNEWS r1 n4 X = vs4’ (fs o wrap o SYM) \\
Q_TAC (RNEWS_TAC (“vs4 :string list”, “r1 :num”, “n4 :num”)) ‘X’ \\
qabbrev_tac ‘W0' = principle_hnf W'’ \\
qabbrev_tac ‘W1' = principle_hnf (W0' @* MAP VAR vs4)’ \\
Q_TAC (HNF_TAC (“W0' :term”, “vs4 :string list”,
“y4' :string”, “Ns4 :term list”)) ‘W1'’ \\
Expand All @@ -7138,30 +7135,71 @@ Proof
Q.PAT_X_ASSUM ‘y4' = y4’ (fs o wrap) \\
Q.PAT_X_ASSUM ‘W0' = LAMl vs4 (VAR y4 @* Ns4)’ (ASSUME_TAC o SYM) \\
gs [GSYM CONJ_ASSOC] >> T_TAC \\
Q.PAT_X_ASSUM ‘r' = r1’ K_TAC \\
Q.PAT_X_ASSUM ‘r'' = r1’ K_TAC \\
Know ‘W = tpm (REVERSE pm) N ISUB ss’
>- (Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) q r <> NONE /\ _’
(MP_TAC o Q.SPEC ‘j1’) >> simp []) >> DISCH_TAC \\
Know ‘W' = tpm (REVERSE pm) N' ISUB ss’
>- (Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) q r <> NONE /\ _’
(MP_TAC o Q.SPEC ‘j2’) >> simp []) >> DISCH_TAC \\
Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) q r <> NONE /\ _’ K_TAC \\
Q.PAT_X_ASSUM ‘n2 = n1’ K_TAC \\
(* stage work, applying hreduce_ISUB and tpm_hreduces *)
‘N -h->* N0 /\ N' -h->* N0'’ by METIS_TAC [principle_hnf_thm'] \\
Know ‘W -h->* tpm (REVERSE pm) N0 ISUB ss /\
W' -h->* tpm (REVERSE pm) N0' ISUB ss’
>- (simp [hreduce_ISUB, tpm_hreduces]) \\
Q.PAT_X_ASSUM ‘y1 = y2’ (fs o wrap o SYM) \\
Q.PAT_X_ASSUM ‘LAMl vs1 (VAR y1 @* Ns1) = N0’ (REWRITE_TAC o wrap o SYM) \\
Q.PAT_X_ASSUM ‘LAMl vs1 (VAR y1 @* Ns2) = N0'’ (REWRITE_TAC o wrap o SYM) \\
Q.PAT_X_ASSUM ‘W = tpm (REVERSE pm) N ISUB ss’ (ASSUME_TAC o SYM) \\
Q.PAT_X_ASSUM ‘W' = tpm (REVERSE pm) N' ISUB ss’ (ASSUME_TAC o SYM) \\
simp [tpm_LAMl, tpm_appstar] \\
qabbrev_tac ‘vs1' = listpm string_pmact (REVERSE pm) vs1’ \\
qabbrev_tac ‘y1' = VAR (lswapstr (REVERSE pm) y1)’ \\
qabbrev_tac ‘y1' = lswapstr (REVERSE pm) y1’ \\
qabbrev_tac ‘Ns1' = listpm term_pmact (REVERSE pm) Ns1’ \\
qabbrev_tac ‘Ns2' = listpm term_pmact (REVERSE pm) Ns2’ \\
(* pm = ZIP (vs,ys), where ys is in ROW r, vs is in ROW 0.
vs1 is in ROW r1 = r + LENGTH q > r, as q <> [].
*)
Know ‘listpm string_pmact (REVERSE pm) vs1 = vs1’
>- (
cheat) >> Rewr' \\
(* NOTE: DOM ss = IMAGE y k, SUBSET Z, SUBSET X UNION RANK r *)
Know ‘DISJOINT (set vs1) (DOM ss)’
>- (
cheat) >> DISCH_TAC \\
simp [LAMl_ISUB, appstar_ISUB] \\
qabbrev_tac ‘Ns1'' = MAP (\t. t ISUB ss) Ns1'’ \\
qabbrev_tac ‘Ns2'' = MAP (\t. t ISUB ss) Ns2'’ \\
(* easy case *)
reverse (Cases_on ‘y1' IN DOM ss’)
>- (simp [ISUB_VAR_FRESH'] >> STRIP_TAC \\
‘hnf (LAMl vs1 (VAR y1' @* Ns1'')) /\
hnf (LAMl vs1 (VAR y1' @* Ns2''))’ by rw [hnf_appstar] \\
‘LAMl vs1 (VAR y1' @* Ns1'') = W0 /\
LAMl vs1 (VAR y1' @* Ns2'') = W0'’ by METIS_TAC [principle_hnf_thm'] \\
‘LAMl_size W0 = n1 /\ LAMl_size W0' = n1’ by rw [LAMl_size_hnf] \\
Know ‘n3 = n1’
>- (Q.PAT_X_ASSUM ‘LENGTH vs3 = n3’ (REWRITE_TAC o wrap o SYM) \\
Q.PAT_X_ASSUM ‘LAMl_size W0 = n1’ (REWRITE_TAC o wrap o SYM) \\
Q.PAT_X_ASSUM ‘LAMl vs3 (VAR y3 @* Ns3) = W0’ (simp o wrap o SYM)) \\
DISCH_TAC \\
Know ‘n4 = n1’
>- (Q.PAT_X_ASSUM ‘LENGTH vs4 = n4’ (REWRITE_TAC o wrap o SYM) \\
Q.PAT_X_ASSUM ‘LAMl_size W0' = n1’ (REWRITE_TAC o wrap o SYM) \\
Q.PAT_X_ASSUM ‘LAMl vs4 (VAR y4 @* Ns4) = W0'’ (simp o wrap o SYM)) \\
DISCH_TAC \\
fs [] (* ‘vs3 = vs4’ is proved here *) \\
Know ‘y3 = y1' /\ y4 = y1' /\ Ns1'' = Ns3 /\ Ns2'' = Ns4’
>- (Q.PAT_X_ASSUM ‘LAMl vs3 (VAR y3 @* Ns3) = W0’ MP_TAC \\
Q.PAT_X_ASSUM ‘_ = W0’ (REWRITE_TAC o wrap o SYM) \\
Q.PAT_X_ASSUM ‘LAMl vs4 (VAR y4 @* Ns4) = W0'’ MP_TAC \\
Q.PAT_X_ASSUM ‘_ = W0'’ (REWRITE_TAC o wrap o SYM) \\
simp []) >> STRIP_TAC \\
simp [] \\
(* last goal: m3 = m4 *)
qunabbrevl_tac [‘m3’, ‘m4’] \\
NTAC 2 (POP_ASSUM (REWRITE_TAC o wrap o SYM)) \\
simp [Abbr ‘Ns1''’, Abbr ‘Ns2''’] \\
simp [Abbr ‘Ns1'’, Abbr ‘Ns2'’]) \\
cheat)
QED

Expand Down

0 comments on commit 09832c3

Please sign in to comment.