The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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.