The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

In this case (and in cases where you have a judgmental inverse), it is easy:

Goal forall n m : nat, S n = S m -> n = m.

Proof.

  intros.

  change (pred (S n) = pred (S m)).

  apply f_equal.

  assumption.

Defined.

So in you case, you can use [change (pred (S (length tl)) = pred (S (n - 1))); apply f_equal.].

Others have already covered the case where the function is injective but you don't have a judgmental inverse.  But you certainly can't do it in general.  For example, say you're trying to prove [1 = 2], and then you want to apply the function [fun _ => 0] to both sides.  Then you could just prove [0 = 0] by reflexivity, and you'd have a proof of [1 = 2], which is bad.

-Jason

On Sun, Feb 16, 2014 at 1:54 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

Hi Mitchell,

I asked this merely for learning purposes. This is not required for
solving my goal. Basically I have `Hsomething : S (length tl) = ...`
and I want to do `rewrite Hsomething` and that would solve my goal
with by `reflexivity`. I always do `inversion Hsomething` to solve
these cases but I just wanted to know if applying same
constructor/function with both sides of an equation is possible and if
it's not, is there a theoretical problem with this.

So you're not missing anything.

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

2014-02-16 20:45 GMT+02:00 Mitchell Wand <wand AT ccs.neu.edu>:

> I'm confused by the question.   Omer says he has the goal
>
> length tl = n - 1
>
> and he wants to transform it to the goal
>
> S (length tl) = S (n - 1)
>
> Omer, why do you want to do this?  Remember that we reason _backward_ from
> goals, not forward.
>
> Transforming the goal in the way you suggest wouldn't help you in reaching
> your original goal of
>
> length tl = n - 1
>
> Am I missing something here?
>
> --Mitch Wand
>
>
>
>
>
>
>
>
>
>
> On Sat, Feb 15, 2014 at 4:29 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com>
> 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)
>>
>> Is this possible? If not, why?
>>
>> Thanks!
>>
>>
>> ---
>> Ömer Sinan Ağacan
>> http://osa1.net
>>
>