The Coq mailing list

[t x <txrev319 AT gmail.com>]

Nuno:

Can you paste the output of

coqtop.opt -v ; echo "=============="; cat minimal.v ; echo "================="; cat minimal.v | coqtop.opt

On Thu, Aug 1, 2013 at 12:40 PM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

I tried your code verbatim; setup a Windows box just to check if there wasn't anything wrong with my Coq version running on OSX, and also tried on ProofWeb: I always get the same type error..

Perhaps you were using an old version of Coq where this used to work :x

2013/8/1 Cedric Auger <sedrikov AT gmail.com>

I can’t really help you as:
– I have no instance of coq running (and cannot presently)
– I do not know what lb0 and Hp are (more precisely, in the old post you refered, I did not have the arguments in the same order (I prefer to put Hp in a closure to have recursive calls only with arguments depending on the decreasing parameter, as I do not want generalization on constant stuff).

As Valentin said, you might need annotations on pattern matching (although in such a simple case, I would expect Coq 8.4 to infer it by itself).

I guess you have done some modifications of the code I sent, and some of those modifications might not have been correct in respect to the type system.

2013/8/1 Nuno Gaspar <nmpgaspar AT gmail.com>

Well, in short I'm not able to reproduce your example from [1]

And apparently my attempt of simplifying it destroyed the original problem :-)

I believe it is similar though.. I get a

The term "p_lb_dec lb0 Hp" has type
 "dec (forall b' : box, In b' nil -> p b')" while it is expected to have type
 "dec (forall b' : box, In b' lb0 -> p b')".

when trying to typecheck [p_lb_dec] .

I'm not even sure how you didn't have this problem yourself..

I'm running Coq 8.4 if that matters..

[1] https://sympa.inria.fr/sympa/arc/coq-club/2013-02/msg00057.html

2013/8/1 Cedric Auger <sedrikov AT gmail.com>

2013/8/1 Nuno Gaspar <nmpgaspar AT gmail.com>

Hello.

Well, I'm having an hard time reproducing an example I was given. I think I can resume it to the following (I'm actually not sure my simplification didn't break the original problem...but heh)

Here follows:

Parameter l : list nat.
Parameter x_nil     : forall n:nat, In n nil.
Parameter x_not_nil : forall (n:nat), In n l.

Fixpoint test l  :=
  match l with
    nil      => x_nil
  | cons e r => x_not_nil
  end.

I imagine you can guess my doubt.. So why doesn't it typecheck? They both live in Prop...  -_-

No.

[True] lives in [Prop].
[False] lives in [Prop].

but

[x_nil] lives in [∀ n, In n nil] (which in turns lives in [Prop], but [x_nil] does not).

Note also that your context is inconsistant, I do not think that what you wrote is what you wanted.
Plus the 'l' in the type of 'x_not_nil' is not the same as the one bound in your [test] fixpoint.

Now, if you want to make it typecheck, you should first know exactly what you want.

For instance I do not know:
– the expected type of [test] (is it "list nat → Prop" ?)
– why you put a fixpoint in a function which does not do any recursion (from my point of view, it is bad taste to put a "Fixpoint" keyword where a "Definition" keyword would work)

--
.../Sedrikov\...

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.

--
.../Sedrikov\...

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.