The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

You can indeed 'cast' a value from type `T (f a)` to type `T (g a)` if
you can prove `f a = g a`. To do that, you use the eliminator on `eq`:

```
eq_rect
: forall (A : Type) (x : A) (P : A -> Type), P x ->
  forall y : A, x = y -> P y
```

MWE:

```
Parameter A : Type.
Parameter f g : A -> A.
Parameter T : A -> Type.
Parameter omega : forall a : A, T (f a).

Parameter f_a_eq_g_a : forall (a : A), f a = g a.


Definition cast : forall a : A, T (g a).
Proof.
  intros a.
  elim (f_a_eq_g_a a).
  apply omega.
 *)
Defined.

Print cast.
(*
cast =
fun a : A => eq_rect (f a) (fun a0 : A => T a0) (omega a) (g a)
(f_a_eq_g_a a)
     : forall a : A, T (g a)
*)
```


On 28/09/2020 08:40, 劉弘毅 wrote:
> Hi,
> I defined a function about (A: Type), (f: A -> A),  and (T: A -> Type)
> as follows.
> 
> Definition omega (a: A): T (f a)  := (* Expression *).
> 
> I also took (g: A -> A) and proved the following lemma.
> 
> Lemma f_a_eq_g_a : forall (a: A),  f a = g a.
> 
> Now, I want to treat (omega a) as a value in (T (g a)). Is there any
> easy way to do this?
> Regards,
> Koki