Inversion leads to unexpected existence in Coq

Question

Here is the inductive type pc that I use in the math 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 containing one or more pc s. pcts is a node sheet constructor that contains one pc , and pctm is an internal node constructor that contains multiple pc s.

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

And the inductively defined contains clause. contains nxt means that the tree t contains at least one occurrence x : pc n .

 Inductive contains ( n : nat ) ( x : pc n ) : pc_tree -> Prop := | contain0 : contains nx ( pcts nx ) | contain1 : forall ( ts : pc_tree ), contains nxt -> contains nx ( pctm ts ) | contain2 : forall ( ts : pc_tree ), contains nxt -> contains nx ( pctm st ). 

Now, the problematic lemma I need to prove:

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

What the lemma means is really simple: if a tree with a single leaf node containing y : pc n contains some x : pc n , it follows that x = y . I thought I could prove it with a simple inversion on contains . So when I wrote

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

I expected to get x = y as a hypothesis in context. Here is what I got instead:

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

H1 very different from expected. (I have 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 it can be used at all.

Any thoughts?

Answer 1

This is a recurring issue when accessing things that are related to dependent types. The equality generated over existT means that Coq cannot invert the equality pcts nx = pcts ny , as it would for ordinary types. The reason for this is that the index n , which appears in types x and y , cannot be generalized when entering the equality x = y , which is required to perform the inversion.

existT is a dependent-pair type constructor that “hides” the nat index and allows Coq to avoid this problem in the general case, creating a statement that looks a bit like what you want, although not exactly the same. Fortunately, for indexes that have decidable equality (for example, nat ), you can actually restore the “normal” equality using the inj_pair2_eq_dec theorem in the standard library.

 Require Import Coq.Logic.Eqdep_dec. Require Import Coq.Arith.Peano_dec. Lemma contains_single_eq : forall ( n : nat ) ( xy : pc n ), contains nx ( pcts ny ) -> x = y. intros nxy H. inversion H. apply inj_pair2_eq_dec in H1; trivial. apply eq_nat_dec. Qed.