The Coq mailing list

[ldou AT cs.ecnu.edu.cn]

thanks for your reply!
when proving lemma "existselement", i do "induction d" and  "simpl", then Coq 
system produce a paticular "e0:e" and replace "d" with "(DE e0)". That's why 
you see such a particular constant string.

What confuse me is the difference when Coq compute the "interp" function. if 
i do:

Compute (interp (DE "e0")).

then i can get the following result  which is what i expect : 
     = (("e0" :: nil) :: nil) :: nil
     : m

but when do "induction d" and  "simpl" in lemma "existselement", i get a 
different result:
((e0 :: nil) :: nil)
which i think is wrong.
because due to  definition ,the type of m should be set (set (list string)). 



------------------ ԭʼÓʼþ ------------------
>From: Adam Chlipala 
><adamc AT csail.mit.edu>
>Reply-To: 
>To: 
>ldou AT cs.ecnu.edu.cn
>Subject: Re: [Coq-Club] [Coq Club]a strange question when using function
>Date: Wed, 24 Aug 2011 10:47:53 -0400
>
>ldou AT cs.ecnu.edu.cn
> wrote:
>>
>> the result turns out to be:
>> exists o' : o, (if o_dec o' ((e0 :: nil) :: nil) then true else false)
>> = true
>> but it should be :
>> exists o' : o, (if o_dec o' ((("e0" :: nil) :: nil) ::nil) then true
>> else false) = true
>> Why is that?
>>
>
>Can you explain why you expected a different result? This looks correct
>to me. Why would you expect an arbitrary [Diag] to be known to contain a
>particular constant string?
> 

--------------------------
Hi,everyone. I just meet a strange issue below:
=======================

Require Import String Bool ListSet List Classical.
Open Scope nat_scope.
Open Scope type_scope.
Open Scope string_scope.
Open Scope list_scope.
Definition e:=string.
Definition t := list e.
Definition o := set t.
Definition m:=set o.

Definition o_dec:forall (a b:o) ,{a = b} + {a <> b}.
   repeat decide equality.
Defined.

Inductive Diag:Set :=
 DE: e->Diag.

Fixpoint interp (D:Diag) {struct D}: m  :=
match D with
|DE e => ((e::nil)::nil)::nil
end.

Lemma test: set_mem o_dec  
   (("e0" :: nil) :: nil) ((("e0" :: nil) :: nil) ::nil)=true.
Proof.
  simpl. auto.
Qed.

Lemma existselement:forall d:Diag, 
  exists o':o, set_mem  o_dec o' (interp d )=true.
Proof.
  intro d.
  induction d. simpl.
=============
the problem is :when do simpl in existselement, the result turns out to be:
exists o' : o, (if o_dec o' ((e0 :: nil) :: nil) then true else false) = true
but it should be :
exists o' : o, (if o_dec o' ((("e0" :: nil) :: nil) ::nil) then true else 
false) = true
Why is that?