Trouble with heterogeneous equality

gistfile1.coq

Set Implicit Arguments.

Require Import Arith.Arith_base List Omega.
Require Import Wellfounded.Lexicographic_Product.
Require Import Relation_Operators.
Require Import JMeq.

(* Notation for heterogeneous equality *)

Infix "==" := JMeq (at level 70, no associativity).

(* kind definitions *)

Inductive Kind : Set :=
  | Star : Kind
  | KFun : Kind -> Kind -> Kind.

Notation "*" := Star.
Notation "k '==>' k'" := (KFun k k') (at level 60, right associativity).

Definition VarCtx := list Kind.
Definition ConCtx := list Kind.

(* type definition *)

Inductive Ty (C : ConCtx) (V : VarCtx) : Kind -> Set :=
  | var : forall k, In k V -> Ty C V k
  | con : forall k, In k C -> Ty C V k
  | app : forall k k', Ty C V (k ==> k') -> Ty C V k -> Ty C V k'.

Definition eq_ty_dec : forall {C V k}(t t' : Ty C V k), {t == t'} + {~ (t == t')}.
   intros C V k t ;
   induction t ; intro t' ; destruct t' ;
   try repeat (match goal with
                 | [V : VarCtx |- context[var _ _ _ _ == var _ _ _ _]] => left
                 | [|- context[con _ _ _ _ == con _ _ _ _]] => left 
                 | [|- context[app _ _ == app _ _]] => left
                 | [|- _ ] => let x := fresh "H" in right ; intro x
               end).

What you want is not doable without proof irrelevance, because In is not unique; if the element appears multiple times, then there are many proofs. However, if you're willing to use a decidable version of In, then it works:

Set Implicit Arguments.

Require Import Arith.Arith_base List Omega.
Require Import Wellfounded.Lexicographic_Product.
Require Import Relation_Operators.
Require Import EqdepFacts Eqdep_dec.

(* kind definitions *)

Inductive Kind : Set :=
  | Star : Kind
  | KFun : Kind -> Kind -> Kind.

Notation "*" := Star.
Notation "k '==>' k'" := (KFun k k') (at level 60, right associativity).

Definition VarCtx := list Kind.
Definition ConCtx := list Kind.

(* type definition *)

Definition eq_dec_kind (k1 k2 : Kind) : {k1 = k2} + {k1 <> k2}.
Proof.
  decide equality.
Defined.

Print In.

Fixpoint In_dec A (dec_eq : forall x y : A, {x = y} + {x <> y})
         (a : A) (l : list A) : Prop :=
  match l with
    | nil => False
    | b :: m => if dec_eq b a then True else @In_dec A dec_eq a m
  end.

Lemma In_dec_irrelevance A dec_eq a l (p1 p2 : @In_dec A dec_eq a l) : p1 = p2.
Proof.
  induction l; simpl in *.
  - destruct p1.
  - repeat match goal with
             | _ => progress trivial
             | [ H : True |- _ ] => destruct H
             | [ H : appcontext[if ?x then _ else _] |- _ ] => destruct x
           end.
Defined.

Inductive Ty (C : ConCtx) (V : VarCtx) : Kind -> Set :=
  | var : forall k, In_dec eq_dec_kind k V -> Ty C V k
  | con : forall k, In_dec eq_dec_kind k C -> Ty C V k
  | app : forall k k', Ty C V (k ==> k') -> Ty C V k -> Ty C V k'.

Local Ltac fin :=
  repeat match goal with
           | _ => reflexivity
           | _ => assumption
           | _ => decide equality
           | _ => progress subst
           | [ H : _ |- _ ] => apply inj_pair2_eq_dec in H
           | [ H1 : In_dec _ _ _, H2 : In_dec _ _ _ |- _ ] =>
             (pose proof (In_dec_irrelevance _ _ _ H1 H2); subst)
           | [ H : _ |- _ ] => solve [ inversion H ]
           | [V : VarCtx |- context[var _ _ _ _ = var _ _ _ _]] => left
           | [|- context[con _ _ _ _ = con _ _ _ _]] => left 
           | [|- context[app _ _ = app _ _]] => left
           | [|- _ ] => (let x := fresh "H" in right ; intro x)
         end.

Ltac dec_kind :=
  match goal with
    | [ k : Kind, k' : Kind |- _ ]
      => match goal with
           | [ H : k <> k' |- _ ] => fail 1
           | _ => destruct (eq_dec_kind k k'); subst
         end
  end.

Definition eq_ty_dec : forall {C V k}(t t' : Ty C V k), {t = t'} + {~ (t = t')}.
   intros C V k t ;
   induction t ;
   try solve [ 
         intro t' ; destruct t' ;
         fin
       ].
   induction t'; intros;
   try solve [ fin ].
   destruct (eq_dec_kind k k0); subst.
   - destruct (IHt1 t'1) as [H|nH]; subst.
     + destruct (IHt2 t'2) as [H|nH]; subst; try solve [ fin ].
       right; intro H.
       apply nH.
       inversion H.
       apply inj_pair2_eq_dec in H1; trivial.
       decide equality.
     + right. intro H.
       apply nH.
       inversion H.
       clear H2.
       apply inj_pair2_eq_dec in H1; trivial; try decide equality.
       apply inj_pair2_eq_dec in H1; trivial; try decide equality.
   - right.
     intro H; apply n.
     inversion H; reflexivity.
Defined.

Print Assumptions eq_ty_dec. (* Closed under the global context *)

Wow... This is really a much better solution! Thanks for your time, Jason!