Done all cheats in ltreeTheory !!!

binghe · Mar 3, 2025 · 5d19e4d · 5d19e4d
1 parent b67325c
commit 5d19e4d
Showing 1 changed file with 50 additions and 7 deletions.
diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml
@@ -1165,7 +1165,7 @@ Proof
 QED
 
 (* NOTE: “ltree_delete” does not remove the parent branch no matter what *)
-Theorem ltree_delete_parent_path :
+Theorem ltree_delete_path_stable :
     !f p t. p IN ltree_paths t ==> p IN ltree_paths (ltree_delete f t p)
 Proof
     Q.X_GEN_TAC ‘f’
@@ -1475,12 +1475,55 @@ Proof
  >> rw [gen_ltree_unchanged_extra]
 QED
 
-(* ltree_finite_ind *)
 Theorem ltree_finite_insert :
-    !p t d len. ltree_finite t /\ ltree_el t p = SOME (d,len) /\
-                ltree_finite t0 ==> ltree_finite (ltree_insert f t p t0)
+    !f p t t0 d len.
+       ltree_finite t /\ ltree_el t p = SOME (d,len) /\
+       ltree_finite t0 ==> ltree_finite (ltree_insert f t p t0)
 Proof
-    cheat
+    Q.X_GEN_TAC ‘f’
+ >> Induct_on ‘p’
+ >- (rw [ltree_el] \\
+     Cases_on ‘t’ >> rw [ltree_insert_NIL] \\
+     rw [ltree_finite, IN_LSET, LNTH_LGENLIST] \\
+     gs [LFINITE_LLENGTH] \\
+     rename1 ‘n < N + 1’ \\
+     Cases_on ‘n < N’ >> simp [] \\
+    ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
+     Know ‘IS_SOME (LNTH n ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
+     rw [IS_SOME_EXISTS] \\
+     simp [] \\
+     Q.PAT_X_ASSUM ‘ltree_finite (Branch a ts)’
+        (MP_TAC o REWRITE_RULE [ltree_finite]) \\
+     rw [IN_LSET] \\
+     POP_ASSUM MATCH_MP_TAC \\
+     Q.EXISTS_TAC ‘n’ >> art [])
+ >> rpt STRIP_TAC
+ >> Cases_on ‘t’ >> fs [ltree_el_def]
+ >> Cases_on ‘LNTH h ts’ >> fs []
+ >> MP_TAC (Q.SPECL [‘f’, ‘a’, ‘ts’, ‘h’, ‘p’, ‘x’, ‘t0’] ltree_insert_CONS)
+ >> simp []
+ >> DISCH_THEN K_TAC
+ >> rw [ltree_finite, IN_LSET, LNTH_LGENLIST]
+ >- (Q.PAT_X_ASSUM ‘ltree_finite (Branch a ts)’
+       (MP_TAC o REWRITE_RULE [ltree_finite]) \\
+     rw [LFINITE_LLENGTH, IN_LSET, GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS])
+ >> Q.PAT_X_ASSUM ‘ltree_finite (Branch a ts)’
+       (MP_TAC o REWRITE_RULE [ltree_finite])
+ >> rw [LFINITE_LLENGTH, IN_LSET, GSYM IS_SOME_EQ_NOT_NONE, IS_SOME_EXISTS]
+ >> rename1 ‘LLENGTH ts = SOME N’
+ >> fs []
+ >> Cases_on ‘n = h’ >> fs []
+ >- (Q.PAT_X_ASSUM ‘ltree_insert f x p t0 = t’ (REWRITE_TAC o wrap o SYM) \\
+     LAST_X_ASSUM MATCH_MP_TAC >> art [] \\
+     qexistsl_tac [‘d’, ‘len’] >> art [] \\
+     FIRST_X_ASSUM MATCH_MP_TAC \\
+     Q.EXISTS_TAC ‘h’ >> art [])
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> Q.EXISTS_TAC ‘n’ >> simp []
+ >> ‘LFINITE ts’ by rw [LFINITE_LLENGTH]
+ >> Know ‘IS_SOME (LNTH n ts)’ >- rw [LFINITE_LNTH_IS_SOME]
+ >> rw [IS_SOME_EXISTS]
+ >> simp []
 QED
 
 (* NOTE: These are simple versions not modifying ltree node data. *)
@@ -1629,14 +1672,14 @@ Proof
  >- (MATCH_MP_TAC ltree_insert_CONS \\
      simp [Abbr ‘ts1’, LNTH_LGENLIST] \\
      Cases_on ‘LLENGTH ts'’ >> simp []
-     >- (MP_TAC (Q.SPECL [‘I’, ‘p’, ‘x’] ltree_delete_parent_path) \\
+     >- (MP_TAC (Q.SPECL [‘I’, ‘p’, ‘x’] ltree_delete_path_stable) \\
          simp [ltree_paths_alt_ltree_el, GSYM ltree_lookup_iff_ltree_el]) \\
      STRONG_CONJ_TAC
      >- (Know ‘IS_SOME (LNTH h ts')’ >- rw [IS_SOME_EXISTS] \\
          simp [LNTH_IS_SOME] \\
          impl_tac >- rw [LFINITE_LLENGTH] >> simp []) >> DISCH_TAC \\
      rename1 ‘h < N’ \\
-     MP_TAC (Q.SPECL [‘I’, ‘p’, ‘x’] ltree_delete_parent_path) \\
+     MP_TAC (Q.SPECL [‘I’, ‘p’, ‘x’] ltree_delete_path_stable) \\
      simp [ltree_paths_alt_ltree_el, GSYM ltree_lookup_iff_ltree_el])
  >> Rewr'
  >> simp [LNTH_EQ, LNTH_LGENLIST, Abbr ‘ts1’]