coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Declarative mode (C-zar): how to work with "suffices"?,
Pierre Corbineau
Archive powered by MhonArc 2.6.16.