The Coq mailing list

[劉弘毅 <liukoki AT gmail.com>]

Thanks! With the method you showed me, I successfully made the typecasting.

Could I ask you another question? Now, is there a way to show the equivalence of "omega" and "cast"?

I would like to do something like

  omega a = cast a

Since (T (f a)) and (T (g a)) are the different expressions of the same type, these values should be comparable. However, the equation does not type-check.

Moreover, I cannot unfold the "cast" function since it is defined with "Proof" and made opaque. Is it impossible to make this kind of comparison?

Regards,

Koki Ryu

On Mon, Sep 28, 2020 at 9:04 PM Maximilian Wuttke <mwuttke97 AT posteo.de> wrote:

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