Stage work before introducing subterm_LAMl_size

examples/lambda/barendregt/boehmScript.sml

@@ -7443,15 +7443,15 @@ Proof
      - zs2 (part of Ns1x), prefix of L, can be chosen to exclude anything;
      - z2, part of L, can be chosen to exclude anything;
      - Ns1'' (part of Ns1x), FV is equal or less than Ns1';
-     - Ns1' is tpm (REVERSE pm) of Ns1
-     - pm = ZIP (vs,ys), vs is in ROW 0, ys s in ROW r
+     - Ns1' is tpm (REVERSE pm) of Ns1;
+     - pm = ZIP (vs,ys), vs is in ROW 0, ys s in ROW r;
 
      - FV (Ns1) <= FV (VAR y1 @* Ns1) <= FV (N0 @* MAP VAR vs1)
                 <= FV N + vs1 <= X UNION RANK r1 + vs1 (in ROW r1)
 
-     - vs1     = RNEWS r1 n1 X     (NOTE: n1 <> n2)
+     - vs1     = RNEWS r1 n1 X (NOTE: n1 <> n2)
      - vs2     = RNEWS r1 n2 X
-     - vs3=vs4 = RNEWS r1 n3=n4 X
+     - vs3/vs4 = RNEWS r1 n3/n4 X
                                       (SUC d_max)
                       ----- L -------------->|
      zs1' = |<--- vs1 --->|<--- zs1 ------>|h| (ROW 0 & r1)
@@ -8280,20 +8280,37 @@ Proof
  >> simp [LAMl_ISUB, appstar_ISUB]
  >> qabbrev_tac ‘Ns1'' = MAP (\t. t ISUB ss) Ns1'’
  >> qabbrev_tac ‘Ns2'' = MAP (\t. t ISUB ss) Ns2'’
- (* stage work
-
-    N  -h->* N0  = LAMl vs1 (VAR y1 @* Ns1)
-    N' -h->* N0' = LAMl vs2 (VAR y2 @* Ns2)
-    W  -h->* W0  = LAMl vs3 (VAR y3 @* Ns3)
-       -h->*       LAMl vs1 ((VAR y1' ISUB ss) @* Ns1'')
-    W' -h->* W0' = LAMl vs4 (VAR y4 @* Ns4)
-       -h->*       LAMl vs2 ((VAR y2' ISUB ss) @* Ns2'')
-  *)
  >> ‘LENGTH Ns1'' = m1 /\ LENGTH Ns2'' = m2’
        by simp [Abbr ‘Ns1''’, Abbr ‘Ns2''’, Abbr ‘Ns1'’, Abbr ‘Ns2'’]
- >> Cases_on ‘y1' NOTIN DOM ss’
- >> Cases_on ‘y2' NOTIN DOM ss’
- (* Case 1 (of 4): easy *)
+ (* stage work (before final case analysis)
+
+    N  -h->* LAMl vs1 (VAR y1 @* Ns1) (= N0)
+    N' -h->* LAMl vs2 (VAR y2 @* Ns2) (= N0')
+   --------------------------------------------
+    W  -h->* LAMl vs3 (VAR y3 @* Ns3) (= W0)
+    W  -h->* LAMl vs1 ((VAR y1' ISUB ss) @* Ns1'')
+   --------------------------------------------
+    W' -h->* LAMl vs4 (VAR y4 @* Ns4) (= W0')
+    W' -h->* LAMl vs2 ((VAR y2' ISUB ss) @* Ns2'')
+
+    Now, to understand the (alternative) principle_hnf of W and W', we need to
+    rewrite ‘VAR y1' ISUB ss’ to either VAR y1' or P, resp., depending on if
+   ‘y1' IN DOM ss’ or not (and also on ‘y2' IN DOM ss’ or not).
+  *)
+ >> Cases_on ‘y1' NOTIN DOM ss’ >> Cases_on ‘y2' NOTIN DOM ss’
+ (* Case 1 (of 4): easy
+
+    W  -h->* LAMl vs3 (VAR y3  @* Ns3) (= W0)
+    W  -h->* LAMl vs1 (VAR y1' @* Ns1''), thus y3 = y1'
+   --------------------------------------------
+    W' -h->* LAMl vs4 (VAR y4  @* Ns4) (= W0')
+    W' -h->* LAMl vs2 (VAR y2' @* Ns2''), thus y4 = y2'
+
+    Abbrev (y1' = lswapstr (REVERSE pm) y1)
+    Abbrev (y2' = lswapstr (REVERSE pm) y2)
+
+    goal: y3 = y3 (<=> y1' = y2') ==> y1 = y2
+  *)
  >- (simp [ISUB_VAR_FRESH'] \\
      STRIP_TAC \\
     ‘hnf (LAMl vs1 (VAR y1' @* Ns1'')) /\
@@ -8318,7 +8335,33 @@ Proof
      Q.PAT_X_ASSUM ‘_ = W0’  (REWRITE_TAC o wrap o SYM) \\
      Q.PAT_X_ASSUM ‘_ = W0'’ (REWRITE_TAC o wrap o SYM) \\
      simp [])
- (* Case 2 (of 4): hard *)
+ (* Case 2 (of 4): hard
+    N  -h->* LAMl vs1  (VAR y1  @* Ns1) (= N0)
+    N' -h->* LAMl vs2  (VAR y2  @* Ns2) (= N0')
+   --------------------------------------------
+    W  -h->* LAMl vs3  (VAR y3  @* Ns3) (= W0)
+           = LAMl vs1  (VAR y1' @* Ns1''), thus y1' = y3
+   --------------------------------------------
+    W' -h->* LAMl vs4  (VAR y4  @* Ns4) (= W0') --+
+    W' -h->* LAMl vs2  (P       @* Ns2'')        =|=
+       -h->* LAMl zs2' (VAR h   @* Ns2x) ---------+
+
+    Abbrev (y1' = lswapstr (REVERSE pm) y1)
+
+    main goal: y1' <> y4 (y2 seems irrelevant now, same is ‘y1 <> y2’)
+
+    Structure of W:
+
+    LAMl |<--------- vs3 --------->| VAR y3/y1'
+
+    Structure of W':
+    LAMl |<---(vs2)--- vs4 ------------>| VAR y4 (= LAST vs4)
+    LAMl |<----------- zs2' ----------->| VAR h
+    LAMl |<----vs2----->|<----zs2---->|h| VAR h
+        n4 =   n2      +  d_max - m2  +1
+    It seems that y4 is ‘LAST vs4’ while y1' (at most in vs1/vs3, which is
+    shorter than vs4), thus cannot be the same (ALL_DISTINCT vs4).
+  *)
  >- (POP_ASSUM MP_TAC \\
      simp [ISUB_VAR_FRESH'] \\
      DISCH_THEN (Q.X_CHOOSE_THEN ‘j3’ STRIP_ASSUME_TAC) \\
@@ -8388,6 +8431,11 @@ Proof
      >- (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 \\
+  (* important assumptions:
+
+     LAMl vs4 (VAR y4 @* Ns4) = W0' = LAMl zs2' (VAR h @* Ns2x)
+     Abbrev (y1' = lswapstr (REVERSE pm) y1) = y3
+   *)
      cheat)
  (* Case 3 (of 4): symmetric with Case 2 *)
  >- (