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

On Wed, May 12, 2010 at 2:21 AM, grechukbogdan <grechukbogdan at> 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.

- Brian

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