The Coq mailing list

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