Some lemmas about eta-reduction and beta-eta equivalence

examples/lambda/barendregt/boehmScript.sml

@@ -1460,8 +1460,7 @@ Proof
  >> POP_ASSUM (rfs o wrap)
  >> Cases_on ‘h < m’ >> simp []
  >> ‘Ms = args’ by rw [Abbr ‘Ms’]
- >> POP_ASSUM (fs o wrap)
- >> T_TAC
+ >> POP_ASSUM (fs o wrap) >> T_TAC
  >> DISCH_TAC
  (* applying IH *)
  >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
@@ -1470,46 +1469,31 @@ Proof
  >> qexistsl_tac [‘M’, ‘M0’, ‘n’, ‘m’, ‘vs’, ‘M1’] >> simp []
 QED
 
-Theorem lameq_subterm_cong_none :
-    !p X M N r. FINITE X /\
-                FV M SUBSET X UNION RANK r /\
-                FV N SUBSET X UNION RANK r /\ M == N ==>
-               (subterm X M p r = NONE <=> subterm X N p r = NONE)
-Proof
-    rpt STRIP_TAC
- >> Suff ‘subterm X M p r <> NONE <=> subterm X N p r <> NONE’ >- rw []
- >> Know ‘subterm X M p r <> NONE <=> p IN ltree_paths (BT' X M r)’
- >- (MATCH_MP_TAC (GSYM BT_ltree_paths_thm) >> art [])
- >> Rewr'
- >> Know ‘subterm X N p r <> NONE <=> p IN ltree_paths (BT' X N r)’
- >- (MATCH_MP_TAC (GSYM BT_ltree_paths_thm) >> art [])
- >> Rewr'
- >> PROVE_TAC [lameq_BT_cong]
-QED
-
+(* NOTE: Improved statements combining with (old) lameq_subterm_cong_none *)
 Theorem lameq_subterm_cong :
-    !p X M N r. FINITE X /\
+    !X M N p r. FINITE X /\
                 FV M SUBSET X UNION RANK r /\
-                FV N SUBSET X UNION RANK r /\
-                M == N /\
-                subterm X M p r <> NONE /\
-                subterm X N p r <> NONE
-            ==> subterm' X M p r == subterm' X N p r
-Proof
-    Q.X_GEN_TAC ‘p’
- >> Cases_on ‘p = []’ >- rw []
- >> POP_ASSUM MP_TAC
- >> Q.ID_SPEC_TAC ‘p’
- >> Induct_on ‘p’ >- rw []
- >> RW_TAC std_ss []
+                FV N SUBSET X UNION RANK r /\ M == N
+           ==> (subterm X M p r = NONE <=> subterm X N p r = NONE) /\
+               (subterm X M p r <> NONE ==>
+                subterm' X M p r == subterm' X N p r)
+Proof
+  Suff
+   ‘!X. FINITE X ==>
+        !p M N r. FV M SUBSET X UNION RANK r /\
+                  FV N SUBSET X UNION RANK r /\ M == N
+             ==> (subterm X M p r = NONE <=> subterm X N p r = NONE) /\
+                 (subterm X M p r <> NONE ==>
+                  subterm' X M p r == subterm' X N p r)’ >- METIS_TAC []
+ >> NTAC 2 STRIP_TAC
+ >> Induct_on ‘p’ >- simp []
+ >> rpt GEN_TAC >> STRIP_TAC
  >> reverse (Cases_on ‘solvable M’)
- >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\
-     Cases_on ‘p’ >> fs [subterm_def])
- >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
- >> Q.PAT_X_ASSUM ‘subterm X N (h::p) r <> NONE’ MP_TAC
- >> Q.PAT_X_ASSUM ‘subterm X M (h::p) r <> NONE’ MP_TAC
- >> RW_TAC std_ss [subterm_of_solvables]
- >> gs []
+ >- (‘unsolvable N’ by PROVE_TAC [lameq_solvable_cong] \\
+     simp [subterm_def])
+ >> ‘solvable N’ by PROVE_TAC [lameq_solvable_cong]
+ >> Q_TAC (UNBETA_TAC [subterm_def]) ‘subterm X M (h::p) r’
+ >> Q_TAC (UNBETA_TAC [subterm_def]) ‘subterm X N (h::p) r’
  >> Know ‘n = n' /\ vs = vs'’
  >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
      qunabbrevl_tac [‘n’, ‘n'’, ‘M0’, ‘M0'’] \\
@@ -1520,9 +1504,10 @@ Proof
  (* applying lameq_principal_hnf_thm' *)
  >> MP_TAC (Q.SPECL [‘r’, ‘X’, ‘M’, ‘N’, ‘M0’, ‘M0'’, ‘n’, ‘vs’, ‘M1’, ‘M1'’]
                      lameq_principal_hnf_thm') >> simp []
- >> RW_TAC std_ss [Abbr ‘m’, Abbr ‘m'’]
+ >> simp [Abbr ‘m’, Abbr ‘m'’]
+ >> STRIP_TAC
+ >> Q.PAT_X_ASSUM ‘n = LAMl_size M0'’ (ASSUME_TAC o SYM)
  (* preparing for hnf_children_FV_SUBSET *)
- >> qabbrev_tac ‘n = LAMl_size M0'’
  >> qunabbrev_tac ‘vs’
  >> Q_TAC (RNEWS_TAC (“vs :string list”, “r :num”, “n :num”)) ‘X’
  >> ‘DISJOINT (set vs) (FV M0) /\ DISJOINT (set vs) (FV M0')’
@@ -1532,6 +1517,8 @@ Proof
                     “y :string”, “args :term list”)) ‘M1’
  >> Q_TAC (HNF_TAC (“M0':term”, “vs :string list”,
                     “y' :string”, “args':term list”)) ‘M1'’
+ >> Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV M0)’  K_TAC
+ >> Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV M0')’ K_TAC
  >> ‘TAKE n vs = vs’ by rw []
  >> POP_ASSUM (rfs o wrap)
  (* refine P1 and Q1 again for clear assumptions using them *)
@@ -1541,9 +1528,8 @@ Proof
  >> ‘args = Ms’ by rw [Abbr ‘Ms’]
  >> POP_ASSUM (fs o wrap o SYM)
  >> Q.PAT_X_ASSUM ‘args' = Ms'’ (fs o wrap o SYM)
- >> qabbrev_tac ‘m = LENGTH args'’
- >> T_TAC
- >> Cases_on ‘p = []’ >> fs []
+ >> qabbrev_tac ‘m = LENGTH args'’ >> T_TAC
+ >> Cases_on ‘h < m’ >> simp []
  (* final stage *)
  >> FIRST_X_ASSUM MATCH_MP_TAC >> simp []
  >> CONJ_TAC (* 2 subgoals *)
@@ -6074,6 +6060,18 @@ Proof
  >> MATCH_MP_TAC BT_ltree_el_cases >> art []
 QED
 
+Theorem ltree_finite_BT_expand' :
+    !X M p r. FINITE X /\ FV M SUBSET X UNION RANK r /\ has_bnf M /\
+              p IN ltree_paths (BT' X M r) ==>
+              ltree_finite (BT_expand X (BT' X M r) p r)
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC ltree_finite_BT_expand_lemma
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC ltree_finite_BT_has_bnf >> art [])
+ >> MATCH_MP_TAC BT_ltree_el_cases' >> art []
+QED
+
 (* NOTE: This lemma is not suitable for induction, because (in general),
    if “compat_closure eta N M” and M is bnf, N may have beta-redexes due
    to eta-expansion. Thus, in general we can only say “has_bnf N” instead
@@ -6094,7 +6092,7 @@ Theorem BT_expand_lemma1 :
        compat_closure eta N M /\ BT' X N r = B
 Proof
     rpt GEN_TAC >> STRIP_TAC
- >> simp []
+ >> ASM_REWRITE_TAC []
  >> Suff ‘!R M r. (?p B. FV M SUBSET X UNION RANK r /\ bnf M /\
                          p IN ltree_paths (BT' X M r) /\
                          B = BT_expand X (BT' X M r) p r /\ R = to_rose B) ==>
@@ -6115,12 +6113,12 @@ Proof
  >> KILL_TAC >> DISCH_TAC
  (* applying induction on rose tree *)
  >> HO_MATCH_MP_TAC rose_tree_induction
- >> rpt GEN_TAC >> STRIP_TAC
- >> rpt GEN_TAC >> STRIP_TAC
+ >> NTAC 2 (rpt GEN_TAC >> STRIP_TAC)
  >> Q.PAT_X_ASSUM ‘Rose a ts = _’ (MP_TAC o SYM)
  >> POP_ORW
  >> DISCH_THEN (MP_TAC o AP_TERM “from_rose :BT_node rose_tree -> boehm_tree”)
  >> simp [to_rose_def, ltree_finite_BT_expand]
+ (* stage work *)
  >> simp [from_rose_def]
  >> DISCH_TAC
  >> Q_TAC (UNBETA_TAC [rose_to_term_def, Once rose_reduce_def])

examples/lambda/barendregt/chap2Script.sml

@@ -326,6 +326,16 @@ val _ = set_fixity "===" (Infix(NONASSOC, 450))
 val _ = overload_on("===", “lameta”);
 val _ = TeX_notation { hol = "===", TeX = ("\\HOLTokenLameta", 1) };
 
+Overload "=/==" = “\M (N :term). ~(M === N)”
+val _ = set_fixity "=/==" (Infix(NONASSOC, 450))
+val _ = TeX_notation { hol = "=/==", TeX = ("\\HOLTokenNotLameta", 1) };
+
+Theorem lameta_LAMl_cong :
+    !vs M N. M === N ==> LAMl vs M === LAMl vs N
+Proof
+    Induct_on ‘vs’ >> rw [lameta_ABS]
+QED
+
 Theorem lameta_subst :
     !M N P x. lameta M N ==> lameta ([P/x] M) ([P/x] N)
 Proof
@@ -1097,6 +1107,12 @@ val (enf_thm, _) = define_recursive_term_function
                                 v IN FV (rator t)))`
 val _ = export_rewrites ["enf_thm"]
 
+Theorem I_eta_normal[simp] :
+    enf I
+Proof
+    simp [enf_thm, I_def]
+QED
+
 Theorem subst_eq_var:
     [v/u] t = VAR s <=> t = VAR u ∧ v = VAR s ∨ t = VAR s ∧ u ≠ s
 Proof
@@ -1123,6 +1139,13 @@ End
 Definition has_benf_def: has_benf t = ?t'. lameta t t' /\ benf t'
 End
 
+Theorem bnf_has_bnf :
+    !M. bnf M ==> has_bnf M
+Proof
+    rw [has_bnf_def]
+ >> Q.EXISTS_TAC ‘M’ >> simp []
+QED
+
 Theorem lameq_ssub_cong :
   !M N. M == N ==> ∀fm. fm ' M == fm ' N
 Proof
@@ -1137,6 +1160,12 @@ Proof
   Induct_on ‘Ns’ using SNOC_INDUCT >> rw [appstar_SNOC, lameq_APPL]
 QED
 
+Theorem lameta_appstar_cong :
+    !M N Ns. M === N ==> M @* Ns === N @* Ns
+Proof
+  Induct_on ‘Ns’ using SNOC_INDUCT >> rw [appstar_SNOC, lameta_APPL]
+QED
+
 (* Lemma 2.1.23 [1, p.30] *)
 Theorem lameq_LAMl_appstar_VAR[simp] :
     !xs. LAMl xs t @* (MAP VAR xs) == t

examples/lambda/barendregt/chap3Script.sml

@@ -5,14 +5,14 @@
 (* AUTHORS : 2005-2011 Michael Norrish                                        *)
 (*         : 2023-2025 Michael Norrish and Chun Tian                          *)
 (* ========================================================================== *)
+
 Theory chap3
 Ancestors
   basic_swap relation list pred_set nomset term chap2 appFOLDL
   horeduction
 Libs
   boolSimps metisLib hurdUtils pred_setLib BasicProvers binderLib
 
-
 (* definition from p30 *)
 Definition beta_def:  beta M N = ?x body arg. (M = LAM x body @@ arg) /\
                                               (N = [arg/x]body)
@@ -1356,22 +1356,43 @@ QED
       §3: Postponement Theorem
    ---------------------------------------------------------------------- *)
 
-Overload "-η->" = “compat_closure eta”
-Overload "-η->*" = “reduction eta”
-Overload "-βη->" = “compat_closure (beta RUNION eta)”
-Overload "-βη->*" = “reduction (beta RUNION eta)”
+val _ = set_fixity "-e->"  (Infix(NONASSOC, 450))
+val _ = set_fixity "-e->*" (Infix(NONASSOC, 450))
+Overload "-e->" = “compat_closure eta”
+Overload "-e->*" = “RTC (-e->)”
 
-val _ = set_fixity "-βη->" (Infix(NONASSOC, 450))
-val _ = set_fixity "-βη->*" (Infix(NONASSOC, 450))
-val _ = set_fixity "-η->" (Infix(NONASSOC, 450))
-val _ = set_fixity "-η->*" (Infix(NONASSOC, 450))
+val ueta_arrow = "-" ^ UnicodeChars.eta ^ "->"
+val _ = Unicode.unicode_version {u = ueta_arrow, tmnm = "-e->"}
+val _ = Unicode.unicode_version {u = ueta_arrow^"*", tmnm = "-e->*"}
 
-val _ = TeX_notation { hol = "-η->",
+val _ = TeX_notation { hol = "-e->",
         TeX = ("\\ensuremath{\\rightarrow_{\\eta}}", 1) };
 
-val _ = TeX_notation { hol = "-η->*",
+val _ = TeX_notation { hol = "-e->*",
         TeX = ("\\ensuremath{\\twoheadrightarrow_{\\eta}}", 1) };
 
+val _ = set_fixity "-be->"  (Infix(NONASSOC, 450))
+val _ = set_fixity "-be->*" (Infix(NONASSOC, 450))
+Overload "-be->"  = “compat_closure (beta RUNION eta)”
+Overload "-be->*" = “RTC (-be->)”
+
+val ubeta_eta_arrow = "-" ^ UnicodeChars.beta ^ UnicodeChars.eta ^ "->"
+val _ = Unicode.unicode_version {u = ubeta_eta_arrow, tmnm = "-be->"}
+val _ = Unicode.unicode_version {u = ubeta_eta_arrow^"*", tmnm = "-be->*"}
+
+val _ = TeX_notation { hol = "-be->",
+        TeX = ("\\ensuremath{\\rightarrow_{\\beta\\eta}}", 1) };
+
+val _ = TeX_notation { hol = "-be->*",
+        TeX = ("\\ensuremath{\\twoheadrightarrow_{\\beta\\eta}}", 1) };
+
+Theorem bestar_lameta :
+    !M N. M -be->* N ==> M === N
+Proof
+    rw [GSYM beta_eta_lameta]
+ >> PROVE_TAC [conversion_rules]
+QED
+
 Theorem eta_FV_EQN:
   eta M N ⇒ FV N = FV M
 Proof
@@ -1465,7 +1486,11 @@ Proof
   metis_tac[eta_beta_reorder0]
 QED
 
-
+Theorem benf_reduction_to_self:
+    !M N. benf M ==> (M -be->* N <=> N = M)
+Proof
+    METIS_TAC [corollary3_2_1, beta_eta_normal_form_benf, RTC_RULES]
+QED
 
 Theorem strong_grandbeta_gen_ind =
         grandbeta_bvc_gen_ind
@@ -1654,6 +1679,13 @@ Proof
   irule (cj 2 RTC_RULES) >> gs[CC_RUNION_DISTRIB, RUNION] >> metis_tac[]
 QED
 
+(* |- M -b->* N ==> M -be->* N *)
+Theorem betastar_bestar =
+        reduction_RUNION1 |> Q.GENL [‘R1’, ‘R2’] |> Q.SPECL [‘beta’, ‘eta’]
+
+(* |- M -e->* N ==> M -be->* N *)
+Theorem etastar_bestar =
+        reduction_RUNION2 |> Q.GENL [‘R1’, ‘R2’] |> Q.SPECL [‘beta’, ‘eta’]
 
 (* ----------------------------------------------------------------------
     Congruence and rewrite rules for -b-> and -b->*
@@ -1722,6 +1754,11 @@ Theorem betastar_TRANS =
         RTC_TRANSITIVE |> Q.ISPEC ‘compat_closure beta’
                        |> REWRITE_RULE [transitive_def]
 
+(* |- !x y z. x -e->* y /\ y -e->* z ==> x -e->* z *)
+Theorem etastar_TRANS =
+        RTC_TRANSITIVE |> Q.ISPEC ‘compat_closure eta’
+                       |> REWRITE_RULE [transitive_def]
+
 Theorem lameq_imp_lameta :
     !M N. M == N ==> lameta M N
 Proof