Reasoning about non reflexive equalities & type conversions

Question

Following-up from the answers to this question, reasoning about conversions between types that have decidable equalities is somewhat trivial (here I'm taking nat as an example for practicity).

Parameter V : nat -> Type.

Definition cast_V {m n : nat} (x : V m) (eq : m = n) : V n.
    destruct eq; exact x.
Defined.

Lemma cast_V_eq {m} (x : V m) (eq : m = m) : cast_V x eq = x.
Proof.
    replace (eq) with (eq_refl m); [ simpl; reflexivity | ].
    apply Eqdep_dec.K_dec_set; [ exact Nat.eq_dec | reflexivity ].
Qed.

Now, suppose a similar situation but there is an equality that is not refl, like the situation below, for instance:

Definition cast_ex {m n} (T : Z -> Type) (x : T (Z.of_nat m)) : Z.of_nat m = n -> T n.
Admitted.

Fail Lemma cast_ex_eq {m n} (T : Z -> Type) (x : T (Z.of_nat m)) 
    (eq : Z.of_nat m = n) : cast_ex T x eq = x <: T n.

Now, in my case, cast_ex and T are not opaque, they are real, implemented functions, operating over an specific inductive (list-like) type.

So, my question is: Can one "get rid" of this kind of casting, where eq is not a simpl refl ? How could I correctly formulate the Lemma cast_ex_eq and what would be the correct way to prove something of this sort ?

Answer 1

First a general answer: you cannot get rid of cast in general without further assumptions because type theory has an interpretation in which such casts may have non-trivial actions, namely homotopy type theory.

You could introduce an assumption that specializes type theory to a setting that prevents homotopy-theoretic phenomena. One such possibility is uniqueness of identity proofs: if $p$ and $q$ are both elements of $x =_A y$ then $p =_{x =_A y} q$. However, it is likely that there is a better solution. If you tell us a bit more about what you'd like to do, perhaps we can suggest one.

Your specific example is actually worse and UIP won't help. There is nothing in there that prevents cast_ex from doing something silly. For example, assuming excluded middle, I could replace your Admitted with:

Definition cast_ex {m n} (T : Z -> Type) (x : T (Z.of_nat m))
  (eq : Z.of_nat m = n) : T n :=
 if T n = Bool then false else convert T eq x.

That is, if T n happens to be Bool then cast_ex is constantly false, otherwise it is the usual conversion along an equality. In this case it simply isn't the case that cast_ex T x eq = x, because it could be that x = true and cast_ex T x eq = false.