Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Please make coqtop and coqide not lie "Proof completed"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Please make coqtop and coqide not lie "Proof completed"


chronological Thread 
  • From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
  • To: Georgi Guninski <guninski AT guninski.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Please make coqtop and coqide not lie "Proof completed"
  • Date: Wed, 25 May 2011 22:51:29 +0800
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:in-reply-to:user-agent; b=mJT4RzuG+w3m9IeSQ/mnymWPtcVhAtmFrM1K/tjqWA6j6VFSsMLYySFiQWDKwz8cs9 fEIqVtfMmJOYVCRnAeHcFzluewYvVrpt6PDmaFM22PgmrUz1dmWjTqsr9vM9ICRGhMOm X91GkSmsVA5tYma7bajo9GVg+n9avoiSD0jVA=
This is a well-known feature. "Proof completed" just means that you
don't have subgals left, but says nothing about guardedness.
Usual tactics don't raise this issue, but fix does.
BTW this tactics is not documented, for some reason...

This is just like writing

Fixpoint l3 (H: CC) : False := l3 H.

So if you happen to try it, you must know what you are doing and not complain.

JF

On Wed, May 25, 2011 at 05:34:16PM +0300, Georgi Guninski wrote:
> coqtop gives misleading message:
> u
> Inductive CC : Prop := C1: (exists B : Prop,CC)->CC | C2 : True->CC.
> Lemma l3: CC->False.
> Proof.
> fix 1. 
> intros.
> exact (l3 H).
> Qed.
> l3 < Proof completed.
> ^ the above is a lie :)
> 
> thank you.

Archive powered by MhonArc 2.6.16.

Top of Page