The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  Could you give us a (small! ) example of this problem?

Pierre


Quoting rooster 
<tidus_franck AT hotmail.com>:

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