Coq的 - 在Ssreflect

Question

證明約序列的元素條件I有一個目標，看起來像這樣：

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引理（表徵mem bership 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.