coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] (soft question) idiomatic inline of assert, t x, 07/03/2013
- [Coq-Club] Re: (soft question) idiomatic inline of assert, t x, 07/03/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, Pierre-Marie Pédrot, 07/03/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, t x, 07/03/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, Pierre-Marie Pédrot, 07/03/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, t x, 07/03/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, Jason Gross, 07/04/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, t x, 07/03/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, Pierre-Marie Pédrot, 07/03/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, t x, 07/03/2013
- Re: [Coq-Club] Re: (soft question) idiomatic inline of assert, Pierre-Marie Pédrot, 07/03/2013
- Re: [Coq-Club] (soft question) idiomatic inline of assert, Adam Chlipala, 07/03/2013
- Re: [Coq-Club] (soft question) idiomatic inline of assert, Enrico Tassi, 07/04/2013
- Re: [Coq-Club] (soft question) idiomatic inline of assert, t x, 07/05/2013
- Re: [Coq-Club] (soft question) idiomatic inline of assert, Enrico Tassi, 07/05/2013
- Re: [Coq-Club] (soft question) idiomatic inline of assert, t x, 07/05/2013
- [Coq-Club] Re: (soft question) idiomatic inline of assert, t x, 07/03/2013
Archive powered by MHonArc 2.6.18.