The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

There is no need for such a tactic, you can just do this by:

  apply (f_equal S) in H.

PS: Ömer seemed to be looking for injectivity of S, this goes the other 
way around.

On 02/16/2014 09:16 AM, Abhishek Anand wrote:
> 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
> <mailto: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