coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Suggestions for Proof General?

From: "John Wiegley" <johnw AT newartisans.com>
To: Pierre Courtieu <pierre.courtieu AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>, Jonathan Leivent <jonikelee AT gmail.com>
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Thu, 23 Jun 2016 08:04:57 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f180.google.com
Ironport-phdr: 9a23:FNBt+hBFpijjUkhQZ8chUyQJP3N1i/DPJgcQr6AfoPdwSP7zpsbcNUDSrc9gkEXOFd2CrakV06yO7eu+BiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd+KyZzpnL7ts7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0r221qtvkg789NV7nhN+R9FOQATWduD2dg3MzmrwPOBSCI+2EAU2gL2k5QAgXf9hy8VZDsqDf7u/dV1yyTPMmwRrcxD2eM9aBuHVXKjycBfwE4/W7Th906xPZZpxKnuDR5zpHdep2UL/N4ZeXWetZMFjkJZdpYSyEUWtD0VIAIFedUeL8A94Q=
Organization: New Artisans LLC

>>>>> Pierre Courtieu
>>>>> <pierre.courtieu AT gmail.com>
>>>>> writes:

> When the goal is large, PG displays as much as possible of the goal, with an
> order of precedence: - prefer conclusion over hyps (1) - prefer bottom of
> the conclusion over its top (2)
>
> This is rather empirical setting. (1) is hardly questionable imho, but (2)
> is indeed arbitrary. I can maybe have an option for (2).

An option for (2) would be very helpful. I'm working with MIT's Fiat system,
which involves proofs that refine monadic, non-deterministic blocks "action by
action", from top to bottom, so knowing the bottom of the conclusion without
seeing the top is relatively useless.

Thanks,
--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

Re: [Coq-Club] Suggestions for Proof General?, (continued)