coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT univ-orleans.fr>
- To: vincent.chatel AT transport.alstom.com
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Forward and backward proof
- Date: Wed, 1 Oct 2003 11:05:05 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
vincent.chatel AT transport.alstom.com
wrote:
> Hi everybody,
>
> I would like to know if COQ supports the forward and backward proof in the
> same proof.
> In other word, it is possible to build new hypothesis from the assumptions
> and to make use of it to prove the goal.
It seems that the tactic Assert (or Cut) is made for this.
Cheers,
Pierre
- [Coq-Club] Forward and backward proof, vincent . chatel
- Re: [Coq-Club] Forward and backward proof, Pierre Courtieu
- Re: [Coq-Club] Forward and backward proof,
Robert R Schneck
- Re: [Coq-Club] Forward and backward proof, Hugo Herbelin
Archive powered by MhonArc 2.6.16.