Destruction of bound dependent types

Question

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?

Answer 1

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.