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 ?

Thanks a lot.
Thomas

Code begins here :

    Require Import Coq.Program.Equality.

    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.

    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.