Email Gateway (Aug 25 2020 at 08:49): Email Gateway (Aug 25 2020 at 08:49):From: Michael Foster <jmafoster1@sheffield.ac.uk>
Hello,
As part of a larger project, I have proved what I am calling for want of
a better name "list minimality". That is, if there exists a list l which
satisfies a property P, then there exists a shortest list which
satisfies that property. This particular proof is very useful to me, and
I was somewhat surprised that it had not already been proven. I
therefore thought that it might be of use generally, and wondered
whether there was any possibility of it being included into List.thy?
The proof is quite short (less than 100 lines including all sub-lemmas)
and I am happy to send it to whoever may be interested.
As an aside, I think I could extend the minimality property to ordered
datatypes reasonably easily and prove that, if there exists an element
which satisfies a given property, there exists a minimal element. I
would be happy to have a go at this if people think this is worthwhile,
and make the proof generally available if I succeed.
Best,
Michael F.
Email Gateway (Aug 25 2020 at 08:53):From: Manuel Eberl <eberlm@in.tum.de>
Hello,
this can be expressed fairly naturally with the "is_arg_min" construct
from the library, then you don't have to prove anything.
lemma
fixes P :: "'a list ⇒ bool"
assumes "∃xs. P xs"
shows "∃xs. is_arg_min length P xs"
using assms is_arg_min_arg_min_nat by metis
Cheers,
Manuel
Email Gateway (Aug 25 2020 at 08:58):From: Tobias Nipkow <nipkow@in.tum.de>
The lemma
lemma ex_has_least_nat: "P k ⟹ ∃x. P x ∧ (∀y. P y ⟶ m x ≤ m y)"
for m :: "'a ⇒ nat"
expresses this in greater generality. In your case, m is length.
Tobias
smime.p7s
Email Gateway (Aug 26 2020 at 08:26):From: Michael Foster <jmafoster1@sheffield.ac.uk>
Both of those are nice proofs. As I said, I was surprised that it hadn't
already been proven - turns out it has! Thanks for pointing me in the
right direction.
Michael F.
Last updated: Jan 04 2025 at 20:18 UTC