The Coq mailing list

[t x <txrev319 AT gmail.com>]

With apologies for 2 emails in rapid succession -- I realized what I wanted in the first case is "replace ... with .... by ... ". However, I'm still not sure how to solve the 2nd case (inlining with pose proof ... ).

On Wed, Jul 3, 2013 at 10:24 AM, t x <txrev319 AT gmail.com> wrote:

Hi,

  I have a very simple proof at https://gist.github.com/anonymous/b05c9da47ddfd9413048

  I'm wondering, using standard tactics (CpdtTactics, software foundations, anything well known) if there is a more idiomatic way to do this.

  Specifically, instead of:

assert ( _statement_ ) as H0 by _tactic_ .

rewrite H0.

I would like to write something closer to:

  rewrite using ( _staement_ ) proved by _tactic_.

Similarly, instead of

assert ( _statement_ ) as H0 by _tactic_ .

pose proof (lemma ... H0 ...).

I would like to write something closer to:

  pose proof (lemma .... (asssert _statement_ by _tactic_) ... ).

The main goal here is that I want to inline statements, and not have to constantly clear hypothesis using clear.

Thanks!