Stream: Coq users

Topic: Proofs on filters (ssreflect.seq)

view this post on Zulip Felipe Lisboa Malaquias (Aug 16 2021 at 12:38):

Hey, beginner question here.

I'm trying to prove a Lemma containing some hypotheses and a goal that look like this:

x : Type_t
R : seq Type_t
H : x \in [seq elem <- R | elem.(field) == value]
------------------------------------------------------------
x.(field) == value

Whereas Type_t ia an eqType Record defined by me.

How could I assert that the predicate used on the filter function is true ? If I can assert such thing, applying the Lemma below might solve my issue.
filter_predT: forall [T : Type] (s : seq T), [seq x <- s | predT x] = s

Thanks in advance,

view this post on Zulip Christian Doczkal (Aug 17 2021 at 11:19):

You should be able to do a move: H; rewrite mem_filter to get x \in R and x.(field) == value. The lemma filter_predT is for eliminating a trivial filter, which yours does not seem to be. Hope this helps.

Last updated: Oct 04 2023 at 22:01 UTC