The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I find the following tactic very handy :

Ltac apply_eq f H := let Hn := fresh H "aeq" in

match type of H with

(?l = ?r) => assert (f l = f r) as Hn by (f_equal;auto)

end.

You don't need injectivity of f for this direction.

Here is an illustrative use of it:

Goal 1=2 -> True.

intro H.

apply_eq S H.

Abort.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Feb 16, 2014 at 4:06 AM, Vilhelm Sjöberg <vilhelm AT cis.upenn.edu> wrote:

On Sat, Feb 15, 2014 at 11:29:23PM +0200, Ömer Sinan A?acan wrote:
> Hi all,
>
> Let's say I have `length tl = n - 1` as goal and `H: n <> 0`. Can I
> apply same constructor/function to both sides of the equation in goal?
> Like applying S and having:
>
> > S (length tl) = S (n - 1)

For constructors yes, because constructors are injective. I don't know of any clever tactic for this, but if you prove injectivity as a lemma, then you can just "apply" the lemma.

    Lemma S_injective : forall n m, S n = S m -> n = m.
    Proof.
      intros n m H; injection H; auto.
    Qed.

    Hypothesis tl : list bool.
    Hypothesis n : nat.
    Goal length tl = n - 1.
      apply S_injective.
      (* goal is now
         S (length tl) = S (n - 1)  *)

Vilhelm Sjöberg