The Coq mailing list

[Zhaohui Li <lizhaohui1991 AT gmail.com>]

For example, I have two tactics:

Ltac tryfalse :=
  (** solve contradictions in context **)
  match goal with
    | H: true = false |- _ =>
      inversion H
    | _ => idtac
  end.

Ltac crush :=
  (** misc solver **)
  try subst;
  tryfalse;
  eauto 2;
  try tauto.

Then I keep using crush, but suddenly I find there is another case which

tryfalse should solve.

For keeping complete proof unchanged, I must write something like:

  Ltac tryfalse1 :=
  (** solve contradictions in context **)
  match goal with
    | H: true = false |- _ =>
      inversion H
    | H: Some _ = None |- _ =>
      inversion H
    | _ => idtac
  end.

Ltac crush1 :=
  (** misc solver **)
  try subst;
  tryfalse1;
  eauto 2;
  try tauto.

This is very ugly and wastes time.

So, is there any method (like in lisp) that I can write:

Ltac tryfalse :=
  (** solve contradictions in context **)
  match goal with
    | H: true = false |- _ =>
      inversion H
    | H: Some _ = None |- _ =>
      inversion H
    | _ => idtac
  end.

and Coq redefining tryfalse to this new definition,

then crush will work as my wish.

Thansk for help.