Coq - Условие доказательства элементов последовательности в Ssreflect

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 lemma (that characterizes 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.