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 ?
P
is preserved by cast :(P n x) -> (P m (cast H x))
whereH : m = n
. $\endgroup$