The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Hello,

No, this property cannot be proved.
Your inductive definition of jdef corresponds to a "sigma type" : an
element in jdef is a (dependent) pair built from a type k:set and an
element x of type k. 

It is impredicative, because it contains all the objects of type Set
and is itself in Set.
We call these types "large inductive definition". In order to avoid an
inconsistency, it is forbiden to do a large elimination on an object
in that type : 
   when j has type jdef, I can write 
        Cases j of (jconst k x) => t end
only when t has type T with T of type Set or Prop but not Type

In particular, it is not possible to write the first projection
 fst(j) =  Cases j of (jconst k x) => k end
because t = k hat type T = Set which has type Type

The second projection,   snd(j) =  Cases j of (jconst k x) => x 
cannot be written either because it is not possible to give it a type 
   the expected type should be fst(j)

The injection tactic works by building the apropriate projection and then 
applying the theorem    j=j' => proj(j)=proj(j')
when j and j' starts with constructors it is equivalent to
     (c x)=(c x')=>x=x'

Because the injection cannot be built in the case of jdef, the
Injection tactic does not work.

I am almost sure that it cannot be proved : 
The more general form 
    (k:Set)(x,y:k)(jconst k x)=(jconst k y)->x=y 
implies what there is a unique proof of x=x, namely refl(x)

    (x,y)(h:(x=y))(jconst (x=y) h)=(jconst (x=x) (refl x)) 
is proven by dependent elimination on the proof h:x=y
then one concludes 
     (h:(x=x))(jconst (x=x) h)=(jconst (x=x) (refl x)) 
and your property implies h=(refl x) which is known not to be provable 
in the Calculus of Inductive Constructions

I would be surprised that your property can be proved just using the
extra axiom of unicity of proofs of equality (that can be added safely
to the systsm). 
Actually, I cannot say wether the injection property you want 
to prove can be assumed without getting an inconsistent system !

One way to get back the projections and injection properties, would be
to build jdef at the predicative level 
   Inductive jdef : Type := jconst : (k:Set)k -> jdef.

It depends of what you want to do with this definition

The explanation in this mail relies on some technical points about
impredicative type theories and may seem obscure if you are not
familiar with this matter.
Please do not hesitate to ask more questions and/or precise your
interest in this subject.

Christine Paulin

Nadeem Abdul Hamid writes:
 > Is is possible to prove the following lemma for this
 > inductive definition?
 > 
 > Inductive jdef : Set
 > := jconst : (k:Set)k -> jdef.
 > 
 > Lemma eq_jdef : (x,y:nat)
 >                           (jconst ? x)=(jconst ? y)
 >                           -> x=y.
 > 
 > Normally, the Injection tactic could be used, but apparently
 > jdef is impredicative so it doesn't work.
 > 
 > --- nadeem

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84