Add subterm_headvar_lemma', etc.

binghe · Dec 8, 2024 · 694af1a · 694af1a
1 parent a2c665b
commit 694af1a
Show file tree

Hide file tree

Showing 2 changed files with 104 additions and 21 deletions.
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -718,6 +718,44 @@ Proof
  >> rw [RNEWS_SUBSET_RANK]
 QED
 
+Theorem subterm_headvar_lemma' :
+    !X M r M0 n vs M1.
+           FINITE X /\ FV M SUBSET X UNION RANK r /\
+           solvable M /\
+           M0 = principle_hnf M /\
+            n = LAMl_size M0 /\
+           vs = RNEWS r n X /\
+           M1 = principle_hnf (M0 @* MAP VAR vs)
+       ==> hnf_headvar M1 IN FV M UNION set vs
+Proof
+    RW_TAC std_ss []
+ >> qabbrev_tac ‘M0 = principle_hnf M’
+ >> qabbrev_tac ‘n = LAMl_size M0’
+ >> Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’
+ >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
+ >> ‘DISJOINT (set vs) (FV M0)’ by PROVE_TAC [subterm_disjoint_lemma']
+ >> Q_TAC (HNF_TAC (“M0 :term”, “vs :string list”,
+                    “y :string”, “args :term list”)) ‘M1’
+ >> ‘TAKE n vs = vs’ by rw []
+ >> POP_ASSUM (rfs o wrap)
+ >> ‘hnf M1’ by rw [hnf_appstar]
+ >> Q.PAT_X_ASSUM ‘M0 = _’ (ASSUME_TAC o SYM)
+ >> Q.PAT_X_ASSUM ‘M1 = _’ (ASSUME_TAC o SYM)
+ >> Know ‘FV (principle_hnf (M0 @* MAP VAR vs)) SUBSET FV (M0 @* MAP VAR vs)’
+ >- (MATCH_MP_TAC principle_hnf_FV_SUBSET' \\
+    ‘solvable M1’ by rw [solvable_iff_has_hnf, hnf_has_hnf] \\
+     Suff ‘M0 @* MAP VAR vs == M1’ >- PROVE_TAC [lameq_solvable_cong] \\
+     rw [])
+ >> simp []
+ >> POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM)
+ >> simp [FV_appstar]
+ >> STRIP_TAC
+ >> Q.PAT_X_ASSUM ‘y IN _’ MP_TAC
+ >> Suff ‘FV M0 SUBSET FV M’ >- SET_TAC []
+ >> qunabbrev_tac ‘M0’
+ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art []
+QED
+
 (* Proposition 10.1.6 [1, p.219] *)
 Theorem lameq_BT_cong :
     !X M N r. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N ==>
@@ -3110,6 +3148,23 @@ Proof
  >> Q.EXISTS_TAC ‘q’ >> rw []
 QED
 
+Theorem subterm_length_last :
+    !X M p q r. FINITE X /\ FV M SUBSET X UNION RANK r /\ q <<= p /\
+                subterm X M q r <> NONE /\
+                solvable (subterm' X M q r) ==>
+                LAMl_size (principle_hnf (subterm' X M q r)) <=
+                subterm_length M p
+Proof
+    rpt STRIP_TAC
+ >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘p’, ‘r’] subterm_length_thm)
+ >> simp [] >> DISCH_THEN K_TAC
+ >> irule MAX_SET_PROPERTY
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC IMAGE_FINITE >> rw [FINITE_prefix])
+ >> simp []
+ >> Q.EXISTS_TAC ‘q’ >> rw []
+QED
+
 Theorem solvable_subst_permutator :
     !X M r P v d. FINITE X /\ FV M SUBSET X UNION RANK r /\ v IN X UNION RANK r /\
                   P = permutator d /\ hnf_children_size (principle_hnf M) <= d /\
@@ -8192,24 +8247,27 @@ Proof
      MATCH_MP_TAC FV_tpm_lemma \\
      Q.EXISTS_TAC ‘r1’ >> simp [Abbr ‘pm’, MAP_REVERSE, MAP_ZIP])
  >> STRIP_TAC
- >> Know ‘m1 <= d_max’ (* m1 = hnf_children_size N0 *)
- >- (Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ \\
-     reverse CONJ_TAC >- rw [Abbr ‘d_max’] \\
-     Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_width (M j1) p’ \\
-     reverse CONJ_TAC >- simp [] \\
+ >> Know ‘m1 <= d’ (* m1 = hnf_children_size N0 *)
+ >- (Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_width (M j1) p’ >> simp [] \\
      qunabbrevl_tac [‘m1’, ‘N0’] \\
     ‘N = subterm' X (M j1) p r’ by rw [] >> POP_ORW \\
      MATCH_MP_TAC subterm_width_last >> simp [])
  >> DISCH_TAC
- >> Know ‘m2 <= d_max’ (* m2 = hnf_children_size N0' *)
+ >> Know ‘m1 <= d_max’ (* m1 = hnf_children_size N0 *)
  >- (Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ \\
-     reverse CONJ_TAC >- rw [Abbr ‘d_max’] \\
-     Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_width (M j2) p’ \\
+     rw [Abbr ‘d_max’])
+ >> DISCH_TAC
+ >> Know ‘m2 <= d’ (* m2 = hnf_children_size N0' *)
+ >- (Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_width (M j2) p’ \\
      reverse CONJ_TAC >- simp [] \\
      qunabbrevl_tac [‘m2’, ‘N0'’] \\
     ‘N' = subterm' X (M j2) p r’ by rw [] >> POP_ORW \\
      MATCH_MP_TAC subterm_width_last >> simp [])
  >> DISCH_TAC
+ >> Know ‘m2 <= d_max’ (* m2 = hnf_children_size N0' *)
+ >- (Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘d’ \\
+     rw [Abbr ‘d_max’])
+ >> DISCH_TAC
  >> Know ‘solvable (subterm' X (H j1) p r) /\
           solvable (subterm' X (H j2) p r)’
  >- (ASM_SIMP_TAC std_ss [] \\
@@ -8241,7 +8299,7 @@ Proof
  >> rename1 ‘subterm X (H j2) p r = SOME (W',r1)’
  >> qabbrev_tac ‘W0' = principle_hnf W'’
  >> qabbrev_tac ‘m4 = hnf_children_size W0'’
- >> rename1 ‘ltree_el (BT' X (H j2) r) q = SOME (SOME (vs4,y4),SOME m4)’
+ >> rename1 ‘ltree_el (BT' X (H j2) r) p = SOME (SOME (vs4,y4),SOME m4)’
  >> Q.PAT_X_ASSUM ‘_ = SOME (vs4,y4)’ K_TAC
  >> Q.PAT_X_ASSUM ‘_ = SOME m4’       K_TAC
  >> qabbrev_tac ‘n4 = LAMl_size W0'’
@@ -8283,11 +8341,11 @@ Proof
  >> simp [head_equivalent_def]
  (* stage work *)
  >> Know ‘W = tpm (REVERSE pm) N ISUB ss’
- >- (Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) q r <> NONE /\ _’
+ >- (Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) p r <> NONE /\ _’
        (MP_TAC o Q.SPEC ‘j1’) >> simp [])
  >> DISCH_TAC
  >> Know ‘W' = tpm (REVERSE pm) N' ISUB ss’
- >- (Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) q r <> NONE /\ _’
+ >- (Q.PAT_X_ASSUM ‘!i. i < k ==> subterm X (H i) p r <> NONE /\ _’
        (MP_TAC o Q.SPEC ‘j2’) >> simp [])
  >> DISCH_TAC
  (* applying hreduce_ISUB and tpm_hreduces *)
@@ -8526,8 +8584,7 @@ Proof
          Q.PAT_X_ASSUM ‘_ = W0'’ (REWRITE_TAC o wrap o SYM) \\
          simp []) >> DISCH_TAC \\
   (* abandon ‘y1 <> y2 \/ m2 + n1 <> m1 + n2’ *)
-     DISCH_THEN K_TAC \\
-     DISJ1_TAC (* focus on ‘y1' <> y4’ as the other part is unprovable *) \\
+     DISCH_THEN K_TAC >> DISJ1_TAC \\
      Know ‘SUC d_max + n2 - m2 = n4’
      >- (POP_ASSUM (REWRITE_TAC o wrap o SYM) \\
          simp [Abbr ‘zs2'’]) >> DISCH_TAC \\
@@ -8581,7 +8638,7 @@ Proof
          Q.EXISTS_TAC ‘set vs4’ >> simp [Abbr ‘ys2’, LIST_TO_SET_DROP] \\
          qunabbrevl_tac [‘ys’, ‘vs4’] \\
          MATCH_MP_TAC DISJOINT_RNEWS \\
-        ‘0 < LENGTH q’ by rw [LENGTH_NON_NIL] \\
+        ‘0 < LENGTH p’ by rw [LENGTH_NON_NIL] \\
          simp [Abbr ‘r1’]) >> DISCH_TAC \\
      Know ‘LAMl xs2 t = LAMl ys2 (pm2 ' t)’
      >- (simp [Abbr ‘pm2’, fromPairs_def] \\
@@ -8664,11 +8721,33 @@ Proof
   (* W -h->* LAMl vs3  (VAR y3  @* Ns3) = LAMl vs1  (VAR y1' @* Ns1'')
 
      Now we show that n1/n3 is strictly smaller than n4. This is only possible
-     after using ‘subterm_length’ when constructing the permutator ‘P’.
+     after using ‘subterm_length’ when constructing the permutator ‘P’:
+
+      LENGTH zs2 = d_max - m2             (assumption)
+      d_max = d + n_max >= m2 + n1        (worst case: d = m2)
+   => LENGTH zs2 >= m2 + n1 - m2 = n1     (worst case: LENGTH zs2 = n1)
+   => n4 = n2 + LENGTH zs2 + 1 > n1       (worst case: n2 = 0 and n4 = n1 + 1)
 
      Then, y3 is at most another variable in ROW r1. While y4 is LAST v4, thus
      cannot be the same with y3 since ‘ALL_DISTINCT vs4’.
    *)
+     Know ‘n1 <= n_max’ (* n1 = LAMl_size N0 *)
+     >- (qunabbrev_tac ‘n_max’ \\
+         Q_TAC (TRANS_TAC LESS_EQ_TRANS) ‘subterm_length (M j1) p’ \\
+         reverse CONJ_TAC
+         >- (MATCH_MP_TAC MAX_LIST_PROPERTY \\
+             simp [MEM_MAP] \\
+             Q.EXISTS_TAC ‘M j1’ >> art [] \\
+             simp [Abbr ‘M’, EL_MEM]) \\
+         qunabbrevl_tac [‘n1’, ‘N0’] \\
+        ‘N = subterm' X (M j1) p r’ by rw [] >> POP_ORW \\
+         MATCH_MP_TAC subterm_length_last >> simp []) >> DISCH_TAC \\
+     Know ‘n1 < n4’
+     >- (Q_TAC (TRANS_TAC LESS_EQ_LESS_TRANS) ‘n_max’ >> art [] \\
+         Q.PAT_X_ASSUM ‘SUC d_max + n2 - m2 = n4’ (REWRITE_TAC  o wrap o SYM) \\
+         Q_TAC (TRANS_TAC LESS_EQ_LESS_TRANS) ‘d_max + n2 - m2’ \\
+         simp [Abbr ‘d_max’]) >> DISCH_TAC \\
+  (* applying subterm_headvar_lemma' *)
      cheat)
  (* Case 3 (of 4): symmetric with Case 2 *)
  >- (

diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
@@ -202,19 +202,23 @@ Proof
  >> simp [LIST_TO_SET_SNOC] >> SET_TAC []
 QED
 
-(* A special case of FV_appstar *)
-Theorem FV_appstar_MAP_VAR[simp] :
-    FV (M @* MAP VAR vs) = FV M UNION set vs
+Theorem BIGUNION_IMAGE_FV_MAP_VAR[simp] :
+    BIGUNION (IMAGE FV (set (MAP VAR vs))) = set vs
 Proof
-    rw [FV_appstar]
- >> Suff ‘BIGUNION (IMAGE FV (set (MAP VAR vs))) = set vs’ >- rw []
- >> rw [Once EXTENSION, IN_BIGUNION_IMAGE]
+    rw [Once EXTENSION, IN_BIGUNION_IMAGE]
  >> reverse EQ_TAC >> rpt STRIP_TAC
  >- (Q.EXISTS_TAC ‘VAR x’ >> rw [MEM_MAP])
  >> rename1 ‘x IN FV t’
  >> gs [MEM_MAP]
 QED
 
+(* A special case of FV_appstar *)
+Theorem FV_appstar_MAP_VAR[simp] :
+    FV (M @* MAP VAR vs) = FV M UNION set vs
+Proof
+    rw [FV_appstar]
+QED
+
 (*---------------------------------------------------------------------------*
  *  LAMl (was in standardisationTheory)
  *---------------------------------------------------------------------------*)