The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Yeah, this does the trick but I'm looking for a more general solution.
With this I have to define <Constructor>_injective for every
constructor I want to apply to both sides of the equation, right?

---
Ömer Sinan Ağacan
http://osa1.net


2014-02-16 0:36 GMT+02:00 Vilhelm Sjöberg 
<vilhelm AT cis.upenn.edu>:
> 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
>
>
>