Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Forward and backward proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Forward and backward proof


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page