The Coq mailing list

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

I don't understand how is that supposed to work.

assert (S (length tl) = S (n - 1)). f_equal.

This just adds same goal one more time to my list of goals. e.g. I had
this as a goal:

Goal 1) length tl = n - 1.

Now I have this

Goal 1) length tl = n - 1.
Goal 2) length tl = n - 1.


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


2014-02-16 0:18 GMT+02:00 AUGER Cédric 
<sedrikov AT gmail.com>:
> Le Sat, 15 Feb 2014 23:29:23 +0200,
> Ömer Sinan Ağacan 
> <omeragacan AT gmail.com>
>  a écrit :
>
>> 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?
>
> It is possible, trivial and you do not even require H.
> Here, "f_equal" would be enough (assert (S (length tl) = S (n-1)).
> f_equal.). There are numerous other ways to do it.
>
>>
>> Thanks!
>>
>>
>> ---
>> Ömer Sinan Ağacan
>> http://osa1.net
>