The Coq mailing list

[ldou AT cs.ecnu.edu.cn]

Thanks for your detail reply.
i think  "interp (DE y)" should be convertible to m ,thus to (list (list 
(list string))) and not to  (list (list string)) .
the problem now is that the proof of lemma "existselement" cann't go on:
------------------------------------------
Lemma existelement:forall d:Diag, 
  exists o':o, set_mem  o_dec o' (interp d )=true.
Proof.
  intro d.
  induction d. 
  exists ((e0 :: nil)::nil).
  simpl.
---------------------------------
then the proof gets stuck. 



------------------ ԭʼÓʼþ ------------------
>From: Pierre Casteran 
><pierre.casteran AT labri.fr>
>Reply-To: 
>To: 
>ldou AT cs.ecnu.edu.cn
>Subject: Re: [Coq-Club] [Coq Club]a strange question when using function
>Date: Thu, 25 Aug 2011 06:55:50 +0200
>
>Hi,
>
>
>Like Adam, I  don't see any error.
>
>For clarity's sake, I decomposed your example into small pieces, adding
>some "Compute" and "Check" commands, and renaming the variable e0 into y
>for avoiding confusion with the string "e0".
>
>
>First, you should not write such sentences like
>" the type of m should be set (set (list string))" :
>
>The correct statement are :
>"the type of m is Type" , and "m is convertible to (set (set (list 
>string)))",
>thus to (list (list (list string)))"
>
>
>
>In the proof of existselement, you can see that the type of o' should be
>convertible to (list (list string)) and not to (list (list (list string)))
>
>Pierre
>
>
>
>
>
>Quoting 
>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

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