The Coq mailing list

[Elazar <elazarg AT gmail.com>]

I guess the distinction is "lossy" vs. "lossless" tactics. 

Elazar 

בתאריך יום ו׳, 14 בדצמ׳ 2018, 13:19, מאת Lily Chung ‏<ikdc AT mit.edu>:

It's true that it can't turn a provable goal into an unprovable one, but imo the problem with thinking of such tactics as "safe" is that they can easily lead down false paths where your goal just keeps getting more complicated.  A common mistake made by newcomers is to use induction (or destruct) where it's not appropriate, which just complicates the goal.  A similar mistake sometimes made by automated search is to repeatedly use etransitivity, creating an exponential-size sidetrack.

So while I agree that such a list would be useful, I think that calling invertible tactics "safe" could be misleading because one must generally have a clear idea of the proof strategy anyway or risk going down a rabbit hole.  On the other hand, there are some tactics which are almost always correct, and which I'd be more willing to call "safe":

- f_equal on a constructor

- destruct on a variable whose type has only one non-recursive constructor

- inversion on an equality between applications of the same constructor

- subst

I'd be interested to hear what others think though!

On Dec 14, 2018 05:14, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

While it is true that f_equal has nothing to do with constructors it
is generally safe to apply it for constructors of for function known
to be injective. In other cases it must be used carefully because it
can transform a provable goal into a unprovable one.

I wonder if there is a list of such "safe" tactics.

For instance "destruct" is safe on variables but unsafe on other
expressions. Whereas "destruct eqn:" is always safe.
P.
Le ven. 14 déc. 2018 à 09:07, Dominique Larchey-Wendling
<dominique.larchey-wendling AT loria.fr> a écrit :
>
> Hi Jeremy,
>
> You can try (apply f_equal with ...), injectivity or inversion
>
> Best,
>
> D.
>
> --------------
>
> Section eq.
>
>   Variable (X : Type) (a b c d : X).
>
>   Fact eq1 : (a,b) = (c,d) -> a=c.
>   Proof.
>     intros H.
>     apply f_equal with (f := fst) in H.
>     simpl in H.
>     trivial.
>   Qed.
>
>   Fact eq2 : (a,b) = (c,d) -> a=c.
>   Proof.
>     injection 1.
>     trivial.
>   Qed.
>
>   Fact eq3 : (a,b) = (c,d) -> a=c.
>   Proof.
>     inversion 1.
>     trivial.
>   Qed.
>
> End eq.
>
> ----- Mail original -----
> > De: "Jeremy Dawson" <Jeremy.Dawson AT anu.edu.au>
> > À: "coq-club" <coq-club AT inria.fr>
> > Envoyé: Vendredi 14 Décembre 2018 04:14:13
> > Objet: Re: [Coq-Club] injectivity of constructors
>
> > Thanks all for the various replies, but injection doesn't work,
> > giving error
> > Ltac call to "injection" failed.
> > Error: Not a negated primitive equality.
> >
> > Jeremy
> >
> > On 12/14/2018 02:07 PM, Jasper Hugunin wrote:
> >> `injection` seems to fit your description, see
> >> https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.injection.
> >>
> >> - Jasper Hugunin
> >>
> >> On Thu, Dec 13, 2018 at 4:54 PM Lily Chung <ikdc AT mit.edu
> >> <mailto:ikdc AT mit.edu>> wrote:
> >>
> >>     That follows from general properties of equality, and has nothing to
> >>     do with constructors.  Try f_equal.