Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proof tree visualization

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof tree visualization


chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: coq-club AT inria.fr
  • Cc: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
  • Subject: Re: [Coq-Club] proof tree visualization
  • Date: Mon, 2 May 2011 14:22:05 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=wh2BT0j7JhA7PaOg/5a05tHSd1YpkDneGUWag0XkKbDXN08eP+4cUhF3Dke9u6wQxM +7cvbiPdyjoao5XClCeGoeoShKkwJAHmlsmgZJMkpjSzoJnyDPWiXYjVYGbbGy4eePZN +92gYxr+B/m7xPlr3YWM2aXzXu4MS5+uVZQ5E=

Well, I cannot be very specific but I was thinking of
1/ Building on bullets (currently experimental) for robust proofs. There is also (already in trunk) BeginSubproof and EndSuproof keywords (the names may change) which have similar effect. Other keywords/semantics can be readily implemented if there is some support for it.
2/ Facilities for naming goals. I haven't thought much of a final form for this.
3/ Extra beefy destruction tactics, with syntax such as: Destruct n. Case S 0. […] Case 0. […] Case S (S p). […]

None of these are promises. Rather things I'm willing to spend some time thinking of at some point.


Arnaud

On 1 May 2011 00:22, Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org> wrote:
Hi Arnaud
2011/4/29 Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>:
> It is quite likely that such features make their way to Coq. Though not for
> the next release I'm afraid.

Do you have any details on that? What sort of plans? I'm not talking
about a time line, just to have an idea of what kind of feature we can
expect. Are you talking about the bullets, or something more advanced?

I would really love to have more informations!

Alexandre




Archive powered by MhonArc 2.6.16.

Top of Page