coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hai WAN <wan.whyhigh AT gmail.com>
- To: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] how to proof this?
- Date: Fri, 14 Aug 2009 23:01:08 +0800
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=rYm73yftjyLue4pnY2QMTPjPT8ZtxNC84kzFstqQxuWSKVPxkTzAGWF0jxlF9slVCp 3yM2plZP4h/ZTql20FIwEqbq9eTdsPY/qVpVZjBY7bdhD9TAVattUGHp3rp+vQ/nt3p0 ARF+60yoaA+aSoplCc+j76Zwd0OaNQZcZHz8w=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear all,
(* Here are the Coq codes abstracted from a real problem.*)
Section test.
Variable P Q : Prop.
Variable a : P /\ Q.
Variable get : P -> Set.
Variable H0 :
match a with
| conj H0 _ => get H0
end.
Variable b : P.
(* I want to prove this goal, but got stuck. Could any one help? Thanks in advance!*)
Goal (get b).
--
Best regards,
Hai WAN
- [Coq-Club] how to proof this?, Hai WAN
- Re: [Coq-Club] how to proof this?, Adam Chlipala
Archive powered by MhonArc 2.6.16.