The Coq mailing list

[Gábor Bakos <aborgabor AT gmail.com>]

Thank you Julien. I will take further look at ProverEditor. (The last
version was not working really well with Coq 8.2 on Vista. Hopefully
just some settings problem on my side.)
Also thanks for the link about finite set facts. I am afraid this is
not really what I want. I would like to use it a bit more
combinatorical way. I think some look at the 4-color theorem proof may
help. :)
Kind Regards, gabor

2009/2/17 Julien Narboux 
<Julien AT narboux.fr>:
> Hi,
>
> Gábor Bakos a écrit :
>>
>> Hi All,
>>
>> (Newbie post, non-native English speaker sorry about it.)
>> (Sorry if double post, the previous went to the mailto address from
>> the contact page 
>> (coq-club_NS AT pauillac.inria.fr)
>>  which seems to be not
>> correct. At least it resulted a mail delivery failure.)
>> I was able to download 8.2 sources from the homepage of Coq at last
>> weekend. Was it accidental? The build sais it is 8.2 (February 2009).
>> If I remember well those sources were marked as stable. Was that
>> release revoked or it was just a dream ;)? (I have seen no signs of
>> 8.2 at the home page of Coq till yesterday.)
>>
>
> You were not dreaming ;-)
>
>> Regarding the FAQ: The question 69 has a little confusing answer.
>> Would not it be better choice what does the error message means? Or
>> finishing by
>> cut (b*a <>0 -> a<>0).
>> cut (b*a <>0 -> b<>0).
>> auto.
>> auto with real.
>> auto with real.
>> Qed.
>> or
>> firstorder.
>> Qed.
>> ?
>>
>
> Thanks, you are right, the problem wad due to a change of the semantics of
> the field tactic.
>
>> Some of the questions (ex.: 133, 135, 144) remain unanswered. Are
>> those intentional?
>
> No, thanks for reporting this.  In the svn/trunk version of the faq, i have
> added an answer to the question about 'dependency graph' and deleted the
> other unanswered questions.
>
>> I miss an entry regarding the cardinality related formulation. I would
>> like to reason about finite sets' cardinality. Is it well supported?
>>
>
> You can get some results about cardinality of finite sets here :
>
> http://logical.saclay.inria.fr/coq/distrib/current/stdlib/Coq.Sets.Finite_sets_facts.html
>
>> PS.: Is not somewhere an eclipse plugin like Proof General for Coq?
>> (It would be interesting to see some of the XText features, like
>> context sensitive completion, content based hilighting, maybe model
>> transformation to MathML, ...)
>>
>>
>
> Have a look here : http://provereditor.gforge.inria.fr/
>
> Best wishes,
>
> Julien
>