Re: [isabelle] Dependent types and existence of n-dimensional space.



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.