Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Weak lemmas in HOL-Analysis.Affine

Email Gateway (Oct 16 2020 at 14:17):

From: Jakub Kądziołka <kuba@kadziolka.net>
Dear Isabelle maintainers,

(which mailinglist should this go on? I'm not sure)

I have encountered some weak theorems in HOL-Analysis.Affine, where a
type is constrained to an euclidean space while any real vector space
suffices. Please consider the following diff.

Regards,
Jakub Kądziołka

@@ -1008,7 +1008,7 @@
using affine_hull_span_gen[of "0" S] assms by auto

lemma extend_to_affine_basis_nonempty:

• fixes S V :: "'n::euclidean_space set"
• fixes S V :: "'n::real_vector set"
  assumes "\<not> affine_dependent S" "S \<subseteq> V" "S \<noteq> {}"
  shows "\<exists>T. \<not> affine_dependent T \<and> S \<subseteq> T \<and> T \<subseteq> V \<and> affine hull T = affine hull V"
  proof -
  @@ -1044,7 +1044,7 @@
  qed

lemma affine_basis_exists:

• fixes V :: "'n::euclidean_space set"
• fixes V :: "'n::real_vector set"
  shows "\<exists>B. B \<subseteq> V \<and> \<not> affine_dependent B \<and> affine hull V = affine hull B"
  proof (cases "V = {}")
  case True
  @@ -1059,7 +1059,7 @@
  qed

proposition extend_to_affine_basis:

• fixes S V :: "'n::euclidean_space set"
• fixes S V :: "'n::real_vector set"
  assumes "\<not> affine_dependent S" "S \<subseteq> V"
  obtains T where "\<not> affine_dependent T" "S \<subseteq> T" "T \<subseteq> V" "affine hull T = affine hull V"
  proof (cases "S = {}")
  @@ -1073,13 +1073,13 @@

subsection \<open>Affine Dimension of a Set\<close>

-definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
+definition\<^marker>\<open>tag important\<close> aff_dim :: "('a::real_vector) set \<Rightarrow> int"
where "aff_dim V =
(SOME d :: int.
\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"

lemma aff_dim_basis_exists:

• fixes V :: "('n::euclidean_space) set"
• fixes V :: "('n::real_vector) set"
  shows "\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = aff_dim V + 1"
  proof -
  obtain B where "\<not> affine_dependent B \<and> affine hull B = affine hull V"

Email Gateway (Oct 16 2020 at 14:31):

From: Lawrence Paulson <lp15@cam.ac.uk>
I will take a look. Many thanks indeed for these! There must be hundreds more, so we need to keep looking.

Larry

Email Gateway (Oct 17 2020 at 10:22):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy with your suggestion in theorems, but does it make sense in this definition? Practically all of the theorems still require euclidean_space, so changing the definition as you suggest will merely force people to write more explicit type class constraints.

Larry

Email Gateway (Oct 17 2020 at 12:38):

From: Jakub Kądziołka <kuba@kadziolka.net>
aff_dim_basis_exists doesn't require euclidean_space. In fact, this
restriction on the definition is what motivated my investigation in the
first place, as I want to speak of an affine dimension in an arbitrary
real vector space in my formalization, and extracting a basis is what
I'm using the assumption for.

Regards,
Jakub Kądziołka

Email Gateway (Oct 17 2020 at 12:59):

From: Lawrence Paulson <lp15@cam.ac.uk>
Can you find any other theorems based on this definition that can similarly be generalised? It seems odd if that is the only one. And it would be nice to have some compensation for the effort that will be needed to add type class constraints for quite a few other theorems.

Larry

Email Gateway (Oct 17 2020 at 13:29):

From: Jakub Kądziołka <kuba@kadziolka.net>
There seems to be a significant fraction that uses the euclidean_space
constraint to deduce that a basis is finite, which is not true in an
infinite-dimensional vector space. This raises a question of what the
value of aff_dim should be in an infinite dimension, if any - currently
card returns 0 in this case, with excruciating results.

Adding a finite B condition to aff_dim wouldn't really work, as the
unspecified value this would result in wouldn't allow you to infer
'aff_dim S = -1 --> finite B'.

Maybe it would make sense to define a typeclass for finite-dimensional
real vector spaces, as an analogue of the
finite_dimensional_vector_space locale?

Regards,
Jakub Kądziołka

Last updated: Apr 26 2024 at 04:17 UTC