New proof of ltree_finite_BT_bnf

binghe · Feb 8, 2025 · 332f79f · 332f79f
1 parent 6c62fe6
commit 332f79f
Show file tree

Hide file tree

Showing 3 changed files with 56 additions and 4 deletions.
diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
@@ -85,6 +85,31 @@ Definition BT_generator_def :
             (NONE, LNIL)
 End
 
+(* M0 is not needed if M is already an hnf *)
+Theorem BT_generator_of_hnf :
+    !X M r. FINITE X /\ hnf M ==>
+            BT_generator X (M,r) =
+           (let
+             n = LAMl_size M;
+             vs = RNEWS r n X;
+             M1 = principle_hnf (M @* MAP VAR vs);
+             Ms = hnf_children M1;
+             y = hnf_headvar M1;
+             l = MAP (\e. (e,SUC r)) Ms
+           in
+             (SOME (vs,y),fromList l))
+Proof
+    rpt STRIP_TAC
+ >> ‘solvable M’ by PROVE_TAC [hnf_solvable]
+ >> RW_TAC std_ss [BT_generator_def]
+ >> ‘M0 = M’ by rw [Abbr ‘M0’, principle_hnf_reduce]
+ >> POP_ASSUM (fs o wrap)
+ >> Q.PAT_X_ASSUM ‘n' = n’   (fs o wrap o SYM)
+ >> Q.PAT_X_ASSUM ‘vs' = vs’ (fs o wrap o SYM)
+ >> Q.PAT_X_ASSUM ‘M1' = M1’ (fs o wrap o SYM)
+ >> Q.PAT_X_ASSUM ‘Ms' = Ms’ (fs o wrap o SYM)
+QED
+
 Definition BT_def[nocompute] :
     BT X = ltree_unfold (BT_generator X)
 End
@@ -793,7 +818,6 @@ QED
  *  More subterm properties
  *---------------------------------------------------------------------------*)
 
-(* M0 is not needed if M is already an hnf *)
 Theorem subterm_of_hnf :
     !X M h p r. FINITE X /\ hnf M ==>
       subterm X M (h::p) r =

diff --git a/examples/lambda/barendregt/lameta_completeScript.sml b/examples/lambda/barendregt/lameta_completeScript.sml
@@ -1351,6 +1351,33 @@ Theorem ltree_finite_BT_bnf :
     !X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ bnf M ==>
             ltree_finite (BT' X M r)
 Proof
+    RW_TAC std_ss [BT_def]
+ >> irule ltree_finite_by_unfolding
+ >> Q.EXISTS_TAC ‘\(M,r). FV M SUBSET X UNION RANK r /\ bnf M’
+ >> RW_TAC std_ss []
+ >> Q.EXISTS_TAC ‘size o FST’
+ >> rpt GEN_TAC
+ >> simp [every_LNTH, o_DEF]
+ >> PairCases_on ‘seed’
+ >> simp []
+ >> NTAC 2 STRIP_TAC
+ >> rename1 ‘FV N SUBSET X UNION RANK r'’
+ >> ‘solvable N /\ hnf N’ by PROVE_TAC [bnf_solvable, bnf_hnf]
+ >> Q.PAT_X_ASSUM ‘_ = (a,seeds)’ MP_TAC
+ >> Q_TAC (UNBETA_TAC [BT_generator_def, principle_hnf_reduce])
+          ‘BT_generator X (N,r')’
+ >> STRIP_TAC
+ >> POP_ASSUM (REWRITE_TAC o wrap o SYM)
+ >> REWRITE_TAC [LFINITE_fromList]
+ >> rw [LNTH_fromList, Abbr ‘l’, EL_MAP] >> rename1 ‘i < LENGTH Ms’
+ >- (simp [] \\
+     MP_TAC (Q.SPECL [‘M0’, ‘FV M0’] bnf_characterisation_X) >> simp [] \\
+     STRIP_TAC \\
+     cheat)
+ (* stage work *)
+ >> cheat
+QED
+(*
     rpt STRIP_TAC
  >> NTAC 2 (POP_ASSUM MP_TAC)
  >> Q.ID_SPEC_TAC ‘r’
@@ -1482,6 +1509,7 @@ Proof
  >> DISCH_TAC
  >> cheat
 QED
+*)
 
 Theorem ltree_finite_BT_has_bnf :
     !X M r. FINITE X /\ FV M SUBSET X UNION RANK r /\ has_bnf M ==>

diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml
@@ -674,7 +674,7 @@ Proof
   \\ fs [IN_LSET,LNTH_fromList,PULL_EXISTS,LFINITE_fromList,EVERY_EL]
 QED
 
-(* ltree_finite and ltree_unfold.
+(* ltree created by finite steps of unfolding is finite
 
    If the ltree is generated from a seed, whose resulting seeds after one-step
    unfolding is finite with smaller "measure", then there must be only finite
@@ -694,7 +694,7 @@ Proof
  >> LAST_X_ASSUM (drule o Q.SPEC ‘seed’)
  >> rw [Once ltree_unfold]
  >> qabbrev_tac ‘t = f seed’
- >> PairCases_on ‘t’ >> fs []
+ >> Cases_on ‘t’ >> fs []
  >> rw [Once ltree_finite, IN_LSET]
  >> FIRST_X_ASSUM irule
  >> fs [every_LNTH]
@@ -973,7 +973,7 @@ QED
  *  ltree_finite and (finite) ltree_paths
  *---------------------------------------------------------------------------*)
 
-Theorem ltree_finite_imp_finite_ltree_paths[local] :
+Theorem ltree_finite_imp_finite_ltree_paths :
     !t. ltree_finite t ==> FINITE (ltree_paths t)
 Proof
     HO_MATCH_MP_TAC ltree_finite_ind