Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] (soft question) idiomatic inline of assert

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] (soft question) idiomatic inline of assert


Chronological Thread 
  • From: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] (soft question) idiomatic inline of assert
  • Date: Thu, 4 Jul 2013 10:34:48 +0200

On Wed, Jul 03, 2013 at 10:24:14AM -0700, t x wrote:
> assert ( _statement_ ) as H0 by _tactic_ .
> pose proof (lemma ... H0 ...).

In ssreflect this could be expressed as

have tmp : _statement_ by _tactic_.
have {tmp} := lemma ... tmp ... .

where {tmp} is the syntax for clear, and have := is the anonymous
cut resulting in a new implication on top of your goal.

I see more compact ways only if know what you want to do with "lemma".
For example, if lemma proves an equality and you want to rewrite with it
you could even do that

have -> := lemma ... (_ : _statement_) ...; last by _tactic_.

or

rewrite (lemma ... (_ : _statement_) ...); last by _tactic_.

that follows Pierre's idea of using type inference to open a new goal.

Cheers
--
Enrico Tassi



Archive powered by MHonArc 2.6.18.

Top of Page