The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

[copy to coq-club]

  Dear Dimitri Hendriks,

> From the following definition
> 
> Variable A : Set.
> 
> Inductive listn : nat->Set :=
>   niln  : (listn O)
> | consn : (n:nat)A->(listn n)->(listn (S n)).
> 
> one might expect (listn O) to be inhabited by niln only.
> In other words (l:(listn O)) l = niln, but how to prove it?
> Case analysis on l:(listn O) is not permitted
> ("Cannot solve a second-order unification problem").

You can prove this goal using a more general form of equality
(named eq_dep and defined in file Eqdep) allowing comparison between
terms whose types are only provably equal and not convertible. Then
case analysis is possible.

Lemma eq_dep_niln : (n:nat;l:(listn n))(n=O)->(eq_dep ? ? n l O niln).
Induction l.
Trivial.
Intros;Discriminate.
Qed.

Lemma eq_niln : (l:(listn O))l = niln.
Intro;Apply eq_dep_eq with P:=listn.
Apply eq_dep_niln;Trivial.
Qed.


  Best regards,
                                                  Hugo