# 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
Commented Jan 31, 2023 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. Commented Jan 31, 2023 at 21:28

## 1 Answer

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 Commented Jan 31, 2023 at 18:35