The Coq mailing list

[左樱 <phoebezz AT 163.com>]

Hi guys,
 
  We meet some problems when using type 'Set'. We think the lemmas are quiet intuitive, any suggestion is appreciated.

 

======================================

Require Export String Bool ListSet List Arith Compare_dec Coq.Unicode.Utf8.
Open Scope nat_scope.
Open Scope type_scope.
Open Scope string_scope.

Inductive Kind:Set:=
|Send:Kind
|Receive:Kind.

Notation "!":=Send (at level 40).
Notation "?":=Receive (at level 40).
Definition Signal:=nat.
Definition Lifeline:=nat.
Definition Message:=Signal*Lifeline*Lifeline.
Definition Event:=Kind*Message.

Definition beq_lifeline (l1:Lifeline)(l2:Lifeline):bool:=
  beq_nat l1 l2.

Fixpoint projLife (l:Lifeline) (se: set Event) : set Event :=
match se with
|nil =>nil
|e::etail => match e with
           |(!,m) => match m with (_,tr,re) => if (beq_lifeline tr l)
                              then e::(projLife l etail)
                              else (projLife l etail)
                              end
           |(?,m) => match m with (_,tr,re) => if (beq_lifeline re l)
                              then e::(projLife l etail)
                              else (projLife l etail)
                              end
           end
end.

(*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)).
  intros;split;intros.
  destruct s1. inversion H0.
  destruct e. destruct k.
  simpl in H0. destruct m. destruct p. destruct (beq_lifeline l1 l).

(*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)).

 

Best Regards,
Phoebe