Email Gateway (Aug 22 2022 at 13:14): Email Gateway (Aug 22 2022 at 13:14):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hi,
I am looking for lemmas that show that from every pair of lists you can
split off a maximal common prefix or suffix. I am looking for this:
lemma maximal_common_prefix:
shows "∃ps xs' ys'. xs = ps @ xs' ∧ ys = ps @ ys'
∧ (xs' = [] ∨ ys' = [] ∨ hd xs' ≠ hd ys')"
by (induct xs ys rule: list_induct2', blast, blast, blast)
(metis (no_types, hide_lams) append_Cons append_Nil list.sel(1))
corollary maximal_common_suffix:
shows "∃ss xs' ys'. xs = xs' @ ss ∧ ys = ys' @ ss
∧ (xs' = Nil ∨ ys' = Nil ∨ last xs' ≠ last ys')"
using maximal_common_prefix[of "rev xs" "rev ys"]
unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
The proofs work, but I would have expected that these statements already
exist somewhere in src/HOL/List.thy. Unfortunately, I couldn't find
these or something similar. I would be glad if someone corrected me.
These two lemmas look to me like they could be useful for many proofs
because they give a general way to decompose two lists.
So my question is, what is the process to propose new lemmas for HOL?
Do these two lemmas look reasonable enough (assuming they don't already
exist)?
Thanks,
Christoph
Email Gateway (Aug 22 2022 at 13:15):From: Tobias Nipkow <nipkow@in.tum.de>
They look indeed interesting, I'll probably add them in some form or another.
Thanks!
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 13:15):From: Joachim Breitner <breitner@kit.edu>
Hi,
so much ∃ quantifiers. Given that for any two lists, the maximal common
prefix is unique, wouldn’t it make sense to give this a name, define it
straight-forwardly using fun, and then possibly add lemmas?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 13:15):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
You can define the longest common prefix with the existing functions in List:
lcp xs ys = map fst (takeWhile (%(x, y). x = y) (zip xs ys))
In AFP/Coinductive, I have defined an operation llcp to return the longest common prefix
of two possibly infinite lists. There are also a few lemmas about llcp.
Andreas
Email Gateway (Aug 22 2022 at 13:15):From: Tobias Nipkow <nipkow@in.tum.de>
I was thinking along those lines as well. Moreover, it makes sense on any set of
lists:
"GREATEST ps WRT length. ∀xs ∈ L. prefix ps xs"
Of course that one is not executable. I'll put something suitable together.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 13:16):From: Tobias Nipkow <nipkow@in.tum.de>
I have added your two lemmas (with "longest" instead of "maximal") to the
distributiuon.
For a more comprehensive treatment of longest common prefixes I have added two
functions
Longest_common_prefix :: "'a list set => 'a list"
longest_common_prefix :: "'a list => 'a list => 'a list"
and their characteristic lemmas to Library/Sublist.
(http://isabelle.in.tum.de/repos/isabelle/rev/3413b1cf30cd)
Thanks for you suggestion, Christoph!
Tobias
smime.p7s
Last updated: Apr 19 2024 at 04:17 UTC