Skip to content

Commit

Permalink
Stage work on agree_upto_thm
Browse files Browse the repository at this point in the history
binghe committed Jan 20, 2025

Verified

This commit was signed with the committer’s verified signature. The key has expired.
binghe Chun Tian
1 parent 893fc41 commit 66211fa
Showing 2 changed files with 82 additions and 48 deletions.
24 changes: 12 additions & 12 deletions examples/lambda/barendregt/boehmScript.sml
Original file line number Diff line number Diff line change
@@ -43,9 +43,7 @@ val _ = set_trace "Goalstack.print_goal_at_top" 0;

fun PRINT_TAC pfx g = (print (pfx ^ "\n"); ALL_TAC g);

(* Disable some conflicting overloads from labelledTermsTheory, by
repeating the desired overloads again (this prioritizes them).
*)
(* Disable some conflicting overloads from labelledTermsTheory *)
Overload FV = “supp term_pmact”
Overload VAR = “term$VAR”

@@ -55,15 +53,12 @@ Overload VAR = “term$VAR”

(* The type of Boehm trees:
For each ltree node, ‘NONE’ represents {\bot} (for unsolvable terms), while
‘SOME (vs,y)’ represents ‘LAMl vs (VAR y)’. This separation of vs and y has
at least two advantages:
NOTE: For each ltree node, ‘NONE’ represents {\bot} for unsolvable terms, and
‘SOME (vs,y)’ represents ‘LAMl vs (VAR y)’. There are at least two advantages:
1. ‘set vs’ is the set of binding variables at that ltree node.
2. ‘LAMl vs (VAR y)’ can easily "expand" (w.r.t. eta reduction) into terms
such as ‘LAMl (vs ++ [z0;z1]) t’ (with two extra children ‘z0’ and ‘z1’)
without changing the head variable (VAR y).
such as “LAMl (vs ++ [z0;z1]) t” without changing the head variable.
*)
Type BT_node[pp] = “:(string list # string) option”
Type boehm_tree[pp] = “:BT_node ltree”
@@ -2662,11 +2657,10 @@ 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 :
Theorem unsolvable_apply :
!pi M. Boehm_transform pi /\ unsolvable M ==> unsolvable (apply pi M)
Proof
Induct_on ‘pi’ using SNOC_INDUCT
>- rw []
Induct_on ‘pi’ using SNOC_INDUCT >- rw []
>> simp [FOLDR_SNOC, Boehm_transform_SNOC]
>> qx_genl_tac [‘t’, ‘M’]
>> reverse (rw [solving_transform_def])
@@ -2676,6 +2670,12 @@ Proof
>> PROVE_TAC [solvable_APP_E]
QED

Theorem solvable_apply_imp :
!pi M. Boehm_transform pi /\ solvable (apply pi M) ==> solvable M
Proof
METIS_TAC [unsolvable_apply]
QED

(* Definition 10.3.5 (ii) *)
Definition head_original_def :
head_original M0 =
106 changes: 70 additions & 36 deletions examples/lambda/barendregt/lameta_completeScript.sml
Original file line number Diff line number Diff line change
@@ -8,7 +8,7 @@
open HolKernel Parse boolLib bossLib;

open hurdUtils arithmeticTheory pred_setTheory listTheory rich_listTheory
ltreeTheory llistTheory relationTheory;
ltreeTheory llistTheory relationTheory tautLib;

open termTheory basic_swapTheory appFOLDLTheory chap2Theory chap3Theory NEWLib
horeductionTheory solvableTheory head_reductionTheory head_reductionLib
@@ -798,10 +798,11 @@ QED
Theorem agree_upto_lemma :
!X Ms p r.
FINITE X /\ Ms <> [] /\ p <> [] /\ 0 < r /\
(!M. MEM M Ms ==> FV M SUBSET X UNION RANK r /\ p IN BT_paths M) ==>
(!M. MEM M Ms ==> FV M SUBSET X UNION RANK r) /\
(!M. MEM M Ms ==> p IN ltree_paths (BT' X M r)) ==>
?pi. Boehm_transform pi /\
(!M. MEM M Ms ==> is_ready' (apply pi M)) /\
(!M. MEM M Ms ==> p IN BT_paths (apply pi M)) /\
(!M. MEM M Ms ==> p IN ltree_paths (BT' X (apply pi M) r)) /\
(!M. MEM M Ms ==> FV (apply pi M) SUBSET X UNION RANK r) /\
(agree_upto X Ms p r ==>
agree_upto X (apply pi Ms) p r) /\
@@ -811,16 +812,13 @@ Theorem agree_upto_lemma :
Proof
rpt STRIP_TAC
>> MP_TAC (Q.SPECL [‘X’, ‘Ms’, ‘p’, ‘r’] subtree_equiv_lemma)
>> simp [BIGUNION_IMAGE_SUBSET, EVERY_MEM, MEM_MAP, GSYM BT_paths_thm]
>> simp [BIGUNION_IMAGE_SUBSET, EVERY_MEM, MEM_MAP]
>> STRIP_TAC
>> Q.EXISTS_TAC ‘pi’ >> rw []
>| [ (* goal 1 (of 4) *)
FIRST_X_ASSUM MATCH_MP_TAC \\
Q.EXISTS_TAC ‘M’ >> art [],
(* goal 2 (of 4) *)
MP_TAC (Q.SPECL [‘X’, ‘apply pi M’, ‘r’] BT_paths_thm) >> simp [] \\
impl_tac >- (FIRST_X_ASSUM MATCH_MP_TAC \\
Q.EXISTS_TAC ‘M’ >> art []) >> Rewr' \\
FIRST_X_ASSUM MATCH_MP_TAC \\
Q.EXISTS_TAC ‘M’ >> art [],
(* goal 3 (of 4) *)
@@ -870,7 +868,8 @@ QED
*)
Theorem agree_upto_thm :
!X p Ms r. FINITE X /\ Ms <> [] /\ 0 < r /\
(!M. MEM M Ms ==> FV M SUBSET X UNION RANK r /\ p IN BT_paths M) /\
(!M. MEM M Ms ==> FV M SUBSET X UNION RANK r) /\
(!M. MEM M Ms ==> p IN ltree_paths (BT' X M r)) /\
agree_upto X Ms p r ==>
?pi. Boehm_transform pi /\ is_faithful p X Ms pi r
Proof
@@ -882,22 +881,22 @@ Proof
(* trivial case: all unsolvable *)
>> Cases_on ‘!M. MEM M Ms ==> unsolvable M’
>- (Q.EXISTS_TAC ‘[]’ \\
rw []
>- (MP_TAC (Q.SPECL [‘X’, ‘M’, ‘r’] BT_valid_paths_thm') >> rw [] \\
Know ‘subterm X M (h::p) r = NONE <=> h::p NOTIN BT_paths M
>- (Suff ‘h::p IN BT_paths M <=> subterm X M (h::p) r <> NONE
>- PROVE_TAC [] \\
MATCH_MP_TAC IN_BT_paths >> simp []) >> Rewr' \\
STRONG_DISJ_TAC \\
Suff ‘solvable M’ >- METIS_TAC [] \\
MATCH_MP_TAC ltree_paths_imp_solvable \\
qexistsl_tac [‘h::p’, ‘X’, ‘r’] >> simp [GSYM BT_paths_thm]) \\
fs [agree_upto_def] \\
Know ‘equivalent M N <=> subtree_equiv X M N [] r’
>- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
MATCH_MP_TAC subtree_equiv_alt_equivalent >> art [] \\
fs [BIGUNION_IMAGE_SUBSET]) >> Rewr' \\
FIRST_X_ASSUM irule >> rw [])
reverse (rw [])
>- (fs [agree_upto_def] \\
Know ‘equivalent M N <=> subtree_equiv X M N [] r
>- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
MATCH_MP_TAC subtree_equiv_alt_equivalent >> art [] \\
fs [BIGUNION_IMAGE_SUBSET]) >> Rewr' \\
FIRST_X_ASSUM irule >> rw []) \\
MP_TAC (Q.SPECL [‘X’, ‘M’, ‘r’] BT_valid_paths_thm') >> rw [] \\
Know ‘subterm X M (h::p) r = NONE <=> h::p NOTIN ltree_paths (BT' X M r)’
>- (Suff ‘h::p IN ltree_paths (BT' X M r) <=> subterm X M (h::p) r <> NONE
>- PROVE_TAC [] \\
MATCH_MP_TAC BT_ltree_paths_thm >> simp []) >> Rewr' \\
STRONG_DISJ_TAC \\
Suff ‘solvable M’ >- METIS_TAC [] \\
MATCH_MP_TAC ltree_paths_imp_solvable \\
qexistsl_tac [‘h::p’, ‘X’, ‘r’] >> simp [])
(* one is solvable, all are solvable *)
>> Know ‘!M. MEM M Ms ==> solvable M’
>- (rpt STRIP_TAC \\
@@ -973,7 +972,7 @@ Proof
‘h < m’, as otherwise p1 (the selector) cannot be properly defined.
*)
>> Know ‘h < m’
>- (Q.PAT_X_ASSUM ‘!i. i < k ==> h::p IN BT_paths (apply p0 (M i))’
>- (Q.PAT_X_ASSUM ‘!i. i < k ==> h::p IN ltree_paths (BT' X (apply p0 (M i)) r)’
(MP_TAC o Q.SPEC ‘0’) >> simp [] \\
MP_TAC (Q.SPECL [‘X’, ‘apply p0 ((M :num -> term) 0)’, ‘r’ ] BT_paths_thm) \\
simp [] >> DISCH_THEN K_TAC \\
@@ -1007,8 +1006,13 @@ Proof
POP_ASSUM MATCH_MP_TAC >> rw [EL_MEM]) >> Rewr' \\
MATCH_MP_TAC hreduce_selector >> rw [])
>> DISCH_TAC
(* redefine Ns as the h-subterms of Ms *)
(* redefine Ns as the h-subterms of Ms
NOTE: So far we don't know if any “EL h (f i)” is solvable, thus it's not
sure whether “principle_hnf (apply (p1 ++ p0) (M i)) = EL h (f i)”.
*)
>> qabbrev_tac ‘Ns = GENLIST (EL h o f) k’
>> ‘LENGTH Ns = k’ by rw [Abbr ‘Ns’, LENGTH_GENLIST]
(* proving one antecedent of IH *)
>> Know ‘agree_upto X Ns p (SUC r)’
>- (fs [agree_upto_def] \\
@@ -1047,15 +1051,22 @@ Proof
Abbr ‘vs’, EL_MAP])
>> DISCH_TAC
(* another antecedent of IH *)
>> Know ‘!P. MEM P Ns ==> FV P SUBSET X UNION RANK (SUC r) /\ p IN BT_paths P
>> Know ‘!P. MEM P Ns ==> FV P SUBSET X UNION RANK (SUC r)’
>- (simp [MEM_EL, Abbr ‘Ns’] \\
NTAC 2 STRIP_TAC \\
POP_ORW >> simp [EL_GENLIST] \\
STRONG_CONJ_TAC
>- (MATCH_MP_TAC subterm_induction_lemma' \\
qexistsl_tac [‘apply p0 (M n)’, ‘N n’, ‘0’, ‘m’, ‘[]’, ‘N n’] \\
simp []) >> DISCH_TAC \\
Q.PAT_X_ASSUM ‘!i. i < k ==> h::p IN BT_paths (apply p0 (M i))’
MATCH_MP_TAC subterm_induction_lemma' \\
qexistsl_tac [‘apply p0 (M n)’, ‘N n’, ‘0’, ‘m’, ‘[]’, ‘N n’] \\
simp [])
>> DISCH_TAC
>> Know ‘!P. MEM P Ns ==> p IN ltree_paths (BT' X P (SUC r))’
>- (Q.X_GEN_TAC ‘P’ >> DISCH_TAC \\
Q.PAT_X_ASSUM ‘!P. MEM P Ns ==> FV P SUBSET X UNION RANK (SUC r)’ drule \\
POP_ASSUM MP_TAC \\
simp [MEM_EL, Abbr ‘Ns’] \\
STRIP_TAC >> POP_ORW \\
simp [EL_GENLIST] >> DISCH_TAC \\
Q.PAT_X_ASSUM ‘!i. i < k ==> h::p IN ltree_paths (BT' X (apply p0 (M i)) r)’
(MP_TAC o Q.SPEC ‘n’) >> simp [] \\
MP_TAC (Q.SPECL [‘X’, ‘apply p0 ((M :num -> term) n)’, ‘r’ ] BT_paths_thm) \\
simp [] >> DISCH_THEN K_TAC \\
@@ -1073,12 +1084,35 @@ Proof
Abbr ‘y'’, Abbr ‘Ms'’, Abbr ‘n'’, Abbr ‘l’, Abbr ‘M1’, Abbr ‘vs’])
>> DISCH_TAC
>> ‘Ns <> []’ by rw [Abbr ‘Ns’, NOT_NIL_EQ_LENGTH_NOT_0]
(* using IH *)
>> Q.PAT_X_ASSUM
‘!Ns r'. _ ==> ?pi. Boehm_transform pi /\ is_faithful p X Ns pi r'’
‘!Ms' r'. Ms' <> [] /\ 0 < r' /\ _ ==>
?pi. Boehm_transform pi /\ is_faithful p X Ms' pi r'’
(MP_TAC o Q.SPECL [‘Ns’, ‘SUC r’])
>> simp []
>> simp [is_faithful_def]
>> Q.PAT_X_ASSUM ‘Ns <> []’ K_TAC
>> DISCH_THEN (Q.X_CHOOSE_THEN ‘p2’ STRIP_ASSUME_TAC)
>> qabbrev_tac ‘pi = p2 ++ p1 ++ p0’
>> Q.EXISTS_TAC ‘pi’
>> CONJ_TAC (* Boehm_transform pi *)
>- (qunabbrev_tac ‘pi’ \\
MATCH_MP_TAC Boehm_transform_APPEND >> art [] \\
MATCH_MP_TAC Boehm_transform_APPEND >> art [])
>> simp [Abbr ‘pi’, GSYM APPEND_ASSOC]
>> qabbrev_tac ‘pi' = p1 ++ p0’
>> REWRITE_TAC [Boehm_apply_APPEND]
>> STRONG_CONJ_TAC
>- (rpt STRIP_TAC \\
cheat)
>> DISCH_TAC
(* stage work *)
>> simp [MEM_EL]
>> qx_genl_tac [‘t1’, ‘t2’] (* temp name *)
>> ONCE_REWRITE_TAC [TAUT ‘P /\ Q ==> R <=> P ==> Q ==> R’]
>> DISCH_THEN (Q.X_CHOOSE_THEN ‘a’ STRIP_ASSUME_TAC)
>> DISCH_THEN (Q.X_CHOOSE_THEN ‘b’ STRIP_ASSUME_TAC)
>> Q.PAT_X_ASSUM ‘_ = M a’ (ONCE_REWRITE_TAC o wrap)
>> Q.PAT_X_ASSUM ‘_ = M b’ (ONCE_REWRITE_TAC o wrap)
>> cheat
QED

@@ -1576,9 +1610,9 @@ Proof
>> STRONG_CONJ_TAC
>- rw [Abbr ‘pi’, Boehm_transform_def, EVERY_SNOC, EVERY_MAP]
>> DISCH_TAC
(* applying Boehm_transform_of_unsolvables *)
(* applying unsolvable_apply *)
>> reverse CONJ_TAC
>- (MATCH_MP_TAC Boehm_transform_of_unsolvables >> art [])
>- (MATCH_MP_TAC unsolvable_apply >> art [])
(* stage work *)
>> MATCH_MP_TAC lameq_TRANS
>> Q.EXISTS_TAC ‘apply pi M0’

0 comments on commit 66211fa

Please sign in to comment.