The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Works well for my particular problem as well. thank you, again.

Great advice, I should read more :)

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

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

Well I installed coqide 8.4pl2 on Windows to see, and I find this error:

The term "p_lb_dec lb0" has type

 "dec (forall b' : box, In box b' nil -> p b')"

 while it is expected to have type

 "dec (forall b' : box, In box b' lb0 -> p b')".

 

which is not the same as the one you reported, so I thought, that you copy/paste it the wrong way.

If you copy/paste it correctly, you just have to patch the code as:

----------------------------------

Lemma p_lb_dec (Hp : ∀ b, p b ∨ ¬ p b)

: ∀ lb, (∀ b', In b' lb → p b') ∨ ¬ (∀ b', In b' lb → p b').

Proof.

exact (fix p_lb_dec lb :=

match lb as lb return dec (∀ b', In b' lb → p b') with (* this line has been patched *)

| nil => p_nil_dec

| cons b lb => p_cons_dec b (Hp b) lb (p_lb_dec lb)

end).

(* Qed. (* Hides recursion to the caller, so don't do it! *) *)

Defined. (* AND NOT Qed! *)

---------------------------------

That is pretty much the advice Valentin Robert gave.

Read the manual on dependant pattern matching for more enlightment.

You can also read CPDT, Coq'Art or the Coq code in the standard library (the .v files, not Ocaml code, assuming you have the sources, which can also be found on the internet).

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.