The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 11/20/2016 10:07 PM, noam neer wrote:
> thanks.
>
> however I just tried to use the same trick in a different goal and it
> didn't work -
>
>     Goal Rpower 2 3 = 8.
>     change 3 with (INR 3).
>
>     Error: Not convertible.
>
> why didn't it work here ?


Numbers are encoded in R with 0 and 1

Compare

Check (1 + ((1 + 1) * 5)).

with

Compute (INR 11).

So now INR 11 = 11 is not a conversion anymore, you have to prove the 
replacement. For example:

replace (INR 11) with (11%R) by (simpl; ring).

--
Laurent



--
Laurent