The Coq mailing list

[t x <txrev319 AT gmail.com>]

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!