The Coq mailing list

[Maxime Dénès <Maxime.Denes AT inria.fr>]

Hello,

If you want to see the normal form of your goal, you should use 
"compute" instead of "simpl".

There may be at least two reasons why "bigFun someArgs" does not reduce 
to a natural number: either bigFun is Defined using constants that are 
themselves opaque (i.e. that were saved using Qed, or made opaque by a 
module signature), or "bigFun someArgs" contains free variables.

As Pierre said, we cannot really help you more without a concrete example.

Maxime.

On 01/05/2013 20:40, rooster wrote:
> Hi,
>
> I am facing a problem with Coq that I've already faced, but I'm not able to
> remember exactly what was the previous solution (or maybe the problem here is
> a bit different).
>
> I have defined some functions, and some of them are defined in the proof mode.
> Specially, I have a function "bigFun" which is defined in the proof mode.
> When I apply bigFun to some arguments, I'm expecting to have a readable
> result, which is of type nat, so I expect simply a natural number.
> Instead, I get a horrible unfolding of my term, but without any reduction.
>
> The first thing I've check was of course if I always finish my definition by
> "Definef" instead of "Qed" for the functions I have defined in the proof mode.
> But that's fine...
>
> So I've try to enunciate a lemma, which states the equality with the value I'm
> expecting :
>
> Lemma isOne : bigFun someArgs = 1.
> Proof.
>
> "reflexivity" doesn't works : the system says that it's impossible to unify
> (bigFun someArgs) and 1. But it doesn't try to reduce the left side of "=".
> I would of course prefer for exemple the error "impossible to unify 3 and 1",
> which would mean that my function doesn't behave like expected.
>
> I've also try "simpl", "red", but nothing enables me to obtain just the
> "final" result : a natural number.
>
> If you have any clue it would be very nice.
>
> Kind regards.