The Coq mailing list

[Zhaohui Li <lizhaohui1991 AT gmail.com>]

Thanks ~

This is exactly what I need.

2016-05-18 17:26 GMT+08:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:

There is such a feature, use

Ltac foo ::= bar.

(https://coq.inria.fr/distrib/current/refman/Reference-Manual011.html#sec480)

Be aware that this is a <evil> side effect </evil> that will survive
your module unless you use "Local" prefix.

Best,
P.

2016-05-18 11:00 GMT+02:00 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.
>
>