coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [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, Pierre Corbineau <Pierre.Corbineau AT imag.fr>
Subject: Re: [Coq-Club] Declarative mode (C-zar): how to work with "suffices"?
Date: Mon, 18 Apr 2011 17:38:05 +0300
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:subject:references :in-reply-to:content-type:content-transfer-encoding; b=n6g633TdQtM9gl3KFsDQwnElv53sNWk0ALxAi3EUIwb/QSAg/TPm1U/AjpoQ06yJkg jApJQOq3+oUTYbSivisd5duDfp8fr5JquoHBUue8zkzDfWc/W/+w1KByzCZYi4X6BriG xH0XBL6B4Kq1lww3CCOUqwRFhLiWOyIT0tCp0=

On 18.04.2011 17:09, Pierre Corbineau wrote:

Case 2: QR |\- thesis (R) : you are missing the 'Q' hypothesis,
instead you should type :
Suffices H':Q to show thesis by H',QR.

Ah! Oh! That is, it is needed to always include Hi in justification in every
"suffices",
i.e. to write

    suffice H1:P1 and H2:P2 and ... to show thesis by H1, H2, ... A1, A2, ...

instead of

    suffice P1 and P2 and ... to show thesis by A1, A2, ...
.

Huge thanks, I could'nt figure out this myself in any way.

Single thing I've missed in great C-zar was fully powered backward reasoning.
Yahoo!

Vag.

(* all works perfectly now *)

Section S.

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

Goal (Q -> R) -> P -> R.
proof.
    assume QR:(Q -> R).
    assume HP:P.
    suffices HQ:Q to show thesis by HQ, QR.
    thus Q by HP, pq.
end proof. Qed.

Axiom qr: Q -> R.

Goal P -> R.
proof.
    assume HP:P.
    suffices HQ:Q to show thesis by HQ, qr.
    thus thesis by HP, pq.
end proof. Qed.

End S.

[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