The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 21 Mar 2012 16:07:29 +0800 (CST),
左樱 
<phoebezz AT 163.com>
 a écrit :

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

Do not write 'Set' (with an uppercase) as it is misleading since
Set is a kind and not a type. What you meant was 'set'.

I think that you shouldn't use beq_nat, but rather eq_nat_dec or
something like that, it makes proof easier since it carry some
specification ({x=y}+{x<>y}) while bool doesn't carry it and you must
rely on extra lemmas (beq_nat_true and beq_nat_false).

Also you should keep in mind what is the relation between your inputs
and your outputs.

So having defined

projLifeSpe : forall l s,
 {s' | forall e, set_In e (projLife l s) <-> (set_In e s ∧ …)}

could have helped a lot.
I don't use Program or Function, but I believe they have some
facilities to deal with that kind of stuff.

As you can see, once this specification is given the proof itself is
really easy (4 lines proof without relying on any highly automated
tactic but 'firstorder').
---------------------------------------------------------------------

(*Q1:We believe this lemma holds,but we get lost when destructing the
event*)
Lemma EventsEqualprojAux:forall e l s,
      set_In e (projLife l s) ↔ (set_In e s ∧
                                 let (k,m) := e in
                                 let (x,re) := m in
                                 let (_,tr) := x in
                                 (if k then tr else re) = l).
Proof.
 intros [k [[x tr] re]] l s.
 induction s; simpl; auto.
  firstorder.
 destruct a as [k' [[x' tr'] re']].
 assert (Heq : forall l', if beq_lifeline l' l then l' = l else l'<>l).
  clear; intros; unfold beq_lifeline.
  now generalize (beq_nat_true l' l); generalize (beq_nat_false l' l);
      destruct (beq_nat l' l); auto.
 generalize (Heq (match k' with ! => tr' | ? => re' end)); clear Heq.
 destruct k'.
  destruct (beq_lifeline tr' l); firstorder; subst; inversion H2; clear
H2; subst. reflexivity.
  destruct H; reflexivity.
 destruct (beq_lifeline re' l); firstorder; subst; inversion H2; clear
H2; subst. reflexivity.
 destruct H; reflexivity.
Qed.

(* Now it is just a piece of cake! *)
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)). Proof.
  intros s1 s2 He e l; generalize (He e); clear He.
  generalize (EventsEqualprojAux e l s1).
  generalize (EventsEqualprojAux e l s2).
  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)). Proof.
 (* I don't know, but there is a one line tactic proof *)
 firstorder.
Qed.


> 
> ======================================
> 
> 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
> 
> 
>  
>