Ssreflect序列元素的协q证明条件

Question

我的目标是这样的：

x \in [seq (f v j) | j <- enum 'I_m & P v j] -> 0 < x

在上面，f是一个定义，根据v, j生成一个不等式的解，P v j是一个谓词，限制j到满足另一个不等式的索引。

我已经证明了Goal : P v j -> (f v j > 0)，但是如何用它来证明序列中的任何x都是有效的呢？我只发现了一些相关的引理，比如nthP，它们引入了序列操作，我对此非常陌生。

提前感谢！

Answer 1

您需要使用mapP引理( membership wrt map的特征)：

Lemma U m (P : rel 'I_m) f v x (hp : forall j, P v j -> f v j > 0) :
  x \in [seq f v j | j <- enum 'I_m & P v j] -> 0 < x.
Proof. by case/mapP=> [y]; rewrite mem_filter; case/andP=> /hp ? _ ->. Qed.