The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/02/2014 09:03 AM, Adam Chlipala wrote:

The [intuition] tactic should have exactly that effect, for your particular example.

If you only want the hypotheses cleaned up, and don't want the rest of intuition's behavior, and you're using a version of Coq with the "$(...)$" syntax, you can do this:

Ltac simplify_hyps := repeat match goal with H:_ -> _ |- _ => specialize (H $(tauto)$) end.

Or, if you aren't using a version of Coq with the "$(...)$" syntax:

Ltac simplify_hyps :=
  repeat match goal with H:?X -> _ |- _ =>
    let H':=fresh in assert X as H' by tauto; specialize (H H'); clear H' end.

-- Jonathan

On 11/02/2014 08:40 AM, Éric Tanter wrote:

Hi Club,

Is there an automatic way to clean up the context of implications with obvious hypotheses?

For instance, I'd like to clean this up:

n : nat
H1: n = n -> fact1
H2: n = n -> fact2
========

as follows:

n : nat
H1: fact1
H2: fact2
========

in order to avoid to explicitly discharge n = n with reflexivity each time I use H1 and H2.

Thanks,

-- Éric