Search code examples
coqssreflect

Coq - Proving condition about elements of sequence in Ssreflect

I have a goal that looks like this:

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

In the above, f is a definition generating a solution of an inequality depending on v, j and P v j is a predicate restricting j to indices which satisfy another inequality.

I have already proven that Goal : P v j -> (f v j > 0), but how can I use this to prove that it holds for any x in the sequence? I have found just a few relevant lemmas like nthP which introduce sequence manipulation, which I'm very unfamiliar with.

Thanks in advance!

Solution

  • You need to use the 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.