Stage work on (full) agree_upto_lemma

binghe · Dec 5, 2024 · 3835471 · 3835471
1 parent 938e4eb
commit 3835471
Show file tree

Hide file tree

Showing 2 changed files with 66 additions and 8 deletions.
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -1,8 +1,8 @@
 (* ========================================================================== *)
 (* FILE    : boehmScript.sml                                                  *)
-(* TITLE   : (Effective) Boehm Trees (Chapter 10 of Barendregt 1984 [1])      *)
+(* TITLE   : (Effective) Boehm Trees [1, Chapter 10]                          *)
 (*                                                                            *)
-(* AUTHORS : 2023-2024 The Australian National University (Chun Tian)         *)
+(* AUTHORS : 2023-2024 The Australian National University (Chun TIAN)         *)
 (* ========================================================================== *)
 
 open HolKernel Parse boolLib bossLib;
@@ -5699,8 +5699,8 @@ End
    NOTE: ‘0 < r’ is to ensure a non-empty ‘RANK r’ to allocate fresh variables
    in it (for the construction of Boehm transform ‘pi’).
 
-   NOTE: This is the last theorem of the current theory. All further results
-   go to completenessTheory.
+   NOTE: This is the last theorem of the current theory. Further results are
+   moved to completenessTheory, etc.
  *)
 Theorem agree_upto_lemma :
     !X Ms p r.
@@ -8291,9 +8291,6 @@ Proof
   *)
  >> ‘LENGTH Ns1'' = m1 /\ LENGTH Ns2'' = m2’
        by simp [Abbr ‘Ns1''’, Abbr ‘Ns2''’, Abbr ‘Ns1'’, Abbr ‘Ns2'’]
- >> qabbrev_tac ‘X' = BIGUNION (IMAGE FV (set Ns1'')) UNION
-                      BIGUNION (IMAGE FV (set Ns2''))’
- >> ‘FINITE X'’ by rw [Abbr ‘X'’]
  >> Cases_on ‘y1' NOTIN DOM ss’
  >> Cases_on ‘y2' NOTIN DOM ss’
  (* Case 1 (of 4): easy *)
@@ -8330,6 +8327,67 @@ Proof
     ‘LAMl vs1 (VAR y1' @* Ns1'') = W0’ by METIS_TAC [principle_hnf_thm'] \\
     ‘LAMl_size W0 = n1’ by rw [LAMl_size_hnf] \\
     ‘n3 = n1’ by PROVE_TAC [] \\
+     Know ‘y3 = y1' /\ Ns1'' = Ns3’
+     >- (Q.PAT_X_ASSUM ‘LAMl vs3 _ = W0’ MP_TAC \\
+         Q.PAT_X_ASSUM ‘_ = W0’ (REWRITE_TAC o wrap o SYM) \\
+         simp [] \\
+         Q.PAT_X_ASSUM ‘_ = W1’ (REWRITE_TAC o wrap o SYM) \\
+         fs []) >> STRIP_TAC \\
+     simp [] \\
+  (* NOTE: The proof completes if we can just show ‘y3 <> y4’. *)
+     qabbrev_tac ‘X' = BIGUNION (IMAGE FV (set Ns2''))’ \\
+    ‘FINITE X'’ by rw [Abbr ‘X'’] \\
+     qabbrev_tac ‘d' = MAX n4 (SUC d_max)’ \\
+     Q_TAC (NEWS_TAC (“L :string list”, “d' :num”)) ‘X'’ \\
+    ‘SUC d_max <= LENGTH L /\ n4 <= LENGTH L’ by simp [Abbr ‘d'’, MAX_LE] \\
+     Know ‘DISJOINT (set L) (set vs2) /\
+           DISJOINT (set L) (set vs4)’
+     >- (rw [Abbr ‘L’, Abbr ‘vs2’, Abbr ‘vs4’] (* 2 subgoals, same tactics *) \\
+         MATCH_MP_TAC DISJOINT_RNEWS >> simp [Abbr ‘r1’]) >> STRIP_TAC \\
+     Q.PAT_X_ASSUM ‘FINITE X'’ K_TAC \\
+     Q.PAT_X_ASSUM ‘DISJOINT (set L) X'’ MP_TAC \\
+     qunabbrev_tac ‘X'’ \\
+     DISCH_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [DISJOINT_UNION']) \\
+     STRIP_TAC (* W -h->* ... *) \\
+  (* applying hreduce_permutator_shared again *)
+     MP_TAC (Q.SPECL [‘Ns2''’, ‘d_max’, ‘L’] hreduce_permutator_shared) \\
+     simp [] \\
+     DISCH_THEN (Q.X_CHOOSE_THEN ‘zs2’ (Q.X_CHOOSE_THEN ‘z2’ STRIP_ASSUME_TAC)) \\
+     Q.PAT_X_ASSUM ‘P @* Ns2'' -h->* _’ MP_TAC \\
+     qabbrev_tac ‘h = LAST L’ (* the new shared head variable *) \\
+     qabbrev_tac ‘L' = FRONT L’ \\
+    ‘L <> []’ by rw [GSYM LENGTH_NON_NIL] \\
+     Q.PAT_X_ASSUM ‘IS_SUFFIX L _’ MP_TAC \\
+    ‘L = SNOC h L'’ by ASM_SIMP_TAC std_ss [Abbr ‘L'’, Abbr ‘h’, SNOC_LAST_FRONT] \\
+     POP_ORW \\
+     simp [IS_SUFFIX] >> STRIP_TAC \\
+     Q.PAT_X_ASSUM ‘h = z2’ (simp o wrap o SYM) \\
+     STRIP_TAC (* P @* Ns2'' -h->* ... *) \\
+     qabbrev_tac ‘xs2 = SNOC h zs2’ \\ (* suffix of L *)
+     Know ‘IS_SUFFIX L xs2’
+     >- (‘L = SNOC h L'’
+           by ASM_SIMP_TAC std_ss [Abbr ‘L'’, Abbr ‘h’, SNOC_LAST_FRONT] \\
+         POP_ORW \\
+         simp [IS_SUFFIX, Abbr ‘xs2’]) >> DISCH_TAC \\
+     Know ‘LAMl vs2 (P @* Ns2'') -h->*
+           LAMl vs2 (LAMl zs2 (LAM h (VAR h @* Ns2'' @* MAP VAR zs2)))’
+     >- simp [hreduce_LAMl] \\
+     Q.PAT_X_ASSUM ‘P @* Ns2'' -h->* _’ K_TAC \\
+     REWRITE_TAC [GSYM LAMl_APPEND, GSYM appstar_APPEND] \\
+     qabbrev_tac ‘Ns2x = Ns2'' ++ MAP VAR zs2’ \\
+     REWRITE_TAC [GSYM LAMl_SNOC] \\
+     qabbrev_tac ‘zs2' = SNOC h (vs2 ++ zs2)’ \\
+     STRIP_TAC \\
+     Know ‘W' -h->* LAMl zs2' (VAR h @* Ns2x)’
+     >- PROVE_TAC [hreduce_TRANS] \\
+     POP_ASSUM K_TAC >> STRIP_TAC \\
+     Know ‘LAMl zs2' (VAR h @* Ns2x) = W0'’
+     >- (‘hnf (LAMl zs2' (VAR h @* Ns2x))’ by rw [hnf_appstar] \\
+         METIS_TAC [principle_hnf_thm']) >> DISCH_TAC \\
+     Know ‘LENGTH zs2' = n4’
+     >- (Q.PAT_X_ASSUM ‘_ = n4’ (REWRITE_TAC o wrap o SYM) \\
+         Q.PAT_X_ASSUM ‘_ = W0'’ (REWRITE_TAC o wrap o SYM) \\
+         simp []) >> DISCH_TAC \\
      cheat)
  (* Case 3 (of 4): symmetric with Case 2 *)
  >- (

diff --git a/examples/lambda/barendregt/completenessScript.sml b/examples/lambda/barendregt/completenessScript.sml
@@ -1,6 +1,6 @@
 (* ========================================================================== *)
 (* FILE    : completenessScript.sml                                           *)
-(* TITLE   : Completeness of (Untyped) Lambda-Calculus                        *)
+(* TITLE   : Completeness of (Untyped) Lambda-Calculus [1, Chapter 10.4]      *)
 (*                                                                            *)
 (* AUTHORS : 2024-2025 The Australian National University (Chun TIAN)         *)
 (* ========================================================================== *)