Email Gateway (Oct 03 2020 at 08:38): Email Gateway (Oct 03 2020 at 08:38):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear all,
in need (of a particular instance of) the following obvious fact:
lemma (in order) fin_max: "finite A ⟹ a ∈ A ⟹ ∃ s ∈ A. a ≤ s ∧ (∀ b ∈
A. s ≤ b ⟶ s = b)"
I have proved it for myself (see below). I wonder whether it can be
obtained somehow more directly from Main.
Best regards
Stepan
proof (induct "card {b ∈ A. a < b}" arbitrary: a rule: nat_less_induct)
case 1
have IH: "⋀ x. x ∈ A ⟹ card {b ∈ A. x < b} < card {b ∈ A. a < b} ⟹
∃s∈A. x ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
by (simp add: "1.hyps" ‹finite A›)
then show ?case
proof (cases "∀b∈A. a ≤ b ⟶ a = b")
assume "∀b∈A. a ≤ b ⟶ a = b"
thus ?thesis
using ‹a ∈ A› by blast
next
assume "¬ (∀b∈A. a ≤ b ⟶ a = b)"
then obtain a' where "a' ∈ A" and "a < a'"
using local.antisym_conv1 by blast
have "{b ∈ A. a' < b} ⊂ {b ∈ A. a < b}" (is "?Ma' ⊂ ?Ma")
proof-
have "a' ∈ ?Ma" and "a' ∉ ?Ma'" and "⋀ c. c ∈ ?Ma' ⟹ c ∈ ?Ma"
using ‹a < a'› ‹a' ∈ A› by auto
thus "?Ma' ⊂ ?Ma"
by blast
qed
hence card: "card {b ∈ A. a' < b} < card {b ∈ A. a < b}"
by (simp add: ‹finite A› psubset_card_mono)
then obtain s where "s ∈ A" "a' ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
using IH[OF ‹a' ∈ A› card] by blast
hence "a ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
using ‹a < a'› by auto
thus ?thesis
using ‹s ∈ A› by blast
qed
qed
Email Gateway (Oct 04 2020 at 12:32):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Stepan,
an alternative is to use the well-foundedness of > restricted to the finite set A. This gives one maximal elements via wf_eq_minimal. Not sure if this qualifies as “more direct”, but at least no explicit induction is needed.
Dmitriy
lemma (in order) fin_max:
assumes "finite A" "a ∈ A"
shows "∃s ∈ A. a ≤ s ∧ (∀b ∈ A. s ≤ b ⟶ s = b)"
proof -
from ‹finite A› have "wf {(x,y). x ∈ A ∧ y ∈ A ∧ x > y}"
by (intro finite_acyclic_wf[OF finite_subset[of _ "A × A"]]) (auto intro!: acyclicI_order)
with ‹a ∈ A› show ?thesis
unfolding wf_eq_minimal using order.trans order.order_iff_strict
by (elim allE[of _ "{x ∈ A. a ≤ x}"] allE[of _ a]) (auto 7 0)
qed
Email Gateway (Oct 05 2020 at 16:23):From: Tobias Nipkow <nipkow@in.tum.de>
Maybe Min/Max (on finite sets) could be defined for arbitrary orders instead of
just linear orders as currently? Florian?
Tobias
smime.p7s
Email Gateway (Oct 05 2020 at 16:30):From: Manuel Eberl <eberlm@in.tum.de>
Note that Min/Max as of course no longer unique for non-linear orders.
Also note that Min/Max are instances of the more general arg_min/arg_max.
There are quite a few missing lemmas for arg_max that do exist for
arg_min, otherwise I would have replied to just use arg_max to the
original question.
Manuel
Email Gateway (Oct 06 2020 at 07:03):From: Tobias Nipkow <nipkow@in.tum.de>
On 03/10/2020 10:37, Stepan Holub wrote:
Dear all,
in need (of a particular instance of) the following obvious fact:
lemma (in order) fin_max: "finite A ⟹ a ∈ A ⟹ ∃ s ∈ A. a ≤ s ∧ (∀ b ∈ A. s ≤ b
⟶ s = b)"
This is a useful theorem and I am happy to add it. However, it seems more
modular to prove the simpler
lemma (in order) finite_has_max: "finite A ⟹ A ≠ {} ⟹ ∃ s ∈ A. (∀ b ∈ A. s ≤ b ⟶
s = b)"
first and derive
lemma (in order) finite_has_max2: "finite A ⟹ a ∈ A ⟹ ∃ s ∈ A. a ≤ s ∧ (∀ b ∈ A.
s ≤ b ⟶ s = b)"
from it in one line. In fact, I wonder if the second one is basic enough to go
into Main, but probably yes.
I would add the lemma(s) to Finite_Set using Stepan's proof because that way
they are added at the earliest point.
Comments, please.
Tobias
I have proved it for myself (see below). I wonder whether it can be obtained
somehow more directly from Main.Best regards
Stepan
proof (induct "card {b ∈ A. a < b}" arbitrary: a rule: nat_less_induct)
case 1
have IH: "⋀ x. x ∈ A ⟹ card {b ∈ A. x < b} < card {b ∈ A. a < b} ⟹ ∃s∈A. x ≤
s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
by (simp add: "1.hyps" ‹finite A›)
then show ?case
proof (cases "∀b∈A. a ≤ b ⟶ a = b")
assume "∀b∈A. a ≤ b ⟶ a = b"
thus ?thesis
using ‹a ∈ A› by blast
next
assume "¬ (∀b∈A. a ≤ b ⟶ a = b)"
then obtain a' where "a' ∈ A" and "a < a'"
using local.antisym_conv1 by blast
have "{b ∈ A. a' < b} ⊂ {b ∈ A. a < b}" (is "?Ma' ⊂ ?Ma")
proof-
have "a' ∈ ?Ma" and "a' ∉ ?Ma'" and "⋀ c. c ∈ ?Ma' ⟹ c ∈ ?Ma"
using ‹a < a'› ‹a' ∈ A› by auto
thus "?Ma' ⊂ ?Ma"
by blast
qed
hence card: "card {b ∈ A. a' < b} < card {b ∈ A. a < b}"
by (simp add: ‹finite A› psubset_card_mono)
then obtain s where "s ∈ A" "a' ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
using IH[OF ‹a' ∈ A› card] by blast
hence "a ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
using ‹a < a'› by auto
thus ?thesis
using ‹s ∈ A› by blast
qed
qed
Email Gateway (Oct 06 2020 at 09:38):From: Lawrence Paulson <lp15@cam.ac.uk>
The names should be “maximal” rather than “max”. The latter would suggest the Max function, which is only meaningful for linear orderings.
Larry
Email Gateway (Oct 06 2020 at 09:53):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear Tobias,
the absence of the simpler lemma is even more surprising. It seems to me
moreover that the version for minimum is not easily obtained either.
Nevertheless, I understood two things, thank to this mailing list:
Dmitriy pointed out that any acyclic relation on a finite list is
known to be wf, whence both maxima and minima are obtained. Which leads
much better proof (posted by Dmitriy up the thread) than the mine is.
Manuel pointed out that arg_max/arg_min can be used. Indeed, for
minima we have ex_min_if_finite in Lattices_Big:
lemma "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < (m::'a::order))"
(a side issue: I do not understand why I cannot get alternative
lemma (in order) "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < m)"
)
while for maxima a similar claim is missing at the moment.
Altogether, it seems to me that a lacking synchronization between
"order" "relation" and possibly "Lattices_Big" is somehow at play here.
Therefore, I really cannot tell
whether adding the lemma is the cleanest solution strategically,
although, of course, it would be handy practically.
Stepan
Email Gateway (Oct 06 2020 at 09:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Maybe Min/Max (on finite sets) could be defined for arbitrary orders
instead of just linear orders as currently?
See Manuel's answer.
Florian
signature.asc
Email Gateway (Oct 06 2020 at 10:57):From: Manuel Eberl <eberlm@in.tum.de>
(a side issue: I do not understand why I cannot get alternative
lemma (in order) "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < m)"
)
Welcome to the wonderfully frustrating world of Isabelle typeclasses!
Unfortunately, arg_min etc. are defined with an "ord" sort constraint.
However, inside the context of the "ord" typeclass itself, you do not
yet have this sort "ord" attached to the type variable. Therefore, this
gives you a type error due to the missing sort.
In this particular case, this issue could be fixed by defining the
constants inside the typeclass:
definition (in ord) is_arg_min :: "('b ⇒ 'a) ⇒ ('b ⇒ bool) ⇒ 'b ⇒
bool" where
"is_arg_min f P x = (P x ∧ ¬(∃y. P y ∧ f y < f x))"definition (in ord) arg_min :: "('b ⇒ 'a) ⇒ ('b ⇒ bool) ⇒ 'b" where
"arg_min f P = (SOME x. is_arg_min f P x)"
Indeed I would suggest we do it that way.
There are, however, cases where this does not work: for instance, any
definition of theorem involving two different types of that type class.
This is a very annoying technical limitation of Isabelle's type classes.
Usually, there is no big downside to just defining/proving stuff outside
the typeclass using explicit sort constraints, but one situation where
it gets really annoying is when want to use constants defined outside
the typeclass in the assumptions of a new subclass (e.g. something
builting on top of euclidean_space that makes some assumptions about the
limit of some function. Limits are not defined in the type class.)
Manuel
Email Gateway (Oct 06 2020 at 19:47):From: Tobias Nipkow <nipkow@in.tum.de>
I have now added some lemmas with succinct proofs (avoiding cardinalities) and
followed Manuel's suggestions concerning arg_min.
See here: http://isabelle.in.tum.de/repos/isabelle/rev/b037517c815b
If anybody has additional suggestions...
Tobias
smime.p7s
Email Gateway (Oct 07 2020 at 09:00):From: "Bisping, Benjamin" <benjamin.bisping@tu-berlin.de>
Adding these facts to Fnite_Set already would be great!
I also once spent an afternoon trying to figure out how to directly obtain such maxima browsing theorems around Finite_Set, order, Max and wf, because I assumed it would be somewhere in Main/Finite_Set. (And then I gave up and proved the instance I needed by an ugly detour through lists ... https://coupledsim.bbisping.de/isabelle/Finite_Partial_Order.html ) The lemmas you propose look as if they would have saved me the afternoon back then! :)
Kind regards,
Benjamin Bisping
smime.p7s
Email Gateway (Oct 07 2020 at 19:50):From: Jakub Kądziołka <kuba@kadziolka.net>
Are these lemmas missing for any other reason than "nobody bothered
yet"? I happened to need the arg_max variants of those today, so I
adjusted some proofs:
theory Scratch
imports
HOL.Lattices_Big
begin
lemma ex_max_if_finite:
"⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x > (m::'a::order))"
by(induction rule: finite.induct) (auto intro: order.strict_trans)
lemma ex_is_arg_max_if_finite: fixes f :: "'a ⇒ 'b :: order"
shows "⟦ finite S; S ≠ {} ⟧ ⟹ ∃x. is_arg_max f (λx. x ∈ S) x"
unfolding is_arg_max_def
using ex_max_if_finite[of "f ` S"]
by auto
lemma arg_max_SOME_Max:
"finite S ⟹ arg_max_on f S = (SOME y. y ∈ S ∧ f y = Max(f ` S))"
unfolding arg_max_on_def arg_max_def is_arg_max_linorder
apply(rule arg_cong[where f = Eps])
apply (auto simp: fun_eq_iff intro: Max_eqI[symmetric])
done
lemma arg_max_if_finite: fixes f :: "'a ⇒ 'b :: order"
assumes "finite S" "S ≠ {}"
shows "arg_max_on f S ∈ S" and "¬(∃x∈S. f x > f (arg_max_on f S))"
using ex_is_arg_max_if_finite[OF assms, of f]
unfolding arg_max_on_def arg_max_def is_arg_max_def
by(auto dest!: someI_ex)
lemma arg_max_greatest: fixes f :: "'a ⇒ 'b :: linorder"
shows "⟦ finite S; S ≠ {}; y ∈ S ⟧ ⟹ f(arg_max_on f S) ≥ f y"
by(simp add: arg_max_SOME_Max inv_into_def2[symmetric] f_inv_into_f)
lemma arg_max_inj_eq: fixes f :: "'a ⇒ 'b :: order"
shows "⟦ inj_on f {x. P x}; P a; ∀y. P y ⟶ f a ≥ f y ⟧ ⟹ arg_max f P = a"
apply(simp add: arg_max_def is_arg_max_def)
apply(rule someI2[of _ a])
apply (simp add: less_le_not_le)
by (metis inj_on_eq_iff less_le mem_Collect_eq)
end
It might've been cleaner to prove these using the equivalent arg_min
theorems by defining an 'inverse' order, but I have no idea how to do
that...
Regards,
Jakub Kądziołka
Last updated: Jul 15 2022 at 23:21 UTC