The Coq mailing list

[Dimitri Hendriks <hendriks AT cs.kun.nl>]

Dear all,

I encountered the following problem considering 
dependent types, the Inversion tactic and 
elimination predicates.

Let me briefly describe what I'm trying to do here.
First I define a type E of syntactic expressions.
Then I define an interpretation relation I; 
(I D e d) is to be read as "e is interpreted by d".
(I don't use an interpretation *function* instead of 
an interpretation relation, because my original goal 
is to reflect partial functions (omitted here)).

The problem arises when I do induction over an expression e,
and then try to invert the obtained instances of (I D e d).

Section aa.

Variable A : Type.

(* syntactic expressions *)

Inductive E : Type->Type :=
  E_var : (E A)
| E_fun : (B,C:Type)(E B)->(E C).

Variable a : A.

(* interpretation relation *)

Inductive I : (D:Type)(E D)->D->Type :=
  I_var : (I A E_var a)
| I_fun : (B,C:Type;f:B->C;e:(E B);b:B)
           (I B e b)->(I C (E_fun B C e) (f b)).

(* Now to be able to prove a lemma like:

Lemma I_ext : (D:Set;e:(E D);d,d':D)(I D e d)->(I D e d')->d=d'.

I need inversion lemmas like: *)

Lemma I_var_inv : (a':A)(I A E_var a')->a=a'.
Intros a' H.
(* Now Inversion doesn't give me what I want: *)
Inversion H.
(*
  A : Type
  a : A
  a' : A
  H : (I A E_var a')
  H0 : A=A
  H1 : (existT Type [x:Type]x A a)=(existT Type [x:Type]x A a')
  ============================
   a=a'
*)
(* 
It is known that the goal is not provable from H1;
for references to the literature see file 
$COQTOP/theories/Logic/Eqdep.v.
*)

Undo.

(* I tried:

Refine
<[e:(E A);t:A]a=t>
Cases H of
 I_var => (refl_equal A a)
| _ => ?
end.
*)

but this is not allowed: 
the elimination predicate should be of arity
  (D:Type)(E D)->D->Type (for non dependent case) 
or
  (D:Type;e:(E D);d:D)(I D e d)->Type (for dependent case).

However, a predicate like <[D:Type;e:(E D);d:D](I D e d)->a=d> 
is not well-typed (for a is not in D).
So, we need something like eq_dep or JMeqT
or sigma types (which is what Inversion did)
to be able to express the elimination predicate.
Ofcourse, this also means that the statement of the lemma
has to be changed, something which I'd like to avoid, if possible.

Is there a way to work around this (without using axioms 
as in Eqdep.v or JMeq.v)?

Thanks in advance,

Dimitri Hendriks