The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Section test.

(* Hello everyone,

   I am having some trouble to define the following operation. The
   idea is that you have a type T that is indexed by values in I, and
   a cast operation that converts between two different indexed types,
   provided that the indices are convertible. The operation would be
   to take t : T i1 to F t if it is possible to make the cast, and map
   it to tt otherwise. I can define the return type, but I can't
   define the actual function. Does anyone have any ideas on how to do
   this?

   Thanks *)

Variable I : Type.
Variable T : I -> Type.
Variable i1 i2 : I.
Variable dT : T i2 -> Type.
Variable F : forall t : T i2, dT t.
Variable convertible : I -> I -> bool.
Variable cast : T i1 -> convertible i1 i2 = true -> T i2.

Definition dT' (t : T i1) := 
  (if convertible i1 i2 as b return (convertible i1 i2 = b -> Type)
    then (fun p : convertible i1 i2 = true => dT (cast t p))
    else (fun p : convertible i1 i2 = false => unit)) (refl_equal _).

Definition F' (t : T i1) : dT' t.

End test.

-- 
Arthur Azevedo de Amorim