The Coq mailing list

[Solange Coupet-Grimal <owner-coq-club AT pauillac.inria.fr>]

Edwin Brady wrote:
 
> If I have a dependent type such as, for example, the following:
>
> Inductive natvect:nat->Set :=
>   empty:(natvect O) |
>   cons:(n:nat;v:(natvect n))(item:nat)(natvect (S n)).
>
> And I try to prove a simple theorem with an object of this type in the
> goal, such as:
>
> Lemma test:(w:(natvect O))(w=empty).
>
> I would expect to be able to prove this by case analysis on w - there is
> only one constructor which can give us a natvect O. However, Case,
> Induction and NewInduction on w all give the following error message:
>
> "Error: Cannot solve a second-order unification problem"
>
> Is there another way to approach this problem?
>
> Thanks,
> Edwin.
>
> -------------------
> To unsubscribe, mail 
> coq-club-request AT pauillac.inria.fr
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/
 
-- Here is a way to solve your problem.
 
This is a piece of a file you can find in the users' contributions
(hardware).
 
I hope it will be useful.
 
    Best regards,
 
                                   Solange COUPET-GRIMAL
 
_____________________________________________________________
 
CMI-39, rue  Frederic Joliot-Curie - 13453 Marseille Cedex 13
Tel : (33) 04 91 11 36 17
_____________________________________________________________
 
Require Export Eqdep.
 
Chapter ...
 
Variable A:Set.
 
Inductive  d_list :nat->Set:=
d_nil:(d_list O)|d_cons:(n:nat)A->(d_list n)->(d_list (S n)).
 
Definition eq_list:=(eq_dep nat d_list).
 
...
 
Lemma empty_dep:(n:nat)(l:(d_list n))n=O->(eq_list O d_nil n l).
(Unfold eq_list ; Intros n l).
(Dependent Inversion_clear l; Auto).
(Intros H; Absurd (eq ? (S n0) O); Auto).
Save.
 
Hint empty_dep.
 
Lemma empty:(l:(d_list O)) d_nil=l.
Intros l.
Apply (eq_dep_eq nat d_list O).
(Apply empty_dep;Auto).
Save.
-------------------
To unsubscribe, mail 
coq-club-request AT pauillac.inria.fr
Bug reports: http://coq.inria.fr/bin/coq-bugs
Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/