Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] show proof at each step

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] show proof at each step


Chronological Thread 
  • From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
  • To: coq-club AT inria.fr
  • Cc: etanter AT dcc.uchile.cl
  • Subject: Re: [Coq-Club] show proof at each step
  • Date: Thu, 25 May 2017 21:01:39 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f175.google.com
  • Ironport-phdr: 9a23:V6GNTxYOkX18Muoc0hs9fqr/LSx+4OfEezUN459isYplN5qZrs2/bnLW6fgltlLVR4KTs6sC0LuI9f2/ESxYuNDa4S9EKMQNHzY+yuwo3CUYQ/S5QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4VvJ6IwxxfTonZFefldyWd0KV6OhRrx6MO98Zx5/yhMp/4t8tNLXLnncag/UbFXAzMqPnwv6sHsqRfNUxaE6GEGUmURnBpIAgzF4w//U5zsrCb0tfdz1TeDM8HuQr86RTqt76FwSB/1kygHLCI28HvWisNrkq1Wpg+qqgFlzI7VZIGVM+d+fr/YcNgHS2dNQtpdWipcCY66coABDfcOPfxAoofguVUOoxuwCwqiCuzhxTBHhGP506Ih3uQ9EgzLxhAsE84AvXnWqtj+KaccUfqyzKnN1TjOcfdW3i346IfWdBAhvemDU6hxccrN0EUiCQfFgU+NqYP4ITyV0vkGvm+H4Op4VOKvl3IoqwVrrTiy28gjlI3Ji5kaylDB7yp5wYI1KcekR058ZN6pCZ1dvDyUOYtxR8MtWWBouCAix7Icop60YCkKyJUhxxHBbvyIaZKE4hX5VOaeOTt4hXRleKi+hxmo60SgxPf8WtG70FZLsipFksTMuWsX2xPP7ciHT+Nx/l2/1jmSyg/T6/1ELVoomqrcLp4sxKM7mJkLsUnbACP6hEH7gLWVe0gk4OSk9frrbqn8qpOBNYJ5ihnyPrktl8ClHOg0LxUCU3KF9em/zrHu/U30TbNXhfMsiKbZqorVJcEDq665HQBV1oEj5g66Dzi80dQYmWALLEtGeB6bloTpNUzCLfL4APuljFSslzBrx//CPrL/GJnCMn/DkLL5cbZ87U5T1hYzwMhB655IDrwNOvH+V0/ruNDGEBM1Lxa4z/vlBdh9zo8eXHiAAq6dMKPcq1+I4ecvLvGQa48NuTb9N+Qq5/r0gn8khFASY62p0IAYaHC9BPtmIkGZbWDwjdcGFGcGphA+Q/DyiF2eTT5TYG6/UL475jEiEY6pEYPDRp22j7Gaxye6HphWZnhcBVyWEHfocZ+EW/YWZy6ILM9hiG9Mab/0QIg4kBqqqQXSyrx9L+OS9DdLm4jk0Y1e42zWmBcuwgR1E4G212iQQ2xw1jcDXz4q16R2vEBwzn+M1KF5h7pTEtkFtKABaRszKZOJl78yMNv1QA+UJto=

Sure there is :) company-coq has it, in the
experiments/company-coq-term-builder folder.

If you already use Proof General and company-coq, you can open
company-coq-term-builder.el, then run M-x eval-buffer, and finally (in a Coq
file) M-x company-coq-TermBuilder.

There's a demo at
https://www.reddit.com/r/dependent_types/comments/3ydylj/incremental_program_construction_in_coq/
(https://asciinema.org/a/bb3fxq5k9cdekaxnb07owf4gn) (though that one shows
extraction, not partial proof, but it works the same).

Clément.

On 2017-05-25 19:21, Jason Gross wrote:
> There is not, but you can make a feature request on ProofGeneral here
> <https://github.com/ProofGeneral/PG/issues/new>, or for CoqIDE here
> <https://coq.inria.fr/bugs/enter_bug.cgi?component=IDE&bug_severity=enhancement>.
> You could also try submitting it as a feature request against Coq itself
> here
> <https://coq.inria.fr/bugs/enter_bug.cgi?component=Main&bug_severity=enhancement>,
> perhaps for a setting that allows any specified vernacular command to be
> executed after every sentence.
>
> On Thu, May 25, 2017 at 6:23 PM Éric Tanter
> <etanter AT dcc.uchile.cl
>
> <mailto:etanter AT dcc.uchile.cl>>
> wrote:
>
> Hi,
>
> When writing a proof, one can use “Show Proof” to display the current
> term in the response pane. This can be really helpful.
> So much that I’d like to be able to turn it on at all steps, in order
> to follow the step-by-step construction of the term without having to write
> down “Show Proof” after each dot.
> I understand that in general it is not practical for efficiency
> reasons, but as a pedagogical tool it would be great to have so that
> students “see” the term being built.
>
> Is there a way to (locally) activate “Show Proof” for each step of the
> term construction?
>
> Thanks,
>
> — Éric
>




Archive powered by MHonArc 2.6.18.

Top of Page