Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Arthur,

 (Emilio Jesús Gallego Arias) writes:

> [I tried to do the same you are trying to do some time back, but for now
> I've settled in using all, allP, elim: (enum P) and friends....]

This is an example of the tricks I use, the previous approach is
super-slow due to having to insubT:

Lemma all_i100_in_200 : [forall i : 'I_100,  i < 200].
Proof.
  have: all [pred i | i < 200] (map val (@enum 'I_100)).
    by rewrite val_enum_ord.
  rewrite all_map=> /allP Hall.
  by apply/forallP=> i; apply: Hall; rewrite mem_enum.
Qed.

So indeed you need something like iota for your finite types.

(Larger examples will become slow due to the peano encoding, but this is
 a different issue)

Best,
Emilio