Add lcp (longest common prefix of list) with cv_trans support

src/list/src/rich_listScript.sml

@@ -3366,6 +3366,170 @@ Proof
   metis_tac[IS_PREFIX_LENGTH_ANTI]
 QED
 
+(* lcp2: binary longest common prefix *)
+Definition lcp2_def:
+  lcp2 x y = longest_prefix {x;y}
+End
+
+Theorem lcp2_thm:
+  lcp2 xs ys =
+    case xs of
+    | x::xs => (case ys of
+                | y::ys => if x = y then x :: lcp2 xs ys else []
+                | _ => [])
+    | _ => []
+Proof
+  Cases_on `xs` >> Cases_on `ys` >> rw[lcp2_def, longest_prefix_PAIR]
+QED
+
+(* lcp: longest common prefix of a list of lists *)
+Definition lcp_def:
+  lcp ls = longest_prefix (set ls)
+End
+
+Theorem lcp_nil[simp]:
+  lcp [] = []
+Proof
+  simp[lcp_def]
+QED
+
+Theorem lcp_sing[simp]:
+  lcp [x] = x
+Proof
+  simp[lcp_def]
+QED
+
+(* lcp2 is a prefix of both arguments *)
+Theorem lcp2_prefix:
+  lcp2 x y <<= x /\ lcp2 x y <<= y
+Proof
+  simp[lcp2_def] >>
+  MAP_EVERY qid_spec_tac [`y`,`x`] >>
+  Induct >> simp[longest_prefix_PAIR] >>
+  gen_tac >> Cases >> simp[longest_prefix_PAIR] >> rw[]
+QED
+
+(* any common prefix of x and y is a prefix of lcp2 x y *)
+Theorem lcp2_maximal:
+  p <<= x /\ p <<= y ==> p <<= lcp2 x y
+Proof
+  simp[lcp2_def] >>
+  MAP_EVERY qid_spec_tac [`y`,`x`,`p`] >>
+  Induct >- simp[] >>
+  rpt strip_tac >>
+  Cases_on `x` >> fs[] >>
+  Cases_on `y` >> fs[longest_prefix_PAIR] >> rw[]
+QED
+
+(* Key lemma: replacing {x;y} with {lcp2 x y} preserves common_prefixes *)
+Theorem common_prefixes_INSERT2:
+  common_prefixes ({x; y} UNION rest) =
+  common_prefixes ({lcp2 x y} UNION rest)
+Proof
+  simp[lcp2_def, common_prefixes_def, EXTENSION] >>
+  gen_tac >> eq_tac >> rw[] >>
+  metis_tac[lcp2_def, lcp2_maximal, lcp2_prefix, IS_PREFIX_TRANS]
+QED
+
+(* Key lemma: replacing {x;y} with {lcp2 x y} preserves longest_prefix *)
+Theorem longest_prefix_INSERT2:
+  longest_prefix ({x; y} UNION rest) = longest_prefix ({lcp2 x y} UNION rest)
+Proof
+  `{x; y} UNION rest <> {} /\ {lcp2 x y} UNION rest <> {}`
+    by simp[] >>
+  simp[longest_prefix_def, lcp2_def, common_prefixes_INSERT2]
+QED
+
+Theorem lcp_cons2:
+  lcp (x::y::xs) = lcp (lcp2 x y :: xs)
+Proof
+  simp[lcp_def, lcp2_def] >>
+  metis_tac[lcp2_def, longest_prefix_INSERT2, INSERT_UNION_EQ, UNION_EMPTY, INSERT_SING_UNION]
+QED
+
+Theorem lcp_thm:
+  !ls. (!x. MEM x ls ==> lcp ls <<= x) /\
+       (ls <> [] ==> !p. (!x. MEM x ls ==> p <<= x) ==> p <<= lcp ls)
+Proof
+  simp[lcp_def] >> rw[]
+  >- (`set ls <> {}` by (Cases_on `ls` >> fs[]) >>
+      simp[longest_prefix_def] >> SELECT_ELIM_TAC >> conj_tac
+      >- (irule FINITE_is_measure_maximal >> simp[]) >>
+      simp[is_measure_maximal_def, common_prefixes_def])
+  >- (`p IN common_prefixes (set ls)` by simp[common_prefixes_def] >>
+      `set ls <> {}` by (Cases_on `ls` >> fs[]) >>
+      simp[longest_prefix_def] >> SELECT_ELIM_TAC >> conj_tac
+      >- (irule FINITE_is_measure_maximal >> simp[]) >>
+      simp[is_measure_maximal_def] >> rw[] >>
+      `x IN common_prefixes (set ls)` by simp[] >>
+      `p <<= x \/ x <<= p` by metis_tac[two_common_prefixes] >>
+      metis_tac[IS_PREFIX_LENGTH, IS_PREFIX_LENGTH_ANTI, LESS_EQUAL_ANTISYM])
+QED
+
+Theorem lcp2_assoc:
+  lcp2 (lcp2 x y) z = lcp2 x (lcp2 y z)
+Proof
+  simp[lcp2_def] >>
+  MAP_EVERY qid_spec_tac [`z`,`y`,`x`] >>
+  Induct >> rw[longest_prefix_PAIR] >>
+  Cases_on `y` >> rw[longest_prefix_PAIR] >>
+  Cases_on `z` >> rw[longest_prefix_PAIR] >>
+  rw[] >> fs[longest_prefix_PAIR]
+QED
+
+Theorem lcp_oneline:
+  lcp ls =
+    case ls of
+    | [] => []
+    | [x] => x
+    | x::y::xs => lcp (lcp2 x y :: xs)
+Proof
+  Cases_on `ls` >> rw[lcp_nil, lcp_sing] >>
+  Cases_on `t` >> rw[lcp_sing, lcp_cons2]
+QED
+
+Theorem lcp_CONS:
+  lcp (x::xs) = if NULL xs then x else lcp2 x (lcp xs)
+Proof
+  qid_spec_tac `x` >>
+  Induct_on `xs` >> rw[lcp_sing, lcp_cons2] >>
+  simp[lcp2_def, lcp2_assoc]
+QED
+
+Theorem lcp2_is_nil:
+  lcp2 x y = [] <=> (x = [] \/ y = [] \/ HD x <> HD y)
+Proof
+  rw[lcp2_def, EQ_IMP_THM]
+  >> Cases_on `x` >> Cases_on `y` >> fs[longest_prefix_PAIR]
+QED
+
+Theorem lcp_is_nil:
+  !ls. lcp ls = [] <=>
+  (ls = [] \/ ?x y. MEM x ls /\ MEM y ls /\ lcp2 x y = [])
+Proof
+  Induct_on `ls` >> rw[]
+  >> rw[lcp_CONS]
+  >> fs[NULL_EQ, lcp2_is_nil]
+  >> Cases_on `lcp ls` >> fs[]
+  >- metis_tac[]
+  >> Cases_on `h` >> fs[]
+  >- metis_tac[]
+  >> Q.MATCH_GOALSUB_RENAME_TAC `h1 = h2 ==> _`
+  >> Q.SPEC_THEN `ls` mp_tac lcp_thm
+  >> rw[NULL_EQ]
+  >> Cases_on `h1 <> h2` >> fs[]
+  >- (Cases_on `ls` >> fs[]
+      >> Q.MATCH_GOALSUB_RENAME_TAC `h1::t1`
+      >> MAP_EVERY Q.EXISTS_TAC [`h1::t1`, `h`]
+      >> simp[]
+      >> Cases_on `h` >> fs[]
+      >> full_simp_tac (srw_ss() ++ boolSimps.DNF_ss) [] >> rw[])
+  >> rw[EQ_IMP_THM]
+  >- metis_tac[]
+  >> TRY (first_x_assum drule >> CASE_TAC >> rw[] >> NO_TAC)
+  >> metis_tac[]
+QED
+
 (*---------------------------------------------------------------------------
    A list of numbers
  ---------------------------------------------------------------------------*)

src/num/theories/cv_compute/automation/cv_stdScript.sml

@@ -258,6 +258,23 @@ QED
 
 val res = cv_trans UNZIP_eq
 
+val lcp2_pre_def = cv_trans_pre "lcp2_pre" rich_listTheory.lcp2_thm;
+
+Theorem lcp2_pre[cv_pre]:
+  !xs ys. lcp2_pre xs ys
+Proof
+  Induct \\ rw[] \\ simp[Once lcp2_pre_def] \\
+  Cases_on `ys` \\ simp[Once lcp2_pre_def]
+QED
+
+val lcp_pre_def = cv_trans_pre "lcp_pre" rich_listTheory.lcp_oneline;
+
+Theorem lcp_pre[cv_pre]:
+  lcp_pre ls
+Proof
+  completeInduct_on `LENGTH ls` \\ rw[Once lcp_pre_def]
+QED
+
 Definition genlist_def:
   genlist i f 0 = [] /\
   genlist i f (SUC n) = f i :: genlist (i+1:num) f n

src/sort/sortingScript.sml

@@ -2012,3 +2012,9 @@ Proof
   first_x_assum(qspec_then`b::rss` mp_tac)>>
   simp[]
 QED
+
+Theorem lcp_PERM:
+  PERM l1 l2 ==> lcp l1 = lcp l2
+Proof
+  rw[lcp_def] >> AP_TERM_TAC >> irule PERM_LIST_TO_SET >> simp[]
+QED