2
$\begingroup$

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 ?

$\endgroup$
1
  • $\begingroup$ I am not sure to understand what you want expect the elimination to do. Remove the match? $\endgroup$
    – Lolo
    Commented Apr 24, 2023 at 20:49

1 Answer 1

3
$\begingroup$

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.
```
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.