The Coq mailing list

[gang chen <gangchen_sh AT yahoo.com>]

thanks for all the replies.

just curious to know what motivates this "better elimination"?

gang chen


Pierre Courtieu-3 wrote:
> 
> Le Thu, 18 Oct 2007 15:16:54 -0700 (PDT), gang chen
> <gangchen_sh AT yahoo.com>
>  a écrit:
>> 
>>  Here is the statement of treesort in Heap:
>> 
>>     forall l:list A, {m : list A | sort leA m & permutation _ eqA_dec l
>> m}.
>>   
>> Is the use '&' here a bug ? I suspect it should be '/\'.
>> 
> 
> No, this notation refers to sig2 which has a better elimination
> principle than sig + conjonction. See the difference:
> 
> Hypothesis H: {m:nat | m=0 & m=1}.   
> Hypothesis H': {m:nat | m=0 /\ m=1}.   
> Goal False.
> 
>  elim H.    gives  forall x : nat, x = 0 -> x = 1 -> False
> whereas 
>  elim H'    gives   forall x : nat, x = 0 /\ x = 1 -> False
> 
> 
> Cheers,
> Pierre Courtieu
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

-- 
View this message in context: 
http://www.nabble.com/standard-library-Coq.Sorting.Heap-treesort-tf4650066.html#a13326339
Sent from the Coq mailing list archive at Nabble.com.