The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Your [projLife] is just an instance of the standard list higher-order 
function [filter], and we can use a theorem about [filter] from the 
standard library to do almost all of the work.  Here's my alternate 
code, which replaces your code starting with the definition of [projLife]:

Definition projLife (l : Lifeline) : set Event -> set Event :=
  filter (fun e => let '(k, (_, tr, re)) := e in
    beq_lifeline (match k with
                    | ! => tr
                    | ? => re
                  end) l).

(*Q1:We believe this lemma holds,but we get lost when destructing the 
event*)
Lemma EventsEqualproj:forall s1 s2, ( ∀e : Event, set_In e s1 ↔ set_In e s2)
                                 ->  (∀e' l, set_In e' (projLife l s1) 
↔ set_In e' (projLife l s2)).
  unfold projLife; intros until l; split; intro Hin;
    apply filter_In in Hin; apply filter_In; firstorder.
Qed.

(*Q2: Is there any lemma in the standard library of Coq to solve the 
following problem?  *)
Lemma setneg:forall s1 s2,( ∀e : Event, set_In e s1 ↔ set_In e s2) -> (( 
∀e : Event, ¬set_In e s1 ↔ ¬set_In e s2)).
  firstorder.
Qed.