The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 16 Feb 2014 13:35:28 +0200,
Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 a écrit :

> I don't understand how is that supposed to work.
> 
> assert (S (length tl) = S (n - 1)). f_equal.

Sorry I misunderstood your original problem.

You wanted "f x = f y -> x = y", while I believed you wanted "x = y ->
f x = f y"

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