Stage work on new proof of subtree_equiv_lemma

binghe · Dec 14, 2024 · 4d96bea · 4d96bea
1 parent dff4d43
commit 4d96bea
Showing 1 changed file with 60 additions and 39 deletions.
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -6187,51 +6187,72 @@ Proof
  >> ‘!i. LENGTH (l i) = m i + (n_max - n i) + SUC d_max + k’
        by rw [Abbr ‘l’, Abbr ‘m’, Abbr ‘args2’, Abbr ‘d_max’, MAP_DROP]
  >> ‘!i. d_max + k < LENGTH (l i)’ by rw []
- >> cheat
-
- (*
-
+ >> DISCH_TAC
+ (* applying TAKE_DROP_SUC to break l into 3 pieces
 
- (* applying TAKE_DROP_SUC to break l into 3 pieces *)
- >> MP_TAC (Q.GEN ‘i’ (ISPECL [“d_max :num”, “l (i :num) :term list”]
-                              (GSYM TAKE_DROP_SUC))) >> simp []
- >> Rewr'
+    NOTE: New the segmentation of ‘l’ also depends on ‘i’.
+  *)
+ >> qabbrev_tac ‘d_max' = \i. d_max + f i’
+ >> Know ‘!i. i < k ==> d_max' i < d_max + k’
+ >- (rw [Abbr ‘d_max'’] \\
+     Q_TAC (TRANS_TAC LESS_TRANS) ‘d_max + k’ >> simp [])
+ >> DISCH_TAC
+ >> Know ‘!i. i < k ==>
+              apply p3 (P (f i) @* args' i @* args2 i) =
+              P (f i) @* (TAKE (d_max' i) (l i) ++ [EL (d_max' i) (l i)] ++
+                          DROP (SUC (d_max' i)) (l i))’
+ >- (RW_TAC std_ss [] \\
+     Suff ‘TAKE (d_max' i) (l i) ++ [EL (d_max' i) (l i)] ++
+           DROP (SUC (d_max' i)) (l i) = l i’ >- Rewr \\
+     MATCH_MP_TAC TAKE_DROP_SUC \\
+     Q.PAT_X_ASSUM ‘!i. LENGTH (l i) = _ + k’ K_TAC \\
+     Q_TAC (TRANS_TAC LESS_TRANS) ‘d_max + k’ >> simp [])
+ >> Q.PAT_X_ASSUM ‘!i. i < k ==> _ = P (f i) @* l i’ K_TAC
  >> REWRITE_TAC [appstar_APPEND, appstar_SING]
- (* The segmentation of list l(i) - apply (p3 ++ p2 ++ p1) (M i)
-
- |<-- m(i)<= d -->|<-- n_max-n(i) -->|<-------------- SUC d_max -------------->|
- |----- args' ----+----- args2 ------+-------------- MAP VAR xs ---------------|
- |------------------------------------ l --------------------------------------|
- |                                   |<-j->|
- |<-------- d_max = d + n_max ---------->| b
- |------------------- Ns ----------------+-+--------------- tl ----------------|
- |<-------------- d_max+1 ---------------->|
+ (* NOTE: The segmentation of list l(i) - apply (p3 ++ p2 ++ p1) (M i)
+
+  |<-- m(i)<= d -->|<-- n_max-n(i) -->|<-------------- SUC d_max + k--------->|
+  |----- args' ----+----- args2 ------+-------------- MAP VAR xs -------------|
+  |------------------------------------ l ------------------------------------|
+  |                                   |<-j->|
+  |<--- d_max + f = d + n_max + f(i) ---->|b
+  |------------------- Ns(i) -------------+-+<-------------- tl(i) ---------->|
+  |<-------------- d_max + k + 1 ---------->|
   *)
- >> qabbrev_tac ‘Ns = \i. TAKE d_max (l i)’
- >> qabbrev_tac ‘B  = \i. EL d_max (l i)’
- >> simp [] (* this put Ns and B in use *)
- >> qabbrev_tac ‘j  = \i. d_max - LENGTH (args' i ++ args2 i)’
- >> ‘!i. j i < LENGTH xs’ by rw [Abbr ‘j’, Abbr ‘args'’, Abbr ‘args2’, Abbr ‘d_max’]
+ >> qabbrev_tac ‘Ns = \i. TAKE (d_max' i) (l i)’
+ >> qabbrev_tac ‘B  = \i. EL (d_max' i) (l i)’
+ >> qabbrev_tac ‘tl = \i. DROP (SUC (d_max' i)) (l i)’
+ >> simp [] (* this put Ns, B and tl in use *)
+ (* What is j here? The purpose of j is to show that (B i) is a fresh name in
+    xs. This j is the offset (d_max' i) of l, translated to offset of xs. *)
+ >> qabbrev_tac ‘j = \i. d_max' i - LENGTH (args' i ++ args2 i)’
+ (* show that (j i) is valid index of xs *)
+ >> Know ‘!i. i < k ==> j i < LENGTH xs’
+ >- (rw [Abbr ‘j’, Abbr ‘args'’, Abbr ‘args2’, Abbr ‘d_max'’, Abbr ‘d_max’] \\
+    ‘f i < k’ by rw [] \\
+     simp [ADD1])
+ >> DISCH_TAC
  >> Know ‘!i. i < k ==> ?b. EL (j i) xs = b /\ B i = VAR b’
  >- (rw [Abbr ‘B’, Abbr ‘l’] \\
-     Suff ‘EL d_max (args' i ++ args2 i ++ MAP VAR xs) = EL (j i) (MAP VAR xs)’
+     Suff ‘EL (d_max' i) (args' i ++ args2 i ++ MAP VAR xs) = EL (j i) (MAP VAR xs)’
      >- rw [EL_MAP] \\
      SIMP_TAC bool_ss [Abbr ‘j’] \\
      MATCH_MP_TAC EL_APPEND2 \\
-     rw [Abbr ‘args'’, Abbr ‘args2’, Abbr ‘d_max’, MAP_DROP] \\
-     MATCH_MP_TAC LESS_EQ_LESS_EQ_MONO >> rw [] \\
-     Q.PAT_X_ASSUM ‘!i. i < k ==> m i <= d’ MP_TAC \\
-     simp [Abbr ‘m’])
+    ‘f i < k’ by rw [] \\
+     rw [Abbr ‘args'’, Abbr ‘args2’, Abbr ‘d_max'’, Abbr ‘d_max’, MAP_DROP] \\
+     MATCH_MP_TAC LESS_EQ_LESS_EQ_MONO >> rw [])
  >> simp [EXT_SKOLEM_THM']
  >> DISCH_THEN (Q.X_CHOOSE_THEN ‘b’ STRIP_ASSUME_TAC) (* this asserts ‘b’ *)
- >> qabbrev_tac ‘tl = \i. DROP (SUC d_max) (l i)’
  >> simp []
  >> DISCH_TAC (* store ‘!i. i < k ==> apply p3 ...’ *)
  (* applying permutator_hreduce_more, it clearly reduces to a hnf *)
  >> Know ‘!i. i < k ==>
-              P @* Ns i @@ VAR (b i) @* tl i -h->* VAR (b i) @* Ns i @* tl i’
+              P (f i) @* Ns i @@ VAR (b i) @* tl i -h->* VAR (b i) @* Ns i @* tl i’
  >- (RW_TAC std_ss [Abbr ‘P’] \\
-     MATCH_MP_TAC permutator_hreduce_more >> rw [Abbr ‘Ns’])
+     MATCH_MP_TAC permutator_hreduce_more >> rw [Abbr ‘Ns’, Abbr ‘d_max'’] \\
+    ‘f i < k’ by rw [] \\
+    ‘d_max + f i <= LENGTH (l i)’ by rw [] \\
+     simp [LENGTH_TAKE])
  >> DISCH_TAC
  >> Know ‘!i. i < k ==> apply pi (M i) == VAR (b i) @* Ns i @* tl i’
  >- (rpt STRIP_TAC \\
@@ -6270,8 +6291,7 @@ Proof
      now on, both ‘apply pi M == ...’ and ‘principle_hnf (apply pi M) = ...’
      are simplified in parallel.
    *)
-     Q.PAT_X_ASSUM ‘!i. i < k ==> apply pi (M i) == _’
-       (fn th => MP_TAC (MATCH_MP th (ASSUME “i < (k :num)”))) \\
+     Q.PAT_X_ASSUM ‘!i. i < k ==> apply pi (M i) == _’ drule \\
      Q.PAT_X_ASSUM ‘Boehm_transform pi’ K_TAC \\
      Q.PAT_X_ASSUM ‘Boehm_transform p3’ K_TAC \\
   (* NOTE: No need to unabbrev ‘p2’ here since ‘apply p2 t = t ISUB sub k’ *)
@@ -6283,23 +6303,22 @@ Proof
      DISCH_TAC (* store ‘M i @* MAP VAR vs @* MAP VAR xs ISUB sub k == ...’ *) \\
   (* rewriting RHS to principle_hnf of ISUB *)
      Know ‘VAR (b i) @* Ns i @* tl i =
-           principle_hnf (P @* args' i @* args2 i @* MAP VAR xs)’
+           principle_hnf (P (f i) @* args' i @* args2 i @* MAP VAR xs)’
      >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
         ‘hnf (VAR (b i) @* Ns i @* tl i)’
             by rw [GSYM appstar_APPEND, hnf_appstar] \\
-         Suff ‘solvable (P @* args' i @* args2 i @* MAP VAR xs)’
+         Suff ‘solvable (P (f i) @* args' i @* args2 i @* MAP VAR xs)’
          >- (METIS_TAC [principle_hnf_thm']) \\
          Suff ‘solvable (VAR (b i) @* Ns i @* tl i) /\
-               P @* Ns i @@ VAR (b i) @* tl i == VAR (b i) @* Ns i @* tl i’
+               P (f i) @* Ns i @@ VAR (b i) @* tl i == VAR (b i) @* Ns i @* tl i’
          >- (METIS_TAC [lameq_solvable_cong]) \\
          reverse CONJ_TAC >- (MATCH_MP_TAC hreduces_lameq >> rw []) \\
          REWRITE_TAC [solvable_iff_has_hnf] \\
          MATCH_MP_TAC hnf_has_hnf >> art []) >> Rewr' \\
-     Know ‘P @* args' i @* args2 i @* MAP VAR xs = M1 i @* MAP VAR xs ISUB ss’
+     Know ‘P (f i) @* args' i @* args2 i @* MAP VAR xs = M1 i @* MAP VAR xs ISUB ss’
      >- (REWRITE_TAC [appstar_ISUB, Once EQ_SYM_EQ] \\
-         Q.PAT_X_ASSUM ‘!i. i < k ==> apply p2 (M1 i) = P @* args' i @* args2 i’
-           (fn th => MP_TAC (MATCH_MP (GSYM (Q.SPEC ‘i’ th))
-                                      (ASSUME “i < k :num”))) >> Rewr' \\
+         Q.PAT_X_ASSUM ‘!i. i < k ==> apply p2 (M1 i) = _’
+           (drule o GSYM) >> Rewr' \\
          Q.PAT_X_ASSUM ‘!t. apply p2 t = t ISUB ss’ (ONCE_REWRITE_TAC o wrap) \\
          AP_TERM_TAC >> art []) >> Rewr' \\
   (* applying principle_hnf_ISUB_cong *)
@@ -6367,6 +6386,8 @@ Proof
      REWRITE_TAC [solvable_iff_has_hnf] \\
      MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar, GSYM appstar_APPEND])
  >> DISCH_TAC
+ >> cheat
+ (*
  >> CONJ_TAC (* EVERY is_ready' ... *)
  >- (rpt (Q.PAT_X_ASSUM ‘Boehm_transform _’ K_TAC) \\
      simp [EVERY_EL, EL_MAP] \\