Rewriting with heterogeneous equality (JMeq)

Question

Consider the below (reproducible) snippet:

From Coq Require Import Vector Program.Equality Arith List.
From mathcomp Require Import ssreflect.

Section Test.

Definition computational_eq {m n} (opaque_eq: m = n) : m = n :=
    match Nat.eq_dec m n with
    | left transparent_eq => transparent_eq
    | _ => opaque_eq (* dead code; could use [False_rect] *)
    end.

Definition vector_cast {A} {nsz sz : nat} (v : Vector.t A sz) (H : sz = nsz) : Vector.t A nsz :=
    @eq_rect nat sz (fun n0 : nat => Vector.t A n0) v nsz (computational_eq H).

(* Can be opaque for demonstration purposes *)
Definition f {T: Type} {m} (n : nat): Vector.t T (n + m) -> Vector.t T m.
Admitted.

Parameter P : Vector.t bool 1 -> Prop.

Goal forall (x y : nat) (H : x + (y - x + 1) = y + 1)
    (vA : Vector.t bool (x + (y - x + 1))),
    let g := vector_cast vA H : t bool (y + 1) in
    let t := f y g : t bool 1 in
    P t.
    cbv zeta; intros.
    cbv [vector_cast eq_rect computational_eq].
    destruct (Nat.eq_dec _ _); [ | done ].
    dependent destruction e.
Abort.

End Test.

vector_cast is a computable casting function for Vectors. Now, on the Goal I'm trying to prove, I have to do a dependent destruction on e, since the type of f depends on e. But doing such elimination produces an heterogeneous equality (JMeq) between the non-opaque equality e0 and eq_refl, after the simplifications done by dependent destruction.

So, my question is: how can I extract a rewritable Leibiniz equality to simplify my goal from JMeq eq_refl e0 ?

Answer 1

A better way to deal with casts is to generalize the goal to make them go away. Instead of quantifying over vectors of some lengths and immediately casting them to another length, you can prove something about all vectors of the other length.

Lemma lem : forall y (vA : Vector.t bool (y + 1)), P (f y vA).
Proof.
Admitted.

Goal forall (x y : nat) (H : x + (y - x + 1) = y + 1)
    (vA : Vector.t bool (x + (y - x + 1))),
    let g := vector_cast vA H : t bool (y + 1) in
    let t := f y g : t bool 1 in
    P t.
Proof.
    intros.
    apply lem.
Qed.
```