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"

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

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

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

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

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: Sep 28 2021 at 19:14 UTC