The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

Dear Vag,

Case 1:  pq |- thesis trivially.

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

Case 3: idem 2.

Hope this helps.


Pierre






On 04/18/2011 11:41 AM, Vag Vagoff wrote:
> 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.

--
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B2G2
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature