Inversion produces unexpected existT in Coq

Question

Here is an inductive type pc that I am using in a mathematical theorem.

Inductive pc ( n : nat ) : Type :=
  | pcs : forall ( m : nat ), m < n -> pc n
  | pcm : pc n -> pc n -> pc n.

And another inductive type pc_tree, which is basically a binary tree that contains one or more pcs. pcts is a leaf node constructor that contains a single pc, and pctm is an internal node constructor that contains multiple pcs.

Inductive pc_tree : Type :=
  | pcts : forall ( n : nat ), pc n -> pc_tree
  | pctm : pc_tree -> pc_tree -> pc_tree.

And an inductively defined proposition contains. contains n x t means that the tree t contains at least one ocurrence of x : pc n.

Inductive contains ( n : nat ) ( x : pc n ) : pc_tree -> Prop :=
  | contain0 : contains n x ( pcts n x )
  | contain1 : forall ( t s : pc_tree ), contains n x t -> contains n x ( pctm t s )
  | contain2 : forall ( t s : pc_tree ), contains n x t -> contains n x ( pctm s t ).

Now, the problematic lemma I need to prove:

Lemma contains_single_eq : forall ( n : nat ) ( x y : pc n ), contains n x ( pcts n y ) -> x = y.

What the lemma means is really simple: if a tree that has a single leaf node containing y : pc n contains some x : pc n, it follows that x = y. I thought I should be able to prove this with a simple inversion on contains. So When I wrote

Lemma contains_single_eq : forall ( n : nat ) ( x y : pc n ), contains n x ( pcts n y ) -> x = y.
intros n x y H. inversion H. 

I was expecting to get x = y as an hypothesis in the context. Here's what I got instead:

1 subgoal
n : nat
x : pc n
y : pc n
H : contains n x (pcts n y)
H1 : existT (fun n : nat => pc n) n x = existT (fun n : nat => pc n) n y
====================================================================== (1/1)
x = y

H1 is quite different from what I expected. (I've never seen existT before.) All I care about is that I prove contains_single_eq, but I'm not sure how to use H1 for it, or whether it is usable at all.

Any thoughts?

Answer 1

This is a recurring problem when doing inversion on things that involve dependent types. The equality that is generated over existT just means that Coq cannot invert the equality pcts n x = pcts n y like it would for normal types. The reason for that is that the index n that appears on the types of x and y cannot be generalized when typing the equality x = y, which is required for doing the inversion.

existT is the constructor for the dependent pair type, which "hides" the nat index and allows Coq to avoid this problem in the general case, producing a statement which is slightly similar to what you want, although not quite the same. Fortunately, for indices that have a decidable equality (such as nat), it is actually possible to recover the "usual" equality using theorem inj_pair2_eq_dec in the standard library.

Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Arith.Peano_dec.

Lemma contains_single_eq : 
  forall ( n : nat ) ( x y : pc n ),
    contains n x ( pcts n y ) -> x = y.
  intros n x y H. inversion H.
  apply inj_pair2_eq_dec in H1; trivial.
  apply eq_nat_dec.
Qed.