Stage work on agree_upto_thm

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

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

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";
 

examples/lambda/barendregt/lameta_completeScript.sml

@@ -794,17 +794,15 @@ 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 /\
       (!M. MEM M Ms ==> FV M SUBSET X UNION RANK r /\ p IN BT_paths M) ==>
        ?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,22 +837,22 @@ 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 []”
 
 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