The Coq mailing list

["Sylvain BOULM'E" <Sylvain.Boulme AT lip6.fr>]

> Hi,
> 
> >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").

Actually, here the idee, is to use an inversion lemma. But coq can't generate 
it because of dependent types. So you have to do the inversion by hand. This 
mean, that you have to find a more general goal than yours, to be able to 
apply the case analysis.

For instance, here a such more general goal is:

(n:nat)(l:(listn n))(<[n:nat](listn n)->Prop>Cases n of
               O => [l:(listn O)]l=niln
             | (S n) => [l:(listn (S n))]True end l).

So here is the complete proof:

Lemma try1:(l:(listn O))l=niln.
Proof.
  Cut (n:nat)(l:(listn n))(<[n:nat](listn n)->Prop>Cases n of
               O => [l:(listn O)]l=niln
             | (S n) => [l:(listn (S n))]True end l).
  Intros H l; Apply H with n:=O.
  Intros n l; Case l; Auto.
Qed.


> 
> Similarly, I need something like:
> 
> (n:nat;l:(listn (S n)))(EX a:A | (EX l':(listn n) | l = (consn n a l')))
> 
> Is it provable?
> 

Yes, but I let you find the generalization, because I'm too much lazy :-)

Actually, a much more simpler approach to handle "listn" is to define it by 
fixpoint instead of "Inductive Type". In this approach, you will only use 
"beta-iota-reduction" instead of boring inversion lemma. Fixpoint definitions 
are indeed much more effective than Inductive ones. (Inductive ones are much 
more expressive: they introduce a kind of indeterminism).

So, here is the code:

(*-----------------------------------------------------------*)
Variable A : Set.

Fixpoint listn[n:nat]:Set :=
  Cases n of
      O    => unit
   | (S n) => A*(listn n) 
  end.


(*** Equivalence with the Inductive definition ***) 
(* Constructors *)
Definition niln:(listn O):=tt. 
Definition consn:(n:nat)A->(listn n)->(listn (S n)):=[_][x][l](pair ? ? x l).

(* Elimination *)
Lemma listn_rec: 
    (P:((n:nat)(listn n)->Set))
        (P O niln)
        ->((n:nat; a:A; l:(listn n))(P n l)->(P (S n) (consn n a l)))
        ->(n:nat; l:(listn n))(P n l).
Proof.
 Unfold niln consn; Intros P H0 H1 n; Elim n; Simpl.
   Intro l; Case l; Auto.
   Intros m HR l; Case l; Auto.
Qed.

(**** Your lemmas ****)
Lemma try1: (l:(listn O)) l = niln.
Proof.
 Simpl; Intro l; Case l; Auto.
Qed.

Hints Resolve ex_intro: foo.
Lemma try2: (n:nat;l:(listn (S n)))(EX a:A | (EX l':(listn n) | l = (consn n 
a 
l'))).
Proof.
 Unfold consn; Simpl; Intros n l; Case l; EAuto with foo.
Qed.
(*-------------------------------------------------------------*)

Best regards,

Sylvain.