The Coq mailing list

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

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
>>
>