Ssreflect Users Discussion List

[Arthur Azevedo de Amorim <>]

Ah, that does help! I guess I was missing the /(enum _) part.

Still, it's a bit unfortunate to have to have to unfold so much before
being able to unlock Finite.enum. It'd be nice if there were an easier
way...

2014-11-30 15:00 GMT-05:00 Emilio Jesús Gallego Arias <>:
> Hi Arthur,
>
> Arthur Azevedo de Amorim <> writes:
>
>> So I guess my _real_ question is: is there a convenient way of proving
>> a quantified statement over a finType by reflection?
>
> I don't know the right way to do it, or if it is really possible to do
> it in general (for instance you cannot unlock FinTuple.enum, etc...)
> but this ugly snippet will do what you want:
>
> Goal [forall i : 'I_5, i < 5].
> Proof.
>   rewrite /FiniteQuant.all /FiniteQuant.quant0b /pred0b cardE.
>   by rewrite /(enum _) unlock /= /ord_enum /= !insubT.
> Qed.
>
> It is likely that the above works only by chance.
>
> Best,
> Emilio



-- 
Arthur Azevedo de Amorim