Ssreflect Users Discussion List

[Arthur Azevedo de Amorim <>]

Hi Enrico and Frédéric,

I guess I was not very clear. My original goal was actually

Goal (cancel (fun n : 'I_2 => 0 < n) (fun b : bool => inZp b)).

which can be easily solved by case analysis by doing

by move=> n; apply: val_inj; case: n => [[|[|]]].

However, given that we're quantifying over a finite domain, I was
wondering if there was an easy way of getting this proof to go through
without doing any case analysis, by getting e.g. [forall n : 'I_2,
inZp (0 < n) == n] to reduce to true.

(Of course, for 'I_2 there's not much point in doing so, but it could
be useful for larger types).

So I guess my _real_ question is: is there a convenient way of proving
a quantified statement over a finType by reflection?

2014-11-30 13:19 GMT-05:00 Enrico Tassi <>:
> On Sun, Nov 30, 2014 at 07:01:36PM +0100, Frederic Chyzak wrote:
>> On Sun, 2014-11-30 at 11:34 -0500, Arthur Azevedo de Amorim wrote:
>> > Suppose that I have a goal such as
>> >
>> > Goal [forall b : bool, b == (0 < (b : nat))].
>>
>> Lemma foo : forall b : bool, b == (0 < (b : nat)).
>> Proof.
>> (* by case. *)
>
> Let me just add that if you really state it with the finite
> quantification [forall ...] provided by fintype, you have to
> start your proof by using the forallP in order to end up in
> the case Frederic explained.  In short:
>
>   by apply/forallP; case.
>
> Cheers,
> --
> Enrico Tassi



-- 
Arthur Azevedo de Amorim