Start lameta_BT_equivalent_cong

binghe · Jan 21, 2025 · 7dd6879 · 7dd6879
1 parent e166de8
commit 7dd6879
Showing 1 changed file with 26 additions and 24 deletions.
diff --git a/examples/lambda/barendregt/lameta_completeScript.sml b/examples/lambda/barendregt/lameta_completeScript.sml
@@ -39,29 +39,6 @@ val _ = hide "Y";
 (* some proofs here are large with too many assumptions *)
 val _ = set_trace "Goalstack.print_goal_at_top" 0;
 
-(*---------------------------------------------------------------------------*
- *  ltreeTheory extras
- *---------------------------------------------------------------------------*)
-
-(* ltree_subset A B <=> A results from B by "cutting off" some subtrees. Thus,
-
-   1) The paths of A is a subset of paths of B
-   2) The node contents for all paths of A is identical to those of B, but the number
-      of successors at those nodes of B may be different (B may have more successors)
-
-   NOTE: Simply defining ‘ltree_subset A B <=> subtrees A SUBSET subtrees B’ is wrong,
-         as A may appear as a non-root subtree of B, i.e. ‘A IN subtrees B’ but there's
-         no way to "cut off" B to get A, the resulting subtree in B always have some
-         more path prefixes.
- *)
-Definition ltree_subset_def :
-    ltree_subset A B <=>
-       (ltree_paths A) SUBSET (ltree_paths B) /\
-       !p. p IN ltree_paths A ==>
-           ltree_node (THE (ltree_lookup A p)) =
-           ltree_node (THE (ltree_lookup B p))
-End
-
 (*---------------------------------------------------------------------------*
  *  An equivalence relation of terms
  *---------------------------------------------------------------------------*)
@@ -558,7 +535,14 @@ QED
  *  Boehm trees of beta/eta equivalent terms
  *---------------------------------------------------------------------------*)
 
-(* Proposition 10.1.6 [1, p.219] *)
+(* Proposition 10.1.6 [1, p.219]
+
+   M -h->* M0
+  /          \b*
+ ==          +---[lameq_CR] y1 = y2, n1 = n2, m1 = m2
+  \         /b*
+   N -h->* Ns
+ *)
 Theorem lameq_BT_cong :
     !X M N r. FINITE X /\ FV M UNION FV N SUBSET X /\ M == N ==>
               BT' X M r = BT' X N r
@@ -660,6 +644,24 @@ Proof
       AP_TERM_TAC >> simp [Abbr ‘Qs’] ]
 QED
 
+(* cf. BT_ltree_paths_thm
+
+   M -h->* M0
+  /          \be*
+lameta        +---[lameta_CR] y1 = y2 /\ n1 + m2 = n2 + m1
+  \         /be*
+   N -h->* Ns
+
+   NOTE: Or “FV M UNION FV N SUBSET X UNION RANK r”.
+ *)
+Theorem lameta_BT_equivalent_cong :
+    !X M N r. FINITE X /\ FV M UNION FV N SUBSET X /\ lameta M N ==>
+              !p. p IN ltree_paths (BT' X M r) /\
+                  p IN ltree_paths (BT' X N r) ==> subtree_equiv X M N p r
+Proof
+    cheat
+QED
+
 (*---------------------------------------------------------------------------*
  *  BT_paths and BT_valid_paths
  *---------------------------------------------------------------------------*)