*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Dependent types and existence of n-dimensional space.*From*: grechukbogdan <grechukbogdan at yandex.ru>*Date*: Wed, 12 May 2010 13:21:21 +0400*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1273651845.2263.50.camel@macbroy12.informatik.tu-muenchen.de>*References*: <580921273596674@web127.yandex.ru> <1273651845.2263.50.camel@macbroy12.informatik.tu-muenchen.de>

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". Using spaces R^1, R^2, ..., R^100... I can prove lemmas "Every convex 1-dimensional set S has a nonempty relative interior" "Every convex 2-dimensional set S has a nonempty relative interior" .. "Every convex 100-dimensional set S has a nonempty relative interior" .. But I cannot prove a single lemma "Every convex nonempty set S has a nonempty relative interior" which looks very paradoxical for me. Also, my critical lemma fixes n :: nat obtains A where “A = (UNIV :: (real^'m) set)” and “dim A = n” could be easily proved by induction if I could prove that cartesian product of (UNIV :: (real^'m) set) and real is again in the form (UNIV :: (real^'n) set)... But probably the same problem here... Sincerely, Bogdan Grechuk. 12.05.10, 12:10, "Johannes Hölzl" <hoelzl at 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. > > - Johannes > > > > Sincerely, > > Bogdan Grechuk. > > > > -- Здесь спама нет http://mail.yandex.ru/nospam/sign

**Follow-Ups**:**Re: [isabelle] Dependent types and existence of n-dimensional space.***From:*Brian Huffman

**References**:**[isabelle] Dependent types and existence of n-dimensional space.***From:*grechukbogdan

**Re: [isabelle] Dependent types and existence of n-dimensional space.***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Next by Date: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Previous by Thread: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Next by Thread: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Cl-isabelle-users May 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list