The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

You could also have used Print Opaque Dependencies to check what were the opaque terms that were used in your bigTerm.

Thomas

On Sat, May 4, 2013 at 4:06 PM, Franck Tidus <tidus_franck AT hotmail.com> wrote:

Hi Maxime and Pierre,

Many thanks for your quick responses.
I've finally find the problem, and I'll try to explain it in case it can help someone else. Every functions that I've defined myself in the proof mode were correctly defined by a "Proof... Defined". So it was not directly the problem. The problem was the use of some lemmas already defined in the Coq library, which were defined by a "Qed".
I've just re-implement them with a "Defined" at the end, and the problem was solved : I can compute completely the output of my "bigFun" function, with "Eval compute in ..."

So, in conclusion, pay attention to what you are using : the problem can come from a little opaque lemma that you are using.
You can find some inspiration by looking at the term produced by the computation ("Eval compute...") of your function. The first lines generally show some calls to some opaque functions/proofs : here is the problem. Rewrite them with a "Defined" at the end (you can just copy their body thanks to "Print ..."), and the problem is solved.

Thanks !

> Date: Wed, 1 May 2013 21:12:04 +0200
> From: Maxime.Denes AT inria.fr
> To: coq-club AT inria.fr
> Subject: Re: [Coq-Club] Reduction of a term (with a def in proof mode)

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