Stage work on finite_ltree_paths_imp_ltree_finite_lemma[local]

src/coalgebras/ltreeScript.sml

@@ -991,7 +991,31 @@ Proof
  (* NOTE: Now a is one of the longest path in t. If we remove this one leaf
     from t, the remaining ltree, say, t', holds for ‘ltree_paths t' = s’,
     and thus is finite by IH. Adding this one leaf back, is still finite.
+
+    Now, how to construct an ltree t' such that (at least):
+
+    1. ltree_lookup t' a = NONE
+    2. !p. p IN s ==> ltree_el t' p = ltree_el t p
+    3. ltree_paths t' = s
+
+    But some trivial cases must be excluded first:
   *)
+ >> Cases_on ‘s = {}’
+ >- (POP_ASSUM (gs o wrap) \\
+     Know ‘a = []’
+     >- (‘[] IN ltree_paths t’ by PROVE_TAC [NIL_IN_ltree_paths] \\
+         ASM_SET_TAC []) \\
+     DISCH_THEN (fs o wrap) \\
+     Q.PAT_X_ASSUM ‘!t. P’ K_TAC \\
+     Cases_on ‘t’ >> fs [ltree_paths_alt, EXTENSION] \\
+     Suff ‘ts = LNIL’ >- simp [ltree_finite] \\
+     CCONTR_TAC >> Cases_on ‘ts’ >> gs [] \\
+     POP_ASSUM (MP_TAC o Q.SPEC ‘[0]’) >> rw [ltree_el])
+ >> Cases_on ‘a = []’
+ >- (gs [GSYM MEMBER_NOT_EMPTY] \\
+     METIS_TAC [])
+ (* “ltree_el t p” is the ltree node where t and t' (to be constructed) differ *)
+ >> qabbrev_tac ‘p = FRONT a’
  >> cheat
 QED