Ssreflect Users Discussion List

[Assia Mahboubi <>]

I was tired: the answer (first given by Laurence, thanks!) is: the rewrite fails 
because of the occurrence of n hidden in the coercion which allows to write #|t|...

The occurrence become visible after a Set Printing All, it's not even one of 
these disturbing cases when even Set Printing All cannot display some 
occurrences (hidden in the type of a match predicate for instance) that are 
caught by rewrite and make it fail. Anyway.

So the "rewrite" should be specialized to the second occurrence:

move=> T n t; rewrite -{2}(size_tuple t).

works perfectly.

Hope this will help somebody someday.

assia

Assia Mahboubi a écrit :
> 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