Ssreflect Users Discussion List

[Assia Mahboubi <>]

Sorry I had an implicit type I did not copy in my previous message; T shouild be 
a finType. hence I want to prove:


Lemma test : forall (T : finType) n (t : n.-tuple T), #|t| <= n.

Sorry again...

assia

Assia Mahboubi a écrit :
> I would like to prove the following (somehow silly) lemma:
>
> Lemma test : forall T n (t : n.-tuple T), #|t| <= n.
>
> I tried the following script:
>
> move=> T n t; rewrite -(size_tuple t).
>
> which fails with the error message (which I wasn't expecting):
>
> Error: dependent type error in rewrite of (fun _pattern_value_ : nat =>
>                                            is_true (#|t| <= 
> _pattern_value_))
>
> I still have to learn about dependent types...
> And also I do not know what is the bast way of proving the result.
>
> Can anyone help?
>
> Thanks in advance.
>
> assia