The Coq mailing list

["Thomas Braibant" <thomas.braibant AT gmail.com>]

Hi,

Maybe this is a very naive question, but I have trouble using dependent
destruction under coq 8.2 beta4.

In the following minimal exemple, I want to prove inversion lemmas on
(dependent) inductive objects. I am able to use the dependent destruction
tactic if our inductive definition is defined in Type, but not in Prop.
However, converting by hand the proof term generated for the Type lemma, we 
are
able to construct a valid proof term for the Prop lemma. Is there a general 
way
to prove this kind of lemmas in Prop (using tactics), rather than hacking a
proof term ?

Moreover, the last part of the code deals with an exemple where I can't use
induction, because it leads to an ill-typed term. Could someone explain this
situation.

Thanks a lot.
Thomas

Code begins here :

Require Import Coq.Program.Equality.

   (* Type part *)
   Variable Z : Type.
   Inductive Obj : Type :=
   | Eq : Obj
   | Neq : Obj.
   Inductive t_typ : Z -> Z -> Obj -> Type :=
   | t_typ_eq : forall A, t_typ A A Eq
   | t_typ_neq : forall A B, t_typ A B Neq
     .

   Lemma lemma_typ : forall A B (u : t_typ A B Eq), (A=B)/\ (JMeq u (t_typ_eq
A)).
   Proof.
     intros A B u; dependent destruction u; constructor; reflexivity.
   Qed.

   (* Prop part *)

   Inductive t_prop : Z -> Z -> Obj -> Prop :=
   | t_prop_eq : forall A, t_prop A A Eq
   | t_prop_neq : forall A B, t_prop A B Neq
     .
   Print lemma_typ.

   (* change the printed term to erase the notation for JMeq *)
   Lemma lemma_prop : forall A B (u : t_prop A B Eq), (A=B)/\ (JMeq u
(t_prop_eq A)).
   Proof.
   (* The proof we would like to use :
      intros A B u; dependent destruction u; constructor; reflexivity.
   *)
     exact (
       fun (A B : Z) (u : t_prop A B Eq) =>
         match
           u as t in (t_prop z z0 o)
             return
             (forall u0 : t_prop z z0 Eq,
               JMeq t u0 ->
               o = Eq ->
               z = z0 /\ JMeq u0 (t_prop_eq z))
           with
           | t_prop_eq A0 =>
             fun (u0 : t_prop A0 A0 Eq)
               (H : JMeq (t_prop_eq A0) u0)
               (_ : Eq = Eq) =>
               let H1 := JMeq_eq H in
                 eq_ind (t_prop_eq A0)
                 (fun u1 : t_prop A0 A0 Eq =>
                   A0 = A0 /\ JMeq u1 (t_prop_eq A0))
                 (conj (refl_equal A0) (JMeq_refl (t_prop_eq A0))) u0 H1
           | t_prop_neq A0 B0 =>
             fun (u0 : t_prop A0 B0 Eq)
               (_ : JMeq (t_prop_neq A0 B0) u0)
               (H0 : Neq = Eq) =>
               let H1 :=
                 eq_ind Neq
                 (fun e : Obj => match e with
                                   | Eq => False
                                   | Neq => True
                                 end) I Eq H0 in
                 False_ind
                 (A0 = B0 /\ JMeq u0 (t_prop_eq A0))
                 H1
         end u (JMeq_refl u) (refl_equal Eq)
     ).
   Qed.

   (* Another exemple : even induction goes wrong *)
   Parameter X : Z -> Z -> Type.
   Parameter zero : forall A B,   X A B.
   Parameter one  : forall A,     X A A.

   Inductive eval :  forall A B u, t_prop A B u -> X A B -> Prop :=
   | eval_eq : forall A, eval (t_prop_eq A) (one A : X A A)
   | eval_neq : forall A B, eval (t_prop_neq A B) (zero A B: X A B)
     .



   Lemma ex_ind_prop : forall A B (u : t_prop A B Neq), eval u (zero A B) .
     intros A B u.
     induction u.
   Abort.