Added fromRose_def, etc.

binghe · Jan 22, 2025 · 0f92f96 · 0f92f96
1 parent fb91c76
commit 0f92f96
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 14 deletions.
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -309,13 +309,6 @@ Proof
  >> qexistsl_tac [‘X’, ‘M’, ‘r’, ‘n’, ‘vs’, ‘M1’] >> simp []
 QED
 
-(* This is the meaning of Boehm tree nodes, ‘fromNote’ translated from BT nodes
-   to lambda terms in form of ‘SOME (LAMl vs (VAR y))’ or ‘NONE’.
- *)
-Definition fromNode_def :
-    fromNode = OPTION_MAP (\(vs,y). LAMl vs (VAR y))
-End
-
 (* Boehm tree of a single (free) variable ‘VAR y’ *)
 Definition BT_VAR_def :
     BT_VAR y :boehm_tree = Branch (SOME ([],y)) LNIL

diff --git a/examples/lambda/barendregt/lameta_completeScript.sml b/examples/lambda/barendregt/lameta_completeScript.sml
@@ -1341,17 +1341,31 @@ Proof
 QED
 
 (*---------------------------------------------------------------------------*
- *
+ * Distinct beta-eta-NFs are not everywhere (subtree) equivalent
  *---------------------------------------------------------------------------*)
 
-(* Exercise 10.6.9 [1, p.272].
-
-   NOTE: the actual statements have ‘has_benf M /\ has_benf N’
+(* NOTE: This definition is impossible for ltree because ltree has no "size",
+   all bottom (\bot) leaves are treated as the “Omega” term. For terms having
+   benf, there should be no bottoms in their Boehm trees.
  *)
+Definition fromRose_def :
+    fromRose (t :BT_node rose_tree) =
+      case (rose_node t) of
+        SOME (vs,y) => LAMl vs (VAR y @* MAP fromRose (rose_children t))
+      | NONE => Omega
+Termination
+    WF_REL_TAC ‘measure (rose_tree_size (\x. 0))’ >> rw []
+ >> MP_TAC (ISPEC “t :BT_node rose_tree” rose_tree_nchotomy)
+ >> STRIP_TAC
+ >> fs [rose_tree_size_def, rose_tree_size_eq, Once MEM_SPLIT_APPEND_first]
+ >> simp [list_size_append, list_size_def]
+End
+
+(* Exercise 10.6.9 [1, p.272] *)
 Theorem distinct_benf_imp_not_subtree_equiv :
-    !X M N r . FINITE X /\ X SUBSET FV M UNION FV N /\
-               benf M /\ benf N /\ M <> N ==>
-               ?p. ~subtree_equiv X M N p r
+    !X M N r. FINITE X /\ X SUBSET FV M UNION FV N /\
+              has_benf M /\ has_benf N /\ ~lameta M N ==>
+              ?p. p IN BT_paths M INTER BT_paths N /\ ~subtree_equiv X M N p r
 Proof
     cheat
 QED

diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml
@@ -987,6 +987,13 @@ Proof
   \\ fs [EVERY_MEM,MEM_MAP,PULL_EXISTS]
 QED
 
+Definition rose_node_def[simp] :
+    rose_node (Rose a ts) = a
+End
+
+Definition rose_children_def[simp] :
+    rose_children (Rose a ts) = ts
+End
 
 (* tidy up theory exports *)