coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Declarative mode (C-zar): how to work with "suffices"?

From: Vag Vagoff <vag.vagoff AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Declarative mode (C-zar): how to work with "suffices"?
Date: Mon, 18 Apr 2011 12:41:40 +0300
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:subject :content-type:content-transfer-encoding; b=RK0QW1AJpARIw6mLlPcaQ+NOT6VaLQo+eN/miMx9zvMmYgyyhKj6K5yqlbdhHUiHCw vfsw4ENc8WSvf73YqQx7Mdm6pzbz0WPM6no3RCPFO/gtlacO8VE9NQaGY8XvvRJriwf0 hEOAszuUvL3tgafenS5mr/ZLoUs0JVWHA/4FY=

Hi!

How to use "suffices"?

According to the documentation the following must work but it does not.

Section S.
Variable P Q R : Prop.
Axiom pq: P -> Q.

Goal P -> Q.
proof.
    suffices Q to show thesis by pq. (* OK!!! Why?! *)
end proof. Admitted.

Goal (Q -> R) -> P -> R.
proof.
    assume QR:(Q -> R).
    assume H:P.
    suffices Q to show thesis by QR. (*!*)
    thus thesis by H, pq.
end proof. Admitted.

Axiom qr: Q -> R.

Goal P -> R.
proof.
    assume H:P.
    suffices Q to show thesis by qr. (*!*)
    thus thesis by H, pq.
end proof. Admitted.

End S.

! - "Warning: Insufficient justification." :(

Vag.

[Coq-Club] Declarative mode (C-zar): how to work with "suffices"?, Vag Vagoff
- Re: [Coq-Club] Declarative mode (C-zar): how to work with "suffices"?, Pierre Corbineau
  - Re: [Coq-Club] Declarative mode (C-zar): how to work with "suffices"?, Vag Vagoff