The Coq mailing list

[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