# Destruction of bound dependent types

I'm having an issue with dependent typing. I have reduced it to the following minimal example:

Require Import Arith.
Require Import Equality.

Inductive Ex (n : nat) :=
| X : Ex n.

Definition Cast (n : nat) {n'}
(eq : n = n') (e : Ex n) : Ex n'.
Proof.
destruct eq.
exact e.
Defined.

Lemma dim_help {x y} (H: x =? y = true) : x = y.
Proof.
apply Nat.eqb_eq; easy.
Defined.

Definition test {dim} (n : nat) : Ex dim.
destruct (n =? dim) eqn:H.
+ apply (Cast _ (dim_help H)).
apply (X n).
+ apply (X dim).
Defined.

Lemma test_lemma : forall n, @test n n = X n.
Proof.
intros.
unfold test.
Abort.


In the following code my goal in test_lemma works out to be

(if n =? n as b return ((n =? n) = b -> Ex n)
then fun H : (n =? n) = true => Cast n (dim_help H) (X n)
else fun _ : (n =? n) = false => X n) eq_refl = X n


Intuitively I'd like to destruct over n =? n however that yields the error

fun b0 : bool =>
(if b0 as b1 return (b0 = b1 -> Ex n)
then fun H : b0 = true => Cast n (dim_help H) (X n)
else fun _ : b0 = false => X n) eq_refl = X n
which is ill-typed.
Reason is: Illegal application:
The term "@dim_help" of type "forall x y : nat, (x =? y) = true -> x = y"
cannot be applied to the terms
"n" : "nat"
"n" : "nat"
"H" : "b0 = true"
The 3rd term has type "b0 = true" which should be coercible to
"(n =? n) = true".


Is there a way to work around this issue? How can I destruct the equality to do case analysis over test?

• Ex n is equivalent to True. Are you sure this is what you intend?
– Trebor
Jan 31 at 2:34
• This is just a reduced minimal example to show issues with the handling of specific proof terms. It is not an actually used proof script. However, the answer still applies to our proof script. Jan 31 at 21:28

Coq simply tells you that when it is trying to do a case on n ?= n in the expression

(if n =? n as b return ((n =? n) = b -> Ex n)
then fun H : (n =? n) = true => Cast n (dim_help H) (X n)
else fun _ : (n =? n) = false => X n) eq_refl = X n


your argument eq_refl does not vary as needed : it should be a proof of (n =? n) = true in the first case and a proof of (n =? n) = false in the second case. There is no way eq_refl will meet this,

You can fix this with a simpler definition of test

Definition test {dim} (n : nat) : Ex dim.
destruct (Nat.eq_dec n dim) as [e|e].
+ apply (Cast _ e).
apply (X n).
+ apply (X dim).
Defined.


Then you are left with proving

forall e : n = n, Cast n e (X n) = X n


which can be done because unicity of identity proof holds in Coq for natural numbers. so we have

forall n (e : n = n), e = refl_eq n.

• Thank you for the clear explanation! This is exactly what I was looking for Jan 31 at 18:35