Email Gateway (Aug 18 2022 at 15:16): Email Gateway (Aug 18 2022 at 15:16):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users
I know that dependent types do not exist in Isabelle. But there should be some alternative way to express any (simple) mathematical fact, should not it? I really need the following lemma.
Lemma. Fix natural number n. Then there exist a n-dimensional real vector space R^n
This fact is absolutely obvious, and it is crucial for my formalization.
In Isabelle, for, say, n=100, I can easily obtain 100-dimensional space by writing
have “CARD(100)=100” by auto
from this obtain A where “A = (UNIV :: (real^100) set)” and “dim A = 100” by (simp add: dim_univ)
But I need this for general n. I can write
fix n :: nat
assume “CARD('m :: finite)=n”
from this obtain A where “A = (UNIV :: (real^'m) set)” and “dim A = n” by (simp add: dim_univ)
But now I need to obtain a n-dimensional universe without additional assumptions. Can somebody help me?
P. S. I hope this is possible. Otherwise how we can hope to formalize significant part of mathematics if we cannot prove such a simple fact?
Sincerely,
Bogdan Grechuk.
Email Gateway (Aug 18 2022 at 15:16):From: Brian Huffman <brianh@cs.pdx.edu>
Isabelle's lack of dependent types means that all types mentioned in a
proof must be fixed up front (like they are in your sample proof
above). You cannot obtain a new type variable in the middle of a proof
that depends on values obtained earlier in the proof.
Higher Order Logic is strictly less powerful than ZF set theory, so
eventually you might hit a point where HOL simply can't formalize the
mathematics you want. Fortunately, I think you are still a long way
from that point.
So you have a proof that might need to refer to a vector space of
arbitrary finite dimension (where no upper bound on the dimension is
known ahead of time). Essentially you would like to existentially
quantify over a countable family of types: real^n for all finite n.
The way to deal with this in HOL is to define a single type that is
large enough to embed all of those types; then you can quantify over
the finite-dimensional subspaces of that type.
Here's an example of a type that would work for this purpose:
typedef inf_vector = "{X::nat => real. finite {n. X n ~= 0}}"
Values of this type are infinite sequences of reals with only finitely
many non-zero entries. You should be able to make inf_vector an
instance of all the relevant type classes for doing linear algebra:
You can define addition, subtraction, scalar multiplication, metric,
norm, and inner product, and prove that those operations satisfy the
appropriate laws.
I know that this is a lot more work than what would be required in a
system with dependent types. But at least it is possible, and you
still get to enjoy all the other benefits (type inference, etc) of
HOL.
Hope this helps,
Email Gateway (Aug 18 2022 at 15:16):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Bogdan,
Am Dienstag, den 11.05.2010, 20:51 +0400 schrieb grechukbogdan:
Dear Isabelle Users
I know that dependent types do not exist in Isabelle. But there
should be some alternative way to express any (simple) mathematical
fact, should not it? I really need the following lemma.Lemma. Fix natural number n. Then there exist a n-dimensional real
vector space R^n
[..]
It works as long as _the type 'n_ is fixed:
fix n :: nat
assume "CARD('n :: finite) = n"
moreover def "A == UNIV :: (real^'n) set"
ultimately have "dim A = n" using dim_univ[where 'n='n]
by simp
What you can't do is to _obtain a type_, i.e. you can not say to obtain
a 'm with CARD('m) = n. You need always to formulate it the other way
round: i.e. n = CARD('m) when 'm is fixed.
But now I need to obtain a n-dimensional universe without additional assumptions. Can somebody help me?
Where do you get n from? If it is a fixed variable at the toplevel of
your prove replace it by some finite type variable. If you get it via
induction or similar it is probably not possible.
P. S. I hope this is possible. Otherwise how we can hope to formalize significant part of mathematics if we
cannot prove such a simple fact?
This is an unfortunate side effect of the formalization of finite
cartesian products in HOL-Multivariate_Analysis. However this is
probably the only sensible formalization possible in HOL. Otherwise all
the advantages of having types is lost and we could also work in ZF.
Sincerely,
Bogdan Grechuk.
Email Gateway (Aug 18 2022 at 15:16):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Johannes
Thank you for the responce.
Email Gateway (Aug 18 2022 at 15:17):From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, May 12, 2010 at 2:21 AM, grechukbogdan <grechukbogdan@yandex.ru> wrote:
Dear Johannes
Thank you for the responce.
Where do you get n from? If it is a fixed variable at the toplevel of
your prove replace it by some finite type variable. If you get it via
induction or similar it is probably not possible.Actually, I am proving lemma "Every convex nonempty set S has a nonempty relative interior", and n is the dimension of set S.
So, I would say that n is a fixed variable at the toplevel, no induction here or similar, I just have fixed set S and it has a fixed dimension. Can I use "some finite type variable"? But I cannot "assume "CARD('n :: finite) = n" inside the proof, in this case I have error when try to write "qed".
Hi Bogdan,
In this particular case, since "S" has a specific (finite) dimension
that is fixed in advance, you should not need to resort to using the
inf_vector type that I recommended in my previous email. You should be
able to prove your lemma using only types like "real^'n".
In order to help you more, I will need to know more details about the
lemma you are trying to prove. I guess that "Every convex nonempty set
S has a nonempty relative interior" would be formalized like
lemma fixes S :: ??? obtains T :: ??? where <some formula of S and T>
or "ALL S::???. EX T::???. <some formula of S and T>"
In particular, I need to know the types of S and T, which would be in
place of "???" above.
Also, my critical lemma
fixes n :: nat obtains A where “A = (UNIV :: (real^'m) set)” and “dim A = n”
My earlier advice applies here: Instead of trying to quantify over
types, you need to rephrase this by quantifying over subspaces of a
single fixed type.
It seems like you are trying to say:
"ALL n::nat. EX 'm. (dim (UNIV :: (real^'m) set)) = n"
which is true, but nonsense in HOL because you can't quantify over types.
Instead, you should be trying to prove something like this, where type
'm is fixed, and you quantify over subsets of real^'m:
"ALL n::nat. n <= CARD('m) --> EX A::(real^'m) set. dim A = n"
Again, it's hard to give more specific advice without knowing more
details about what exactly you are trying to prove.
Email Gateway (Aug 18 2022 at 15:17):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Brian
No, unfortunately, I really need exactly what I have asked.
lemma *: fixes n :: nat obtains A where “A = (UNIV :: (real^'m) set)” and “dim A = n”
Here is the citation from the book which I am formalizing
"m-dimentional affine hull of S can be regarded as a copy of space R^m. It is often possible in this manner to reduce a question about general convex set to the special case where the convex set is of full dimension, i.e. has the whole space as its affine hull."
After this remark every second prove in the book start with "without loss of generality assume that S is of full dimension", so I actually cannot proceed without formalization of this remark.
The plan of proving any property P of set S in this way is the following
1) Prove it for the case when S is of full dimension
2) Prove that property P is preserved under isomorphism
3) Constract an isomorphism from affine hull S to the WHOLE SPACE with the same dimension.
So, I cannot rephrase this by quantifying over subspaces of a single fixed type. I really need to use that A in the lemma * ubove is the whole space, whole universe, not a subspace. For example, I need inclusion "ball 0 1 <= A" which does not hold if A is just a subspace.
In my particular case property P is "has nonempty relative interior".
So, first, I have proved this for the case of full dimension:
lemma interior_convex_ndim_nonempty:
fixes S :: "(real^'n) set"
assumes "convex S" and "aff_dim S = int(CARD('n))"
shows "rel_interior S ~= {}"
Then I have proved that relative interior is preserved under the injective linear transformation
lemma rel_interior_injective_on_span_linear_image:
fixes f :: "(real ^'m) => (real ^'n)"
fixes S :: "(real ^'m) set"
assumes "bounded_linear f" and "inj_on f (span S)"
shows "rel_interior (f S) = f (rel_interior S)"
And finally, I have lemma subspace_isomorphism, stating that any two subspaces of the same dimension are isomorpic, and I can use it to construct the desired isomorhism f (provided that I can obtain universe A with the same dimension as S)
obtain A where A_def: "A = (UNIV :: (real^'m::finite) set)" and A: "dim A = dim S" sorry
obtain f where f_def: "linear f & f ` span S = (UNIV :: (real^'m) set) & inj_on f (span S)"
using subspace_isomorphism[of "span S" "(UNIV :: (real^'m) set)"]
A_def A dim_span[of S] subspace_span[of S] by auto
Again, what is important, I will need this isomorphism to UNIV for many other lemmas.
Probably, now it is claer, that type
typedef inf_vector = "{X::nat => real. finite {n. X n ~= 0}}"
of infinite sequences of reals with only finitely many non-zero entries, does not work at all. Here the universe is infinite-dimensional, and what I need is m-dimensional universe...
So, is there a point where HOL simply can't formalize the mathematics I want?
Sincerely,
Bogdan.
Email Gateway (Aug 18 2022 at 15:17):From: Timothy McKenzie <tjm1983@gmail.com>
This discussion reminds me of The QED Manifesto Revisited:
http://mizar.org/trybulec65/8.pdf
In particular, the second of the four "benchmark" statements
discussed in section 3.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 15:18):From: Lawrence Paulson <lp15@cam.ac.uk>
Let's go back to first principles and consider how a mathematician would represent a point in a multi-dimensional space. If we are to include finite and infinite dimensions in the same framework, then a point must be a map from an ordinal into the set of real numbers. I can't think of a better approach. Note that such a point contains in it not merely the values of its components, but its dimension.
Such an approach can be done in higher-order logic, although with more effort. Possibly you could use the primitives in Library/FuncSet.thy. You could fix some linearly ordered type to use in place of the ordinals, or make the construction parametric in a type of variable belonging to class linorder. A point would be given by an element N of this index type, coupled with a map from the initial segment of elements below N into the reals. If you only need finite-dimensional spaces, then a point could obviously be represented by a list of real numbers. You
But it looks to me like you have adopted an approach in which the dimension of a point is part of its type, rather than part of its value. This is inevitably going to be a lot less flexible; it is similar to the situation in group theory, where the carrier of a group really must be formalised as a set rather than as a type.
Larry Paulson
Last updated: Apr 25 2024 at 08:20 UTC