Stage work on agree_upto_lemma

binghe · Oct 28, 2024 · 64633e1 · 64633e1
1 parent 2bdd1ed
commit 64633e1
Showing 1 changed file with 58 additions and 0 deletions.
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -6203,6 +6203,9 @@ Proof
          >- (MATCH_MP_TAC BT_ltree_el_of_unsolvables >> rw []) \\
          DISCH_THEN (REWRITE_TAC o wrap o SYM) \\
          DISCH_TAC \\
+         Know ‘!i. i < k ==> d_max <= LENGTH (hnf_children (H i))’
+         >- (rw [Abbr ‘H’, GSYM appstar_APPEND] \\
+             simp [Abbr ‘Ns’]) >> DISCH_TAC \\
       (* p <> [] from now on, now applying subterm_isub_cong' *)
          Know ‘!i. i < k ==>
                    subterm X (H i) p r <> NONE /\
@@ -6218,9 +6221,64 @@ Proof
              >- (rw [Abbr ‘H’, LAMl_size_appstar, GSYM appstar_APPEND]) \\
              DISCH_TAC \\
              simp [] \\
+          (* NOTE: popping this assume will eventually bring us ‘h < m i’ *)
              Q.PAT_X_ASSUM ‘!i. i < k ==> h::t IN ltree_paths (BT' X (M i) r)’
                 (MP_TAC o Q.SPEC ‘i’) \\
              simp [BT_def, BT_generator_def, Once ltree_unfold] \\
+             Q_TAC (RNEWS_TAC (“ys :string list”, “r :num”, “(n :num -> num) i”)) ‘X’ \\
+             qabbrev_tac ‘vs' = TAKE (n i) vs’ \\
+            ‘ALL_DISTINCT vs' /\ LENGTH vs' = n i’ by rw [ALL_DISTINCT_TAKE, Abbr ‘vs'’] \\
+             simp [ltree_paths_def, ltree_lookup_def] \\
+             simp [LMAP_fromList, GSYM BT_def, LNTH_fromList, EL_MAP] \\
+             qabbrev_tac ‘t0 = VAR (y i) @* args i’ \\
+             Know ‘DISJOINT (set vs') (set ys)’
+             >- (MATCH_MP_TAC DISJOINT_SUBSET' \\
+                 Q.EXISTS_TAC ‘set vs’ \\
+                 reverse CONJ_TAC >- simp [Abbr ‘vs'’, LIST_TO_SET_TAKE] \\
+                 qunabbrev_tac ‘ys’ \\
+                 MATCH_MP_TAC DISJOINT_SUBSET' \\
+                 Q.EXISTS_TAC ‘RANK r’ >> rw [DISJOINT_RANK_RNEWS'] \\
+                 MATCH_MP_TAC SUBSET_TRANS \\
+                 Q.EXISTS_TAC ‘ROW 0’ \\
+                 CONJ_TAC >- rw [Abbr ‘vs’, RNEWS_SUBSET_ROW] \\
+                 MATCH_MP_TAC ROW_SUBSET_RANK >> art []) >> DISCH_TAC \\
+          (* applying for principle_hnf_tpm_reduce *)
+             Know ‘principle_hnf (LAMl vs' t0 @* MAP VAR ys) = tpm (ZIP (vs',ys)) t0’
+             >- (‘hnf t0’ by rw [Abbr ‘t0’, hnf_appstar] \\
+                 MATCH_MP_TAC principle_hnf_tpm_reduce' >> art [] \\
+                 MATCH_MP_TAC subterm_disjoint_lemma \\
+                 qexistsl_tac [‘X’, ‘r’, ‘n i’] >> simp [] \\
+                 MATCH_MP_TAC SUBSET_TRANS \\
+                 Q.EXISTS_TAC ‘Z’ >> art [] \\
+                 rw [Abbr ‘t0’, FV_appstar]) >> Rewr' \\
+                 simp [Abbr ‘t0’, tpm_appstar, hnf_children_appstar] \\
+                 Cases_on ‘h < m i’ >> simp [] \\
+             Know ‘h < LENGTH (hnf_children (H i))’
+             >- (Q_TAC (TRANS_TAC LESS_LESS_EQ_TRANS) ‘d_max’ >> simp [] \\
+                 Q_TAC (TRANS_TAC LESS_LESS_EQ_TRANS) ‘m i’ >> art [] \\
+                 Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ >> simp [] \\
+                 simp [Abbr ‘d_max’]) >> Rewr \\
+             Know ‘EL h (hnf_children (H i)) = EL h (Ns i)’
+             >- (simp [Abbr ‘H’, GSYM appstar_APPEND] \\
+                 MATCH_MP_TAC EL_APPEND1 \\
+                 simp [Abbr ‘Ns’] \\
+                 Q_TAC (TRANS_TAC LESS_LESS_EQ_TRANS) ‘m i’ >> art [] \\
+                 Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ >> simp [] \\
+                 simp [Abbr ‘d_max’]) >> Rewr' \\
+             Know ‘EL h (Ns i) = EL h (args' i)’
+             >- (simp [Abbr ‘Ns’] \\
+                 Know ‘EL h (TAKE d_max (l i)) = EL h (l i)’
+                 >- (MATCH_MP_TAC EL_TAKE \\
+                     Q_TAC (TRANS_TAC LESS_LESS_EQ_TRANS) ‘m i’ >> art [] \\
+                     Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ >> simp [] \\
+                     simp [Abbr ‘d_max’]) >> Rewr' \\
+                 simp [Abbr ‘l’] \\
+                 REWRITE_TAC [GSYM APPEND_ASSOC] \\
+                 MATCH_MP_TAC EL_APPEND1 \\
+                 simp [Abbr ‘args'’]) >> Rewr' \\
+             qabbrev_tac ‘f = \t. t ISUB ss’ \\
+             simp [Abbr ‘args'’, EL_MAP] \\
+             qabbrev_tac ‘N = EL h (args i)’ \\
              cheat) >> DISCH_TAC \\
          Know ‘unsolvable (subterm' X (H j1) p r) /\
                unsolvable (subterm' X (H j2) p r)’