From 893fc4107d1b7e9c57c375df475d17b3aa328cde Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Mon, 20 Jan 2025 15:48:06 +1100 Subject: [PATCH] Stage work on agree_upto_thm --- examples/lambda/barendregt/boehmScript.sml | 11 +- examples/lambda/barendregt/chap2Script.sml | 42 +++++ .../barendregt/head_reductionScript.sml | 27 ++++ .../barendregt/lameta_completeScript.sml | 149 +++++++++++++++--- 4 files changed, 204 insertions(+), 25 deletions(-) diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml index f494da2a4c..f78e3d902e 100644 --- a/examples/lambda/barendregt/boehmScript.sml +++ b/examples/lambda/barendregt/boehmScript.sml @@ -60,6 +60,7 @@ Overload VAR = “term$VAR” 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). @@ -119,7 +120,7 @@ Definition subterm_def : NONE End -(* NOTE: The use of ‘subterm' X M p r’ assumes that ‘subterm X M p r <> NONE’ *) +(* The use of ‘subterm' X M p r’ assumes that ‘subterm X M p r <> NONE’ *) Overload subterm' = “\X M p r. FST (THE (subterm X M p r))” (* |- subterm X M [] r = SOME (M,r) *) @@ -234,8 +235,8 @@ Proof >> qexistsl_tac [‘X’, ‘M’, ‘r’, ‘n’, ‘n’] >> simp [] QED -(* NOTE: Essentially, ‘hnf_children_size (principle_hnf M)’ is irrelevant with - the excluding list. This lemma shows the equivalence in defining ‘m’. +(* Essentially, ‘hnf_children_size (principle_hnf M)’ is irrelevant with + the excluding list. This lemma shows the equivalence in defining ‘m’. *) Theorem hnf_children_size_alt : !X M r M0 n vs M1 Ms. @@ -1021,6 +1022,7 @@ Proof >> qexistsl_tac [‘M’, ‘M0’, ‘n’, ‘m’, ‘vs’, ‘M1’] >> simp [] QED +(* NOTE: cf. BT_paths M *) Theorem BT_ltree_paths_thm : !X M p r. FINITE X /\ FV M SUBSET X UNION RANK r ==> (p IN ltree_paths (BT' X M r) <=> subterm X M p r <> NONE) @@ -1030,8 +1032,7 @@ QED Theorem subterm_imp_ltree_paths : !p X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ - subterm X M p r <> NONE ==> - p IN ltree_paths (BT' X M r) + subterm X M p r <> NONE ==> p IN ltree_paths (BT' X M r) Proof PROVE_TAC [BT_ltree_paths_thm] QED diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml index 8bd9d214b7..af377fcb52 100644 --- a/examples/lambda/barendregt/chap2Script.sml +++ b/examples/lambda/barendregt/chap2Script.sml @@ -1454,6 +1454,48 @@ QED (* |- !i n. i < n ==> FV (selector i n) = {} *) Theorem FV_selector[simp] = REWRITE_RULE [closed_def] closed_selector +Theorem selector_alt : + !X i n. FINITE X /\ i < n ==> + ?vs v. LENGTH vs = n /\ ALL_DISTINCT vs /\ DISJOINT X (set vs) /\ + v = EL i vs /\ selector i n = LAMl vs (VAR v) +Proof + RW_TAC std_ss [selector_def] + >> qabbrev_tac ‘Z = GENLIST n2s n’ + >> ‘ALL_DISTINCT Z /\ LENGTH Z = n’ by rw [Abbr ‘Z’, ALL_DISTINCT_GENLIST] + >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0] + >> qabbrev_tac ‘z = EL i Z’ + >> ‘MEM z Z’ by rw [Abbr ‘z’, EL_MEM] + >> ‘n2s i = z’ by rw [Abbr ‘z’, Abbr ‘Z’, EL_GENLIST] + >> POP_ORW + (* preparing for LAMl_ALPHA_ssub *) + >> qabbrev_tac ‘Y = NEWS n (set Z UNION X)’ + >> ‘FINITE (set Z UNION X)’ by rw [] + >> ‘ALL_DISTINCT Y /\ DISJOINT (set Y) (set Z UNION X) /\ LENGTH Y = n’ + by rw [NEWS_def, Abbr ‘Y’] + >> fs [] + >> qabbrev_tac ‘M = VAR z’ + >> Know ‘LAMl Z M = LAMl Y ((FEMPTY |++ ZIP (Z,MAP VAR Y)) ' M)’ + >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [Abbr ‘M’] \\ + Q.PAT_X_ASSUM ‘DISJOINT (set Z) (set Y)’ MP_TAC \\ + rw [DISJOINT_ALT]) + >> Rewr' + >> ‘Y <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0] + >> REWRITE_TAC [GSYM fromPairs_def] + >> qabbrev_tac ‘fm = fromPairs Z (MAP VAR Y)’ + >> ‘FDOM fm = set Z’ by rw [FDOM_fromPairs, Abbr ‘fm’] + >> qabbrev_tac ‘y = EL i Y’ + >> Know ‘fm ' M = VAR y’ + >- (simp [Abbr ‘M’, ssub_appstar] \\ + rw [Abbr ‘fm’, Abbr ‘z’] \\ + Know ‘fromPairs Z (MAP VAR Y) ' (EL i Z) = EL i (MAP VAR Y)’ + >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\ + rw [EL_MAP, Abbr ‘y’]) + >> Rewr' + >> Q.EXISTS_TAC ‘Y’ + >> rw [Abbr ‘y’] +QED + +(* TODO: rework this proof by (the new) selector_alt *) Theorem selector_thm : !i n Ns. i < n /\ LENGTH Ns = n ==> selector i n @* Ns == EL i Ns Proof diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml index a1e62e1f95..79459c6717 100644 --- a/examples/lambda/barendregt/head_reductionScript.sml +++ b/examples/lambda/barendregt/head_reductionScript.sml @@ -2558,6 +2558,33 @@ Proof >> simp [] QED +(* This theorem is more general than selector_thm *) +Theorem hreduce_selector : + !i n Ns. i < n /\ LENGTH Ns = n ==> selector i n @* Ns -h->* EL i Ns +Proof + rpt STRIP_TAC + >> qabbrev_tac ‘X = BIGUNION (IMAGE FV (set Ns))’ + >> ‘FINITE X’ by rw [Abbr ‘X’] + >> MP_TAC (Q.SPECL [‘X’, ‘i’, ‘n’] selector_alt) >> rw [] + >> POP_ORW + >> qabbrev_tac ‘t :term = VAR (EL i vs)’ + >> qabbrev_tac ‘fm = fromPairs vs Ns’ + >> ‘FDOM fm = set vs’ by rw [Abbr ‘fm’, FDOM_fromPairs] + >> Know ‘EL i Ns = fm ' t’ + >- (simp [ssub_thm, Abbr ‘t’, EL_MEM] \\ + simp [Abbr ‘fm’, Once EQ_SYM_EQ] \\ + MATCH_MP_TAC fromPairs_FAPPLY_EL >> art []) + >> Rewr' + >> qunabbrev_tac ‘fm’ + >> MATCH_MP_TAC hreduce_LAMl_appstar + >> rw [EVERY_MEM] + >> Q.PAT_X_ASSUM ‘DISJIONT X (set vs)’ MP_TAC + >> rw [DISJOINT_ALT, Abbr ‘X’] + >> FIRST_X_ASSUM irule + >> Q.EXISTS_TAC ‘FV e’ >> art [] + >> Q.EXISTS_TAC ‘e’ >> art [] +QED + val _ = export_theory() val _ = html_theory "head_reduction"; diff --git a/examples/lambda/barendregt/lameta_completeScript.sml b/examples/lambda/barendregt/lameta_completeScript.sml index 8558a3e6c9..b6df7c678a 100644 --- a/examples/lambda/barendregt/lameta_completeScript.sml +++ b/examples/lambda/barendregt/lameta_completeScript.sml @@ -794,10 +794,7 @@ Proof >> FIRST_X_ASSUM MATCH_MP_TAC >> art [] QED -(* Lemma 10.3.11 [1. p.251] - - NOTE: ‘!M. MEM M Ms ==> p IN BT_paths (apply pi M)’ is needed by agree_upto_thm. - *) +(* Lemma 10.3.11 [1. p.251] *) Theorem agree_upto_lemma : !X Ms p r. FINITE X /\ Ms <> [] /\ p <> [] /\ 0 < r /\ @@ -805,6 +802,7 @@ Theorem agree_upto_lemma : ?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 ==> FV (apply pi M) SUBSET X UNION RANK r) /\ (agree_upto X Ms p r ==> agree_upto X (apply pi Ms) p r) /\ !M N. MEM M Ms /\ MEM N Ms /\ @@ -816,16 +814,19 @@ Proof >> simp [BIGUNION_IMAGE_SUBSET, EVERY_MEM, MEM_MAP, GSYM BT_paths_thm] >> STRIP_TAC >> Q.EXISTS_TAC ‘pi’ >> rw [] - >| [ (* goal 1 (of 3) *) + >| [ (* goal 1 (of 4) *) FIRST_X_ASSUM MATCH_MP_TAC \\ Q.EXISTS_TAC ‘M’ >> art [], - (* goal 2 (of 3) *) + (* 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 3) *) + (* goal 3 (of 4) *) + FIRST_X_ASSUM MATCH_MP_TAC \\ + Q.EXISTS_TAC ‘M’ >> art [], + (* goal 4 (of 4) *) MATCH_MP_TAC subtree_equiv_imp_agree_upto >> rw [] \\ METIS_TAC [] ] QED @@ -836,10 +837,10 @@ QED *) Definition is_faithful_def : is_faithful p X Ms pi r <=> - !M N. MEM M Ms /\ MEM N Ms ==> - (subtree_equiv X M N p r <=> - equivalent (apply pi M) (apply pi N)) /\ - (p IN BT_valid_paths M <=> solvable (apply pi M)) + (!M. MEM M Ms ==> (p IN BT_valid_paths M <=> solvable (apply pi M))) /\ + !M N. MEM M Ms /\ MEM N Ms ==> + (subtree_equiv X M N p r <=> + equivalent (apply pi M) (apply pi N)) End Overload is_faithful' = “is_faithful []” @@ -847,11 +848,11 @@ Overload is_faithful' = “is_faithful []” Theorem is_faithful' : !X Ms pi r. FINITE X /\ 0 < r /\ (!M. MEM M Ms ==> FV M SUBSET X UNION RANK r) ==> - (is_faithful' X Ms pi r <=> - !M N. MEM M Ms /\ MEM N Ms ==> - (equivalent M N <=> - equivalent (apply pi M) (apply pi N)) /\ - (solvable M <=> solvable (apply pi M))) + (is_faithful' X Ms pi r <=> + (!M. MEM M Ms ==> (solvable M <=> solvable (apply pi M))) /\ + !M N. MEM M Ms /\ MEM N Ms ==> + (equivalent M N <=> + equivalent (apply pi M) (apply pi N))) Proof rw [is_faithful_def] >> Suff ‘!M N. MEM M Ms /\ MEM N Ms ==> @@ -881,7 +882,7 @@ Proof (* trivial case: all unsolvable *) >> Cases_on ‘!M. MEM M Ms ==> unsolvable M’ >- (Q.EXISTS_TAC ‘[]’ \\ - reverse (rw []) + 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’ @@ -905,6 +906,7 @@ Proof >> POP_ASSUM K_TAC >> DISCH_TAC (* applying agree_upto_lemma *) >> MP_TAC (Q.SPECL [‘X’, ‘Ms’, ‘h::p’, ‘r’] agree_upto_lemma) >> rw [] + (* p0 is asserted *) >> rename1 ‘Boehm_transform p0’ >> fs [is_ready_alt'] (* decomposing Ms *) @@ -963,13 +965,120 @@ Proof simp [head_equivalent_def]) >> simp [EXT_SKOLEM_THM'] >> STRIP_TAC (* this assert f as the children function of all Ms *) + >> Q.PAT_X_ASSUM ‘!i. i < k ==> ?y Ns. _’ K_TAC >> Know ‘Ns = f 0’ (* eliminate Ns by f *) >- (POP_ASSUM (MP_TAC o Q.SPEC ‘0’) >> rw []) >> DISCH_THEN (FULL_SIMP_TAC std_ss o wrap) - (* Now we use ‘h::p IN BT_paths (apply p0 (M i))’ to show that ‘h < m’ *) + (* Now we use ‘h::p IN BT_paths (apply p0 (M i))’ (and ‘M 0’) to show that + ‘h < m’, as otherwise p1 (the selector) cannot be properly defined. + *) >> Know ‘h < m’ - >- ( - cheat) + >- (Q.PAT_X_ASSUM ‘!i. i < k ==> h::p IN BT_paths (apply p0 (M i))’ + (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 \\ + Know ‘BT' X (apply p0 (M 0)) r = BT' X (N 0) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘N’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + Q.PAT_X_ASSUM ‘N 0 = _’ (REWRITE_TAC o wrap) \\ + simp [BT_def, Once ltree_unfold, BT_generator_def, LMAP_fromList, + ltree_paths_alt, ltree_el_def] \\ + simp [GSYM BT_def, LNTH_fromList, MAP_MAP_o] \\ + Cases_on ‘h < m’ >> rw []) + >> DISCH_TAC + >> Q.PAT_X_ASSUM ‘N 0 = _’ K_TAC + (* p1 is defined as a selector *) + >> qabbrev_tac ‘p1 = [[selector h m/y]]’ + >> ‘Boehm_transform p1’ by rw [Boehm_transform_def, Abbr ‘p1’] + >> Know ‘!i. i < k ==> apply (p1 ++ p0) (M i) -h->* EL h (f i)’ + >- (rw [Boehm_transform_APPEND, Abbr ‘p1’] \\ + MATCH_MP_TAC hreduce_TRANS \\ + Q.EXISTS_TAC ‘[selector h m/y] (VAR y @* f i)’ \\ + CONJ_TAC + >- (MATCH_MP_TAC hreduce_substitutive \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> N i = VAR y @* f i /\ _’ drule \\ + simp [Abbr ‘N’, principle_hnf_thm']) \\ + simp [appstar_SUB] \\ + Know ‘MAP [selector h m/y] (f i) = f i’ + >- (rw [Once LIST_EQ_REWRITE, EL_MAP] \\ + MATCH_MP_TAC lemma14b \\ + Q.PAT_X_ASSUM ‘!i. i < k ==> N i = VAR y @* f i /\ _’ drule \\ + rw [EVERY_MEM] \\ + 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 *) + >> qabbrev_tac ‘Ns = GENLIST (EL h o f) k’ + (* proving one antecedent of IH *) + >> Know ‘agree_upto X Ns p (SUC r)’ + >- (fs [agree_upto_def] \\ + rw [Abbr ‘Ns’, MEM_GENLIST] \\ + NTAC 2 (POP_ASSUM MP_TAC) \\ + rename1 ‘a < k ==> b < k ==> _’ >> NTAC 2 STRIP_TAC \\ + Q.PAT_X_ASSUM ‘!q M N. q <<= h::p /\ MEM M (apply p0 Ms) /\ _ ==> _’ + (MP_TAC o Q.SPECL [‘h::q’, ‘apply p0 ((M :num -> term) a)’, + ‘apply p0 ((M :num -> term) b)’]) \\ + simp [MEM_MAP] \\ + impl_tac + >- (CONJ_TAC >| (* 2 subgoals *) + [ (* goal 1 (of 2) *) + Q.EXISTS_TAC ‘M a’ >> rw [EL_MEM, Abbr ‘M’], + (* goal 2 (of 2) *) + Q.EXISTS_TAC ‘M b’ >> rw [EL_MEM, Abbr ‘M’] ]) \\ + simp [subtree_equiv_def] \\ + Know ‘BT' X (apply p0 (M a)) r = BT' X (N a) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘N’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + Know ‘BT' X (apply p0 (M b)) r = BT' X (N b) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘N’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + simp [] \\ + ‘!i. solvable (VAR y @* f i)’ by rw [] \\ + ‘!i. principle_hnf (VAR y @* f i) = VAR y @* f i’ by rw [] \\ + Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold, + LMAP_fromList]) ‘BT' X (VAR y @* f a) r’ \\ + simp [Abbr ‘M0’, GSYM appstar_APPEND, LNTH_fromList, ltree_el_def, + GSYM BT_def, Abbr ‘y'’, Abbr ‘Ms'’, Abbr ‘n’, Abbr ‘l’, Abbr ‘M1’, + Abbr ‘vs’, EL_MAP] \\ + Q_TAC (UNBETA_TAC [BT_def, BT_generator_def, Once ltree_unfold, + LMAP_fromList]) ‘BT' X (VAR y @* f b) r’ \\ + simp [Abbr ‘M0’, GSYM appstar_APPEND, LNTH_fromList, ltree_el_def, + GSYM BT_def, Abbr ‘y'’, Abbr ‘Ms'’, Abbr ‘n’, Abbr ‘l’, Abbr ‘M1’, + 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’ + >- (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))’ + (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 \\ + MP_TAC (Q.SPECL [‘X’, ‘EL h (f (n :num))’, ‘SUC r’ ] BT_paths_thm) \\ + simp [] >> DISCH_THEN K_TAC \\ + Know ‘BT' X (apply p0 (M n)) r = BT' X (N n) r’ + >- (SIMP_TAC std_ss [Once EQ_SYM_EQ, Abbr ‘N’] \\ + MATCH_MP_TAC BT_of_principle_hnf >> simp []) >> Rewr' \\ + ‘!i. solvable (VAR y @* f i)’ by rw [] \\ + ‘!i. principle_hnf (VAR y @* f i) = VAR y @* f i’ by rw [] \\ + Q_TAC (UNBETA_TAC [BT_def, Once ltree_unfold, BT_generator_def]) + ‘BT' X (N (n :num)) r’ \\ + simp [LMAP_fromList, ltree_paths_alt, ltree_el_def, GSYM BT_def] \\ + simp [Abbr ‘M0’, GSYM appstar_APPEND, LNTH_fromList, EL_MAP, + 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] + >> Q.PAT_X_ASSUM + ‘!Ns r'. _ ==> ?pi. Boehm_transform pi /\ is_faithful p X Ns pi r'’ + (MP_TAC o Q.SPECL [‘Ns’, ‘SUC r’]) + >> simp [] + >> DISCH_THEN (Q.X_CHOOSE_THEN ‘p2’ STRIP_ASSUME_TAC) + >> qabbrev_tac ‘pi = p2 ++ p1 ++ p0’ >> cheat QED